skip to main content
research-article

Complexity of pattern-based verification for multithreaded programs

Published:26 January 2011Publication History
Skip Abstract Section

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.

Skip Supplemental Material Section

Supplemental Material

46-mpeg-4.mp4

References

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

Index Terms

  1. Complexity of pattern-based verification for multithreaded programs

            Recommendations

            Comments

            Login options

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

            Sign in

            Full Access

            • 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
              • 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

              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

              Check for updates

              Qualifiers

              • research-article

            PDF Format

            View or Download as a PDF file.

            PDF

            eReader

            View online with eReader.

            eReader