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