Sample multi-core verification runs for Small Verification Models

This first set contains six relatively small examples of verification models, together with measurements of the performance of single and dual-core verification runs. All measurements were made with a pre-release version of Spin version 5.0, in May 2007, on a multi-core system running at 2.3 GHz.

The examples are: leader election, sliding window, Peterson's mutual exclusion, dining philosophers, a phone-switch model, and a standard reference model that has been used in much of the development.

The verifications were all run on a 64-bit Linux system, but can also be run on 32-bit linux, 32-bit cygwin, or native Windows (with the Visual Studio compiler). The shared memory support on 64-bit Windows XP (with the matching 64-bit Visual Studio compiler) did not seem stable at the time these experiments were done, leading to unresolved corruption issues in the shared memory segments that we believe originate in the O/S -- so this mode is not currently supported.

To compile the small benchmarks on other platforms, the makefiles would have to be adjusted:

	Linux   32-bit: compile gcc -m32 -DHASH32
	Cygwin  32-bit: compile gcc -DCYGWIN (and make sure cygserver is running)
	Windows 32-bit: compile cl -DWIN32 -wd4996 -nologo
	Windows 64-bit: compile cl -DWIN64 (but be aware of platform instability)

We include default runs, with minimally necessary settings, and runs with an attempt at more carefully tuned problem-specific parameter settings. The more carefully tuned runs often give better performance, but there are a few exceptions.

Some notes: