Abstract
In verification by explicit state enumeration a randomly accessed state table is maintained. In practice, the total main memory available for this state table is a major limiting factor in verification. We describe a version of the explicit state enumeration verifier Murϕ that allows the use of magnetic disk instead of main memory for storing almost all of the state table. The algorithm avoids costly random accesses to disk and amortizes the cost of linearly reading the state table from disk over all states in a given breadth-first level. The remaining runtime overhead for accessing the disk is greatly reduced by combining the scheme with hash compaction. We show how to do this combination efficiently and analyze the resulting algorithm. In experiments with three complex cache coherence protocols, the new algorithm achieves memory savings factors of one to two orders of magnitude with a runtime overhead of typically only around 15%.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Sequential circuit verification using symbolic model checking. In 27th ACM/IEEE Design Automation Conference, pages 46–51, 1990.
J. L. Carter and M. N. Wegman. Universal classes of hash functions. Journal of Computer and System Sciences, 18(2):143–54, 1979.
C.-T. Chou and D. Peled. Formal verification of a partial-order reduction technique for model checking. In Tools and Algorithms for the Construction and Analysis of Systems. 2nd International Workshop, pages 241–57, 1996.
D. L. Dill. The Murφ verification system. In Computer Aided Verification. 8th International Conference, pages 390–3, 1996.
]G. J. Holzmann. On limits and possibilities of automated protocol analysis. In Protocol Specification, Testing, and Verification. 7th International Conference, pages 339–44, 1987.
G. J. Holzmann and D. Peled. The state of SPIN. In Computer Aided Verification. 8th International Conference, pages 385–9, 1996.
IEEE Std 1596-1992, IEEE Standard for Scalable Coherent Interface (SCI).
C. N. Ip. State Reduction Methods for Automatic Formal Verification. PhD thesis, Stanford University, 1996.
J. Kuskin, D. Ofelt, M. Heinrich, J. Heinlein, R. Simoni, K. Gharachorloo, J. Chapin, D. Nakahira, J. Baxter, M. Horowitz, A. Gupta, M. Rosenblum, and J. Hennessy. The Stanford FLASH multiprocessor. In 21st Annual International Symposium on Computer Architecture, pages 302–13, 1994.
D. Lenoski, J. Laudon, K. Gharachorloo, W.-D. Weber, A. Gupta, J. Hennessy, M. Horowitz, and M. S. Lam. The Stanford DASH multiprocessor. Computer, 25(3):63–79, 1992.
D. Peled. Combining partial order reductions with on-the-fly model-checking. In Computer Aided Verification. 6th International Conference, pages 377–90, 1994.
A. W. Roscoe. Model-checking CSP. In A Classical Mind, Essays in Honour of C. A. R. Hoare. Prentice-Hall, 1994.
U. Stern. Algorithmic Techniques in Verification by Explicit State Enumeration. PhD thesis, Technical University of Munich, 1997.
U. Stern and D. L. Dill. Improved probabilistic verification by hash compaction. In Advanced Research Working Conference on Correct Hardware Design and Verification Methods, pages 206–24, 1995.
U. Stern and D. L. Dill. A new scheme for memory-efficient probabilistic verification. In Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification, pages 333–48, 1996.
U. Stern and D. L. Dill. Parallelizing the Murφ verifier. In Computer Aided Verification. 9th International Conference, pages 256-67, 1997.
P. Wolper and D. Leroy. Reliable hashing without collision detection. In Computer Aided Verification. 5th International Conference, pages 59–70, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stern, U., Dill, D.L. (1998). Using magnetic disk instead of main memory in the Mur ϕ verifier. In: Hu, A.J., Vardi, M.Y. (eds) Computer Aided Verification. CAV 1998. Lecture Notes in Computer Science, vol 1427. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028743
Download citation
DOI: https://doi.org/10.1007/BFb0028743
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64608-2
Online ISBN: 978-3-540-69339-0
eBook Packages: Springer Book Archive