Setup Instructions for Multi-Core Spin Verifications

Generally, you have to follow these instructions only once for any system. In the unlikely case that the settings are not preserved across a boot though, you may have to repeat them.

Supported platforms for the multi-core algorithms in Spin include Windows, Linux, and Cygwin systems, and possibly also Mac OS/X. The following specifics apply to each platform:

The most stable, and recommended, platform for the Spin multi-core extension is either 32-bit or 64-bit Linux. Most of our development and testing was done under Ubuntu 12.04, with gcc version 4.6.3, using 64-bit compilation.

Setup for Linux (64-bit recommended)

The maximum size of a shared memory segment is defined in /usr/include/linux/shm.h. The default size of a shared segment after a reboot is 32Mb. Before doing multi-core verifications you should change this value with the /sbin/sysctl command (for which you will need superuser privileges).
To check the currently used value:
         $ sudo /sbin/sysctl -a | grep shmmax           # check what the current value is
         kernel.shmmax = 33554432                       # the default value
Change this to close to the size of physical memory on your system. To change the value:
         $ sudo /sbin/sysctl kernel.shmmax=6442450944   # set new limit of 6 Gb
         kernel.shmmax = 6442450944			# done
or
         $ sudo /sbin/sysctl kernel.shmmax=32212254720 	# 30 Gbyte
         kernel.shmmax = 32212254720			# done
(Note that you cannot increase the value above 4 GByte on a 32-bit system and probably shouldn't go above 2 GB to leave room for the rest of the system.)

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

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

On a MAC, the instructions can be found at http://support.apple.com/kb/HT4022#. For instance, you can do:

	$ getconf PAGESIZE	# if needed
	$ sudo echo "kern.sysv.shmmax=1073741824" > /etc/sysctl.conf
	$ sudo echo "kern.sysv.shmall=4096"       > /etc/sysctl.conf
and then restart your system.

Setup for 32-bit or 64-bit Windows

You will need to install the Visual Studio Express C compiler, (e.g. VC2005 or VC2008, or perhaps a more recent version, which can be downloaded from the Microsoft website), and set up the environment for 64-bit or 32-bit compilation. The configuration can be a bit of a discovery process, especially for 64-bit systems if you want to be able to call the cl compiler from the command line. In addition to the compiler proper, you will also need to install the Platform SDK toolkit.
	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 32-bit Windows compiler (VC2005 or VC2008) is free, but not the 64-bit Windows compiler.
(At some point you could download a trial version for free -- a very large file. The use of this 64-bit compiler cannot be recommended though.)

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

	INCLUDE='C:\Program Files\Microsoft Platform SDK for Windows Server 2003 R2\Include;C:\Program Files\Microsoft Platform SDK for Windows Server 2003 R2\Include\crt;C:\Program Files\Microsoft Platform SDK for Windows Server 2003 R2\Include\crt\sys;C:\Program Files\Microsoft Platform SDK for Windows Server 2003 R2\Include\mfc;C:\Program Files\Microsoft Platform SDK for Windows Server 2003 R2\Include\atl'

	LIB='C:\Program Files\Microsoft Platform SDK for Windows Server 2003 R2\Lib\AMD64;C:\Program Files\Microsoft Platform SDK for Windows Server 2003 R2\Lib\AMD64\atlmfc;'

	PATH='/cygdrive/c/cygwin/bin:/cygdrive/c/Program Files/Microsoft Platform SDK for Windows Server 2003 R2/Bin/Win64/x86/AMD64:/cygdrive/c/Program Files/Microsoft Platform SDK for Windows Server 2003 R2/Bin:/cygdrive/c/Program Files/Microsoft Platform SDK for Windows Server 2003 R2/Bin/WinNT:/cygdrive/c/WINDOWS/system32:/cygdrive/c/WINDOWS:/cygdrive/c/WINDOWS/System32/Wbem:/cygdrive/c/PROGRA~2/QuickTime/QTSystem/:/cygdrive/c/Program Files (x86)/Microsoft SQL Server/90/Tools/bin/'

	export PATH INCLUDE LIB
To actually compile a program, you can use a command line such as:
	$ cl -nologo hello.c bufferoverflowu.lib
Note, the explicit listing of the bufferoverflowu.lib file which is needed for the 64-bit compiler only -- the compiler will know where to find it.

With the standard 32-bit compiler, you may run into the problem 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 placed 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

Edit the value of kern.ipc.shmmaxpgs in /etc/cygserver.conf (or /etc/defaults/etc/cygserver.conf if this is the first time you're doing this on a new machine). The default value is 8,192. The maximum value you can set is 32,767. Multiply the number you use by the pagesize (e.g., 4096) to get the maximum size of a shared memory segment that corresponds to this setting. The default size of a shareed memory segment is 32MB and the maximum is 128MB. (In some versions of cygwin, it seems to be impossible to allocate more than about 484 MB of shared memory, which is a serious limitation.)

If cygserver is not running, it should be started first. The following two commands require Administrator privileges. On newer versions of Windows/Cygwin this means that you have to (even if you are already logged in with administrator privileges) right-click the cygwin shell icon and start the bash shell with menu choice "Run as administrator". (This is the cygwin moral equivalent of a sudo on Linux systems.)

        $ sh /usr/bin/cygserver-config		# the very first time only
        $ cygrunsrv -S cygserver		# once or repeat when it dies
Finally, a shell variable CYGWIN=server should be set in the environment. Assuming you use the standard bash shell on cygwin, you can type:
	$ echo $CYGSERVER	# check
	$			# not set
	$ CYGSERVER=server	# set it
	$ export CYGSERVER
It is of course more convenient to set the CYGSERVER variable in your profile, or as part of the standard environment setting.

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
If this command fails the cygserver is not running and should be (re)started.

Both Linux and Cygwin

In case of trouble or confusion, you can use the command 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 should only rarely happen).
To manually remove a stale shared memory segment, use the command 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 possible stale segments from previous runs, and a reboot will of course also cleanup all stale segments.
An example of a cleanup script (that you can place in /bin or /usr/local/bin):
	$ cat 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

Spin home page