Spin Multi-Core Depth-First Search

Spin Multi-Core Depth-First Search
Supported in Spin Version 5 and later

Overview

This page describes Spin's multi-core depth-first search mode, supported in Spin Version 5.0 and later.
For a description of the (much simpler) multi-core breadth-first search mode, supported in Spin Version 6.2 and later, click here. For multicore swarm search, click here.
Generic installation and setup instructions for shared memory use with Spin can be found here.
An overview of the directives that support multicore Depth-First search can be found here.

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.

Shell Scripts used

do_clean -- to remove stale shared memory segments (linux)
keys -- to extract summary data from ./pan output to generate the summaries below.

Spin Models

peterson_v1.pml -- Basic Spin model of Peterson's algorithm for 2 processes.
peterson_v2.pml -- More detailed model of Peterson's algorithm.
termination.pml -- Spin model for Distributed termination detection.

Other issues mentioned in the paper

peterson.c -- C implementation of Peterson's algorithm, to demonstrate faulty mutual exclusion on modern CPUs with out of order execution.
peterson_asm.txt -- disassembly of compiled code
Wikipedia entry on Peterson's algorithm.

Data

`Table 1:`

dimc_send.c (Windows)

dimc_recv.c (Linux)

`Tables 3 and 4:`

Notes

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

`Tables 5 and 6, and Figure 7:`

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

1) The DEOS model was built by Murali Rangarajan from Honeywell.
2) The EO1 model was mechanically extracted from an AI planning model, by Klaus Havelund at NASA/JPL.
3) The Gurdag model was built by A. Burak Gurdag.
4) The NVDS model was built by Rajeev Joshi at NASA/JPL.

*) The article is (c) 2007 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

Spin home page

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