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

research-article

Complexity of pattern-based verification for multithreaded programs

Authors:

Javier Esparza,

Pierre GantyAuthors Info & Claims

POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 499 - 510

https://doi.org/10.1145/1926385.1926443

Published: 26 January 2011 Publication History

Abstract

Pattern-based verification checks the correctness of the program executions that follow a given pattern, a regular expression over the alphabet of program transitions of the form w₁* ... w_n*. For multithreaded programs, the alphabet of the pattern is given by the synchronization operations between threads. We study the complexity of pattern-based verification for abstracted multithreaded programs in which, as usual in program analysis, conditions have been replaced by nondeterminism (the technique works also for boolean programs). While unrestricted verification is undecidable for abstracted multithreaded programs with recursive procedures and PSPACE-complete for abstracted multithreaded while-programs, we show that pattern-based verification is NP-complete for both classes. We then conduct a multiparameter analysis in which we study the complexity in the number of threads, the number of procedures per thread, the size of the procedures, and the size of the pattern. We first show that no algorithm for pattern-based verification can be polynomial in the number of threads, procedures per thread, or the size of the pattern (unless P=NP). Then, using recent results about Parikh images of regular languages and semilinear sets, we present an algorithm exponential in the number of threads, procedures per thread, and size of the pattern, but polynomial in the size of the procedures.

Supplementary Material

MP4 File (46-mpeg-4.mp4)

Download
358.13 MB

References

[1]

CHESS: Find and reproduce heisenbugs in concurrent programs. URL http://research.microsoft.com/en-us/projects/CHESS/.

[2]

M. F. Atig, B. Bollig, and P. Habermehl. Emptiness of multi-pushdown automata is 2EXPTIME-complete. In DLT '08: Proc. 12th Int. Conf. on Developments in Language Theory, volume 5257 of LNCS, pages 121--133. Springer, 2008.

Digital Library

[3]

M. F. Atig, A. Bouajjani, and T. Touili. On the reachability analysis of acyclic networks of pushdown systems. In CONCUR '08: Proc. 19th Int. Conf. on Concurrency Theory, volume 5201 of LNCS, pages 356--371. Springer, 2008.

Digital Library

[4]

M. F. Atig, A. Bouajjani, and S. Qadeer. Context-bounded analysis for concurrent programs with dynamic creation of threads. In TACAS '09: Proc. 15th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 5505 of LNCS, pages 107--123. Springer, 2009.

Digital Library

[5]

T. Ball and S. K. Rajamani. The SLAM project: debugging system software via static analysis. In POPL '02: Proc. 29th ACM SIGPLAN- SIGACT Symp. on Principles of Programming Languages, pages 1--3. ACM Press, 2002.

Digital Library

[6]

A. Bouajjani, M. Mqller-Olm, and T. Touili. Regular symbolic analysis of dynamic networks of pushdown systems. In CONCUR '05: Proc. 16th Int. Conf. on Concurrency Theory, volume 3653 of LNCS, pages 473--487. Springer, 2005.

Digital Library

[7]

J. Esparza. Petri nets, commutative context-free grammars, and basic parallel processes. Fundamenta Informaticae, 31:13--26, 1997.

Digital Library

[8]

J. Esparza, P. Ganty, S. Kiefer, and M. Luttenberger. Parikh's theorem: A simple and direct construction. CoRR, 1006.3825, 2010.

Digital Library

[9]

P. Ganty, B. Monmege, and R. Majumdar. Bounded under approximations. In CAV '10: Proc. 20th Int. Conf. on Computer Aided Verification, volume 6174 of LNCS, pages 600--614. Springer, 2010.

Digital Library

[10]

M. R. Garey and D. S. Johnson. Computers and Intractability, A Guide to the Theory of NP-Completeness. New York, 1979.

Digital Library

[11]

S. Ginsburg and E. H. Spanier. Semigroups, presburger formulas, and languages. Pacific Journal of Mathematics, 16(2):285--296, 1966.

[12]

E. Graedel. Subclasses of presburger arithmetic and the polynomial time hierarchy. Theoretical Computer Science, 56(3):289--301, 1988.

Digital Library

[13]

J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1st edition, 1979.

Digital Library

[14]

V. Kahlon. Boundedness vs. unboundedness of lock chains: Characterizing decidability of pairwise cfl-reachability for threads communicating via locks. In LICS '09: Proc. 24th Annual IEEE Symp. on Logic in Computer Science, pages 27--36. IEEE Computer Society, 2009.

Digital Library

[15]

V. Kahlon. Tractable dataflow analysis for concurrent programs via bounded languages. Patent WO/2009/094439, July 2009.

[16]

V. Kahlon and A. Gupta. On the analysis of interacting pushdown systems. In POPL '03: Proc. 30th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pages 303--314. ACM, 2007.

Digital Library

[17]

V. Kahlon, F. Ivancic, and A. Gupta. Reasoning about threads communicating via locks. In CAV '05: Proc. 17th Int. Conf. on Computer Aided Verification, volume 3576 of LNCS, pages 505--518. Springer, 2005.

Digital Library

[18]

A. Kaiser, D. Kroening, and T. Wahl. Dynamic cutoff detection in parameterized concurrent programs. In CAV '10: Proc. 20th Int. Conf. on Computer Aided Verification, volume 6174 of LNCS. Springer, 2010.

Digital Library

[19]

E. Kopczynski and A. W. To. Parikh images of grammars: Complexity and applications. In LICS '10: Proc. 25th Annual IEEE Symp. on Logic in Computer Science. IEEE, 2010.

Digital Library

[20]

A. Lal and T. Reps. Reducing concurrent analysis under a context bound to sequential analysis. In CAV '08: Proc. 20th Int. Conf. on Computer Aided Verification, volume 5128 of LNCS, pages 37--51. Springer, 2008.

Digital Library

[21]

A. Lal, T. Touili, N. Kidd, and T. W. Reps. Interprocedural analysis of concurrent programs under a context bound. In TACAS '08: Proc. 14th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 4963 of LNCS, pages 282--298. Springer, 2008.

Digital Library

[22]

J. Lenstra, H. W. Integer programming with a fixed number of variables. Mathematics of Operations Research, 8(4):538--548, 1983.

Digital Library

[23]

R. J. Parikh. On context-free languages. Journal of the ACM, 13(4): 570--581, 1966.

Digital Library

[24]

S. Qadeer. The case for context-bounded verification of concurrent programs. In SPIN '08: Proc. of 15th Int. Model Checking Software Workshop, volume 5156 of LNCS, pages 3--6. Springer, 2008.

Digital Library

[25]

S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. In TACAS '05: Proc. 11th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 3440 of LNCS, pages 93--107. Springer, 2005.

Digital Library

[26]

G. Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. ACM TOPLAS, 22(2):416--430, 2000.

Digital Library

[27]

B. Scarpellini. Complexity of subcases of presburger arithmetic. Trans. of the American Mathematical Society, 284(1):203--218, 1984.

[28]

D. Suwimonteerabuth, J. Esparza, and S. Schwoon. Symbolic context-bounded analysis of multithreaded java programs. In SPIN '08: Proc. of 15th Int. Model Checking Software Workshop, volume 5156 of LNCS, pages 270--287. Springer, 2008.

Digital Library

[29]

A. W. To. Parikh images of regular languages: Complexity and applications. CoRR, 1002.1464, 2010.

[30]

S. La Torre, G. Parlato, and P. Madhusudan. Reducing context-bounded concurrent reachability to sequential reachability. In CAV'09: Proc. 21st Int. Conf. on Computer Aided Verification, volume 5643 of LNCS, pages 477--492. Springer, 2009.

Digital Library

[31]

K. N. Verma, H. Seidl, and T. Schwentick. On the complexity of equational horn clauses. In CADE '00: 20th Int. Conf. on Automated Deduction, volume 1831 of LNCS, pages 337--352. Springer, 2005.

Digital Library

[32]

J. von zur Gathen and M. Sieveking. A bound on solutions of linear integer equalities and inequalities. Proc. of the American Mathematical Society, 72:155--158, 1978.

Cited By

Hague MJeż ALin A(2024)Parikh’s Theorem Made SymbolicProceedings of the ACM on Programming Languages10.1145/36329078:POPL(1945-1977)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632907
Hague M(2019)Strings at MOSCAACM SIGLOG News10.1145/3373394.33733966:4(4-22)Online publication date: 25-Nov-2019
https://dl.acm.org/doi/10.1145/3373394.3373396
Demri S(2018)Reasoning About Reversal-Bounded Counter MachinesEwa Orłowska on Relational Methods in Logic and Computer Science10.1007/978-3-319-97879-6_17(441-479)Online publication date: 7-Dec-2018
https://doi.org/10.1007/978-3-319-97879-6_17
Show More Cited By

Index Terms

Complexity of pattern-based verification for multithreaded programs

Recommendations

Context-bounded verification of liveness properties for multithreaded shared-memory programs

We study context-bounded verification of liveness properties of multi-threaded, shared-memory programs, where each thread can spawn additional threads. Our main result shows that context-bounded fair termination is decidable for the model; context-...
Complexity of pattern-based verification for multithreaded programs
POPL '11

Pattern-based verification checks the correctness of the program executions that follow a given pattern, a regular expression over the alphabet of program transitions of the form w₁* ... w_n*. For multithreaded programs, the alphabet of the pattern is ...
Pattern-Based Verification for Multithreaded Programs

Pattern-based verification checks the correctness of program executions that follow a given pattern, a regular expression over the alphabet of program transitions of the form w₁^* … w_n^*. For multithreaded programs, the alphabet of the pattern is given by ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

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

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

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]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 January 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '11

Sponsor:

SIGPLAN

POPL '11: The 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 26 - 28, 2011

Texas, Austin, USA

Acceptance Rates

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

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

34
Total Citations
View Citations
470
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Hague MJeż ALin A(2024)Parikh’s Theorem Made SymbolicProceedings of the ACM on Programming Languages10.1145/36329078:POPL(1945-1977)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632907
Hague M(2019)Strings at MOSCAACM SIGLOG News10.1145/3373394.33733966:4(4-22)Online publication date: 25-Nov-2019
https://dl.acm.org/doi/10.1145/3373394.3373396
Demri S(2018)Reasoning About Reversal-Bounded Counter MachinesEwa Orłowska on Relational Methods in Logic and Computer Science10.1007/978-3-319-97879-6_17(441-479)Online publication date: 7-Dec-2018
https://doi.org/10.1007/978-3-319-97879-6_17
Abdulla PAtig MChen YDiep BHolík LRezine ARümmer P(2017)Flatten and conquer: a framework for efficient analysis of string constraintsACM SIGPLAN Notices10.1145/3140587.306238452:6(602-617)Online publication date: 14-Jun-2017
https://dl.acm.org/doi/10.1145/3140587.3062384
Abdulla PAtig MChen YDiep BHolík LRezine ARümmer PCohen AVechev M(2017)Flatten and conquer: a framework for efficient analysis of string constraintsProceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3062341.3062384(602-617)Online publication date: 14-Jun-2017
https://dl.acm.org/doi/10.1145/3062341.3062384
Atig MChistikov DHofman PKumar KSaivasan PZetzsche GKoskinen EGrohe MShankar N(2016)The complexity of regular abstractions of one-counter languagesProceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/2933575.2934561(207-216)Online publication date: 5-Jul-2016
https://dl.acm.org/doi/10.1145/2933575.2934561
Hague MKochems JOng C(2016)Unboundedness and downward closures of higher-order pushdown automataACM SIGPLAN Notices10.1145/2914770.283762751:1(151-163)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2914770.2837627
Hague MKochems JOng CBodik RMajumdar R(2016)Unboundedness and downward closures of higher-order pushdown automataProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2837614.2837627(151-163)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2837614.2837627
Gange GNavas JSchachte PSøndergaard HStuckey P(2016)A complete refinement procedure for regular separability of context-free languagesTheoretical Computer Science10.1016/j.tcs.2016.01.026625:C(1-24)Online publication date: 25-Apr-2016
https://dl.acm.org/doi/10.1016/j.tcs.2016.01.026
Furbach FMeyer RSchneider KSenftleben M(2015)Memory-Model-Aware TestingACM Transactions on Embedded Computing Systems10.1145/275376114:4(1-25)Online publication date: 24-Sep-2015
https://dl.acm.org/doi/10.1145/2753761
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