Spin Version 5.0 Multi-core Options

• The working of Spin 5.0 is unchanged for single-core verifications (the default).
  This means that if you do not explicitly enable a multi-core verification, Spin will work as before.
• The multi-core options are designed for true multi-core machines (not large multi-cpu shared memory machines with NUMA architectures). The multi-core mode tends to work best for large verification models, but not for small models of a few million states or less. The multi-core options can in the best cases give a near linear speedup with the number of cpu-cores used. In the worst case, though, the added overhead can also cause a slowdown. Sometimes one has to experiment to find the right settings to achieve a true speedup (follow, for instance, the hints for recompilation that the verifier sometimes prints at the end of a run).
• The multi-core option allows one to compile the pan.c verifiers with extra directives (e.g., -DNCORE=4) that define the number of cpu-cores that will be used during the model checking process. There no point in setting the number of cores larger than the number of real cpu-cores on your system. It will, for instance, generally cause a slow-down if you compile pan.c for dual-core when you only have a single-core system, etc.
• A multi-core verification run uses shared memory segments that are pre-allocated before all worker processes are spawned. This is different from the default single-core behavior, where memory is allocated on the fly, as needed. This means that you generally have to define the amount of memory that should be made available for the complete run (using -DMEMLIM=N where N is a memory size in Megabytes).
• As before, you should never set the memory limit to a larger value than the amount of physical (not virtual) memory that is available on your system. Note that the maximum amount of memory that your operating system makes available to shared memory segments may be small (e.g., 32 Mbyte on Cygwin) -- see below for ways to increase this to a more realistic number.

Currently supported platforms include Windows, Linux, and Cygwin systems, and possibly also Mac OS/X.
The following specifics apply to each platform:

• Linux (32 and 64 bit recommended)
  • Gnu gcc, both 32-bit and 64-bit versions.
• Windows (32 bit recommended)
  • using the (freely available) Visual Studio Express 2008 compiler for native Windows support
    The 32-bit version is reliable, but the 64-bit compiler cannot currently be recommended.
    With the 64-bit Windows compiler shared memory segments can inexplicably get corrupted or disconnected.
• Cygwin (not recommended)
  • Gnu gcc, using cygserver. At present, no 64-bit version of cygserver is available or expected, so multi-core verification in this mode will is restricted to 32-bit mode. Recent versions of cygwin/cygserver also appear to put additional (seemingly arbitrarily) low memory bounds on shared memory segments (e.g., 482 MB), which limits its use for multi-core verifications.
• Mac OS/X
  • This platform has not been thoroughly tested, but early beta-users have reported that the multi-core options work.

	./pan --

Setup for Linux (64-bit recommended)

         $ /sbin/sysctl -a | grep shmmax   # check what the current value is
         kernel.shmmax = 33554432          # the default value

         $ /sbin/sysctl kernel.shmmax=6442450944        # set new limit of 6 Gb
         kernel.shmmax = 6442450944			# done
or
         $ /sbin/sysctl kernel.shmmax=32212254720 	# 30 Gbyte
         kernel.shmmax = 32212254720			# done

You should also increase the maximum number of shared pages shmall to the number used above divided by the pagesize (e.g., 4096), for instance:

	$ /sbin/sysctl kernel.shmall=7864320 		# for a 30 Gbyte shared memory max

Setup for 32-bit or 64-bit Windows

	To use PSDK with VC2005 Express:
	1. Create a directory "PlatformSDK" under "\ProgramFiles\Microsoft Visual Studio 8\VC"
	2. Copy the "bin", "include" and "lib" directory from the PSDK-installation
	   \Program Files\Microsoft Platform SDK\ into this directory.
	Then you do not need to change any config file.

The following settings for environment variables worked on a Windows XP64 system, but will almost certainly need to be changed for different systems or compiler installations. It is provided here as a example only. Caveat emptor.

	$ cl -nologo hello.c bufferoverflowu.lib

With the standard 32-bit compiler, you will note that the header file stdint.h is missing from the regular Visual Studio installation. The file can be found in Wikipedia, in the entry for stdint.h, and should be place in the include directory, e.g., for VC2008 this is:

	C:/Program\ Files/Microsoft\ Visual\ Studio\ 9.0/VC/include

Setup for 32-bit Cygwin under Windows

If cygserver is not running, it should be started first:

        $ sh /usr/bin/cygserver-config		# the very first time only
        $ cygrunsrv -S cygserver		# once or repeat when it dies

	$ echo $CYGSERVER	# check
	$			# not set
	$ CYGSERVER=server	# set it
	$ export CYGSERVER

You can tell if cygserver is running by executing:

        $ ipcs   # print a list of all current shared memory uses
        Message Queues:
        T     ID               KEY        MODE       OWNER    GROUP
        
        Shared Memory:
        T     ID               KEY        MODE       OWNER    GROUP
        m  65536                    0 --rwarwarwa       gh    Users
        
        Semaphores:
        T     ID               KEY        MODE       OWNER    GROUP

You can use ipcs to see which shared memory segments are in use, and if any stale segments are left over from an aborted run of the model checker (this shouldn't happen, but occassionally it may). To manually remove a stale shared memory segment, use ipcrm
You can also use a script to cleanup after a failed run, possibly with some of the pan processes from a multi-core run lingering. This is optional, every new run of the verifier will try to cleanup any stale segments from previous runs, and a reboot will also cleanup any stale segments. For instance:

	$ cat /bin/doclean
	#!/bin/sh

	# adapt this script to the specific output format of ps
	# and ipcs on your system
	
	ps | sed 1d | grep pan$ | awk '	{ print $1 }' > __id
	for i in `cat __id`
	do	# echo kill stale pan process $i
		kill -9 $i
	done
	
	ipcs | sed 1d | awk '$1=="m"	{ print $2 }' > __id
	
	for i in `cat __id`
	do	# echo remove shared memory segment $i
		ipcrm -m $i
	done
	
	rm -f __id	# cleanup temporary file

Directives Supported for Multi-core Verification

	-DMEMLIM=8000	# allow up to 8 GB of shared memory

	-DDUALCORE  --> same as -DNCORE=2
	-DQUADCORE  --> same as -DNCORE=4
	-DNCORE=N   --> enables multi_core verification if N>1

	-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)

	$ spin -a model.pml	# as before
	$ gcc -DNCORE=3 -DMEMLIM=8000 -DSAFETY -o pan pan.c
	$ ./pan

	-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)

To change the size of the global workqueue (rarely needed):

	-DSET_WQ_SIZE=N --> default 128 (Mbytes)

	-DGLOB_HEAP

	"-DC_INIT=fct()"

	-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 Verification

Liveness Verification

Tuning a Verification run

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

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 --

Full Counter-Examples

	$ ./pan -r

	$ gcc -DNCORE=32 -DFULL_TRAIL -o pan pan.c

Other New Directives

	-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 run

	-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