Although these papers use Spin for experimental validation, the ideas are relevant to the design and use of 3Murphi, which incorporates virutally all of the techniques discussed therein:
Fast and Accurate Bitstate Verification for SPIN,
by Peter C. Dillinger and Panagiotis Manolios,
In Proc. of 11th Int'l SPIN Workshop,
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
The process of generating a C++ verifier with 3Murphi is exactly as with generating a hash compaction based verifier with Murphi, mu -c mymodel.m. Using -b with 3Murphi presents a similar trade-off as it does with a hash compaction based Murphi verifier.
Users should refer to Murphi documentation for details on the process of building a model and generating a verifier.
-DTRIPLE_MURPHI may or may not be compatible with other various preprocessing flags used in compiling the verifier, but none should be required. However, we recommend compiling with optimizations (e.g. -O3) because we have seen greater than two-fold speed-ups from enabling optimization in Murphi and 3Murphi.
| -c | Use hash compaction instead of the default of using a Bloom filter. Note that this is a change of default behavior from regular Murphi, but it works well with the probabilistic verification methodology described in our research papers. |
| -bxx |
In Bloom filter mode (no -c): Set xx bits
per state instead of the default of 3 (inherited from Spin and "supertrace").
Must be at least 1 and values larger than 40 will be truncated to 40.
In Hash Compaction mode (with -c): Store xx bits per state instead of the 3Murphi default of 32. Values outside the valid range of 4 to 64 will be truncated to the nearest valid value. |
| -j | Use the Jenkins LOOKUP2 hash function instead of Murphi's default. This hash function can be faster but might not be quite as accurate. |
| -mxxx | Use xxx megabytes for the Bloom filter or compacted hash table. No subtractions are made for stack/queue space. (see below) |
| -kxxx | Use xxx kilobytes for the Bloom filter or compacted hash table. No subtractions are made for stack/queue space. (see below) |
The storage of todo states presents some interesting trade-offs. Using bit-compaction (-b to mu) means these states will be much smaller, but Murphi is much slower at processing bit-compacted states. This is the first trade-off.
The second trade-off deals with how much memory to dedicate to the visited list. Dedicating nearly all of main memory to the visited list (e.g. -m480 on a 512MB machine) maximizes accuracy without killing the execution time by having the visited list spill into swap space. However, in our experience, the todo list gets much bigger than an appropriately-sized visited list, meaning the bulk of the todo list will be swapped out if the visited list is taking up 90+% of main memory. This will slow down the verification process, but not intractably. The todo list is accessed linearly, whereas the visited list is accessed randomly. But the entire process is fastest if both lists fit in main memory.
A good strategy would be to dedicate about 20% of main memory to the visited list when first verifying a model. Using the default setting of a 3-bit Bloom filter will almost certainly find errors if there are any, and the todo list is likely to fit in the rest of main memory. In following up to double-check error-freedom, one could dedicate more memory to the visited list, enabling more accuracy at a possible speed cost. Notice that the recommendations output by 3Murphi are based on -e, which does not need to change if you increase the memory dedicated to the visited list. Drastically reducing the visited list memory could, however, hurt coverage enough to make the visitable size estimate too large.
Taking advantage of 64-bit architectures would require significant changes/updates to 3Murphi and might happen in the future.
patch -p0 < 3murphi-3_2.patchThis patches files in include, so no rebuilding is necessary other than compiling verifiers with -DTRIPLE_MURPHI (see instructions above).