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


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

Spin Models

Other issues mentioned in the paper


*) 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