research-article

Predicate abstraction and refinement for verifying multi-threaded programs

Authors:

Ashutosh Gupta,

Corneliu Popeea,

Andrey RybalchenkoAuthors Info & Claims

ACM SIGPLAN Notices, Volume 46, Issue 1

Pages 331 - 344

https://doi.org/10.1145/1925844.1926424

Published: 26 January 2011 Publication History

Abstract

Automated verification of multi-threaded programs requires explicit identification of the interplay between interacting threads, so-called environment transitions, to enable scalable, compositional reasoning. Once the environment transitions are identified, we can prove program properties by considering each program thread in isolation, as the environment transitions keep track of the interleaving with other threads. Finding adequate environment transitions that are sufficiently precise to yield conclusive results and yet do not overwhelm the verifier with unnecessary details about the interleaving with other threads is a major challenge. In this paper we propose a method for safety verification of multi-threaded programs that applies (transition) predicate abstraction-based discovery of environment transitions, exposing a minimal amount of information about the thread interleaving. The crux of our method is an abstraction refinement procedure that uses recursion-free Horn clauses to declaratively state abstraction refinement queries. Then, the queries are resolved by a corresponding constraint solving algorithm. We present preliminary experimental results for mutual exclusion protocols and multi-threaded device drivers.

Supplementary Material

MP4 File (31-mpeg-4.mp4)

Download
280.22 MB

References

[1]

Y. Bar-David and G. Taubenfeld. Automatic discovery of mutual exclusion algorithms. In DISC, pages 136--150, 2003.

Digital Library

[2]

G. Basler, M. Mazzucchi, T. Wahl, and D. Kroening. Symbolic counter abstraction for concurrent software. In CAV, pages 64--78, 2009.

Digital Library

[3]

G. Basler, M. Hague, D. Kroening, C.-H. L. Ong, T. Wahl, and H. Zhao. Boom: Taking boolean program model checking one step further. In TACAS, pages 145--149, 2010.

Digital Library

[4]

E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV, pages 154--169, 2000.

Digital Library

[5]

A. Cohen and K. S. Namjoshi. Local proofs for global safety properties. FMSD, 34 (2): 104--125, 2009.

Digital Library

[6]

J. Corbet, A. Rubini, and G. Kroah-Hartman. Linux Device Drivers, 3rd Edition. O'Reilly Media, Inc., 2005.

Digital Library

[7]

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, pages 238--252, 1977.

Digital Library

[8]

C. Flanagan and P. Godefroid. Dynamic partial-order reduction for model checking software. In POPL, pages 110--121, 2005.

Digital Library

[9]

C. Flanagan and S. Qadeer. Thread-modular model checking. In SPIN, pages 213--224, 2003.

Digital Library

[10]

C. Flanagan, S. N. Freund, and S. Qadeer. Thread-modular verification for shared-memory programs. In ESOP, pages 262--277, 2002.

Digital Library

[11]

P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. PhD thesis, University of Liege, Computer Science Department, 1994.

[12]

S. Graf and H. Saıdi. Construction of abstract state graphs with PVS. In CAV, pages 72--83, 1997.

Digital Library

[13]

A. Gupta, C. Popeea, and A. Rybalchenko. Non-monotonic refinement of control abstraction for concurrent programs. In phATVA, pages 188--202, 2010.

Digital Library

[14]

T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL, pages 58--70, 2002.

Digital Library

[15]

T. A. Henzinger, R. Jhala, and R. Majumdar. Race checking by context inference. In PLDI, pages 1--13, 2004.

Digital Library

[16]

C. B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst., 5 (4): 596--619, 1983.

Digital Library

[17]

C. B. Jones. Specification and design of (parallel) programs. In IFIP Congress, pages 321--332, 1983.

[18]

L. Lamport. A new solution of Dijkstra's concurrent programming problem. Commun. ACM, 17 (8): 453--455, 1974.

Digital Library

[19]

L. Lamport. A fast mutual exclusion algorithm. ACM Trans. Comput. Syst., 5 (1): 1--11, 1987.

Digital Library

[20]

S. Lu, S. Park, E. Seo, and Y. Zhou. Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In ASPLOS, pages 329--339, 2008.

Digital Library

[21]

A. Malkis, A. Podelski, and A. Rybalchenko. Thread-modular verification is cartesian abstract interpretation. In ICTAC, pages 183--197, 2006.

Digital Library

[22]

Z. Manna and A. Pnueli. Temporal verification of reactive systems: safety. Springer-Verlag, 1995.

Digital Library

[23]

P. McKenney. Using Promela and Spin to verify parallel algorithms. LWN.net weekly edition, 2007.

[24]

M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. A. Nainar, and I. Neamtiu. Finding and reproducing Heisenbugs in concurrent programs. In OSDI, pages 267--280, 2008.

Digital Library

[25]

G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. In CC, pages 213--228, 2002.

Digital Library

[26]

S. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Inf., 6: 319--340, 1976.

Digital Library

[27]

A. Pnueli, J. Xu, and L. D. Zuck. Liveness with (0, 1, infty)-counter abstraction. In CAV, pages 107--122, 2002.

Digital Library

[28]

A. Podelski and A. Rybalchenko. Transition predicate abstraction and fair termination. In POPL, pages 132--144, 2005.

Digital Library

[29]

A. Podelski and A. Rybalchenko. Armc: The logical choice for software model checking with abstraction refinement. In PADL, pages 245--259, 2007.

Digital Library

[30]

S. Qadeer and D. Wu. KISS: keep it simple and sequential. In PLDI, pages 14--24, 2004.

Digital Library

[31]

A. Rybalchenko. The ARMC tool. Available from http://www7.in.tum.de/ rybal/armc/.

[32]

B. K. Szymanski. A simple solution to Lamport's concurrent programming problem with linear wait. In ICS, pages 621--626, 1988.

Digital Library

[33]

The Intelligent Systems Laboratory. SICStus Prolog User's Manual. Swedish Institute of Computer Science, 2001. Release 3.8.7.

[34]

C. Wang, Z. Yang, V. Kahlon, and A. Gupta. Peephole partial order reduction. In TACAS, pages 382--396, 2008.

Digital Library

Cited By

Henkel EHoenicke JSchindler T(2023)Choose Your Colour: Tree Interpolation for Quantified Formulas in SMTAutomated Deduction – CADE 2910.1007/978-3-031-38499-8_15(248-265)Online publication date: 2-Sep-2023
https://doi.org/10.1007/978-3-031-38499-8_15
Dietsch DHeizmann MKlumpp DNaouar MPodelski ASchätzle C(2021)Verification of Concurrent Programs Using Petri Net UnfoldingsVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-67067-2_9(174-195)Online publication date: 12-Jan-2021
https://doi.org/10.1007/978-3-030-67067-2_9
Andrianov P(2020)Analysis of Correct Synchronization of Operating System ComponentsProgramming and Computing Software10.1134/S036176882008002246:8(712-730)Online publication date: 1-Dec-2020
https://dl.acm.org/doi/10.1134/S0361768820080022
Show More Cited By

Index Terms

Predicate abstraction and refinement for verifying multi-threaded programs

Recommendations

Predicate abstraction and refinement for verifying multi-threaded programs
POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Automated verification of multi-threaded programs requires explicit identification of the interplay between interacting threads, so-called environment transitions, to enable scalable, compositional reasoning. Once the environment transitions are ...
Compositional Abstraction Refinement for Timed Systems
TASE '10: Proceedings of the 2010 4th IEEE International Symposium on Theoretical Aspects of Software Engineering

Model checking suffers from the state explosion problem. Compositional abstraction and abstraction refinement have been investigated in many areas to address this problem. This paper considers the compositional model checking for timed systems. We ...
A counterexample guided abstraction refinement framework for verifying concurrent c programs

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 46, Issue 1

POPL '11

January 2011

624 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1925844

Issue’s Table of Contents

POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2011
652 pages
ISBN:9781450304900
DOI:10.1145/1926385
General Chair:
Thomas Ball
Microsoft Research, USA
,
Program Chair:
Mooly Sagiv
Tel Aviv University, Israel

Copyright © 2011 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 January 2011

Published in SIGPLAN Volume 46, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

95
Total Citations
View Citations
888
Total Downloads

Downloads (Last 12 months)40
Downloads (Last 6 weeks)16

Reflects downloads up to 25 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Henkel EHoenicke JSchindler T(2023)Choose Your Colour: Tree Interpolation for Quantified Formulas in SMTAutomated Deduction – CADE 2910.1007/978-3-031-38499-8_15(248-265)Online publication date: 2-Sep-2023
https://doi.org/10.1007/978-3-031-38499-8_15
Dietsch DHeizmann MKlumpp DNaouar MPodelski ASchätzle C(2021)Verification of Concurrent Programs Using Petri Net UnfoldingsVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-67067-2_9(174-195)Online publication date: 12-Jan-2021
https://doi.org/10.1007/978-3-030-67067-2_9
Andrianov P(2020)Analysis of Correct Synchronization of Operating System ComponentsProgramming and Computing Software10.1134/S036176882008002246:8(712-730)Online publication date: 1-Dec-2020
https://dl.acm.org/doi/10.1134/S0361768820080022
Xu WZhao YMa DZhang YXiao Q(2020)Rely-Guarantee Reasoning about Messaging System for Autonomous Vehicles2020 International Symposium on Theoretical Aspects of Software Engineering (TASE)10.1109/TASE49443.2020.00021(89-96)Online publication date: Dec-2020
https://doi.org/10.1109/TASE49443.2020.00021
Michaliszyn JOtop J(2019)Non-deterministic weighted automata evaluated over Markov chainsJournal of Computer and System Sciences10.1016/j.jcss.2019.10.001Online publication date: Oct-2019
https://doi.org/10.1016/j.jcss.2019.10.001
Rasin DGrumberg OShoham S(2018)Modular Verification of Concurrent Programs via Sequential Model CheckingAutomated Technology for Verification and Analysis10.1007/978-3-030-01090-4_14(228-247)Online publication date: 30-Sep-2018
https://doi.org/10.1007/978-3-030-01090-4_14
Chen HDavid CKroening DSchrammel PWachter B(2017)Bit-Precise Procedure-Modular Termination AnalysisACM Transactions on Programming Languages and Systems10.1145/312113640:1(1-38)Online publication date: 10-Dec-2017
https://dl.acm.org/doi/10.1145/3121136
Unno HTorii SSakamoto H(2017)Automating Induction for Solving Horn ClausesComputer Aided Verification10.1007/978-3-319-63390-9_30(571-591)Online publication date: 13-Jul-2017
https://doi.org/10.1007/978-3-319-63390-9_30
Liu TTyszberowicz SHerda MBeckert BGrahl DTaghdiri M(2016)Computing Specification-Sensitive Abstractions for Program VerificationDependable Software Engineering: Theories, Tools, and Applications10.1007/978-3-319-47677-3_7(101-117)Online publication date: 6-Oct-2016
https://doi.org/10.1007/978-3-319-47677-3_7
Qiang WBliudze S(2016)Verification of Component-Based Systems via Predicate Abstraction and Simultaneous Set ReductionTrustworthy Global Computing10.1007/978-3-319-28766-9_10(147-162)Online publication date: 5-Jan-2016
https://doi.org/10.1007/978-3-319-28766-9_10
Show More Cited By

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.

Media

Figures

Other

Tables

View Issue’s Table of Contents