[banner]

Verifying
Multi-threaded
Software
with Spin

[logo]
Spin is a popular open-source software verification tool, used by thousands of people worldwide. The tool can be used for the formal verification of multi-threaded software applications. The tool was developed at Bell Labs in the Unix group of the Computing Sciences Research Center, starting in 1980. The software has been available freely since 1991, and continues to evolve to keep pace with new developments. In April 2002 the tool was awarded the ACM System Software Award. [read more]


      discover       learn       use       community

The Spin 2015 workshop will be held at the University of Stellenbosch, in South Africa, 24-26 August 2015. The workshop organizers are Bernd Fischer and Jaco Geldenhuys.
    • Abstracts: 17 April 2015
    • Full papers: 24 April 2015
    • Author notifications: 15 June 2015
    • Camera ready papers: 6 July 2015
    // a small example spin model
    // Peterson's solution to the mutual exclusion problem (1981)
    
    bool turn, flag[2];		// the shared variables, booleans
    byte ncrit;        		// nr of procs in critical section
    
    active [2] proctype user()	// two processes
    {
    	assert(_pid == 0 || _pid == 1);
    again:
    	flag[_pid] = 1;
    	turn = _pid;
    	(flag[1 - _pid] == 0 || turn == 1 - _pid);
    
    	ncrit++;
    	assert(ncrit == 1);	// critical section
    	ncrit--;
    
    	flag[_pid] = 0;
    	goto again
    }
    // analysis: 
    // $ spin -a peterson.pml
    // $ cc -o pan pan.c
    // $ ./pan

[revert to the old spin homepage]