Content-type: text/html Manpage of PROTOCON

PROTOCON

Section: User Commands (1)
Updated: April 2015
Index Return to Main Contents

NAME

protocon - add convergence to shared memory protocols

SYNOPSIS

protocon RUN_MODE? -x specification-file.prot (-o solution-file.prot)? OPTIONS

DESCRIPTION

Protocon adds convergence to shared memory protocols.

RUN_MODE

-search: Randomized backtracking with restarts. This is the default.
-verify: Verify a given protocol.
-nop: Do not perform any verification or synthesis. This is useful when paired with -o or any of the other output options.
-rank-shuffle: This is a -search that uses incomplete heuristics rather than backtracking. This is a swarm synthesis algorithm that ranks actions and permutes the actions within each rank.
-minimize-conflicts: Attempt to minimize the conflicts recorded from a previous run.

OPTIONS

-h: 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?: Use N threads for the task. If N is not given, then it is automatically detected by OpenMP or the value of the $OMP_NUM_THREADS environment variable. Note that this option is ignored when using protocon-mpi since the number of parallel processes is determined by the MPI runtime.
-def key val: Override or define a constant key in the input file to have the value val.
-param key val: A solution protocol must satisfy the input system with the constant key defined as val. This is different from -def 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 -param flags specify systems in order of increasing computational cost.
-param [ -def key val ... ]: This alternative form of -param allows some extra options to be specified between brackets (note: parentheses are allowed too). Except for -no-partial, these options are all valid outside of a -param block as well.
: -def key val Multiple constants can be defined.
: -no-conflict Do not consider this parameterized system when minimizing and recording conflicts. When used outside of and before all -param blocks, this can affect the completeness of the search.
: -no-partial 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 -no-conflict.
: -synchronous Consider this system to be synchronous.
-sysrand: Use a system random number generator which takes includes system entropy. Executions using this option are not reproducible.
-no-random: Do not use randomization in backtracking, simply make decisions in order. This does not make sense in conjunction with the -parallel flag.
-pick (mrv|lcv|fully-random|conflict|quick)
: mrv minimum remaining values heuristic. This is used by default, and it is always used since (most) other picking heuristics build on its functionality.
: lcv Least constraining value heuristic. Attempt to choose actions which constrain the possibilities the least.
: fully-random Randomly choose a candidate action without the MRV heuristic. The mrv method already uses randomization in a backtracking search when the run mode is -random (this is the default) rather than -serial.
: conflict Try to choose actions which correspond with existing conflicts. This is constrained by the MRV heuristic.
: quick For testing, don't use this. The mrv picking method is fast.
-pick-reach: 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 log-file.tid, where tid 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.
-snapshot-conflicts: After every iteration, write the current conflicts to a file conflicts-file.tid, where tid is the thread id.
-max-conflict N: For recorded conflicts, limit the number of actions involved to N. There is no limit by default.
-ntrials N: Limit the number of trials per thread to N.
-optimize: 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 -optimize to start optimization at a fairly good solution.
-try-all: Keep searching, even if a solution is found. This is helpful for accumulating conflicts.
-max-depth N: Limit search depth to N levels before restarting. This is useful if you are searching for small conflicts. Consider using the -pick fully-random option with this.
-max-height N: Limit backtracking to N levels before restarting. Default is 3. A value of 0 disables restarts.
-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 -try-all flag to test (to some degree) that the search method is complete.
-o-promela model-file.pml
: -o-pml 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.

EXAMPLES

The examplesoln/ 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 5:

    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 protocon is not in your $PATH, then you must specify the full pathname to it, such as ./bin/protocon in order to run these commands.

In the examplespec/ directory, there are some nice example problem instances.

EXAMPLE: Coloring

To find a 3-coloring protocol on a ring of size 5, run:

    protocon -serial -x examplespec/ColorRing.prot -o found.prot -def N 5

The -serial -no-random 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 -o-log 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 6.

    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 -pick-reach flag. 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 -pick lcv flag. 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

Since -pick-reach helped, we might try the -rank-shuffle search which does not use backtracking at all, but takes reachability into account as a fundamental concept. Use the -no-conflict flag to speed up the trials.

    protocon -rank-shuffle -x examplespec/LeaderRingHuang.prot -no-conflict -def N 5

We can similarly use -no-conflict with backtracking, which works fairly well in this case.

    protocon -x examplespec/LeaderRingHuang.prot -no-conflict -def N 5

Be warned that the -no-conflict flag makes a search incomplete and usually hurts a backtracking search.

For rings of size 6, the randomized searches do not compete with the -serial -no-random search.

EXAMPLE: Three Bit Token Ring

Let's try to find a stabilizing token ring using three bits on a ring of size 5.

    protocon -x examplespec/ThreeBitTokenRing.prot -o found.prot -def N 5

Is the protocol stabilizing on a ring of size 3?

    protocon -verify -x found.prot -def N 3

How about of size 4 or 6?

    protocon -verify -x found.prot -def N 4
    protocon -verify -x found.prot -def N 6

Probably not. 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 7, but it takes too long check a system of that size at each decision level? Use the -no-partial 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 ]

BUGS

The MPI version currently does not support -nop and never will.

This document was created by man2html, using the manual pages.
Time: 12:16:20 GMT, February 10, 2016