Michalis Kokologiannakis
Ori Lahav
Konstantinos Sagonas
Viktor Vafeiadis
Skip Abstract Section
Skip Supplemental Material SectionAbstract
We present a stateless model checking algorithm for verifying concurrent programs running under RC11, a repaired version of the C/C++11 memory model without dependency cycles. Unlike most previous approaches, which enumerate thread interleavings up to some partial order reduction improvements, our approach works directly on execution graphs and (in the absence of RMW instructions and SC atomics) avoids redundant exploration by construction. We have implemented a model checker, called RCMC, based on this approach and applied it to a number of challenging concurrent programs. Our experiments confirm that RCMC is significantly faster, scales better than other model checking tools, and is also more resilient to small changes in the benchmarks.
Supplemental Material
Available for Download
zip
popl18-p80-aux.zip (2.1 GB)
This is the artifact of our paper. The zip file contains a Virtual Machine image with the benchmark programs and the binaries of the three tools we have used, as well as a .pdf file that provides more information about the artifact and instructions on how to use the three tools on user-specified programs.
- Parosh Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2014. Optimal dynamic partial order reduction. In POPL 2014. ACM, New York, NY, USA, 373–384. Google Scholar
Digital Library
- Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas. 2015. Stateless Model Checking for TSO and PSO. In TACAS 2015 (LNCS), Vol. 9035. Springer, Berlin, Heidelberg, 353–367. Google ScholarDigital Library
- Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2017. Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction. 64, 4, Article 25 (Sept. 2017), 49 pages. Google ScholarDigital Library
- Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Carl Leonardsson. 2016. Stateless Model Checking for POWER. In CAV 2016 (LNCS), Vol. 9780. Springer, Berlin, Heidelberg, 134–156. Google ScholarCross Ref
- Jade Alglave. 2013. Weakness is a virtue (position paper). In EC 2 . http://www0.cs.ucl.ac.uk/staff/j.alglave/papers/ec213.pdfGoogle Scholar
- Jade Alglave, Daniel Kroening, Vincent Nimal, and Michael Tautschnig. 2013b. Software Verification for Weak Memory via Program Transformation. In ESOP 2013. Springer-Verlag, Berlin, Heidelberg, 512–532. Google ScholarDigital Library
- Jade Alglave, Daniel Kroening, and Michael Tautschnig. 2013a. Partial Orders for Efficient Bounded Model Checking of Concurrent Software. In CAV 2013 (LNCS), Vol. 8044. Springer, Berlin, Heidelberg, 141–157. Google ScholarDigital Library
- Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory. ACM Trans. Program. Lang. Syst. 36, 2, Article 7 (July 2014), 74 pages. Google ScholarDigital Library
- Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter Sewell. 2015. The Problem of Programming Language Concurrency Semantics. In ESOP 2015 (LNCS), Vol. 9032. Springer, Berlin, Heidelberg, 283–307. Google ScholarCross Ref
- Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ Concurrency. In POPL 2011. ACM, New York, NY, USA, 55–66. Google ScholarDigital Library
- Hans-J. Boehm and Brian Demsky. 2014. Outlawing Ghosts: Avoiding Out-of-thin-air Results. In MSPC 2014. ACM, New York, NY, USA, Article 7, 6 pages. Google ScholarDigital Library
- Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, and Jad Hamza. 2017. On Verifying Causal Consistency. In POPL 2017. ACM, New York, NY, USA, 626–638. Google ScholarDigital Library
- Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla. 1983. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logics Specification: A Practical Approach. In POPL 1983. ACM Press, 117–126. Google ScholarDigital Library
- Edmund M. Clarke, Daniel Kroening, and Flavio Lerda. 2004. A Tool for Checking ANSI-C Programs. In TACAS 2004 (LNCS), Vol. 2988. Springer, Berlin, Heidelberg, 168–176. Google ScholarCross Ref
- Brian Demsky and Patrick Lam. 2015. SATCheck: SAT-directed Stateless Model Checking for SC and TSO. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2015). ACM, New York, NY, USA, 20–36. Google ScholarDigital Library
- Cormac Flanagan and Patrice Godefroid. 2005. Dynamic partial-order reduction for model checking software. In POPL 2005. ACM, New York, NY, USA, 110–121. Google ScholarDigital Library
- Phillip B. Gibbons and Ephraim Korach. 1997. Testing Shared Memories. SIAM J. Comput. 26, 4 (Aug. 1997), 1208–1244. Google ScholarDigital Library
- Patrice Godefroid. 1997. Model Checking for Programming Languages using VeriSoft. In POPL 1997. ACM, New York, NY, USA, 174–186. Google ScholarDigital Library
- Patrice Godefroid. 2005. Software Model Checking: The VeriSoft Approach. Formal Methods in System Design 26, 2 (March 2005), 77–101. Google ScholarDigital Library
- Jeff Huang. 2015. Stateless model checking concurrent programs with maximal causality reduction. In PLDI 2015. ACM, New York, NY, USA, 165–174. Google ScholarDigital Library
- Shiyou Huang and Jeff Huang. 2016. Maximal Causality Reduction for TSO and PSO. In OOPSLA 2016. ACM, New York, NY, USA, 447–461. Google ScholarDigital Library
- Kari Kähkönen, Olli Saarikivi, and Keijo Heljanko. 2015. Unfolding Based Automated Testing of Multithreaded Programs. Autom. Softw. Eng. 22, 4 (Dec. 2015), 475–515. Google ScholarDigital Library
- 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 ECOOP 2017, Vol. 74. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 17:1–17:29. Google ScholarCross Ref
- Ori Lahav and Viktor Vafeiadis. 2015. Owicki-Gries Reasoning for Weak Memory Models. In ICALP 2015 (LNCS), Vol. 9135. Springer, 311–323. Google ScholarDigital Library
- Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. 2017. Repairing Sequential Consistency in C/C++11. In PLDI 2017. ACM, New York, NY, USA, 618–632. Google ScholarDigital Library
- Leslie Lamport. 1979. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Trans. Computers 28, 9 (Sept. 1979), 690–691. Google ScholarDigital Library
- Antoni Mazurkiewicz. 1987. Trace Theory. In Petri Nets: Applications and Relationships to Other Models of Concurrency (LNCS), Vol. 255. Springer, Berlin, Heidelberg, 279–324. Google ScholarCross Ref
- Kenneth L. McMillan. 1995. A Technique of a State Space Search Based on Unfolding. Formal Methods in System Design 6, 1 (Jan. 1995), 45–65. Google ScholarDigital Library
- Mandanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gerald Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. 2008. Finding and Reproducing Heisenbugs in Concurrent Programs. In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation. USENIX Association, Berkeley, CA, USA, 267–280.Google ScholarDigital Library
- Brian Norris and Brian Demsky. 2016. A Practical Approach for Model Checking C/C++11 Code. ACM Trans. Program. Lang. Syst. 38, 3, Article 10 (May 2016), 51 pages. Google ScholarDigital Library
- Jean-Pierre Queille and Joseph Sifakis. 1982. Specification and Verification of Concurrent Systems in CESAR. In Intl. Symp. on Progr. (LNCS), Vol. 137. Springer-Verlag, Berlin, Heidelberg, 337–351. Google ScholarCross Ref
- César Rodríguez, Marcelo Sousa, Subodh Sharma, and Daniel Kroening. 2015. Unfolding-based Partial Order Reduction. In 26th International Conference on Concurrency Theory, CONCUR 2015 (LIPIcs), Vol. 42. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 456–469. Google ScholarCross Ref
- Dennis Shasha and Marc Snir. 1988. Efficient and Correct Execution of Parallel Programs That Share Memory. ACM Trans. Program. Lang. Syst. 10, 2 (April 1988), 282–312. Google ScholarDigital Library
- Aaron Turon, Viktor Vafeiadis, and Derek Dreyer. 2014. GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation. In OOPSLA 2014. ACM, 691–707. Google ScholarDigital Library
- Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, and Francesco Zappa Nardelli. 2015. Common Compiler Optimisations Are Invalid in the C11 Memory Model and What We Can Do About It. In POPL 2015. ACM, New York, NY, USA, 209–220. Google ScholarDigital Library
- Viktor Vafeiadis and Chinmay Narayan. 2013. Relaxed Separation Logic: A program logic for C11 concurrency. In OOPSLA 2013. ACM, New York, NY, USA, 867–884. Google ScholarDigital Library
- Naling Zhang, Markus Kusano, and Chao Wang. 2015. Dynamic partial order reduction for relaxed memory models. In PLDI 2015. ACM, New York, NY, USA, 250–259. Google ScholarDigital Library
Index Terms
- Effective stateless model checking for C/C++ concurrency
Recommendations
Optimal stateless model checking under the release-acquire semantics
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, ...
Effective lock handling in stateless model checking
Stateless Model Checking (SMC) is a verification technique for concurrent programs that checks for safety violations by exploring all possible thread interleavings. SMC is usually coupled with Partial Order Reduction (POR), which exploits the ...
Race checking by context inference
PLDI '04Software model checking has been successful for sequential programs, where predicate abstraction offers suitable models, and counterexample-guided abstraction refinement permits the automatic inference of models. When checking concurrent programs, we ...
Comments