3Spin Home/Documentation

Intro

New Version Coming Soon

Peter C. Dillinger and Panagiotis Manolios.
Fast, All-Purpose State Storage.
(To appear) 16th International SPIN Workshop on Model Checking Software (SPIN), 2009.

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:

• -DBITSTATE is required both for bitstate (Bloom filter) storage or for Cleary table storage.
• -DCLEARY enables adaptive Cleary tables rather than Bloom filter storage.
• You must specify one of the following unless -DNOREDUCE is used: (See the section on stack matching below.)
  • -DCNTRSTACK uses a counting Bloom filter. Built-in to SPIN.
  • -DFULLSTACK uses a bulky, slow hash table. Built-in to SPIN.
  • -DTABLESTACK uses a compact, fast chaining hash table. Requires -DBITSTATE (with or without -DCLEARY). Not compatible with -DSC.
  • -DCLEARYSTACK uses integrated stack matching the the Cleary table. Requires -DCLEARY. Compatible with -DSC.

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

• -DSC swaps the stack out to disk as needed rather than clipping at depth limit.
• -DSAFETY speeds up verification of safety properties. (I haven't tested my implementation with liveness.)
• -DNOREDUCE disables partial-order reduction, which eliminates the need for the stack proviso but is likely to blow up state space size.

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

• -oN specifies the maximum occupancy of the Cleary tables before adaption, as an integer percentage. This should typically be between 50 and 95. The default is 85. Higher means slower but possibly more accurate. Lower means faster and possibly less accurate.

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)