Abstract
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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bloom, B.H.: Space/time trade-offs in hash coding with allowable errors. Communications of the ACM 13(7), 422–426 (1970)
Broder, A., Mitzenmacher, M.: Network applications of Bloom filters: A survey. In: Proc. of the 40th Annual Allerton Conference on Communication, Control, and Computing, pp. 636–646 (2002)
Ip, C.N., Dill, D.L.: Better verification through symmetry. In: Agnew, D., Claesen, L., Camposano, R. (eds.) Computer Hardware Description Languages and their Applications, Ottawa, Canada, pp. 87–100. Elsevier Science Publishers B.V., Amsterdam (1993)
Cormen, T.H., Stein, C., Rivest, R.L., Leiserson, C.E.: Introduction to Algorithms. McGraw-Hill Higher Education, New York (2001)
Dillinger, P.C.: 3SPIN Home Page, http://www.cc.gatech.edu/~peterd/3spin/
Godefroid, P., Wolper, P.: A partial approach to model checking. In: Logic in Computer Science, pp. 406–415 (1991)
Gonnet, G.H.: Handbook of Algorithms and Data Structures. Addison-Wesley, Reading (1984)
Holzmann, G., Peled, D.: Partial order reduction of the state space. In: First SPIN Workshop, Montrèal, Quebec (1995)
Holzmann, G.J.: Algorithms for automated protocol validation. Technical Report 69:32-44, AT&T Technical Journal (1990)
Holzmann, G.J.: An analysis of bitstate hashing. In: Proc. 15th Int. Conf on Protocol Specification, Testing, and Verification, INWG/IFIP, Warsaw, Poland, pp. 301–314. Chapman & Hall, Boca Raton (1995)
Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Boston (2003)
Jenkins, B.: (1996), http://burtleburtle.net/bob/c/lookup2.c
Jenkins, B.: Algorithm alley: Hash functions. Dr. Dobb’s Journal (September 1997)
Knuth, D.E.: The Art of Computer Programming, 2nd edn. Sorting and Searching, vol. 3. Addison Wesley Longman Publishing Co., Inc., Amsterdam (1997)
Stern, U., Dill, D.L.: Improved probilistic verification by hash compaction. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, Springer, Heidelberg (1995)
Stern, U., Dill, D.L.: A new scheme for memory-efficient probabilistic verification. In: Joint Int. Conf. on Formal Description Techn. for Distr. Systems and Comm. Protocols, and Protocol Spec., Testing, and Verification, pp. 333–348 (1996)
Wolper, P., Leroy, D.: Reliable hashing without collision detection. In: 5th International Conference on Computer Aided Verification, pp. 59–70 (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dillinger, P.C., Manolios, P. (2004). Fast and Accurate Bitstate Verification for SPIN. In: Graf, S., Mounier, L. (eds) Model Checking Software. SPIN 2004. Lecture Notes in Computer Science, vol 2989. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24732-6_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-24732-6_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21314-7
Online ISBN: 978-3-540-24732-6
eBook Packages: Springer Book Archive