Optimal stateless model checking under the release-acquire semantics

Abstract

We present a framework for the efficient application of stateless model checking (SMC) to concurrent programs running under the Release-Acquire (RA) fragment of the C/C++11 memory model. Our approach is based on exploring the possible program orders, which define the order in which instructions of a thread are executed, and read-from relations, which specify how reads obtain their values from writes. This is in contrast to previous approaches, which also explore the possible coherence orders, i.e., orderings between conflicting writes. Since unexpected test results such as program crashes or assertion violations depend only on the read-from relation, we avoid a potentially significant source of redundancy. Our framework is based on a novel technique for determining whether a particular read-from relation is feasible under the RA semantics. We define an SMC algorithm which is provably optimal in the sense that it explores each program order and read-from relation exactly once. This optimality result is strictly stronger than previous analogous optimality results, which also take coherence order into account. We have implemented our framework in the tool Tracer. Experiments show that Tracer can be significantly faster than state-of-the-art tools that can handle the RA semantics.

References

1. P.A. Abdulla, S. Aronis, M. Faouzi Atig, B. Jonsson, C. Leonardsson, and K. Sagonas. 2015a. Stateless Model Checking for TSO and PSO. In Tools and Algorithms for the Construction and Analysis of Systems, (TACAS) (LNCS), Vol. 9035. Springer, London, UK, 353–367.
2. Parosh Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2014. Optimal Dynamic Partial Order Reduction. In Symposium on Principles of Programming Languages, (POPL). ACM, San Diego, CA, USA, 373–384.
3. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. 2016a. The Benefits of Duality in Verifying Concurrent Programs under TSO. In CONCUR 2016. 5:1–5:15.
4. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. 2017. Context-Bounded Analysis for POWER. In TACAS 2017. 56–74.
5. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Carl Leonardsson. 2016b. Stateless Model Checking for POWER. In Computer Aided Verification, (CAV) (LNCS), Vol. 9780. Springer, Toronto, ON, Canada, 134–156.
6. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Ngo Tuan Phong. 2015b. The Best of Both Worlds: Trading Efficiency and Optimality in Fence Insertion for TSO. In ESOP 2015. 308–332.
7. Jade Alglave, Daniel Kroening, Vincent Nimal, and Michael Tautschnig. 2013b. Software Verification for Weak Memory via Program Transformation. In European Symposium on Programming, (ESOP) (LNCS), Vol. 7792. Springer, Rome, Italy, 512–532.
8. Jade Alglave, Daniel Kroening, and Michael Tautschnig. 2013a. Partial Orders for Efficient Bounded Model Checking of Concurrent Software. In Computer Aided Verification, (CAV) (LNCS), Vol. 8044. Springer, Saint Petersburg, Russia, 141–157.
9. J. Alglave, L. Maranget, and M. Tautschnig. 2014. Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory. ACM Trans. Program. Lang. Syst. 36, 2 (2014), 7:1–7:74.
10. Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi. 2010. On the verification problem for weak memory models. In POPL 2010. 7–18.
11. S. Burckhardt, R. Alur, and M.M.K. Martin. 2007. CheckFence: checking consistency of concurrent data types on relaxed memory models. In Programming Language Design and Implementation, (PLDI). ACM, San Diego, California, USA, 12–21.
12. S. Burckhardt and M. Musuvathi. 2008. Effective Program Verification for Relaxed Memory Models. In Computer Aided Verification, (CAV) (LNCS) , Vol. 5123. Springer, Princeton, NJ, USA, 107–120.
13. J. Burnim, K. Sen, and C. Stergiou. 2011. Testing concurrent programs on relaxed memory models. In International Symposium on Software Testing and Analysis, (ISSTA) . ACM, Toronto, ON, Canada, 122–132.
14. Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. 2018. Data-centric dynamic partial order reduction. PACMPL 2, POPL (2018), 31:1–31:30.
15. M. Christakis, A. Gotovos, and K. Sagonas. 2013. Systematic Testing for Detecting Concurrency Errors in Erlang Programs. In International Conference on Software Testing, Verification and Validation, (ICST). IEEE, Luxembourg, Luxembourg, 154–163.
16. Edmund M. Clarke, Orna Grumberg, Marius Minea, and Doron A. Peled. 1999. State Space Reduction Using Partial Order Techniques. STTT 2, 3 (1999), 279–287.
17. Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. Introduction to Algorithms. The MIT Press.
18. Brian Demsky and Patrick Lam. 2015. SATCheck: SAT-directed stateless model checking for SC and TSO. In Object-Oriented Programming, Systems, Languages, and Applications, (OOPSLA) . ACM, Pittsburgh, PA, USA, 20–36.
19. C. Flanagan and P. Godefroid. 2005. Dynamic partial-order reduction for model checking software. In Principles of Programming Languages, (POPL) . ACM, Long Beach, California, USA, 110–121.
20. P. Godefroid. 1996. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem . Ph.D. Dissertation. University of Liège. Also, volume 1032 of LNCS, Springer.
21. P. Godefroid. 1997. Model Checking for Programming Languages using VeriSoft. In Principles of Programming Languages, (POPL) . ACM Press, Paris, France, 174–186.
22. Patrice Godefroid. 2005. Software Model Checking: The VeriSoft Approach. Formal Methods in System Design 26, 2 (2005), 77–101.
23. P. Godefroid, B. Hammer, and L. Jagadeesan. 1998. Model Checking Without a Model: An Analysis of the Heart-Beat Monitor of a Telephone Switch using VeriSoft. In Proc. ACM SIGSOFT International Symposium on Software Testing and Analysis . 124–133.
24. Jeff Huang. 2015. Stateless model checking concurrent programs with maximal causality reduction. In Programming Language Design and Implementation, (PLDI) . ACM, Portland, OR, USA, 165–174.
25. Shiyou Huang and Jeff Huang. 2016. Maximal causality reduction for TSO and PSO. In Object-Oriented Programming, Systems, Languages, and Applications, (OOPSLA) . ACM, Amsterdam, The Netherlands, 447–461.
26. ISO. 2012. C++ Specification Standard. International Organization for Standardization. 1338 (est.) pages.
27. Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. 2017. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In Proceedings of the 31st European Conference on Object-Oriented Programming, ECOOP 2017 . 17:1–17:29.
28. M. Kokologiannakis, O. Lahav, K. Sagonas, and V. Vafeiadis. 2018. Effective Stateless Model Checking for C/C++ Concurrency. In POPL. to appear, available from http://plv.mpi-sws.org/rcmc/ .
29. M. Kokologiannakis and K. Sagonas. 2017. Stateless model checking of the Linux kernel’s hierarchical read-copy-update (tree RCU). In Symposium on Model Checking of Software, (SPIN). ACM, Santa Barbara, CA, USA, 172–181.
30. Michael Kuperstein, Martin T. Vechev, and Eran Yahav. 2011. Partial-coherence abstractions for relaxed memory models. In Programming Language Design and Implementation (PLDI) . San Jose, CA, USA, 187–198.
31. Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis. 2016. Taming release-acquire consistency. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016 . ACM, 649–662.
32. F. Liu, N. Nedev, N. Prisadnikov, M.T. Vechev, and E. Yahav. 2012. Dynamic synthesis for relaxed memory models. In Programming Language Design and Implementation (PLDI) . ACM, 429–440.
33. Peter S. Magnusson, Anders Landin, and Erik Hagersten. 1994. Queue Locks on Cache Coherent Multiprocessors. In Proceedings of the 8th International Symposium on Parallel Processing, Cancún, Mexico, April 1994 . 165–171.
34. A. Mazurkiewicz. 1986. Trace Theory. In Advances in Petri Nets.
35. John M. Mellor-Crummey and Michael L. Scott. 1991. Algorithms for Scalable Synchronization on Shared-Memory Multiprocessors. ACM Trans. Comput. Syst. 9, 1 (1991), 21–65.
36. M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P.A. Nainar, and I. Neamtiu. 2008. Finding and Reproducing Heisenbugs in Concurrent Programs. In OSDI. USENIX Association, 267–280.
37. B. Norris and B. Demsky. 2016. A Practical Approach for Model Checking C/C++11 Code. ACM Trans. Program. Lang. Syst. 38, 3 (2016), 10:1–10:51.
38. Doron A. Peled. 1993. All from one, one for all, on model-checking using representatives. In Computer Aided Verification, (CAV) (LNCS) , Vol. 697. Elounda, Greece, 409–423.
39. Personal-com. 2018. Personal communication with authors of RCMC.
40. Pedro Ramalhete and Andreia Correia. 2016. Tidex: a mutual exclusion lock. In Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2016, Barcelona, Spain, March 12-16, 2016 . 52:1–52:2.
41. Pedro Ramalhete and Andreia Correia. 2018. https://github.com/pramalhe/ConcurrencyFreaks. {Online; accessed 2018-07-10}.
42. César Rodríguez, Marcelo Sousa, Subodh Sharma, and Daniel Kroening. 2015. Unfolding-based Partial Order Reduction. In CONCUR 2015 . 456–469.
43. O. Saarikivi, K. Kähkönen, and K. Heljanko. 2012. Improving Dynamic Partial Order Reductions for Concolic Testing. In Application of Concurrency to System Design, (ACSD) . IEEE, Hamburg, Germany, 132–141.
44. Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams. 2011. Understanding POWER multiprocessors. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011 . 175–186.
45. K. Sen and G. Agha. 2007. A Race-Detection and Flipping Algorithm for Automated Testing of Multi-threaded Programs. In Haifa Verification Conference . 166–182. LNCS 4383.
46. D. Shasha and M. Snir. 1988. Efficient and Correct Execution of Parallel Programs that Share Memory. ACM Trans. on Programming Languages and Systems 10, 2 (April 1988), 282–312.
47. Abraham Silberschatz, Peter B. Galvin, and Greg Gagne. 2012. Operating System Concepts (9th ed.). Wiley Publishing.
48. SPSC-bug. 2008. https://groups.google.com/forum/#!msg/comp.programming.threads/nSSFT9vKEe0/7eD3ioDg6nEJ. {Online; accessed 2018-04-11}.
49. SV-COMP. 2018. Competition on Software Verification. https://sv-comp.sosy-lab.org/2018 . {Online; accessed 2017-11-10}.
50. E. Torlak, M.andana Vaziri, and J. Dolby. 2010. MemSAT: checking axiomatic specifications of memory models. In Programming Language Design and Implementation (PLDI) . ACM, Toronto, Ontario, Canada, 341–350.
51. A. Valmari. 1990. Stubborn Sets for Reduced State Space Generation. In Advances in Petri Nets (LNCS), Vol. 483. 491–515.
52. Naling Zhang, Markus Kusano, and Chao Wang. 2015. Dynamic partial order reduction for relaxed memory models. In Programming Language Design and Implementation (PLDI) . ACM, Portland, OR, USA, 250–259.

Index Terms

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Formal software verification