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

Article

Proving thread termination

Authors:

Andreas Podelski,

Andrey RybalchenkoAuthors Info & Claims

PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 320 - 330

https://doi.org/10.1145/1250734.1250771

Published: 10 June 2007 Publication History

Abstract

Concurrent programs are often designed such that certain functions executing within critical threads must terminate. Examples of such cases can be found in operating systems, web servers, e-mail clients, etc. Unfortunately, no known automatic program termination prover supports a practical method of proving the termination of threads. In this paper we describe such a procedure. The procedure's scalability is achieved through the use of environment models that abstract away the surrounding threads. The procedure's accuracy is due to a novel method of incrementally constructing environment abstractions. Our method finds the conditions that a thread requires of its environment in order to establish termination by looking at the conditions necessary to prove that certain paths through the thread represent well-founded relations if executed in isolation of the other threads. The paper gives a description of experimental results using an implementation of our procedureon Windows device drivers and adescription of a previously unknown bug found withthe tool.

References

[1]

B. Alpern and F. Schneider. Defining liveness. Information processing letters, 21:181--185, 1985.

[2]

I. Balaban, A. Cohen, and A. Pnueli. Ranking abstraction of recursive programs. In VMCAI'06: Verification, Model Checking, and Abstract Interpretation, 2006.

Digital Library

[3]

T. Ball et al. Thorough static analysis of device drivers. In EuroSys'06: European Systems Conference, 2006.

Digital Library

[4]

J. Berdine, A. Chawdhary, B. Cook, D. Distefano, and P. O'Hearn. Variance analyses from invariance analyses. In POPL'07: Principles of Programming Languages, 2007.

Digital Library

[5]

J. Berdine, B. Cook, D. Distefano, and P. O'Hearn. Automatic termination proofs for programs with shape-shifting heaps. In CAV'06: International Conference on Computer Aided Verification, 2006.

Digital Library

[6]

A. Biere, C. Artho, and V. Schuppan. Liveness checking as safety checking. In FMICS'02: Formal Methods for Industrial Critical Systems, 2002.

[7]

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. A static analyzer for large safety--critical software. In PLDI'03: Programming Language Design and Implementation, 2003.

Digital Library

[8]

A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro, and T. Vojnar. Programs with lists are counter automata. In CAV'06: International Conference on Computer Aided Verification, 2006.

Digital Library

[9]

A. Bradley, Z. Manna, and H. Sipma. Linear ranking with reachability. In CAV'05: Computer-Aided Verification, 2005.

Digital Library

[10]

A. Bradley, Z. Manna, and H. Sipma. The polyranking principle. In ICALP'05: International Colloquium on Automata, Languages and Programming, 2005.

Digital Library

[11]

A. Bradley, Z. Manna, and H. Sipma. Termination analysis of integer linear loops. In CONCUR'05: Concurrency Theory, 2005.

Digital Library

[12]

A. Bradley, Z. Manna, and H. Sipma. Termination of polynomial programs. In VMCAI'05: Verification, Model Checking, and Abstract Interpretation, 2005.

Digital Library

[13]

S. Chaki, E. M. Clarke, J. Ouaknine, N. Sharygia, and N. Sinha. Efficient verification of sequential and concurrent C programs. Formal Methods in System Design, 25(2--3):129--166, 2004.

Digital Library

[14]

E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000.

Digital Library

[15]

E. M. Clarke, M. Talupur, and H. Veith. Environment abstraction for parameterized verification. In VMCAI'06: Verification, Model Checking, and Abstract Interpretation, 2006.

Digital Library

[16]

J. M. Cobleigh, D. Giannakopoulou, and C. S. Pasareanu. Learning assumptions for compositional verification. In TACAS'04: Tools and Algorithms for the Construction and Analysis of Systems, 2003.

Digital Library

[17]

M. Codish and C. Taboch. A semantic basis for the termination analysis of logic programs. The Journal of Logic Programming, 41(1):103--123, 1999.

[18]

M. Colón and H. Sipma. Practical methods for proving program termination. In CAV'02: Computer Aided Verification, 2002.

Digital Library

[19]

E. Contejean, C. Marché, B. Monate, and X. Urbain. Proving Termination of Rewriting with sc CtextitiME. In WST'03: International Workshop on Termination, 2003.

[20]

B. Cook, A. Gotsman, A. Podelski, A. Rybalchenko, and M. Vardi. Proving that software eventually does something good. In POPL'07: Principles of Programming Languages, 2007.

Digital Library

[21]

B. Cook, A. Podelski, and A. Rybalchenko. Termination proofs for systems code. In PLDI'06: Programming Language Design and Implementation, 2006.

Digital Library

[22]

P. Cousot. Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In VMCAI'05: Verification, Model Checking, and Abstract Interpretation, 2005.

Digital Library

[23]

P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In POPL'78: Principles of Programming Languages, 1978.

Digital Library

[24]

C. Flanagan, S. N. Freund, S. Qadeer, and S. A. Seshia. Modular verification of multithreaded programs. Journal on Theoretical Computer Science, 338(1-3):153--183, 2005.

Digital Library

[25]

C. Flanagan and P. Godefroid. Dynamic partial-order reduction for model checking software. In POPL'05: Principles of Programming Languages, 2005.

Digital Library

[26]

C. Flanagan and S. Qadeer. Thread-modular model checking. In SPIN'03, 2003.

Digital Library

[27]

P. Godefroid. Partial-order methods for the verification of concurrent systems - an approach to the state-explosion problem. PhD thesis, 1994.

[28]

K. Havelund and T. Pressburger. Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer, 2(4), 1998.

[29]

T. A. Henzinger, R. Jhala, and R. Majumdar. Permissive interfaces. In FSE'05, 2005.

Digital Library

[30]

T. A. Henzinger, R. Jhala, R. Majumdar, and S. Qadeer. Thread-modular abstraction refinement. In CAV'03, 2003.

[31]

G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279--295, 1997.

Digital Library

[32]

B. Jacobs, K. R. M. Leino, F. Piessens, and W. Schulte. Safe concurrency for aggregate objects with invariants. In SEFM'05: Software Engineering and Formal Methods, 2005.

Digital Library

[33]

C. Jones. Specification and design of (parallel) programs. In IFIP Congress, 1983.

[34]

V. Kahlon, A. Gupta, and N. Sinha. Symbolic model checking of concurrent programs using partial orders and on-the-fly transactions. In CAV'06: International Conference on Computer Aided Verification, 2006.

Digital Library

[35]

R. J. Lipton. Reduction: a method of proving properties of parallel programs. Communications of the ACM, 18(12):717--721, 1975.

Digital Library

[36]

Z. Manna and A. Pnueli. Axiomatic approach to total correctness of programs. Acta Informatica, 1974.

Digital Library

[37]

A. Miné. The octagon abstract domain. Higher-Order and Symbolic Computation, 19:31--100, 2006.

Digital Library

[38]

A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In VMCAI'04: Verification, Model Checking, and Abstract Interpretation, 2004.

[39]

J. C. Reynolds. The Craft of Programming. London, 1981.

Digital Library

[40]

A. Tiwari. Termination of linear programs. In CAV'04: Computer Aided Verification, 2004.

Cited By

Al-Bataineh OMoonen LVidziunas L(2024)Extending the range of bugs that automated program repair can handleJournal of Systems and Software10.1016/j.jss.2023.111918209(111918)Online publication date: Mar-2024
https://doi.org/10.1016/j.jss.2023.111918
Pani TWeissenbacher GZuleger F(2023)Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verificationFormal Methods in System Design10.1007/s10703-023-00439-664:1-3(108-145)Online publication date: 6-Oct-2023
https://doi.org/10.1007/s10703-023-00439-6
Lette DFarzan A(2023)Commutativity for Concurrent Program Termination ProofsComputer Aided Verification10.1007/978-3-031-37706-8_6(109-131)Online publication date: 17-Jul-2023
https://doi.org/10.1007/978-3-031-37706-8_6
Show More Cited By

Index Terms

Proving thread termination

Recommendations

Proving thread termination
Proceedings of the 2007 PLDI conference

Concurrent programs are often designed such that certain functions executing within critical threads must terminate. Examples of such cases can be found in operating systems, web servers, e-mail clients, etc. Unfortunately, no known automatic program ...
Proving non-termination
POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

The search for proof and the search for counterexamples (bugs) are complementary activities that need to be pursued concurrently in order to maximize the practical success rate of verification tools.While this is well-understood in safety verification, ...
Proving non-termination
POPL '08

The search for proof and the search for counterexamples (bugs) are complementary activities that need to be pursued concurrently in order to maximize the practical success rate of verification tools.While this is well-understood in safety verification, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2007

508 pages

ISBN:9781595936332

DOI:10.1145/1250734

General Chair:
Jeanne Ferrante
University of California, San Diego, USA
,
Program Chair:
Kathryn S. McKinley
University of Texas at Austin, USA

ACM SIGPLAN Notices Volume 42, Issue 6
Proceedings of the 2007 PLDI conference
June 2007
491 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1273442
Issue’s Table of Contents

Copyright © 2007 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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 June 2007

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

PLDI '07

Sponsor:

PLDI '07: ACM SIGPLAN Conference on Programming Language Design and Implementation

June 10 - 13, 2007

California, San Diego, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

50
Total Citations
View Citations
575
Total Downloads

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

Reflects downloads up to 31 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Al-Bataineh OMoonen LVidziunas L(2024)Extending the range of bugs that automated program repair can handleJournal of Systems and Software10.1016/j.jss.2023.111918209(111918)Online publication date: Mar-2024
https://doi.org/10.1016/j.jss.2023.111918
Pani TWeissenbacher GZuleger F(2023)Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verificationFormal Methods in System Design10.1007/s10703-023-00439-664:1-3(108-145)Online publication date: 6-Oct-2023
https://doi.org/10.1007/s10703-023-00439-6
Lette DFarzan A(2023)Commutativity for Concurrent Program Termination ProofsComputer Aided Verification10.1007/978-3-031-37706-8_6(109-131)Online publication date: 17-Jul-2023
https://doi.org/10.1007/978-3-031-37706-8_6
Al-Bataineh OMoonen L(2022)Towards Extending the Range of Bugs That Automated Program Repair Can Handle2022 IEEE 22nd International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS57517.2022.00031(209-220)Online publication date: Dec-2022
https://doi.org/10.1109/QRS57517.2022.00031
Baumann PMajumdar RThinniyam RZetzsche G(2021)Context-bounded verification of liveness properties for multithreaded shared-memory programsProceedings of the ACM on Programming Languages10.1145/34343255:POPL(1-31)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434325
Shoshi TIshikawa TKobayashi NSakayori KSato RTsukada T(2021)Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program TerminationProgramming Languages and Systems10.1007/978-3-030-89051-3_15(265-284)Online publication date: 12-Oct-2021
https://doi.org/10.1007/978-3-030-89051-3_15
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
Kusano MWang CBodden ESchäfer WDeursen AZisman A(2017)Thread-modular static analysis for relaxed memory modelsProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering10.1145/3106237.3106243(337-348)Online publication date: 21-Aug-2017
https://dl.acm.org/doi/10.1145/3106237.3106243
Albert EFlores-Montoya AGenaim SMartin-Martin E(2017)Rely-Guarantee Termination and Cost Analyses of Loops with Concurrent InterleavingsJournal of Automated Reasoning10.1007/s10817-016-9400-659:1(47-85)Online publication date: 1-Jun-2017
https://dl.acm.org/doi/10.1007/s10817-016-9400-6
Piterman N(2017)Advances in verification presented in TACAS'13International Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-017-0460-719:5(511-515)Online publication date: 1-Oct-2017
https://dl.acm.org/doi/10.1007/s10009-017-0460-7
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 Table of Contents