More Web Proxy on the site http://driver.im/

research-article

Open access

Effective lock handling in stateless model checking

Authors:

Michalis Kokologiannakis,

Viktor VafeiadisAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 3, Issue OOPSLA

Article No.: 173, Pages 1 - 26

https://doi.org/10.1145/3360599

Published: 10 October 2019 Publication History

Abstract

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 independence of instructions to avoid redundant explorations when an equivalent one has already been considered. While effective POR techniques have been developed for many different memory models, they are only able to exploit independence at the instruction level, which makes them unsuitable for programs with coarse-grained synchronization mechanisms such as locks.

We present a lock-aware POR algorithm, LAPOR, that exploits independence at both instruction and critical section levels. This enables LAPOR to explore exponentially fewer interleavings than the state-of-the-art techniques for programs that use locks conservatively. Our algorithm is sound, complete, and optimal, and can be used for verifying programs under several different memory models. We implement LAPOR in a tool and show that it can be exponentially faster than the state-of-the-art model checkers.

References

[1]

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.

Digital Library

[2]

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.

Digital Library

[3]

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.

[4]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Tuan Phong Ngo. 2018. Optimal Stateless Model Checking Under the Release-acquire Semantics. Proc. ACM Program. Lang. 2, OOPSLA, Article 135 (Oct. 2018), 29 pages.

Digital Library

[5]

Elvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel, and Albert Rubio. 2018. Constrained Dynamic Partial Order Reduction. In CAV 2018 (LNCS), Vol. 10982. Springer, Berlin, Heidelberg, 392–410.

[6]

Jade Alglave, Daniel Kroening, and Michael Tautschnig. 2013. Partial Orders for Efficient Bounded Model Checking of Concurrent Software. In CAV 2013 (LNCS), Vol. 8044. Springer, Berlin, Heidelberg, 141–157.

Digital Library

[7]

Stavros Aronis, Bengt Jonsson, Magnus Lång, and Konstantinos Sagonas. 2018. Optimal Dynamic Partial Order Reduction with Observers. In TACAS 2018 (LNCS), Vol. 10806. Springer, Berlin, Heidelberg, 229–248.

[8]

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.

Digital Library

[9]

Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. 2017. Data-centric Dynamic Partial Order Reduction. Proc. ACM Program. Lang. 2, POPL, Article 31 (Dec. 2017), 30 pages.

Digital Library

[10]

Cormac Flanagan and Patrice Godefroid. 2005. Dynamic partial-order reduction for model checking software. In POPL 2005. ACM, New York, NY, USA, 110–121.

Digital Library

[11]

Patrice Godefroid. 1997. Model Checking for Programming Languages using VeriSoft. In POPL 1997. ACM, New York, NY, USA, 174–186.

Digital Library

[12]

Jeff Huang. 2015. Stateless model checking concurrent programs with maximal causality reduction. In PLDI 2015. ACM, New York, NY, USA, 165–174.

Digital Library

[13]

Shiyou Huang and Jeff Huang. 2016. Maximal Causality Reduction for TSO and PSO. In OOPSLA 2016. ACM, New York, NY, USA, 447–461.

Digital Library

[14]

Dileep Kini, Umang Mathur, and Mahesh Viswanathan. 2017. Dynamic Race Prediction in Linear Time. In PLDI 2017. ACM, New York, NY, USA, 157–170.

Digital Library

[15]

Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis. 2017. Effective Stateless Model Checking for C/C++ Concurrency. Proc. ACM Program. Lang. 2, POPL, Article 17 (Dec. 2017), 32 pages.

Digital Library

[16]

Michalis Kokologiannakis, Azalea Raad, and Viktor Vafeiadis. 2019. Model Checking for Weakly Consistent Libraries. In PLDI 2019. ACM, New York, NY, USA, 15.

Digital Library

[17]

Ori Lahav and Viktor Vafeiadis. 2015. Owicki-Gries Reasoning for Weak Memory Models. In ICALP 2015 (LNCS), Vol. 9135. Springer, Berlin, Heidelberg, 311–323.

Digital Library

[18]

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.

Digital Library

[19]

Leslie Lamport. 1979. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Trans. Computers 28, 9 (Sept. 1979), 690–691.

Digital Library

[20]

Antoni Mazurkiewicz. 1987. Trace Theory. In Petri nets: Applications and relationships to other models of concurrency (LNCS), Vol. 255. Springer, Berlin, Heidelberg, 279–324.

[21]

Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gérard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. 2008. Finding and Reproducing Heisenbugs in Concurrent Programs. In OSDI 2008. USENIX Association, Berkeley, CA, USA, 267–280.

Digital Library

[22]

Brian Norris and Brian Demsky. 2013. CDSChecker: Checking concurrent data structures written with C/C++ atomics. In OOPSLA 2013. ACM, New York, NY, USA, 131–150.

Digital Library

[23]

Scott Owens, Susmit Sarkar, and Peter Sewell. 2009. A Better x86 Memory Model: x86-TSO. In TPHOLs 2009. Springer, 391–407.

Digital Library

[24]

Christos H. Papadimitriou. 1979. The Serializability of Concurrent Database Updates. J. ACM 26, 4 (Oct. 1979), 631–653.

Digital Library

[25]

César Rodríguez, Marcelo Sousa, Subodh Sharma, and Daniel Kroening. 2015. Unfolding-based Partial Order Reduction. In CONCUR 2015 (LIPIcs), Vol. 42. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 456–469.

[26]

Jake Roemer, Kaan Genç, and Michael D. Bond. 2018. High-coverage, Unbounded Sound Predictive Race Detection. In PLDI 2018. ACM, New York, NY, USA, 374–389.

Digital Library

[27]

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.

Digital Library

[28]

Yannis Smaragdakis, Jacob Evans, Caitlin Sadowski, Jaeheon Yi, and Cormac Flanagan. 2012. Sound Predictive Race Detection in Polynomial Time. In POPL 2012. ACM, New York, NY, USA, 387–400.

Digital Library

[29]

SPARC International Inc. 1994. The SPARC architecture manual (version 9). Prentice-Hall.

Digital Library

[30]

SV-COMP. 2019. Competition on Software Verification (SV-COMP). https://sv-comp.sosy-lab.org/2019/ [Online; accessed 27-March-2019].

[31]

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.

Digital Library

Cited By

Kokologiannakis MMarmanis IVafeiadis V(2024)SPORE: Combining Symmetry and Partial Order ReductionProceedings of the ACM on Programming Languages10.1145/36564498:PLDI(1781-1803)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656449
Beck MBhat KStričević LChen GBehrens DFu MVafeiadis VChen HHärtig HAamodt TJerger NSwift M(2023)AtoMig: Automatically Migrating Millions Lines of Code from TSO to WMMProceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 210.1145/3575693.3579849(61-73)Online publication date: 27-Jan-2023
https://dl.acm.org/doi/10.1145/3575693.3579849
Albert Ede la Banda MGómez-Zamalloa MIsabel MStuckey P(2023)Optimal dynamic partial order reduction with context-sensitive independence and observersJournal of Systems and Software10.1016/j.jss.2023.111730202:COnline publication date: 1-Aug-2023
https://dl.acm.org/doi/10.1016/j.jss.2023.111730
Show More Cited By

Index Terms

Effective lock handling in stateless model checking
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis
        Software testing and debugging
2. Theory of computation
  1. Logic
    1. Verification by model checking

Recommendations

Effective stateless model checking for C/C++ concurrency

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 ...
Fair stateless model checking
PLDI '08

Stateless model checking is a useful state-space exploration technique for systematically testing complex real-world software. Existing stateless model checkers are limited to the verification of safety properties on terminating programs. However, ...
Fair stateless model checking
PLDI '08: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation

Stateless model checking is a useful state-space exploration technique for systematically testing complex real-world software. Existing stateless model checkers are limited to the verification of safety properties on terminating programs. However, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 3, Issue OOPSLA

October 2019

2077 pages

EISSN:2475-1421

DOI:10.1145/3366395

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 October 2019

Published in PACMPL Volume 3, Issue OOPSLA

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

H2020 European Research Council

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

18
Total Citations
View Citations
520
Total Downloads

Downloads (Last 12 months)117
Downloads (Last 6 weeks)27

Reflects downloads up to 21 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kokologiannakis MMarmanis IVafeiadis V(2024)SPORE: Combining Symmetry and Partial Order ReductionProceedings of the ACM on Programming Languages10.1145/36564498:PLDI(1781-1803)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656449
Beck MBhat KStričević LChen GBehrens DFu MVafeiadis VChen HHärtig HAamodt TJerger NSwift M(2023)AtoMig: Automatically Migrating Millions Lines of Code from TSO to WMMProceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 210.1145/3575693.3579849(61-73)Online publication date: 27-Jan-2023
https://dl.acm.org/doi/10.1145/3575693.3579849
Albert Ede la Banda MGómez-Zamalloa MIsabel MStuckey P(2023)Optimal dynamic partial order reduction with context-sensitive independence and observersJournal of Systems and Software10.1016/j.jss.2023.111730202:COnline publication date: 1-Aug-2023
https://dl.acm.org/doi/10.1016/j.jss.2023.111730
Abdulla PAtig MBønneland FDas SJonsson BLång MSagonas K(2023)Tailoring Stateless Model Checking for Event-Driven Multi-threaded ProgramsAutomated Technology for Verification and Analysis10.1007/978-3-031-45332-8_9(176-198)Online publication date: 19-Oct-2023
https://doi.org/10.1007/978-3-031-45332-8_9
Kokologiannakis MMarmanis IVafeiadis V(2023)Unblocking Dynamic Partial Order ReductionComputer Aided Verification10.1007/978-3-031-37706-8_12(230-250)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37706-8_12
Deligiannis PSenthilnathan ANayyar FLovett CLal A(2023)Industrial-Strength Controlled Concurrency Testing for Programs with Tools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-30820-8_26(433-452)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30820-8_26
Raad AMaranget LVafeiadis V(2022)Extending Intel-x86 consistency and persistency: formalising the semantics of Intel-x86 memory types and non-temporal storesProceedings of the ACM on Programming Languages10.1145/34986836:POPL(1-31)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498683
Trimananda RLuo WDemsky BXu G(2022)Stateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applications that Do Not TerminateVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-94583-1_20(400-424)Online publication date: 14-Jan-2022
https://doi.org/10.1007/978-3-030-94583-1_20
Bui TChatterjee KGautam TPavlogiannis AToman V(2021)The reads-from equivalence for the TSO and PSO memory modelsProceedings of the ACM on Programming Languages10.1145/34855415:OOPSLA(1-30)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485541
Oberhauser JChehab RBehrens DFu MPaolillo AOberhauser LBhat KWen YChen HKim JVafeiadis VSherwood TBerger EKozyrakis C(2021)VSync: push-button verification and optimization for synchronization primitives on weak memory modelsProceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3445814.3446748(530-545)Online publication date: 19-Apr-2021
https://dl.acm.org/doi/10.1145/3445814.3446748
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents