Abstract
Data races are among the most difficult software bugs to discover. They arise from multiple threads accessing the same memory location, a situation which is often hard to discern from source code alone. Detection of such bugs is further complicated by individual CPUs’ use of relaxed memory models. As a matter of fact, proving absence of data races is a typical task for automated formal verification. In this paper, we present a new approach for verification of multi-threaded C and C++ programs under weakened memory models (using store buffer emulation), using an unmodified model checker that assumes Sequential Consistency. In our workflow, a C or C++ program is translated into LLVM bitcode, which is then automatically extended with store buffer emulation. After this transformation, the extended LLVM bitcode is model-checked against safety and/or liveness properties with our explicit-state model checker DIVINE.
This work has been partially supported by the Czech Science Foundation Grant no. 15-08772S.
P. Ročkai—The contribution of Petr Ročkai has been partially supported by Red Hat, Inc.
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
Similar content being viewed by others
Notes
References
Alglave, J., Maranget, L.: Stability in weak memory models. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 50–66. Springer, Heidelberg (2011)
Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: Proceedings of the 37th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 7–18. ACM, New York, NY, USA (2010)
Barnat, J., Brim, L., Havel, V.: LTL Model checking of parallel programs with under-approximated TSO memory model. In: Application of Concurrency to System Design (ACSD), pp. 51–59. IEEE (2013)
Barnat, J., Brim, L., Havel, V., Havlíček, J., Kriho, J., Lenčo, M., Ročkai, P., Štill, V., et al.: DiVinE 3.0 - an explicit-state model checker for multithreaded C & C++ programs. CAV 2013. LNCS, vol. 8044, pp. 863–868. Springer, Heidelberg (2013)
Burckhardt, S., Musuvathi, M.: Effective program verification for relaxed memory models. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 107–120. Springer, Heidelberg (2008)
Burnim, J., Sen, K., Stergiou, C.: Sound and complete monitoring of sequential consistency in relaxed memory models. In: Technical report UCB/EECS-2010-31, EECS Department, University of California, Berkeley, March 2010
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Dill, D.: The murphi verification system. Computer Aided Verification. LLNC, vol. 1102, pp. 390–393. Springer, Heidelberg (1996)
Fang, X., Lee, J., Midkiff, S.P.: Automatic fence insertion for shared memory multiprocessing. In: International Conference on Supercomputing (ICS 2003), pp. 285–294. ACM (2003)
Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)
Jonsson, B.: State-space exploration for concurrent algorithms under weak memory orderings: (preliminary version). SIGARCH Comput. Archit. News 36, 65–71 (2009)
Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692–707. Springer, Heidelberg (2015)
Kuperstein, M., Vechev, M., Yahav, E.: Partial-coherence abstractions for relaxed memory models. In: Programming Language Design and Implementation (PLDI 2011), pp. 187–198. ACM (2011)
Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690–691 (1979)
Lehmann, D.J., Pnueli, A., Stavi, J.: Impartiality, justice, fairness: the ethics of concurrent termination. ICALP. LNCS, vol. 115, pp. 264–277. Springer, Heidelberg (1981)
Linden, A., Wolper, P.: An automata-based symbolic approach for verifying programs on relaxed memory models. In: van de Pol, J., Weber, M. (eds.) Model Checking Software. LNCS, vol. 6349, pp. 212–226. Springer, Heidelberg (2010)
Linden, A., Wolper, P.: A verification-based approach to memory fence insertion in relaxed memory systems. In: Groce, A., Musuvathi, M. (eds.) SPIN Workshops 2011. LNCS, vol. 6823, pp. 144–160. Springer, Heidelberg (2011)
Mador-Haim, S., Alur, R., Martin, M.M.K.: Specifying relaxed memory models for state exploration tools. In: \((EC)^2\): Workshop on Exploting Concurrency Eficiently and Correctly (2009)
Mckenney, P.E.: Memory Barriers: a Hardware View for Software Hackers. Linux Technology Center, Beaverton (2009)
Kuperstein, M., Vechev, M.T., Yahav, E.: Automatic inference of memory fences. In: Formal Methods in Computer-Aided Design, pp. 111–119. IEEE (2010)
Park, S., Dill, D.: An executable specification and verifier for relaxed memory order. IEEE Trans. Comput. 48(2), 227–235 (1999)
Ročkai, P.: Model checking software. Disertation thesis, Faculty of Informatics, Masaryk University (2015)
Ročkai, P., Barnat, J., Brim, L.: Improved state space reductions for LTL model checking of C and C++ programs. NFM 2013. LNCS, vol. 7871, pp. 1–15. Springer, Heidelberg (2013)
Ročkai, P., Barnat, J., Brim, L.: Model checking C++ with exceptions. In: Automated Verification of Critical Systems, vol. 70 (2014)
CORPORATE SPARC International, Inc.: The SPARC architecture manual (version 9). Prentice-Hall Inc., Upper Saddle River (1994)
Štill, V., Ročkai, P., Barnat, J.: Context-switch-directed verification in DIVINE. In: Hliněný, P., Dvořák, Z., Jaroš, J., Kofroň, J., Kořenek, J., Matula, P., Pala, K. (eds.) MEMICS 2014. LNCS, vol. 8934, pp. 135–146. Springer, Heidelberg (2014)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Štill, V., Ročkai, P., Barnat, J. (2016). Weak Memory Models as LLVM-to-LLVM Transformations. In: Kofroň, J., Vojnar, T. (eds) Mathematical and Engineering Methods in Computer Science. MEMICS 2015. Lecture Notes in Computer Science(), vol 9548. Springer, Cham. https://doi.org/10.1007/978-3-319-29817-7_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-29817-7_13
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-29816-0
Online ISBN: 978-3-319-29817-7
eBook Packages: Computer ScienceComputer Science (R0)