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 |
dimc_disk.c |
dimc_send.c (Windows) |
dimc_recv.c (Linux) |
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 |