Fast and Accurate Bitstate Verification for SPIN
Peter C. Dillinger and Panagiotis Manolios.
SPIN 2004, 11th International SPIN Workshop on Model Checking of Software. © Springer-Verlag
Bitstate hashing in SPIN has proved invaluable in probabilistically detecting errors in large models, but in many cases, the number of omitted states is much higher than it would be if SPIN allowed more than two hash functions to be used. For example, adding just one more hash function can reduce the probability of omitting states at all from 99% to under 3%. Because hash computation accounts for an overwhelming portion of the total execution cost of bitstate verification with SPIN, adding additional independent hash functions would slow down the process tremendously. We present efficient ways of computing multiple hash values that, despite sacrificing independence, give virtually the same accuracy and even yield a speed improvement in the two hash function case when compared to the current SPIN implementation.
Another key to accurate bitstate hashing is utilizing as much
memory as is available. The current SPIN implementation is
limited to only 512MB and allows only power-of-two granularity
(256MB, 128MB, etc). However, using 768MB instead of 512MB could
reduce the probability of a single omission from 20% to less than
one chance in 10,000, which demonstrates the magnitude of both the
maximum and the granularity limitation. We have modified SPIN to
utilize any addressable amount of memory and use any number of
efficiently-computed hash functions, and we present empirical
results from extensive experimentation comparing various
configurations of our modified version to the original SPIN.
PDF (164K) © Springer-Verlag