Abstract
This paper discusses a generalised incremental hashing scheme for explicit state model checkers. The hashing scheme has been implemented into the model checker Spin. The incremental hashing scheme works for Spin’s exhaustive and both approximate verification modes: bitstate hashing and hash compaction. An implementation is provided for 32-bit and 64-bit architectures.
We performed extensive experiments on the BEEM benchmarks to compare the incremental hash functions against Spin’s traditional hash functions. In almost all cases, incremental hashing is faster than traditional hashing. The amount of performance gain depends on several factors, though.
We conclude that incremental hashing performs best for the (64-bits) Spin’s bitstate hashing mode, on models with large state vectors, and using a verifier, that is optimised by the C compiler.
This is a preview of subscription content, log in via an institution to check access.
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
Baase, S., van Gelder, A.: Computer Algorithms, 3rd edn. Addison-Wesley (2000)
Cohen, J.D.: Recursive Hashing Functions for N-grams. Transaction On Information Systems 15(3), 291–320 (1997)
Dillinger, P.C., Manolios, P.: Fast and Accurate Bitstate Verification for SPIN. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 57–75. Springer, Heidelberg (2004)
Holzmann, G.J.: On Limits and Possibilities of Automated Protocol Analysis. In: Proc. 7th Int. Workshop on Protocol Specification, Testing and Verification (PSTV 1987), pp. 137–161. North-Holland, Amsterdam (1987)
Holzmann, G.J.: An Analysis of Bitstate Hashing. Formal Methods in System Design 13, 289–307 (1998)
Holzmann, G.J.: The Spin Model Checker – Primer and Reference Manual. Addison-Wesley, Boston (2004)
Jenkins, B.: Hash Functions. Dr. Dobbs Journal 22(9) (September 1997)
Karp, R.M., Rabin, M.O.: Efficient Randomized Pattern-Matching Algorithms. IBM Journal of Research and Development 31(2), 249–260 (1987)
Knuth, D.E.: The Art of Computer Programming, 2nd edn. Sorting and Searching, vol. 3. Addison Wesley Longman Publishing Co., Inc., Redwood City (1998)
Kuntz, M., Lampka, K.: Probabilistic Methods in State Space Analysis. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 339–383. Springer, Heidelberg (2004)
Mehler, T., Edelkamp, S.: Dynamic Incremental Hashing in Program Model Checking. ENTCS 149(2), 51–69 (2006); Proc. of Third Workshop of Model Checking and Artificial Intelligence (MoChArt 2005)
Nguyen, V.Y.: Optimising Techniques for Model Checkers. Master’s thesis, University of Twente, Enschede, The Netherlands (December 2007)
Pelánek, R.: BEEM: Benchmarks for Explicit Model Checkers. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 263–267. Springer, Heidelberg (2007)
Ruys, T.C., de Brugh, N.H.M.A.: MMC: the Mono Model Checker. ENTCS 190(1), 149–160 (2007)
Wolper, P., Leroy, D.: Reliable Hashing without Collosion Detection. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 59–70. Springer, Heidelberg (1993)
BEEM: BEnchmarks for Explicit Model checkers, http://anna.fi.muni.cz/models/
CHASH - Incremental Hashing for SPIN, http://www-i2.cs.rwth-aachen.de/~nguyen/incrementalHashing
Fowler/Noll/Vo (FNV) Hash, http://isthe.com/chongo/tech/comp/fnv/
Hsieh, P.: Hash functions, http://www.azillionmonkeys.com/qed/hash.html
Jenkins, B.: A Hash Function for Hash Table Lookup, http://burtleburtle.net/bob/hash/doobs.html
SPIN: on-the-fly, LTL model checking, http://spinroot.com/
Wang, T.: Integer Hash Function (2007), http://www.cris.com/~Ttwang/tech/inthash.htm
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nguyen, V.Y., Ruys, T.C. (2008). Incremental Hashing for Spin . In: Havelund, K., Majumdar, R., Palsberg, J. (eds) Model Checking Software. SPIN 2008. Lecture Notes in Computer Science, vol 5156. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85114-1_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-85114-1_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85113-4
Online ISBN: 978-3-540-85114-1
eBook Packages: Computer ScienceComputer Science (R0)