Spin Multi-Core Depth-First Search
Spin supports options to perform model checking on multi-core machines (version 5 and later). Version 5 introduced multicore depth-first search, and Version 6 added multicore breadth-first search. This page describes the multicore depth-first search. See here for the multicore breadth-first search options.
Directives Supported for Multi-Core Depth-First SearchIn multi-core DFS mode, Spin will have to pre-allocate the maximum allowable amount of shared memory at the start of the run. It is therefore recommended to always us the directive MEMLIM:
-DMEMLIM=8000 # allow up to 8 GB of shared memoryOther directives, new to Spin version 5.0 are,the first few being most important. The following list applies specificatlly to version 5.1.2 and later:
-DDUALCORE --> same as -DNCORE=2 -DQUADCORE --> same as -DNCORE=4 -DNCORE=N --> enables multi_core verification if N>1Additional directives supported in multi-core DFS mode:
-DSEP_STATE --> forces separate statespaces instead of a single shared state space -DUSE_DISK --> use disk for storing states when a work queue overflows -DMAX_DSK_FILE=N --> max nr of states per diskfile (default: 1000000) -DFULL_TRAIL --> support full error trails (but increases memory use)Normally, and probably the recommended way, to do a first compilation and multi-core run for a verification model, would be to decide on the amount of memory, and the number of available core and then execute, e.g.:
$ spin -a model.pml # as before $ gcc -DNCORE=3 -DMEMLIM=8000 -DSAFETY -o pan pan.c $ ./panAnd let ./pan tell you what if anything would need changing in the compilation. For instance, to increase the number of states that can be stored in the shared queues that connect the different CPU cores (default values are in parentheses):
-DVMAX=N --> upperbound on statevector for handoffs (default N=1024) -DPMAX=N --> upperbound on nr of procs (default N=64) -DQMAX=N --> upperbound on nr of channels (default N=64)As noted, it is safe to do a default run first, and let ./pan recommend a setting for the above three directives, if the defaults are not right, rather than trying to guess what they should be up front.
To change the size of the global workqueue (rarely needed):
-DSET_WQ_SIZE=N --> default 128 (Mbytes)To force the use of a single global heap, rather than separate heaps for shared memory per core (usually not helpful):
-DGLOB_HEAPTo define a function to initialize data before spawning processes (must be enclosed in quotes to protect the round braces from the shell):
"-DC_INIT=fct()"Timer settings etc. for termination and crash detection (the default settings are shown below). Should very rarely need changing:
-DSHORT_T=0.1 --> short timeout for termination detection trigger -DLONG_T=600 --> long timeout for giving up on termination detection -DONESECOND=(1<<29) --> timeout waiting for a free slot -DT_ALERT --> collect stats on crash alert timeouts
Safety VerificationRecommended use is to use -DSAFETY -DNCORE=N with N equal to the number of physical cores on your system, or lower, but never larger. Do not use -DSEP_STATE in this mode (it will lead to redundant work being done unnecessarily.)
Liveness VerificationCompile with -DNCORE=2 -DSEP_STATE. Using a larger number of cores than 2 is not useful with the exisiting implementation, since the multi-core liveness algorithm is fundamentally dual-core. Since we know that the two statespaces generated for the first and the second depth-first search are disjoint, the use of -DSEP_STATE is recommended, although it can somewhat increase memory use. Omit -DSEP_STATE only if there isn't sufficient memory.
Fine-TuningAt the end of a verification run, ./pan will print some statistics. Many more are printed if you run in verbose mode by adding a -v to the parameters. Included in verbose mode is the number of internal ticks spent waiting for incoming states and free slots in work queues. If the latter is non-zero, it may be advisable to enlarge the global workqueue (-DSET_WQ_SIZE), and/or to enable disk swapping (-DUSE_DISK).
Another statistic printed is the number of states that is explored by each CPU core. If the numbers look uneven -- you can experiment with different handoff depths. The default handoff depth is 20, but you can give ./pan a command-line argument to override this. To set a handoff depth to 100, for instance, use:
$ ./pan -z100(For liveness verification, the actual handoff depth is fixed to accepting states, but the -z argument still changes the number of slots in the circular handoff queues used.)
Usually, the verification run is not very sensitive to the absolute value of the handoff depth chosen. When large numbers of cores are used, or when the maximum search depth is relatively small, it is probably wise not to also use a large value for the handoff-depth, to make sure that each CPU core can get sufficient work.
To see all supported options, use:
$ ./pan --In rare cases a run may abort due to timeouts, even when the run itself isn't really finished. In this case, you could try to give -DSHORT_T a larger value. (Since there is some hardware speed dependence in this setting, this may also be necessary on very fast machines -- although this is unlikely.)
Full Counter-ExamplesBy default, ./pan when run in multi-core DFS mode will generate a short counter-example that contains only the last few steps before an error is found. All counter-examples must be replayed with ./pan itself (you can nor use spin -t for replay in this mode). For instance:
$ ./pan -rIf the counter-example is too short -- you can try a run with a larger handoff depth to see if that triggers a longer part of the error trail. To get a full counter-example that starts from the global initial system state, you must compile with -DFULL_TRAIL, for instance:
$ gcc -DNCORE=32 -DFULL_TRAIL -o pan pan.cThis increases the memory requirements to store the extra information needed for the full error-trails (a stack-tree), but will generate a traditional counter-example that can be replayed with ./pan -r as well as with spin -t (unless embedded C-code is used in the model of course -- in that case you can only replay the counter-example with ./pan -r as before).
Other New Directives in 5.0Two other new compile time directives for pan.c files were introduced in Version 5.0. Their use is not related to multi-core verification, but have a more general purpose. They are:
-DFREQ=N --> changes the frequency of snapshot updates during a run from once every 1000000 states to once every N states -DNSUCC --> computes the average fanout of states in the statespace and prints a summary at the end of the runThe remaining directives are for testing only, and should probably not be used for routine applications:
-DLOOPSTATE --> testing only -- enables a failed attempt to enforce a variant of a partial order cycle proviso based on local loopstates -DNO_V_PROVISO --> testing only -- disables a key proviso for partial order reduction during multi-core verification runs (based on cpu id numbers) -DBUDGET --> testing only -- enables an experiment search reduction strategy for bitstate search, restricting the maximum size of a subtree searched within the dfs, in an attempt to divide available memory more evenly across the entire dfs search tree in exceptionally large state spaces -DTHROTTLE=N --> testing only -- changes the throttle value for -DBUDGET searches; the default value for N is 1.5