protocon.1

.TH PROTOCON 1 "April 2015" "Version 2015.04.13"
.LS 1
.SH NAME
protocon \- add convergence to shared memory protocols
.SH SYNOPSIS
.B protocon
.IR RUN_MODE ?
.BI -x\  specification-file.prot
.RB ( -o
.IR solution-file.prot )?
.I OPTIONS
.SH DESCRIPTION
.I Protocon
adds convergence to shared memory protocols.
.SH RUN_MODE
.TP
.B -search
Randomized backtracking with restarts.
This is the default.
.TP
.B -verify
Verify a given protocol.
.TP
.B -nop
Do not perform any verification or synthesis.
This is useful when paired with
.B -o
or any of the other output options.
.TP
.B -rank-shuffle
This is a
.B -search
that uses incomplete heuristics rather than backtracking.
This is a swarm synthesis algorithm that ranks actions and permutes the actions within each rank.
.TP
.B -minimize-conflicts
Attempt to minimize the conflicts recorded from a previous run.
.SH OPTIONS
.TP
.B -h
Print a summary of available options and exit.
(Doesn't actually do this :D)
.TP
.BI -x-args\  args-file
Load a file containing command-line arguments.
.TP
.BI -parallel\  N \fR?\fI
Use
.I N
threads for the task.
If
.I N
is not given, then it is automatically detected by OpenMP or the value of the
.B $OMP_NUM_THREADS
environment variable.
Note that this option is ignored when using
.B protocon-mpi
since the number of parallel processes is determined by the MPI runtime.
.TP
.BI -def\  key\ val
Override or define a constant
.I key
in the input file to have the value
.IR val .
.TP
.BI -param\  key\ val
A solution protocol must satisfy the input system with the constant
.I key
defined as
.IR val .
This is different from
.B -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
.B -param
flags specify systems in order of increasing computational cost.
.TP
.BI -param\ [\ -def\  key\ val\  \fR...\fB\ ]
This alternative form of
.B -param
allows some extra options to be specified between brackets (note: parentheses are allowed too).
Except for
.BR -no-partial ,
these options are all valid outside of a
.B -param
block as well.
.IP
.BI -def\  key\ val
Multiple constants can be defined.
.IP
.B -no-conflict
Do not consider this parameterized system when minimizing and recording conflicts.
When used outside of and before all
.B -param
blocks, this can affect the completeness of the search.
.IP
.B -no-partial
Do not build a partial solution for this parameterized system.
This system will only be considered when a solution is found that 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
.BR -no-conflict .
.IP
.B -synchronous
Consider this system to be synchronous.
.TP
.B -sysrand
Use a random number generator that includes system entropy.
Executions using this option are not reproducible.
.TP
.BR -no-random
Do not use randomization in backtracking, simply make decisions in order.
This does not make sense in conjunction with the
.B -parallel
flag.
.TP
.BR -pick\  ( mrv | lcv | fully-random | conflict | quick )
.IP
.B mrv
minimum remaining values heuristic.
This is used by default, and it is always used since (most) other picking heuristics build on its functionality.
.IP
.B lcv
Least constraining value heuristic.
Attempt to choose actions that constrain the possibilities the least.
.IP
.B fully-random
Randomly choose a candidate action without the MRV heuristic.
The
.B mrv
method already uses randomization in a backtracking search when the run mode is
.B -random
(this is the default) rather than
.BR -serial .
.IP
.B conflict
Try to choose actions that correspond with existing conflicts.
This is constrained by the MRV heuristic.
.IP
.B quick
For testing, don't use this.
The
.B mrv
picking method is fast.
.TP
.BR -pick-reach
Without breaking the minimum remaining valuesheuristic, try to pick actions that resolve a deadlock that can reach the invariant using the partial solution.
.TP
.BI -o-log\  log-file
Output log file
.IR log-file.tid ,
where
.I tid
is the thread id.
.TP
.BI -x-conflicts\  conflicts-file
Load conflicts from a previous run.
.TP
.BI -o-conflicts\  conflicts-file
Store the conflicts found by this search.
.TP
.BI -snapshot-conflicts
After every iteration, write the current conflicts to a file
.IR conflicts-file.tid ,
where
.I tid
is the thread id.
.TP
.BI -max-conflict\  N
For recorded conflicts, limit the number of actions involved to
.IR N .
There is no limit by default.
.TP
.BI -ntrials\  N
Limit the number of trials per thread to
.IR N .
.TP
.B -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.
.TP
.BI -x-try\  possible-solution.prot
Try a solution before others.
Multiple solutions may be specified by multiple flags.
This flag is useful with
.B -optimize
to start optimization at a fairly good solution.
.TP
.B -try-all
Keep searching, even if a solution is found.
This is helpful for accumulating conflicts.
.TP
.BI -max-depth\  N
Limit search depth to
.I N
levels before restarting.
This is useful if you are searching for small conflicts.
Consider using the
.B -pick fully-random
option with this.
.TP
.BI -max-height\  N
Limit backtracking to
.I N
levels before restarting.
Default is
.IR 3 .
A value of
.I 0
disables restarts.
.TP
.BI -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
.B -try-all
flag to test (to some degree) that the search method is complete.
.TP
.BI -o-promela\  model-file.pml
.PD 0
.TP
.PD 1
.BI -o-pml\  model-file.pml
Write a Promela model.
This functionality is incomplete, in that the invariant is not included in the model.
.TP
.BI -o-graphviz\  dot-file.gv
Write the system topology to a GraphViz DOT file to show which processes access the same variables.
.SH EXAMPLES
The
.B 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
.IR 5 :
.nf
    protocon -verify -x examplesoln/TokenRingThreeBit.prot -def N 5
.fi
Similarly, you can verify a similar token ring generated by this tool:
.nf
    protocon -verify -x examplesoln/TokenRingSixState.prot -def N 5
.fi

Note that if the executable
.B protocon
is not in your
.BR $PATH ,
then you must specify the full pathname to it, such as
.B ./bin/protocon
in order to run these commands.

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

.SH EXAMPLE: Coloring
To find a 3-coloring protocol on a ring of size
.IR 5 ,
run:
.nf
    protocon -serial -x examplespec/ColorRing.prot -o found.prot -def N 5
.fi

The
.B -serial
.B -no-random
flag is merely there to force a serial execution without randomization.
If there are more cores available, run:
.nf
    protocon -x examplespec/ColorRing.prot -o found.prot -def N 5 -o-log search.log
.fi
We use the
.B -o-log
flag to create log files for each search thread.
If these are not desired, simply do not give the flag.

.SH 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!
.nf
    protocon -x inst/LeaderRingHuang.prot -def N 5
.fi

But notice that removing randomization solves this problem very quickly without any special flags.
.nf
    protocon -serial -no-random -x examplespec/LeaderRingHuang.prot -def N 5
.fi
This even works well when the ring, and each variable domain, is of size
.IR 6 .
.nf
    protocon -serial -no-random -x examplespec/LeaderRingHuang.prot -def N 6
.fi

The random method can make better decisions (for this problem, at least) by trying to choose actions that make an execution from some deadlock state to the invariant, rather than just resolving some deadlock.
This is accomplished with the
.B -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
.B -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.
.nf
    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
.fi

Since
.B -pick-reach
helped, we might try the
.B -rank-shuffle
search that does not use backtracking at all, but takes reachability into account as a fundamental concept.
Use the
.B -no-conflict
flag to speed up the trials.
.nf
    protocon -rank-shuffle -x examplespec/LeaderRingHuang.prot -no-conflict -def N 5
.fi
We can similarly use
.B -no-conflict
with backtracking, which works fairly well in this case.
.nf
    protocon -x examplespec/LeaderRingHuang.prot -no-conflict -def N 5
.fi
Be warned that the
.B -no-conflict
flag makes a search incomplete and usually hurts a backtracking search.

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

.SH EXAMPLE: Three Bit Token Ring
Let's try to find a stabilizing token ring using three bits on a ring of size
.IR 5 .
.nf
    protocon -x examplespec/ThreeBitTokenRing.prot -o found.prot -def N 5
.fi

Is the protocol stabilizing on a ring of size
.IR 3 ?
.nf
    protocon -verify -x found.prot -def N 3
.fi

How about of size
.I 4
or
.IR 6 ?
.nf
    protocon -verify -x found.prot -def N 4
    protocon -verify -x found.prot -def N 6
.fi

Probably not.
Let's try again, taking those sizes into account!
.nf
    protocon -x examplespec/TokenRingThreeBit.prot -o found.prot -def N 5 -param N 3 -param N 4 -param N 6
.fi

But what if we want to search up to size
.IR 7 ,
but it takes too long check a system of that size at each decision level?
Use the
.B -no-partial
flag to just verify the protocol on that system after finding a protocol that is self-stabilizing for all smaller sizes.
.nf
    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 ]
.fi

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