Nothing Special   »   [go: up one dir, main page]

skip to main content
10.1145/3009837.3009893acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Thread modularity at many levels: a pearl in compositional verification

Published: 01 January 2017 Publication History

Abstract

A thread-modular proof for the correctness of a concurrent program is based on an inductive and interference-free annotation of each thread. It is well-known that the corresponding proof system is not complete (unless one adds auxiliary variables). We describe a hierarchy of proof systems where each level k corresponds to a generalized notion of thread modularity (level 1 corresponds to the original notion). Each level is strictly more expressive than the previous. Further, each level precisely captures programs that can be proved using uniform Ashcroft invariants with k universal quantifiers. We demonstrate the usefulness of the hierarchy by giving a compositional proof of the Mach shootdown algorithm for TLB consistency. We show a proof at level 2 that shows the algorithm is correct for an arbitrary number of CPUs. However, there is no proof for the algorithm at level 1 which does not involve auxiliary state.

References

[1]
Mart´ın Abadi and Leslie Lamport. Conjoining specifications. Transactions on Programming Languages and Systems, 17(3), 1995.
[2]
P. A. Abdulla, K. ˇ Cerans, B. Jonsson, and Y.-K. Tsay. Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation, 160(1–2), 2000.
[3]
Parosh Aziz Abdulla, Yu-Fang Chen, Giorgio Delzanno, Frédéric Haziza, Chih-Duo Hong, and Ahmed Rezine. Constrained monotonic abstraction: A CEGAR for parameterized verification. In CONCUR, 2010.
[4]
Parosh Aziz Abdulla, Frédéric Haziza, and Lukás Hol´ık. All for the price of few. In VMCAI, 2013.
[5]
Parosh Aziz Abdulla, Frédéric Haziza, and Lukás Hol´ık. Parameterized verification through view abstraction. STTT, 18(5), 2016.
[6]
Krzysztof R. Apt, Frank S. de Boer, and Ernst-Rüdiger Olderog. Verification of Sequential and Concurrent Programs. Springer, 2009.
[7]
Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, and Lenore D. Zuck. Parameterized verification with automatically computed inductive assertions. In CAV, 2001.
[8]
Edward A. Ashcroft. Proving assertions about parallel programs. J. Comput. Syst. Sci., 10(1), 1975.
[9]
Thomas Ball, Andreas Podelski, and Sriram K. Rajamani. Boolean and cartesian abstraction for model checking C programs. STTT, 5(1), 2003.
[10]
Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, and Shmuel Sagiv. Thread quantification for concurrent shape analysis. In CAV, 2008.
[11]
Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, and Shmuel Sagiv. Thread quantification for concurrent shape analysis. In CAV, 2008.
[12]
David L. Black. Personal communication., 2016.
[13]
David L. Black, Richard F. Rashid, David B. Golub, Charles R. Hill, and Robert V. Baron. Translation lookaside buffer consistency: A software approach. In ASPLOS-III, 1989.
[14]
Ariel Cohen and Kedar S. Namjoshi. Local proofs for global safety properties. Formal Methods in System Design, 34(2), 2009.
[15]
Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, 1977.
[16]
Patrick Cousot and Radhia Cousot. Reasoning about program invariance proof methods. Res. rep. CRIN-80-P050, Centre de Recherche en Informatique de Nancy (CRIN), Institut National Polytechnique de Lorraine, Nancy, France, July 1980.
[17]
Patrick Cousot and Radhia Cousot. Invariance proof methods and analysis techniques for parallel programs. In Automatic program construction techniques. Macmillan, 1984.
[18]
Alastair Donaldson, Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Symmetry-aware predicate abstraction for shared-variable concurrent programs. In CAV, volume 6806, 2011.
[19]
Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, and Thomas Wahl. Counterexample-guided abstraction refinement for symmetric concurrent programs. Formal Methods in System Design, 41(1), 2012.
[20]
Klaus Dräger, Andrey Kupriyanov, Bernd Finkbeiner, and Heike Wehrheim. SLAB: A certifying model checker for infinite-state concurrent systems. In TACAS, 2010.
[21]
Michael Emmi, Rupak Majumdar, and Roman Manevich. Parameterized verification of transactional memories. In PLDI, 2010.
[22]
Azadeh Farzan and Zachary Kincaid. Verification of parameterized concurrent programs by modular reasoning about data and control. In POPL, 2012.
[23]
Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. Inductive data flow graphs. In POPL, 2013.
[24]
Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. Proofs that count. In POPL, 2014.
[25]
Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. Proof spaces for unbounded parallelism. In POPL, 2015.
[26]
Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. Proving liveness of parameterized programs. In LICS, 2016.
[27]
Cormac Flanagan, Stephen N. Freund, and Shaz Qadeer. Threadmodular verification for shared-memory programs. In ESOP, 2002.
[28]
Cormac Flanagan, Stephen N. Freund, Shaz Qadeer, and Sanjit A. Seshia. Modular verification of multithreaded programs. Theoretical Computer Science, 338(1-3), 2005.
[29]
Silvio Ghilardi and Silvio Ranise. Backward reachability of arraybased systems by SMT solving: Termination and invariant synthesis. Logical Methods in Computer Science, 6(4), 2010.
[30]
Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. Synthesizing software verifiers from proof rules. In PLDI, 2012.
[31]
Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. Threader: A constraint-based verifier for multi-threaded programs. In CAV, 2011.
[32]
Arie Gurfinkel, Sharon Shoham, and Yuri Meshman. SMT-based verification of parameterized systems. In FSE, 2016.
[33]
Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Race checking by context inference. In PLDI, 2004.
[34]
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Shaz Qadeer. Thread-modular abstraction refinement. In CAV, 2003.
[35]
Hossein Hojjat, Philipp Rümmer, Pavle Subotic, and Wang Yi. Horn clauses for communicating timed systems. In Workshop on Horn Clauses for Verification and Synthesis, 2014.
[36]
Joxan Jaffar and Andrew E. Santosa. Recursive abstractions for parameterized systems. In FM, 2009.
[37]
Cliff B. Jones. Tentative steps toward a development method for interfering programs. Transactions on Programming Languages and Systems, 5(4), 1983.
[38]
Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Lost in abstraction: Monotonicity in multi-threaded programs. In CONCUR, 2014.
[39]
Shuvendu K. Lahiri, Alexander Malkis, and Shaz Qadeer. Abstract threads. In VMCAI, 2010.
[40]
Leslie Lamport. Proving the correctness of multiprocess programs. Transactions on Software Engineering, 3(2), 1977.
[41]
R. Lipton. The reachability problem is exponential-space hard. Technical Report 62, Department of Computer Science, Yale University, 1976.
[42]
Alexander Malkis, Andreas Podelski, and Andrey Rybalchenko. Thread-modular verification is Cartesian abstract interpretation. In ICTAC, 2006.
[43]
Alexander Malkis, Andreas Podelski, and Andrey Rybalchenko. Precise thread-modular verification. In SAS, 2007.
[44]
David Monniaux and Laure Gonnord. Cell morphing: From array programs to array-free horn clauses. In SAS, 2016.
[45]
Kedar S. Namjoshi. Symmetry and completeness in the analysis of parameterized systems. In VMCAI, 2007.
[46]
Leonor Prensa Nieto. Completeness of the Owicki-Gries system for parameterized parallel programs. In IPDPS, 2001.
[47]
Susan S. Owicki. Axiomatic proof techniques for parallel programs. PhD thesis, Cornell University, 1975.
[48]
Amir Pnueli, Sitvanit Ruah, and Lenore D. Zuck. Automatic deductive verification with invisible invariants. In TACAS, 2001.
[49]
Hartley Rogers, Jr. Theory of recursive functions and effective computability. MIT Press, 1987.
[50]
Alejandro Sánchez and César Sánchez. Parametrized invariance for infinite state processes. Acta Inf., 52(6), 2015.
[51]
Alejandro Sánchez, Sriram Sankaranarayanan, César Sánchez, and Bor-Yuh Evan Chang. Invariant generation for parametrized systems using self-reflection. In SAS, 2012.
[52]
Michal Segalov, Tal Lev-Ami, Roman Manevich, Ganesan Ramalingam, and Mooly Sagiv. Abstract transformers for thread correlation analysis. In APLAS, 2009.
[53]
Natarajan Shankar. Combining theorem proving and model checking through symbolic analysis. In CONCUR, 2000.

Cited By

View all
  • (2024)Commutativity Simplifies Proofs of Parameterized ProgramsProceedings of the ACM on Programming Languages10.1145/36329258:POPL(2485-2513)Online publication date: 5-Jan-2024
  • (2024)Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking FunctionsProceedings of the ACM on Programming Languages10.1145/36328778:POPL(1028-1059)Online publication date: 5-Jan-2024
  • (2024)Petrification: Software Model Checking for Programs with Dynamic Thread ManagementVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50521-8_1(3-25)Online publication date: 15-Jan-2024
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
January 2017
901 pages
ISBN:9781450346603
DOI:10.1145/3009837
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 the author(s) 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

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2017

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Concurrency
  2. Owicki-Gries
  3. Parameterized verification
  4. Thread-modularity

Qualifiers

  • Research-article

Conference

POPL '17
Sponsor:

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)58
  • Downloads (Last 6 weeks)9
Reflects downloads up to 14 Dec 2024

Other Metrics

Citations

Cited By

View all
  • (2024)Commutativity Simplifies Proofs of Parameterized ProgramsProceedings of the ACM on Programming Languages10.1145/36329258:POPL(2485-2513)Online publication date: 5-Jan-2024
  • (2024)Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking FunctionsProceedings of the ACM on Programming Languages10.1145/36328778:POPL(1028-1059)Online publication date: 5-Jan-2024
  • (2024)Petrification: Software Model Checking for Programs with Dynamic Thread ManagementVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50521-8_1(3-25)Online publication date: 15-Jan-2024
  • (2022)Decomposing reach set computations with low-dimensional sets and high-dimensional matrices (extended version)Information and Computation10.1016/j.ic.2022.104937289:PAOnline publication date: 1-Nov-2022
  • (2021)Sound Verification Procedures for Temporal Properties of Infinite-State SystemsComputer Aided Verification10.1007/978-3-030-81688-9_16(337-360)Online publication date: 20-Jul-2021
  • (2021)On Symmetry and Quantification: A New Approach to Verify Distributed ProtocolsNASA Formal Methods10.1007/978-3-030-76384-8_9(131-150)Online publication date: 24-May-2021
  • (2019)Ultimate TreeAutomizer (CHC-COMP Tool Description)Electronic Proceedings in Theoretical Computer Science10.4204/EPTCS.296.7296(42-47)Online publication date: 9-Jul-2019
  • (2019)Pretend synchrony: synchronous verification of asynchronous distributed programsProceedings of the ACM on Programming Languages10.1145/32903723:POPL(1-30)Online publication date: 2-Jan-2019
  • (2018)Reach Set Approximation through Decomposition with Low-dimensional Sets and High-dimensional MatricesProceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)10.1145/3178126.3178128(41-50)Online publication date: 11-Apr-2018
  • (2018)Abstract Interpretation of Stateful NetworksStatic Analysis10.1007/978-3-319-99725-4_8(86-106)Online publication date: 29-Aug-2018
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media