3Spin Home/Documentation


3Spin (pronounced "Triple Spin") is a modified version of the Spin model checker with advances in the efficiency, configurability, and usability of probabilistic state storage. You can access the web page for the old 3Spin v3.3 here.

New Version Coming Soon

I am in the process of completely rewriting 3Spin (and 3Murphi) to use a new state storage scheme introduced in a 2009 SPIN workshop paper:
Peter C. Dillinger and Panagiotis Manolios.
Fast, All-Purpose State Storage.
(To appear) 16th International SPIN Workshop on Model Checking Software (SPIN), 2009.
Below are links to the code I used in the experiments for that paper and a follow-up paper. That code is essentially an alpha version of a new 3Spin.

Implementation for follow-up paper (under review)

This implementation builds on the implementation below by doing more adaption, making it a little slower but more accurate. The faster (SPIN 2009) design can be enabled with -DFASTCLEARY (in addition to -DCLEARY). This implementation was tested in the follow-up paper under review: tgz | patch (license)

Implementation for SPIN 2009 paper

I added adaptive Cleary table state storage to SPIN 5.1.7 for the "Fast, All-Purpose State Storage" paper. You can download the implementation tested in the paper here: tgz | patch (license)

With my modifications, pan.c must be linked against the math library, which often requires -lm be passed to the compiler.

Here are the important pan.c compile-time options:

Here are some FYI pan.c compile-time options:

If using -DCLEARY, there is one additional runtime option:

Whenever using -DBITSTATE, it outputs expected hash omissions. Some expertise is required to really understand those numbers. More information is in the paper.

Stack Matching in SPIN (an appendix to the SPIN 2009 paper)

SPIN 5.1.7 only has two stack-matching schemes, which under some common conditions are not as fast or compact as classical methods allow. To make a fair comparison to known "state of the art," we implemented another scheme, referred to in the paper as "ChainTable," that fills this void where SPIN's methods are not the fastest or most compact known. "ChainTable," which we call TABLESTACK in the code, is a reasonably simple application of classical techniques, so we do not consider it new science. You can download an implementation of TABLESTACK for SPIN 5.1.7 here: tgz | patch (license)

In communication with Gerard Holzmann, he has acknowledged this is an area that should be looked at again and is investigating TABLESTACK for inclusion the the main SPIN distribution.

SPIN's FULLSTACK is the default in SPIN 5.1.7 except when verifying safety properties in bitstate mode on a 32-bit machine. It keeps all information needed about states on the stack and makes them accessible from a hashtable. This method is by far the slowest and its memory usage is sometimes the worst, but it might be the only one that properly supports liveness verification. This technique is not referred to or compared against in the paper, because it is not a fair comparison in the cases we support.

SPIN's CNTRSTACK, as described in the paper, uses a counting Bloom filter to approximate the set of states on the stack. This is the default in SPIN 5.1.7 when verifying safety properties in bitstate mode on a 32-bit machine. It is the same size as the visited list when that size is a power of two, or occupies 1MB otherwise. The reason for this disparity might be a regression oversight. We conclude that this scheme is probably only merited when the stack is expected to be very large, stack cycling is used (dumping to disk, -DSC), and the visited list is not based on cells. If the visited list is based on cells and very large, tracking active states in the visited list is likely the best option--as shown in the validation section of the paper. If the stack depth is limited to be orders of magnitude smaller than the visited list can accomodate, TABLESTACK is superior in speed, accuracy, and memory usage.

We have written TABLESTACK (referred to as "ChainTable" in the paper) to allow quick lookup of stack states based on the hash value used to store the state in the visited list. When using approximate storage for the visited list, TABLESTACK does not introduce any further approximation (unlike CNTRSTACK). It uses a simple chaining hash table, and memory usage adds only a little to that already needed for the in-memory stack. The in-memory stack is always there anyway unless stack cycling (dumping to disk, -DSC) is used, which TABLESTACK does not support. TABLESTACK is much faster than FULLSTACK but might not properly support liveness verification. TABLESTACK seems to be a little faster than CNTRSTACK.

In speed tests performed for the paper, TABLESTACK is about 4\% faster than CNTRSTACK. FULLSTACK is not presented but is only 2/3rds the speed of TABLESTACK. FULLSTACK also used about three times the memory for the stack as TABLESTACK. For this reason, we compared against TABLESTACK rather than attempting to explain why FULLSTACK performs so poorly in the context of safety verification with an approximate visited list.

The Author(s)

Peter C. Dillinger, advised by Panagiotis (Pete) Manolios