This page gives access to the data from the measurements of multi-core depth-first search model checking runs that were reported in The design of a multi-core extension of the Spin model checker, which appeared in IEEE Trans. on Software Engineering, October 2007. That paper, and a few related ones, can be found at the following links.
All measurements reported here were made in May and June 2007, with a pre-release version of Spin 5.0 on a 64-bit Linux system, running Ubuntu version 7.0.4, and with gcc version 4.1.2. The 64-bit machine had two quad-cores (giving a total of 8 CPUs), and 32 GB of main memory. Each quad-core had a 4 MB cache, and each CPU ran at 2.3 GHz. The machine further had several 750 GB disks (not used for these measurements). All measurements were made on an otherwise idle system.
|Tcl code Client side|
|Tcl code Server side|
|Leader Election Protocol (8 processes)||makefile||summary|
|Peterson's Algorithm (4 processes)||makefile||summary|
|Dining Philosophers (9 processes)||makefile||summary|
|Phone Switch Model (4 processes)||makefile||summary|
|Sliding Window Protocol (window size 4)||makefile||summary|
|Reference Model (b=8,S=200,t=13)||makefile||summary|
|Model||StateVector||Model Size (lines)||C code linked||Depth of DFS tree||Nr. States||Data|
|DS1||3,246||487||10,781||179 K||216 M||summary|
|DEOS 1)||576||6,635||0||24,763 K||22 M||summary|
|EO1 2)||2,736||3,949||0||0.3 K||10 M||summary|
|Gurdag 3)||964||1,646||0||597 K||601 M||summary|
|NVDS 4)||180||1,229||6,068||1.5 K||247 M||summary|