Notes on Measurements

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:

Multi-core verification shows most promise for larger applications, and especially for the verification of safety properties. This is good news because that is where a speedup can be most effective. The downside is though that it becomes somewhat harder to show the potential with the standard small benchmark examples. In some cases, there is no speedup for small models, and sometimes there is a penalty for invoking the machinery of shared memory in very short runs. It is generally not productive to try multi-core verification for runs that would normally take less than a few minutes of run time with an optimized single-core Spin verification. Where it starts to matter is for runs that would take an hour or more -- state-vector sizes that run into the thousands of bytes, heavy use of non-determinism, and transitions with embedded C code. Longer runtimes are often an exception for Spin, but with large problem sizes and large main memory sizes (64 GB and up) this is longer be the case. Unfortunately, the large examples in our database, where we can show linear speedup of multi-core over single-core verifications, cannot be publically distributed, but we can of course report the performance results for the verification of these models with multi-core algorithms.

For liveness verification, only dual-core verification is currently supported.

There appear to be some obscure issues when compiling with the Windows Visual Studio compiler in 64 bit mode -- so results for this mode are not yet included here. We may temporarily need to rely on the Intel 64-bit compiler for this mode to work reliably.