Javier Esparza
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 w1* … wn*. 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 stO(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.
- 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
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Javier Esparza. 1997. Petri nets, commutative context-free grammars, and basic parallel processes. Fundamenta Informaticae 31 (1997), 13--26. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Pierre Ganty, Rupak Majumdar, and Benjamin Monmege. 2012. Bounded underapproximations. Formal Methods Syst. Des. 40, 2 (2012), 206--231. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Seymour Ginsburg. 1966. The Mathematical Theory of Context-Free Languages. McGraw-Hill, New York, NY. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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
- 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. Google ScholarDigital Library
- John E. Hopcroft and Jeffrey D. Ullman. 1979. Introduction to Automata Theory, Languages and Computation (1st ed.). Addison-Wesley. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Vineet Kahlon. 2009b. Tractable Dataflow Analysis for Concurrent Programs via Bounded Languages. (July 2009). Patent WO/2009/094439.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Akash Lal and Thomas Reps. 2009. Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods Syst. Des., 1 (2009), 73--97. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Rohit J. Parikh. 1966. On context-free languages. J. ACM 13, 4 (1966), 570--581. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Ganesan Ramalingam. 2000. Context-sensitive synchronization-sensitive analysis is undecidable. ACM TOPLAS 22, 2 (2000), 416--430. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
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 languagesPattern-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 w1* ... wn*. For multithreaded programs, the alphabet of the pattern is ...
Complexity of pattern-based verification for multithreaded programs
POPL '11Pattern-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 w1* ... wn*. 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
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