Weak Memory Models as LLVM-to-LLVM Transformations

  • Vladimír ŠtillEmail author
  • Petr RočkaiEmail author
  • Jiří BarnatEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9548)


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.


Model Checker Memory Model Store Buffer Data Race Sequential Consistency 
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.


  1. 1.
    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)CrossRefGoogle Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    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)Google Scholar
  4. 4.
    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)CrossRefGoogle Scholar
  5. 5.
    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)CrossRefGoogle Scholar
  6. 6.
    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 2010Google Scholar
  7. 7.
    Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  8. 8.
    Dill, D.: The murphi verification system. Computer Aided Verification. LLNC, vol. 1102, pp. 390–393. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  9. 9.
    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)Google Scholar
  10. 10.
    Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)Google Scholar
  11. 11.
    Jonsson, B.: State-space exploration for concurrent algorithms under weak memory orderings: (preliminary version). SIGARCH Comput. Archit. News 36, 65–71 (2009)CrossRefGoogle Scholar
  12. 12.
    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)Google Scholar
  13. 13.
    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)Google Scholar
  14. 14.
    Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690–691 (1979)CrossRefzbMATHGoogle Scholar
  15. 15.
    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)CrossRefGoogle Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    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)CrossRefGoogle Scholar
  18. 18.
    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)Google Scholar
  19. 19.
    Mckenney, P.E.: Memory Barriers: a Hardware View for Software Hackers. Linux Technology Center, Beaverton (2009)Google Scholar
  20. 20.
    Kuperstein, M., Vechev, M.T., Yahav, E.: Automatic inference of memory fences. In: Formal Methods in Computer-Aided Design, pp. 111–119. IEEE (2010)Google Scholar
  21. 21.
    Park, S., Dill, D.: An executable specification and verifier for relaxed memory order. IEEE Trans. Comput. 48(2), 227–235 (1999)CrossRefGoogle Scholar
  22. 22.
    Ročkai, P.: Model checking software. Disertation thesis, Faculty of Informatics, Masaryk University (2015)Google Scholar
  23. 23.
    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)CrossRefGoogle Scholar
  24. 24.
    Ročkai, P., Barnat, J., Brim, L.: Model checking C++ with exceptions. In: Automated Verification of Critical Systems, vol. 70 (2014)Google Scholar
  25. 25.
    CORPORATE SPARC International, Inc.: The SPARC architecture manual (version 9). Prentice-Hall Inc., Upper Saddle River (1994)Google Scholar
  26. 26.
    Š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)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Faculty of InformaticsMasaryk University BrnoBrnoCzech Republic

Personalised recommendations