A description of the parallel breadth-first search mode can be found in this paper:
$ spin -a model.pml $ cc -DBFS_PAR -o pan pan.c $ ./panIt is generally recommended to compile the pan sources with some compiler optimization enabled (e.g., -O2) -- although it can slow down the compilation by a small amount, it can make a big difference in the speed of verification (often a factor of two).
The executable has a few more options. The most important of these is the -u flag that allows you to choose how many cores you want to use for a run. On Linux systems this number will default to the number of available cores minus one -- but you can set it to any other number as well. (Don't set it higher than the number of cores you have on your system though -- that wont make the run go any faster of course.) For instance:
$ ./pan -u3 # use 3 coresBy default the executable will try to use as much shared memory as you have available on your system. You can define a lower limit for shared memory use in the familiar way, by adding the -DMEMLIMIT=... directive.
The parallel breadth-first search mode allows you to verify both safety and a range of liveness properties (using pan runtime flag -a), as explained in the 2012 paper.
-DNO_HCGenerally this is not recommended since it increases the memory requirements substantially and affects performance with generally only minimal increases in coverage.
-DBITSTATEand disk memory can be used for the breadth-first queues by adding directive
-DBFS_DISKThe latter can save memory, but will also cause the verifier to run slower, which may defeat the use of multiple cores.
By default a verification run with -DBFS_PAR will continue as long as possible, but it can be forced to stop when the hashcompact table is filled to capacity by adding compiler directive
-DSTOP_ON_FULLThe maximum length of a cycle for liveness violations is currently set to 10. This can be changed by defining
-DL_BOUND=N(although this seems only rarely useful).
When no compare and swap function __sync_bool_compare_and_swap is available (e.g. when using Cygwin and compiling with gcc) you can define:
|Return to Spin homepage||Page last updated May 4, 2012|