research-article

Open access

Pattern-Based Verification for Multithreaded Programs

Authors:

Javier Esparza,

Pierre Ganty,

Tomáš PochAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 36, Issue 3

Article No.: 9, Pages 1 - 29

https://doi.org/10.1145/2629644

Published: 15 September 2014 Publication History

PDF eReader

Abstract

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 the reads and writes to the shared storage. We study the complexity of pattern-based verification for multithreaded programs with shared counters and finite variables. While unrestricted verification is undecidable for abstracted multithreaded programs with recursive procedures and PSPACE-complete for abstracted multithreaded while-programs (even without counters), we show that pattern-based verification is NP-complete for both classes, even in the presence of counters. We then conduct a multiparameter analysis to study the complexity of the problem on its three natural parameters (number of threads+counters+variables, maximal size of a thread, size of the pattern) and on two parameters related to thread structure (maximal number of procedures per thread and longest simple path of procedure calls). We present an algorithm that for a fixed number of threads, counters, variables, and pattern size solves the verification problem in st^{O(lsp+ ⌈ log (pr+1) ⌉)} time, where st is the maximal size of a thread, pr is the maximal number of procedures per thread, and lsp is the longest simple path of procedure calls.

References

[1]

Tony Andrews, Shaz Qadeer, Sriram K. Rajamani, Jakob Rehof, and Yichen Zie. 2004. Zing: A Model Checker for Concurrent Software. Technical Report MSR-TR-2004-10. Microsoft Research.

Google Scholar

[2]

Mohamed Faouzi Atig, Benedikt Bollig, and Peter Habermehl. 2008. Emptiness of multi-pushdown automata is 2EXPTIME-complete. In Proc. 12th Int. Conf. on Developments in Language Theory. Springer, 121--133.

Digital Library

Google Scholar

[3]

Mohamed Faouzi Atig, Ahmed Bouajjani, and Shaz Qadeer. 2011. Context-Bounded analysis for concurrent programs with dynamic creation of threads. Logical Methods in Computer Science (LMCS) 7, 4 (2011), 1--48.

Crossref

Google Scholar

[4]

Mohamed Faouzi Atig, Ahmed Bouajjani, and Tayssir Touili. 2008. On the reachability analysis of acyclic networks of pushdown systems. In Proc. 19th Int. Conf. on Concurrency Theory. Springer, 356--371.

Digital Library

Google Scholar

[5]

Ahmed Bouajjani, Markus Müller-Olm, and Taissir Touili. 2005. Regular symbolic analysis of dynamic networks of pushdown systems. In Proc. 16th Int. Conf. on Concurrency Theory. Springer, 473--487.

Digital Library

Google Scholar

[6]

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

Digital Library

Google Scholar

[7]

Javier Esparza, Pierre Ganty, Stefan Kiefer, and Michael Luttenberger. 2011. Parikh’s theorem: A simple and direct automaton construction. Inform. Process. Lett. 111 (2011), 614--619.

Digital Library

Google Scholar

[8]

Pierre Ganty, Rupak Majumdar, and Benjamin Monmege. 2012. Bounded underapproximations. Formal Methods Syst. Des. 40, 2 (2012), 206--231.

Digital Library

Google Scholar

[9]

Michael R. Garey and David S. Johnson. 1979. Computers and Intractability, A Guide to the Theory of NP-Completeness. W. H. Freeman & Co., New York.

Digital Library

Google Scholar

[10]

Seymour Ginsburg. 1966. The Mathematical Theory of Context-Free Languages. McGraw-Hill, New York, NY.

Digital Library

Google Scholar

[11]

Eitan M. Gurari and Oscar H. Ibarra. 1981. The complexity of decision problems for finite-turn multicounter machines. J. Comput. System Sci. 22 (1981), 220--229.

Crossref

Google Scholar

[12]

Matthew Hague. 2011. Parameterised pushdown systems with non-atomic writes. In Proc. 31st IARCS Annual Conf. on Foundation of Software Technology and Theoretical Computer Science (Leibniz International Proceedings in Informatics (LIPIcs)).Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 457--468.

Google Scholar

[13]

Matthew Hague and Anthony Widjaja Lin. 2012. Synchronisation- and reversal-bounded analysis of multithreaded programs with counters. In Proc. 24th Int. Conf. on Computer Aided Verification. Springer, 260--276.

Digital Library

Google Scholar

[14]

John E. Hopcroft and Jeffrey D. Ullman. 1979. Introduction to Automata Theory, Languages and Computation (1st ed.). Addison-Wesley.

Digital Library

Google Scholar

[15]

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

Digital Library

Google Scholar

[16]

Vineet Kahlon. 2009b. Tractable Dataflow Analysis for Concurrent Programs via Bounded Languages. (July 2009). Patent WO/2009/094439.

Google Scholar

[17]

Vineet Kahlon and Aarti Gupta. 2007. On the analysis of interacting pushdown systems. In Proc. 30th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. ACM, 303--314.

Digital Library

Google Scholar

[18]

Vineet Kahlon, Franjo Ivancic, and Aarti Gupta. 2005. Reasoning about threads communicating via locks. In Proc. 17th Int. Conf. on Computer Aided Verification. Springer, 505--518.

Digital Library

Google Scholar

[19]

Alexander Kaiser, Daniel Kroening, and Thomas Wahl. 2010. Dynamic cutoff detection in parameterized concurrent programs. In Proc. 20th Int. Conf. on Computer Aided Verification. Springer, 645--659.

Digital Library

Google Scholar

[20]

Akash Lal and Thomas Reps. 2009. Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods Syst. Des., 1 (2009), 73--97.

Digital Library

Google Scholar

[21]

Akash Lal, Tayssir Touili, Nicholas Kidd, and Thomas W. Reps. 2008. Interprocedural analysis of concurrent programs under a context bound. In Proc. 14th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 282--298.

Digital Library

Google Scholar

[22]

Zhenyue Long, Georgel Calin, Rupak Majumdar, and Roland Meyer. 2012. Language-theoretic abstraction refinement. In Proc. 15th Int. Conf. Fundamental Approaches to Software Engineering. Springer, 362--376.

Digital Library

Google Scholar

[23]

Madanlal Musuvathi and Shaz Qadeer. 2007. Iterative context bounding for systematic testing of multithreaded programs. In Proc. 28th ACM-SIGPLAN Conf. on Programming Language Design and Implementation. ACM, 446--455.

Digital Library

Google Scholar

[24]

Rohit J. Parikh. 1966. On context-free languages. J. ACM 13, 4 (1966), 570--581.

Digital Library

Google Scholar

[25]

Shaz Qadeer and Jakob Rehof. 2005. Context-Bounded model checking of concurrent software. In Proc. 11th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems.Springer, 93--107.

Digital Library

Google Scholar

[26]

Shaz Qadeer and Dinghao Wu. 2004. KISS: keep it simple and sequential. In Proc. 25th ACM-SIGPLAN Conf. on Programming Language Design and Implementation. ACM, 14--24.

Digital Library

Google Scholar

[27]

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

Digital Library

Google Scholar

[28]

Dejvuth Suwimonteerabuth, Javier Esparza, and Stefan Schwoon. 2008. Symbolic context-bounded analysis of multithreaded Java programs. In Proc. of 15th Int. Model Checking Software Workshop. Springer, 270--287.

Digital Library

Google Scholar

[29]

Salvatore La Torre, Gennaro Parlato, and Parthasarathy Madhusudan. 2009. Reducing context-bounded concurrent reachability to sequential reachability. In Proc. 21st Int. Conf. on Computer Aided Verification. Springer, 477--492.

Digital Library

Google Scholar

[30]

Kumar N. Verma, Helmut Seidl, and Thomas Schwentick. 2005. On the complexity of equational horn clauses. In Proc. 20th Int. Conf. on Automated Deduction. Springer, 337--352.

Digital Library

Google Scholar

[31]

Joachim von zur Gathen and Malte Sieveking. 1978. A bound on solutions of linear integer equalities and inequalities. Proc. Amer. Math. Soc. 72 (1978), 155--158.

Crossref

Google Scholar

Cited By

View all

Malkis A(2022)Reachability in parallel programs is polynomial in the number of threadsJournal of Parallel and Distributed Computing10.1016/j.jpdc.2021.11.008162:C(1-16)Online publication date: 1-Apr-2022
https://dl.acm.org/doi/10.1016/j.jpdc.2021.11.008
Zetzsche G(2021)Recent Advances on Reachability Problems for Valence Systems (Invited Talk)Reachability Problems10.1007/978-3-030-89716-1_4(52-65)Online publication date: 22-Oct-2021
https://doi.org/10.1007/978-3-030-89716-1_4
Chistikov DVyalyi MHermanns HZhang LKobayashi NMiller D(2020)Re-pairing bracketsProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3373718.3394752(312-326)Online publication date: 8-Jul-2020
https://dl.acm.org/doi/10.1145/3373718.3394752
Show More Cited By

Index Terms

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 ...
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 ...
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, ...

Reviews

Reviewer: Markus Wolf

The verification of some program properties via model checking has matured in recent years for sequential programming. However, for multithreaded programming, an area becoming ever more important, several complexity-theory-related questions are still open. This paper solves some problems related to the complexity of verification of multithreaded programs against shared storage read/write execution patterns. A short introduction presents current approaches to the verification problem and how the results of the paper fit into the landscape. Next, the programming model is explained. The main restriction of the program model is that threads communicate through shared global variables that either are of finite range or counters with a limited set of operations acting on them. Dynamic thread creation is not allowed in this model. The program model is formally mapped to certain context-free grammars and program execution is then mapped to certain words in the language of these grammars. Patterns are then defined to be regular expressions over the alphabet of program actions. Pattern-based verification is thus reduced to a language-theoretic problem. The core sections of the paper explore the language-theoretic problems posed. The authors conduct a rigorous multiparameter analysis, where the parameters are the size of threads, size of pattern, number of threads, and so on. The main result is a tree of complexity classes resulting from certain choices of the parameters and a verification algorithm that is polynomial if the number of procedure variables is fixed. The final section, as usual, contains a summary of the results achieved and a comparison to related work. The paper is very well written, and for every proof there is sufficient detail given to comprehend it. The paper may be especially interesting for language and complexity theorists, first, because it nicely shows how current problems can be reduced to known results from the '60s or '70s, and, second, because one of the proofs given is essentially a novel constructive proof of Parikh's theorem. This is a very enjoyable paper indeed. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 36, Issue 3

September 2014

124 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/2669618

Editor:
Jens Palsberg
University of California, Los Angeles, USA

Issue’s Table of Contents

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: 15 September 2014

Accepted: 01 January 2014

Revised: 01 December 2013

Received: 01 March 2012

Published in TOPLAS Volume 36, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
455
Total Downloads

Downloads (Last 12 months)96
Downloads (Last 6 weeks)12

Reflects downloads up to 30 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Malkis A(2022)Reachability in parallel programs is polynomial in the number of threadsJournal of Parallel and Distributed Computing10.1016/j.jpdc.2021.11.008162:C(1-16)Online publication date: 1-Apr-2022
https://dl.acm.org/doi/10.1016/j.jpdc.2021.11.008
Zetzsche G(2021)Recent Advances on Reachability Problems for Valence Systems (Invited Talk)Reachability Problems10.1007/978-3-030-89716-1_4(52-65)Online publication date: 22-Oct-2021
https://doi.org/10.1007/978-3-030-89716-1_4
Chistikov DVyalyi MHermanns HZhang LKobayashi NMiller D(2020)Re-pairing bracketsProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3373718.3394752(312-326)Online publication date: 8-Jul-2020
https://dl.acm.org/doi/10.1145/3373718.3394752
Chini PMeyer RSaivasan P(2020)Fine-Grained Complexity of Safety VerificationJournal of Automated Reasoning10.1007/s10817-020-09572-x64:7(1419-1444)Online publication date: 1-Oct-2020
https://dl.acm.org/doi/10.1007/s10817-020-09572-x
Hague MLin A(2018)Decidable models of integer-manipulating programs with recursive parallelismTheoretical Computer Science10.1016/j.tcs.2018.04.050750(24-37)Online publication date: Nov-2018
https://doi.org/10.1016/j.tcs.2018.04.050
Dimitrova RMajumdar R(2018)Reachability analysis of reversal-bounded automata on series---parallel graphsActa Informatica10.1007/s00236-016-0290-155:2(153-189)Online publication date: 1-Mar-2018
https://dl.acm.org/doi/10.1007/s00236-016-0290-1
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
Atig MNarayan Kumar KSaivasan P(2016)Acceleration in Multi-PushDown SystemsProceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 963610.1007/978-3-662-49674-9_45(698-714)Online publication date: 2-Apr-2016
https://dl.acm.org/doi/10.1007/978-3-662-49674-9_45
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Index Terms

Recommendations

Complexity of pattern-based verification for multithreaded programs

Complexity of pattern-based verification for multithreaded programs

Runtime Analysis of Atomicity for Multithreaded Programs

Reviews

Access critical reviews of Computing literature here

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Get Access

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations