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 w1* ... wn*. 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.
Supplemental Material
- CHESS: Find and reproduce heisenbugs in concurrent programs. URL http://research.microsoft.com/en-us/projects/CHESS/.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- J. Esparza. Petri nets, commutative context-free grammars, and basic parallel processes. Fundamenta Informaticae, 31:13--26, 1997. Google ScholarDigital Library
- J. Esparza, P. Ganty, S. Kiefer, and M. Luttenberger. Parikh's theorem: A simple and direct construction. CoRR, 1006.3825, 2010. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- M. R. Garey and D. S. Johnson. Computers and Intractability, A Guide to the Theory of NP-Completeness. New York, 1979. Google ScholarDigital Library
- S. Ginsburg and E. H. Spanier. Semigroups, presburger formulas, and languages. Pacific Journal of Mathematics, 16(2):285--296, 1966.Google ScholarCross Ref
- E. Graedel. Subclasses of presburger arithmetic and the polynomial time hierarchy. Theoretical Computer Science, 56(3):289--301, 1988. Google ScholarDigital Library
- J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1st edition, 1979. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- V. Kahlon. Tractable dataflow analysis for concurrent programs via bounded languages. Patent WO/2009/094439, July 2009.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- J. Lenstra, H. W. Integer programming with a fixed number of variables. Mathematics of Operations Research, 8(4):538--548, 1983.Google ScholarDigital Library
- R. J. Parikh. On context-free languages. Journal of the ACM, 13(4): 570--581, 1966. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- G. Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. ACM TOPLAS, 22(2):416--430, 2000. Google ScholarDigital Library
- B. Scarpellini. Complexity of subcases of presburger arithmetic. Trans. of the American Mathematical Society, 284(1):203--218, 1984.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- A. W. To. Parikh images of regular languages: Complexity and applications. CoRR, 1002.1464, 2010.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
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 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 ...
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 w1* … wn*. 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