Manpage of PROTOCON
Section: User Commands (1)
Updated: April 2015
Return to Main Contents
protocon - add convergence to shared memory protocols
adds convergence to shared memory protocols.
Randomized backtracking with restarts.
This is the default.
Verify a given protocol.
Do not perform any verification or synthesis.
This is useful when paired with
or any of the other output options.
This is a
that uses incomplete heuristics rather than backtracking.
This is a swarm synthesis algorithm that ranks actions and permutes the actions within each rank.
Attempt to minimize the conflicts recorded from a previous run.
Print a summary of available options and exit.
(Doesn't actually do this :D)
- -x-args args-file
Load a file containing command-line arguments.
- -parallel N?
threads for the task.
is not given, then it is automatically detected by OpenMP or the value of the
Note that this option is ignored when using
since the number of parallel processes is determined by the MPI runtime.
- -def key val
Override or define a constant
in the input file to have the value
- -param key val
A solution protocol must satisfy the input system with the constant
This is different from
since it forces the search to consider an additional system.
If this parameter changes the size of variables, bad things will happen.
For performance, is assumed that the
flags specify systems in order of increasing computational cost.
- -param [ -def key val ... ]
This alternative form of
allows some extra options to be specified between brackets (note: parentheses are allowed too).
these options are all valid outside of a
block as well.
-def key val
Multiple constants can be defined.
Do not consider this parameterized system when minimizing and recording conflicts.
When used outside of and before all
blocks, this can affect the completeness of the search.
Do not build a partial solution for this parameterized system.
This system will only be considered when a solution is found which satisfies all other systems, at which point the protocol will be verified to work or fail for this system.
In the case of a failed verification, the search will restart.
This flag also implies
Consider this system to be synchronous.
Use a system random number generator which takes includes system entropy.
Executions using this option are not reproducible.
Do not use randomization in backtracking, simply make decisions in order.
This does not make sense in conjunction with the
- -pick (mrv|lcv|fully-random|conflict|quick)
minimum remaining values heuristic.
This is used by default, and it is always used since (most) other picking heuristics build on its functionality.
Least constraining value heuristic.
Attempt to choose actions which constrain the possibilities the least.
Randomly choose a candidate action without the MRV heuristic.
method already uses randomization in a backtracking search when the run mode is
(this is the default) rather than
Try to choose actions which correspond with existing conflicts.
This is constrained by the MRV heuristic.
For testing, don't use this.
picking method is fast.
Without breaking the minimum remaining valuesheuristic, try to pick actions which resolve a deadlock which can reach the invariant using the partial solution.
- -o-log log-file
Output log file
is the thread id.
- -x-conflicts conflicts-file
Load conflicts from a previous run.
- -o-conflicts conflicts-file
Store the conflicts found by this search.
After every iteration, write the current conflicts to a file
is the thread id.
- -max-conflict N
For recorded conflicts, limit the number of actions involved to
There is no limit by default.
- -ntrials N
Limit the number of trials per thread to
Optimize the result by minimizing the number of asynchronous layers required to reach a fixpoint.
The minimization applies to the sum of such layers of all systems being considered.
- -x-try possible-solution.prot
Try a solution before others.
Multiple solutions may be specified by multiple flags.
This flag is useful with
to start optimization at a fairly good solution.
Keep searching, even if a solution is found.
This is helpful for accumulating conflicts.
- -max-depth N
Limit search depth to
levels before restarting.
This is useful if you are searching for small conflicts.
Consider using the
option with this.
- -max-height N
Limit backtracking to
levels before restarting.
A value of
- -x-test-known known-solution.prot
After each iteration, test to make sure a known solution can still be found.
This is useful with the
flag to test (to some degree) that the search method is complete.
- -o-promela model-file.pml
Write a Promela model.
This functionality is incomplete, in that the invariant is not included in the model.
- -o-graphviz dot-file.gv
Write the system topology to a GraphViz DOT file to show which processes access the same variables.
directory contains known solutions to some protocols.
It is instructional to verify these.
For example, this is how you would verify that the token ring of three bits from Gouda and Haddix is self-stabilizing for a ring of size
protocon -verify -x examplesoln/TokenRingThreeBit.prot -def N 5
Similarly, you can verify a similar token ring generated by this tool:
protocon -verify -x examplesoln/TokenRingSixState.prot -def N 5
Note that if the executable
is not in your
then you must specify the full pathname to it, such as
in order to run these commands.
directory, there are some nice example problem instances.
To find a 3-coloring protocol on a ring of size
protocon -serial -x examplespec/ColorRing.prot -o found.prot -def N 5
flag is merely there to force a serial execution without randomization.
If there are more cores available, run:
protocon -x examplespec/ColorRing.prot -o found.prot -def N 5 -o-log search.log
We use the
flag to create log files for each search thread.
If these are not desired, simply do not give the flag.
EXAMPLE: Agreement / Leader Election
One particular instance of agreement on a ring poses some issues.
Using the default heuristics, the following may take a long time!
protocon -x inst/LeaderRingHuang.prot -def N 5
But notice that removing randomization solves this problem very quickly without any special flags.
protocon -serial -no-random -x examplespec/LeaderRingHuang.prot -def N 5
This even works well when the ring, and each variable domain, is of size
protocon -serial -no-random -x examplespec/LeaderRingHuang.prot -def N 6
The random method can make better decisions (for this problem, at least) by trying to choose actions which make an execution from some deadlock state to the invariant, rather than just resolving some deadlock.
This is accomplished with the
We can also make better decisions by using the least-constraining value heuristic on top of the default minimum remaining values heuristic.
This is accomplished with the
Alone, each of these two flags make the runtime finish in a reasonable amount of time (55 seconds on a 2 GHz machine).
Together, they rival the non-random version.
protocon -x examplespec/LeaderRingHuang.prot -pick-reach -def N 5
protocon -x examplespec/LeaderRingHuang.prot -pick lcv -def N 5
protocon -x examplespec/LeaderRingHuang.prot -pick-reach -pick lcv -def N 5
helped, we might try the
search which does not use backtracking at all, but takes reachability into account as a fundamental concept.
flag to speed up the trials.
protocon -rank-shuffle -x examplespec/LeaderRingHuang.prot -no-conflict -def N 5
We can similarly use
with backtracking, which works fairly well in this case.
protocon -x examplespec/LeaderRingHuang.prot -no-conflict -def N 5
Be warned that the
flag makes a search incomplete and usually hurts a backtracking search.
For rings of size
the randomized searches do not compete with the
EXAMPLE: Three Bit Token Ring
Let's try to find a stabilizing token ring using three bits on a ring of size
protocon -x examplespec/ThreeBitTokenRing.prot -o found.prot -def N 5
Is the protocol stabilizing on a ring of size
protocon -verify -x found.prot -def N 3
How about of size
protocon -verify -x found.prot -def N 4
protocon -verify -x found.prot -def N 6
Let's try again, taking those sizes into account!
protocon -x examplespec/TokenRingThreeBit.prot -o found.prot -def N 5 -param N 3 -param N 4 -param N 6
But what if we want to search up to size
but it takes too long check a system of that size at each decision level?
flag to just verify the protocol on that system after finding a protocol which is self-stabilizing for all smaller sizes.
protocon -x examplespec/TokenRingThreeBit.prot -o found.prot -def N 5 -param N 3 -param N 4 -param N 6 -param [ -def N 7 -no-partial ]
The MPI version currently does not support
and never will.
- EXAMPLE: Coloring
- EXAMPLE: Agreement / Leader Election
- EXAMPLE: Three Bit Token Ring
This document was created by
using the manual pages.
Time: 12:16:20 GMT, February 10, 2016