SPIN Models

This page contains SPIN models for a concurrent set algorithm with the instructions of how to use them. The models contains the procedure for checking linearizability with linearization points (fixed and in another thread). The models were used in the following papers:

Experience with Model Checking Linearizability
Martin Vechev, Eran Yahav, Greta Yorsh
SPIN 2009
PDF

Deriving Linearizable Fine-Grained Concurrent Objects
Martin Vechev and Eran Yahav.
ACM PLDI 2008
PDF

Instructions:

  • Download model: Model (Right click and Save As)
  • Download shell file: compile.sh (Right click and Save As)
  • Download SPIN here: Download Spin
  • Type: "bash compile.sh".
  • You will get as output a file called "test".
  • You can run "test". That should require several gigabytes of memory to complete.
    Note: we only tested these models under Linux

Explanations:

  • The model contains 2 threads that execute an (unbounded) most-general client (randomly picks an operation and a key).
  • The maximum number of objects (#define NODES 12) is determined by a formula as a function of the number of distinct keys. See comments in the model. This allows us to explore up to a certain number of keys and adjust the number of nodes accordingly.
  • The model contains the checking for linearizability for non-fixed points as described in the papers.
  • The model contains a reference counting garbage collector.
  • Note that the USETRACE macro is commented out. It means that here we only use the method for checking linearizability with linearization points specified.