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

ACM SIGPLAN Notices, Volume 46, Issue 1

Pages 499 - 510

https://doi.org/10.1145/1925844.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

Li XGardy PDeng YSeki H(2020)Reachability of Patterned Conditional Pushdown SystemsJournal of Computer Science and Technology10.1007/s11390-020-0541-z35:6(1295-1311)Online publication date: 30-Nov-2020
https://doi.org/10.1007/s11390-020-0541-z
Dartois LFiliot ETalbot J(2019)Two-Way Parikh Automata with a Visibly Pushdown StackFoundations of Software Science and Computation Structures10.1007/978-3-030-17127-8_11(189-206)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1007/978-3-030-17127-8_11
Ganty PIosif R(2015)Interprocedural Reachability for Flat Integer ProgramsFundamentals of Computation Theory10.1007/978-3-319-22177-9_11(133-145)Online publication date: 4-Aug-2015
https://doi.org/10.1007/978-3-319-22177-9_11
Show More Cited By

Index Terms

Complexity of pattern-based verification for multithreaded programs

Recommendations

Complexity of pattern-based verification for multithreaded programs
POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

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 ...
Runtime Analysis of Atomicity for Multithreaded Programs

Atomicity is a correctness condition for concurrent systems. Informally, atomicity is the property that every concurrent execution of a set of transactions is equivalent to some serial execution of the same transactions. In multithreaded 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

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

Li XGardy PDeng YSeki H(2020)Reachability of Patterned Conditional Pushdown SystemsJournal of Computer Science and Technology10.1007/s11390-020-0541-z35:6(1295-1311)Online publication date: 30-Nov-2020
https://doi.org/10.1007/s11390-020-0541-z
Dartois LFiliot ETalbot J(2019)Two-Way Parikh Automata with a Visibly Pushdown StackFoundations of Software Science and Computation Structures10.1007/978-3-030-17127-8_11(189-206)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1007/978-3-030-17127-8_11
Ganty PIosif R(2015)Interprocedural Reachability for Flat Integer ProgramsFundamentals of Computation Theory10.1007/978-3-319-22177-9_11(133-145)Online publication date: 4-Aug-2015
https://doi.org/10.1007/978-3-319-22177-9_11
Kochems JOng C(2013)Safety verification of asynchronous pushdown systems with shaped stacksProceedings of the 24th international conference on Concurrency Theory10.1007/978-3-642-40184-8_21(288-302)Online publication date: 27-Aug-2013
https://dl.acm.org/doi/10.1007/978-3-642-40184-8_21
Lammich PMüller-Olm MSeidl HWenner A(2013)Contextual Locking for Dynamic Pushdown NetworksStatic Analysis10.1007/978-3-642-38856-9_25(477-498)Online publication date: 2013
https://doi.org/10.1007/978-3-642-38856-9_25
Bansal KDemri S(2013)Model-Checking Bounded Multi-Pushdown SystemsComputer Science – Theory and Applications10.1007/978-3-642-38536-0_35(405-417)Online publication date: 2013
https://doi.org/10.1007/978-3-642-38536-0_35
Lin A(2012)Weakly-Synchronized ground tree rewritingProceedings of the 37th international conference on Mathematical Foundations of Computer Science10.1007/978-3-642-32589-2_55(630-642)Online publication date: 27-Aug-2012
https://dl.acm.org/doi/10.1007/978-3-642-32589-2_55
Hague MLin A(2012)Synchronisation- and reversal-bounded analysis of multithreaded programs with countersProceedings of the 24th international conference on Computer Aided Verification10.1007/978-3-642-31424-7_22(260-276)Online publication date: 7-Jul-2012
https://dl.acm.org/doi/10.1007/978-3-642-31424-7_22
Kahlon VWang C(2012)Lock removal for concurrent trace programsProceedings of the 24th international conference on Computer Aided Verification10.1007/978-3-642-31424-7_20(227-242)Online publication date: 7-Jul-2012
https://dl.acm.org/doi/10.1007/978-3-642-31424-7_20
Long ZCalin GMajumdar RMeyer R(2012)Language-Theoretic abstraction refinementProceedings of the 15th international conference on Fundamental Approaches to Software Engineering10.1007/978-3-642-28872-2_25(362-376)Online publication date: 24-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-28872-2_25
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