Fast and Accurate Bitstate Verification for SPIN,
by Peter C. Dillinger and Panagiotis Manolios,
In Proc. of 11th International SPIN Workshop (2004),
Volume 2989 of
Springer LNCS
Bloom Filters in Probabilistic Verification,
by Peter C. Dillinger and Panagiotis Manolios,
In Proc. of FMCAD 2004, Formal Methods in Computer-Aided Design, 2004,
Volume 3312 of
Springer LNCS
Enhanced Probabilistic Verification with 3Spin and 3Murphi,
by Peter C. Dillinger and Panagiotis Manolios,
In Proc. of 12th International SPIN Workshop (2005),
Volume 3639 of
Springer LNCS
The process of generating a C verifier (pan.c) with 3Spin is exactly as with Spin. Users should refer to Spin documentation for this process.
After adding 3Spin capabilities to a Spin 4.2.2 installation, the user won't notice any difference unless the pan.c verifier is compiled with -DTRIPLE_SPIN. Specifying -DTRIPLE_SPIN means the compiled verifier includes both 3Spin's bitstate hashing and hash compaction implementations; neither -DBITSTATE or -DHC is needed. Non-probabilistic verification modes should be used as usual, without -DTRIPLE_SPIN.
3spin requires the math library to be linked into the verifier, which is usually accomplished by adding -lm to the compile command of pan.c
Most Spin compile-time options for BITSTATE mode are supported by 3Spin, including these:
| -DNOREDUCE | Disable partial order reductions (enabled by default). There shouldn't be any reason to disable these--except for experimentation. |
| -DSAFETY | More efficient checking of only safety properties. |
| -DMEMLIM=xxxx | Abort before attempting to use more than xxxx megabytes of memory. This is useful for keeping oneself from accidentally using a configuration that will spill into swap space (slow!). |
| -D | (Advanced use only) Bitstate mode: Instead of triple hashing for
the Bloom filter, use
double hashing (slightly faster; slight limitation on accuracy; only
matters if -k value is greater than 3) Hash Compaction mode: disable ordered hashing (maybe faster; reduces accuracy) |
| -kxx | Instead of the default of 3 (inherited from Spin), use xx
index functions in the Bloom filter (for Bitstate mode). 3Spin truncates
large values to 40 because there's no tangible benefit for using more than
40, and 40 slows things down quite a bit as it is.
New to v3: a negative value passed to -k is treated as the negative of the estimated number of states to be seen. The best number of index functions for this estimate is computed and used. If the best number is quite large, a suitable number that is still quite accurate will be used instead. |
| -hxxx | (Advanced use only) Seed hash functions with specified 32-bit integer. By default, the seed is time-based and practically unique for every run. Specifying a seed enables you to reproduce behavior (though if you specify a file to -U, that file also becomes part of the seed). |
| -Hxxx | Use hash compaction (instead of bitstate) and store the specified number
of bits per state. (min 4; max 64) There is no default because -H requires
and argument and bitstate mode is used if -H is not given.
New to v3: a negative value passed to -H is treated as the negative of the estimated number of states to be seen. The best number of bits per state (up to 64) for this estimate is computed and used. If bitstate mode would be more accurate, that mode is used instead. |
| -Mxxx | Use xxx megabytes between the visited list and the DFS stack.
These will usually be vast majority of the memory allocated by 3Spin.
The size of the DFS stack is determined by -m, so the visited list
will use what is left over.
Set this to about how much memory you can dedicate to 3Spin, and it shouldn't need changing. Default is -M32. For backward compatability, -w is supported. In this case, the power of 2 number of bits is entirely dedicated to the visited list, which might result in a slight speed improvement (bit masking). |
| -Rxx | Run xx times using independent hash functions each time. Default is 1. |
| -U | (New to v3) Instead of the Jenkins hash function, use
a universal hash function and differential hashing. In many cases this
hash function is faster and it more consistently meets theoretical expectation
in terms of accuracy.
(Advanced use only) -Ufff where fff names a file to read random data from (such as /dev/urandom (/dev/random usually blocks waiting for enough information)). With or without a parameter, data from the standard library function random() will be XORed in (so that the -h or time-based seed is significant). Note that a file (if specified) must provide <value to -R> * 96 * sizeof(State) bytes of data. |
| -Q | "Quiet." By default, 3Spin will output a summary of memory usage, give estimated accuracy information, and make recommendations for future runs of the same or a similar model. Analysis is near instantaneous on modern machines, but -Q disables the computation and all of this output. |
For large, complex models, we recommend using about as much physical memory as is available (specified with -M). CNTRSTACK, which eats into memory requirements, is no longer used by 3Spin, so the overhead for partial order reductions is small--but taken into account for -M. -M does not include memroy allocated as part of simulating the system, but this is typically small.
3Spin is optimized for 32-bit machines and may or may not work on machines with different word sizes. 3Spin is also optimized for Intel x86 architectures such as the Pentium 4 and the Pentium III. We developed 3Spin with various versions of GNU/Linux, but should work for other 32-bit platforms supported by Spin.
Taking advantage of 64-bit architectures would require significant changes/updates to 3Spin and might happen in the future.
X3Spin is a graphical user interface (based on XSpin) for interacting with 3Spin (and Spin for exhaustive modes).
After installing 3Spin, X3Spin 3.3 is available in XSpin4.2/x3spin33.tcl. You might need to edit the top of this file to get it working on your machine. The only difference in this process for 3Spin is the line that sets the LIBM variable, which should be
set LIBM "-lm"for systems that need a parameter to include the math library and
set LIBM ""for systems that do not need a parameter. Commenting out the line will cause a problem. Refer to documentation in the file to see if you need to tweak the first few lines, the SPIN variable, or other variables.
Differences with XSpin are mostly confined to the Basic Verification Options screen (accessed by Run... | Set Verification Parameters...) and its subscreens. More specifically, the options in the Search Mode area have been changed. Here you choose between Automatic Config and Manual Config, though the Advanced Options apply to both.
More information can be found in the Help and Explain buttons in these screens.
3Spin version 3.3 is a patch against Spin 4.2.2, available here, according to this license. You should install and be familiar with Spin 4.2.2 before using 3Spin.
To install 3Spin, save the gzipped patch file in the Spin 4.2.2 directory, along side of Src4.2.2, Test, etc., and apply the patch:
gunzip 3spin-3_3.patch.gzSimply recompile Spin (in Src4.2.2) and it works as usual, except that -DTRIPLE_SPIN activates 3Spin's enhancements to pan.c verifiers (see instructions above).
patch -p0 < 3spin-3_3.patch