research-article

Concurrency verification with maximal path causality

Authors:

Jeff HuangAuthors Info & Claims

ESEC/FSE 2018: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering

Pages 366 - 376

https://doi.org/10.1145/3236024.3236048

Published: 26 October 2018 Publication History

Abstract

We present a technique that systematically explores the state spaces of concurrent programs across both the schedule space and the input space. The cornerstone is a new model called Maximal Path Causality (MPC), which captures all combinations of thread schedules and program inputs that reach the same path as one equivalency class, and generates a unique schedule+input combination to explore each path. Moreover, the exploration for different paths can be easily parallelized. Our extensive evaluation on both popular concurrency benchmarks and real-world C/C++ applications shows that MPC significantly improves the performance of existing techniques.

References

[1]

{n. d.}. SV-COMP. http://sv-comp.sosy-lab.org. ({n. d.}).

[2]

Parosh Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2014. Optimal Dynamic Partial Order Reduction. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.

Digital Library

[3]

Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas. 2015. Stateless Model Checking for TSO and PSO. In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems.

Digital Library

[4]

Tom Bergan, Luis Ceze, and Dan Grossman. 2013. Input-covering Schedules for Multithreaded Programs. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages &#38; Applications.

Digital Library

[5]

Sebastian Burckhardt, Rajeev Alur, and Milo M. K. Martin. 2007. Check-Fence: Checking Consistency of Concurrent Data Types on Relaxed Memory Models. In Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation.

Digital Library

[6]

Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX conference on Operating systems design and implementation.

Digital Library

[7]

Alessandro Cimatti, Alberto Griggio, and Roberto Sebastiani. 2011. Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories. J. Artif. Int. Res. (2011).

Digital Library

[8]

Edmund Clarke, Daniel Kroening, and Flavio Lerda. 2004. A tool for checking ANSI-C programs. In In Tools and Algorithms for the Construction and Analysis of Systems. Springer, 168–176.

[9]

E M Clarke, O Grumberg, M Minea, and D Peled. 1999. State space reduction using partial order techniques. International Journal on Software Tools for Technology Transfer (1999).

[10]

E M Clarke, O Grumberg, M Minea, and D Peled. 1999. State space reduction using partial order techniques. International Journal on Software Tools for Technology Transfer (1999).

[11]

ConCREST. last accessed May 2017.

[12]

ConCREST. http://forsyte.at/software/concrest/. (last accessed May 2017).

[13]

Heming Cui, Jingyue Wu, John Gallagher, Huayang Guo, and Junfeng Yang. 2011. Efficient Deterministic Multithreading Through Schedule Relaxation. In Proceedings of the Twenty-Third ACM Symposium on Operating Systems Principles.

Digital Library

[14]

Heming Cui, Jingyue Wu, Chia-Che Tsai, and Junfeng Yang. 2010. Stable Deterministic Multithreading Through Schedule Memoization. In Proceedings of the 9th USENIX Conference on Operating Systems Design and Implementation.

Digital Library

[15]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.

Digital Library

[16]

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.

Digital Library

[17]

Azadeh Farzan, Andreas Holzer, Niloofar Razavi, and Helmut Veith. 2013. Con2Colic Testing. In Joint European Software Engineering Conference and ACM SIGSOFT Symposium on Foundations of Software Engineering.

Digital Library

[18]

Cormac Flanagan and Patrice Godefroid. 2005. Dynamic Partial-order Reduction for Model Checking Software. In Proceedings of the 32Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.

Digital Library

[19]

Jeff Huang. 2015. Stateless Model Checking Concurrent Programs with Maximal Causality Reduction. In PLDI.

Digital Library

[20]

Jeff Huang, Patrick O’Neil Meredith, and Grigore Rosu. 2014. Maximal Sound Predictive Race Detection with Control Flow Abstraction. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation.

Digital Library

[21]

Shiyou Huang and Jeff Huang. 2016. Maximal Causality Reduction for TSO and PSO. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications.

Digital Library

[22]

Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. 2014. Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization. In Proceedings of the 16th International Conference on Computer Aided Verification - Volume 8559. 585–602.

Digital Library

[23]

Maged M. Michael and Michael L. Scott. 1996. Simple, Fast, and Practical Non-blocking and Blocking Concurrent Queue Algorithms. In Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing.

Digital Library

[24]

Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. 2008. Finding and Reproducing Heisenbugs in Concurrent Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation.

Digital Library

[25]

Shaz Qadeer and Dinghao Wu. 2004. KISS: Keep It Simple and Sequential. In Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation. 14–24.

Digital Library

[26]

Zvonimir Rakamaric and Michael Emmi. 2014. SMACK: Decoupling Source Language Details from Verifier Implementations. In 26th International Conference on Computer Aided Verification. 106–113.

Digital Library

[27]

Stephen F. Siegel, Manchun Zheng, Ziqing Luo, Timothy K. Zirkel, Andre V. Marianiello, John G. Edenhofner, Matthew B. Dwyer, and Michael S. Rogers. 2015. CIVL: The Concurrency Intermediate Verification Language. In Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis. 61:1–61:12.

Digital Library

[28]

Emina Torlak, Mandana Vaziri, and Julian Dolby. 2010. MemSAT: Checking Axiomatic Specifications of Memory Models. In Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation.

Digital Library

[29]

Anthony Williams. 2012. Dekker’s algorithm implementation. In https://www.justsoftwaresolutions.co.uk/threading/.

[30]

Min Xu, Rastislav Bodik, and Mark D. Hill. 2003. A ”Flight Data Recorder” for Enabling Full-system Multiprocessor Deterministic Replay. In Proceedings of the 30th Annual International Symposium on Computer Architecture.

Digital Library

[31]

REFERENCES

[32]

MPC. https://github.com/parasolaser/MPC. (2018).

[33]

SV-COMP. http://svcomp.sosylab.org. (2018).

[34]

Parosh Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2014. Optimal Dynamic Partial Order Reduction. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.

Digital Library

[35]

Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas. 2015.

[36]

Stateless Model Checking for TSO and PSO. In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems.

Digital Library

[37]

Tom Bergan, Luis Ceze, and Dan Grossman. 2013. Input-covering Schedules for Multithreaded Programs. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages and Applications.

Digital Library

[38]

Sebastian Burckhardt, Rajeev Alur, and Milo M. K. Martin. 2007. CheckFence: Checking Consistency of Concurrent Data Types on Relaxed Memory Models. In Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation.

Digital Library

[39]

Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008.

[40]

KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX conference on Operating systems design and implementation.

Digital Library

[41]

Cristian Cadar and Koushik Sen. 2013. Symbolic Execution for Software Testing: Three Decades Later. Commun. ACM 56, 2 (2013), 82–90.

Digital Library

[42]

Alessandro Cimatti, Alberto Griggio, and Roberto Sebastiani. 2011. Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories. J. Artif. Int. Res. (2011).

Digital Library

[43]

Edmund Clarke, Daniel Kroening, and Flavio Lerda. 2004. A tool for checking ANSI-C programs. In In Tools and Algorithms for the Construction and Analysis of Systems. Springer, 168–176.

[44]

E M Clarke, O Grumberg, M Minea, and D Peled. 1999. State space reduction using partial order techniques. International Journal on Software Tools for Technology Transfer (1999).

[45]

E M Clarke, O Grumberg, M Minea, and D Peled. 1999. State space reduction using partial order techniques. International Journal on Software Tools for Technology Transfer (1999).

[46]

ConCREST. last accessed May 2017.

[47]

ConCREST. http://forsyte.at/software/concrest/. (last accessed May 2017).

[48]

Heming Cui, Jingyue Wu, John Gallagher, Huayang Guo, and Junfeng Yang. 2011. Efficient Deterministic Multithreading Through Schedule Relaxation. In Proceedings of the Twenty-Third ACM Symposium on Operating Systems Principles.

Digital Library

[49]

Heming Cui, Jingyue Wu, Chia-Che Tsai, and Junfeng Yang. 2010. Stable Deterministic Multithreading Through Schedule Memoization. In Proceedings of the 9th USENIX Conference on Operating Systems Design and Implementation.

Digital Library

[50]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.

Digital Library

[51]

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.

Digital Library

[52]

Azadeh Farzan, Andreas Holzer, Niloofar Razavi, and Helmut Veith. 2013.

[53]

Con2Colic Testing. In Joint European Software Engineering Conference and ACM SIGSOFT Symposium on Foundations of Software Engineering.

Digital Library

[54]

Cormac Flanagan and Patrice Godefroid. 2005. Dynamic Partial-order Reduction for Model Checking Software. In Proceedings of the 32Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Concurrency Verification with Maximal Path Causality ESEC/FSE ’18, November 4–9, 2018, Lake Buena Vista, FL, USA

Digital Library

[55]

Jeff Huang. 2015. Stateless Model Checking Concurrent Programs with Maximal Causality Reduction. In PLDI.

Digital Library

[56]

Jeff Huang, Patrick O’Neil Meredith, and Grigore Rosu. 2014. Maximal Sound Predictive Race Detection with Control Flow Abstraction. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation.

Digital Library

[57]

Shiyou Huang and Jeff Huang. 2016.

[58]

Maximal Causality Reduction for TSO and PSO. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications.

Digital Library

[59]

Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. 2014. Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization. In Proceedings of the 16th International Conference on Computer Aided Verification - Volume 8559. 585–602.

Digital Library

[60]

Sergey Mechtaev, Jooyong Yi, and Abhik Roychoudhury. 2016. Angelix: Scalable multiline program patch synthesis via symbolic analysis. In Proceedings of the 38th International Conference on Software Engineering. 691–701.

Digital Library

[61]

Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. 2008. Finding and Reproducing Heisenbugs in Concurrent Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation.

Digital Library

[62]

Hoang Duong Thien Nguyen, Dawei Qi, Abhik Roychoudhury, and Satish Chandra. 2013. SemFix: Program Repair via Semantic Analysis. In Proceedings of the 2013 International Conference on Software Engineering. 772–781.

Digital Library

[63]

Chris Parnin and Alessandro Orso. 2011. Are Automated Debugging Techniques Actually Helping Programmers?. In ACM International Symposium on Software Testing and Analysis. 199–209.

Digital Library

[64]

Shaz Qadeer and Dinghao Wu. 2004.

[65]

KISS: Keep It Simple and Sequential. In Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation. 14–24.

Digital Library

[66]

Zvonimir Rakamaric and Michael Emmi. 2014.

[67]

SMACK: Decoupling Source Language Details from Verifier Implementations. In 26th International Conference on Computer Aided Verification. 106–113.

Digital Library

[68]

Malavika Samak, Omer Tripp, and Murali Krishna Ramanathan. 2016. Directed Synthesis of Failing Concurrent Executions. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. 430–446.

Digital Library

[69]

Emina Torlak, Mandana Vaziri, and Julian Dolby. 2010.

[70]

MemSAT: Checking Axiomatic Specifications of Memory Models. In Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation.

Digital Library

[71]

Min Xu, Rastislav Bodik, and Mark D. Hill. 2003. A "Flight Data Recorder" for Enabling Full-system Multiprocessor Deterministic Replay. In Proceedings of the 30th Annual International Symposium on Computer Architecture.

Digital Library

[72]

Liangze Yin, Wei Dong, Wanwei Liu, and Ji Wang. 2017. Scheduling Constraint Based Abstraction Refinement for Multi-Threaded Program Verification. CoRR abs/1708.08323 (2017). arXiv: 1708.08323

[73]

Cristian Zamfir and George Candea. 2010. Execution synthesis: a technique for automated software debugging. In European Conference on Computer Systems. 321–334.

Digital Library

Cited By

Yavuz T(2022)SIFT: A Tool for Property Directed Symbolic Execution of Multithreaded Software2022 IEEE Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST53961.2022.00049(433-443)Online publication date: Apr-2022
https://doi.org/10.1109/ICST53961.2022.00049
Minh Do COgata K(2020)A Divide & Conquer Approach to Testing Concurrent Java Programs with JPF and MaudeStructured Object-Oriented Formal Language and Method10.1007/978-3-030-41418-4_4(42-58)Online publication date: 20-Feb-2020
https://doi.org/10.1007/978-3-030-41418-4_4

Index Terms

Concurrency verification with maximal path causality
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
      2. Software defect analysis
        Software testing and debugging

Recommendations

Sequential verification of serializability
POPL '10

Serializability is a commonly used correctness condition in concurrent programming. When a concurrent module is serializable, certain other properties of the module can be verified by considering only its sequential executions. In many cases, concurrent ...
Sequential verification of serializability
POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Serializability is a commonly used correctness condition in concurrent programming. When a concurrent module is serializable, certain other properties of the module can be verified by considering only its sequential executions. In many cases, concurrent ...
Distributed optimistic concurrency control with reduced rollback

Concurrency control algorithms have traditionally been based on locking and timestamp ordering mechanisms. Recently optimistic schemes have been proposed. In this paper a distributed, multi-version, optimistic concurrency control scheme is described ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ESEC/FSE 2018: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering

October 2018

987 pages

ISBN:9781450355735

DOI:10.1145/3236024

General Chair:
Gary T. Leavens
University of Central Florida, USA
,
Program Chairs:
Alessandro Garcia
PUC-Rio, Brazil
,
Corina S. Păsăreanu
NASA Ames Research Center, USA

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 October 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ESEC/FSE '18

Sponsor:

SIGSOFT

ESEC/FSE '18: 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering

November 4 - 9, 2018

FL, Lake Buena Vista, USA

Acceptance Rates

Overall Acceptance Rate 112 of 543 submissions, 21%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
322
Total Downloads

Downloads (Last 12 months)21
Downloads (Last 6 weeks)1

Reflects downloads up to 23 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Yavuz T(2022)SIFT: A Tool for Property Directed Symbolic Execution of Multithreaded Software2022 IEEE Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST53961.2022.00049(433-443)Online publication date: Apr-2022
https://doi.org/10.1109/ICST53961.2022.00049
Minh Do COgata K(2020)A Divide & Conquer Approach to Testing Concurrent Java Programs with JPF and MaudeStructured Object-Oriented Formal Language and Method10.1007/978-3-030-41418-4_4(42-58)Online publication date: 20-Feb-2020
https://doi.org/10.1007/978-3-030-41418-4_4

View Options

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten