Setup Instructions for Multi-Core Spin Verifications

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:

• Linux
  • use gcc (freely available), both 32-bit and 64-bit versions.
• Windows
  • use the (freely available) Visual Studio Express 2008 compiler for native Windows support
    The 32-bit version is reliable. We don't have good experience with the 64-bit compiler. The last time we tried to use the 64-bit Windows compiler (approx 2009), shared memory segments could inexplicably get corrupted or disconnected.
• Cygwin/Windows (not recommended)
  • use gcc, with the cygserver enabled. At present (2012), no 64-bit version of cygserver is available or expected, so multi-core verification in this mode remains restricted to 32-bit mode. The last versions of cygwin/cygserver that we tried appear to put 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 beta-users have reported that the multi-core options do work. Your mileage may vary.

Setup for Linux (64-bit recommended)

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

         $ sudo /sbin/sysctl kernel.shmmax=6442450944   # set new limit of 6 Gb
         kernel.shmmax = 6442450944			# done

         $ sudo /sbin/sysctl kernel.shmmax=32212254720 	# 30 Gbyte
         kernel.shmmax = 32212254720			# done

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

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

	$ cl -nologo hello.c bufferoverflowu.lib

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

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

	$ 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

Both Linux and Cygwin

	$ 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