Abstract
We present an overview of techniques that, in combination, lead to a memory-efficient implementation of a model checker for LLVM bitcode, suitable for verification of realistic C and C++ programs.
As a central component, we present the design of a tree compression scheme and evaluate the implementation in context of explicit-state safety, LTL and untimed-LTL (for timed automata) model checking. Our design is characterised by dynamic, multi-way adaptive partitioning of state vectors for efficient storage in a tree-compressed hash table, representing the closed set in the model checking algorithm. To complement the tree compression technique, we present a special-purpose memory allocation algorithm with very compact memory layout and negligible performance penalty.
This work has been partially supported by the Czech Science Foundation grant No. 15-08772S.
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
Notes
- 1.
In theory, nothing about LLVM per se causes states to be large; in practice, however, inputs that are expressed in terms of LLVM have a tendency to have much richer state than more traditional formalisms, like DVE or ProMeLa.
- 2.
The LTSmin model checker avoids this particular resource split by storing state vectors decomposed, each fixed-size chunk stored inline in the large pre-allocated hash table.
- 3.
Intra-process parallelism can be very useful even when multiple verification instances are involved. A 64-core system can easily accommodate 4 verification tasks running on 16 cores each, splitting memory between those 4 tasks as needed. If memory becomes scarce, some of the processes can be suspended and swapped out to disk and later, when other tasks have finished, resumed again.
- 4.
If we extrapolate from the biggest model, hashset-3-1, we can estimate maximum tractable state space size to be over 40 billion vertices considering high-end server with 2TB of RAM, this could result in around 950 TB of raw uncompressed state space.
References
Barnat, J., et al.: DiVinE 3.0 – an explicit-state model checker for multithreaded C and C++ programs. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 863–868. Springer, Heidelberg (2013)
Blom, S., Lisser, B., van de Pol, J., Weber, M.: A database approach to distributed state space generation. Electron. Notes Theor. Comput. Sci. 198(1), 17–32 (2008)
Geldenhuys, J., de Villiers, P.J.A., Rushby, J.: Runtime efficient state compaction in SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 12–21. Springer, Heidelberg (1999)
Holzmann, G.J.: State compression in SPIN: recursive indexing and compression training runs. In: The International SPIN Workshop (1997)
Holzmann, G.J., Godefroid, P., Pirottin, D.: Coverage preserving reduction strategies for reachability analysis. In: PSTV, pp. 349–363 (1992)
Laarman, A., van de Pol, J., Weber, M.: Parallel recursive state compression for free. In: Groce, A., Musuvathi, M. (eds.) SPIN Workshops 2011. LNCS, vol. 6823, pp. 38–56. Springer, Heidelberg (2011)
Peled, D.: Ten years of partial order reduction. In: Vardi, Moshe Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 17–28. Springer, Heidelberg (1998)
Ročkai, P., Barnat, J., Brim, L.: Improved state space reductions for LTL model checking of C and C++ programs. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 1–15. Springer, Heidelberg (2013)
Štill, V.: Compression, State Space, for the DiVinE Model Checker, : Bachelor’s thesis. Masaryk University Brno, Faculty of Informatics (2013)
Ziv, J., Lempel, A.: A universal algorithm for sequential data compression. IEEE Trans. Inf. Theor. 23(3), 337–343 (1977)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Ročkai, P., Štill, V., Barnat, J. (2015). Techniques for Memory-Efficient Model Checking of C and C++ Code. In: Calinescu, R., Rumpe, B. (eds) Software Engineering and Formal Methods. SEFM 2015. Lecture Notes in Computer Science(), vol 9276. Springer, Cham. https://doi.org/10.1007/978-3-319-22969-0_19
Download citation
DOI: https://doi.org/10.1007/978-3-319-22969-0_19
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-22968-3
Online ISBN: 978-3-319-22969-0
eBook Packages: Computer ScienceComputer Science (R0)