Abstract
Pthread-style multithreaded programs feature rich thread communication mechanisms, such as shared variables, signals, and broadcasts. In this article, we consider the automated verification of such programs where an unknown number of threads execute a given finite-data procedure in parallel. Such procedures are typically obtained as predicate abstractions of recursion-free source code written in C or Java. Many safety problems over finite-data replicated multithreaded programs are decidable via a reduction to the coverability problem in certain types of well-ordered infinite-state transition systems. On the other hand, in full generality, this problem is Ackermann-hard, which seems to rule out efficient algorithmic treatment.
We present a novel, sound, and complete yet empirically efficient solution. Our approach is to judiciously widen the original set of coverability targets by configurations that involve fewer threads and are thus easier to decide, and whose exploration may well be sufficient: if they turn out uncoverable, so are the original targets. To soften the impact of “bad guesses”—configurations that turn out coverable—the exploration is accompanied by a parallel engine that generates coverable configurations; none of these is ever selected for widening. Its job being merely to prevent bad widening choices, such an engine need not be complete for coverability analysis, which enables a range of existing partial (e.g., nonterminating) techniques. We present extensive experiments on multithreaded C programs, including device driver code from FreeBSD, Solaris, and Linux distributions. Our approach outperforms existing coverability methods by orders of magnitude.
- P. A. Abdulla. 2010. Well (and better) quasi-ordered transition systems. Bulletin of Symbolic Logic 16, 4, 457--515.Google ScholarCross Ref
- P. A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay. 1996. General decidability theorems for infinite-state systems. In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS’96). 313--321. Google ScholarDigital Library
- P. A. Abdulla, F. Haziza, and L. Holík. 2013. All for the price of few. In Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, Vol. 7737. Springer, 476--495.Google Scholar
- P. A. Abdulla, S. P. Iyer, and A. Nylén. 2004. SAT-solving the coverability problem for Petri nets. Formal Methods in System Design 24, 1, 25--43. Google ScholarDigital Library
- G. Basler, M. Mazzucchi, T. Wahl, and D. Kroening. 2009. Symbolic counter abstraction for concurrent software. In Proceedings of the 21st International Conference on Computer Aided Verification (CAV’09). 64--78. Google ScholarDigital Library
- B. Berthomieu and F. Vernadat. 2009. The Tina Tool, Release 2.9.6, LAAS/CNRS. Retrieved September 4, 2014, from http://projects.laas.fr/tina.Google Scholar
- E. Cardoza, R. J. Lipton, and A. R. Meyer. 1976. Exponential space complete problems for Petri nets and commutative semigroups: Preliminary report. In Proceedings of the 8th Annual ACM Symposium on Theory of Computing (STOC’76). 50--54. Google ScholarDigital Library
- G. Ciardo. 1994. Petri nets with marking-dependent arc cardinality: Properties and analysis. In Application and Theory of Petri Nets. Lecture Notes in Computer Science, Vol. 815. 179--198. Google ScholarDigital Library
- G. Delzanno, J.-F. Raskin, and L. V. Begin. 2002. Towards the automated verification of multithreaded Java programs. In Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’02). 173--187. Google ScholarDigital Library
- A. F. Donaldson, A. Kaiser, D. Kroening, M. Tautschnig, and T. Wahl. 2012. Counterexample-guided abstraction refinement for symmetric concurrent programs. Formal Methods in System Design 41, 1, 25--44. Google ScholarDigital Library
- A. F. Donaldson, A. Kaiser, D. Kroening, and T. Wahl. 2011. Symmetry-aware predicate abstraction for shared-variable concurrent programs. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV’11). 356--371. Google ScholarDigital Library
- C. Dufourd, A. Finkel, and P. Schnoebelen. 1998. Reset nets between decidability and undecidability. In Proceedings of the 25th International Colloquium on Automata, Languages, and Programming (ICALP’98). 103--115. Google ScholarDigital Library
- A. Eliëns and E. P. de Vink. 1992. Asynchronous rendez-vous in distributed logic programming. In Proceedings of the REX Workshop on Semantics: Foundations and Applications. 174--203. Google ScholarDigital Library
- E. A. Emerson and K. S. Namjoshi. 1998. On model checking for non-deterministic infinite-state systems. In Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS’98). 70--80. Google ScholarDigital Library
- J. Esparza, A. Finkel, and R. Mayr. 1999. On the verification of broadcast protocols. In Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS’99). 352--359. Google ScholarDigital Library
- A. Farzan and Z. Kincaid. 2012. Verification of parameterized concurrent programs by modular reasoning about data and control. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’12). 297--308. Google ScholarDigital Library
- A. Farzan, Z. Kincaid, and A. Podelski. 2013. Inductive data flow graphs. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’13). 129--142. Google ScholarDigital Library
- D. Figueira, S. Figueira, S. Schmitz, and P. Schnoebelen. 2011. Ackermannian and primitive-recursive bounds with Dickson’s lemma. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS’11). 269--278. Google ScholarDigital Library
- A. Finkel, G. Geeraerts, J.-F. Raskin, and L. V. Begin. 2006. On the omega-language expressive power of extended Petri nets. Theoretical Computer Science 356, 3, 374--386. Google ScholarDigital Library
- A. Finkel and J. Goubault-Larrecq. 2009. Forward analysis for WSTS, part II: Complete WSTS. In Automata, Languages, and Programming. Lecture Notes in Computer Science, Vol. 2009. Springer, 188--199. Google ScholarDigital Library
- A. Finkel, J.-F. Raskin, M. Samuelides, and L. V. Begin. 2002. Monotonic extensions of Petri nets: Forward and backward search revisited. Electronic Notes in Theoretical Computer Science 68, 6, 85--106.Google ScholarCross Ref
- A. Finkel and P. Schnoebelen. 2001. Well-structured transition systems everywhere! Theoretical Computer Science 256, 1--2, 63--92. Google ScholarDigital Library
- C. Flanagan and S. Qadeer. 2003. Thread-modular model checking. In Proceedings of the 10th International Conference on Model Checking Software (SPIN’03). 213--224. Google ScholarDigital Library
- P. Ganty, L. V. Begin, and A. Piron. n.d. The MIST2 Tool (Version 0.1). Retrieved September 4, 2014, from https://github.com/pierreganty/mist.Google Scholar
- P. Ganty, G. Geeraerts, J.-F. Raskin, and L. V. Begin. 2009. Le problème de couverture pour les réseaux de Petri: Résultats classiques et développements récents. Technique et Science Informatiques 28, 9, 1107--1142.Google ScholarCross Ref
- P. Ganty, C. Meuter, G. Delzanno, G. Kalyon, J.-F. Raskin, and L. Van Begin. 2007. Symbolic data structure for sets of k-uples. Technical Report. Université Libre de Bruxelles, Belgium.Google Scholar
- P. Ganty, J.-F. Raskin, and L. V. Begin. 2006. A complete abstract interpretation framework for coverability properties of WSTS. In Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’06). 49--64. Google ScholarDigital Library
- G. Geeraerts, J.-F. Raskin, and L. V. Begin. 2006. Expand, enlarge and check: New algorithms for the coverability problem of WSTS. Journal of Computer and Systems Sciences 72, 1, 180--203. Google ScholarDigital Library
- G. Geeraerts, J.-F. Raskin, and L. V. Begin. 2007. On the efficient computation of the minimal coverability set for Petri nets. In Proceedings of the 5th International Conference on Automated Technology for Verification and Analysis (ATVA’07). 98--113. Google ScholarDigital Library
- S. M. German and A. P. Sistla. 1992. Reasoning about systems with many processes. Journal of the ACM 39, 3, 675--735. Google ScholarDigital Library
- B. Goetz, T. Peierls, J. Bloch, J. Bowbeer, D. Holmes, and D. Lea. 2006. Java Concurrency in Practice. Addison-Wesley. Google ScholarDigital Library
- A. Gupta, C. Popeea, and A. Rybalchenko. 2011a. Predicate abstraction and refinement for verifying multi-threaded programs. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’11). 331--344. Google ScholarDigital Library
- A. Gupta, C. Popeea, and A. Rybalchenko. 2011b. Threader: A constraint-based verifier for multi-threaded programs. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV’11). 412--417. Google ScholarDigital Library
- C. B. Jones. 1983. Tentative steps toward a development method for interfering programs. ACM Transactions on Programming Languages and Systems 5, 4, 596--619. Google ScholarDigital Library
- A. Kaiser, D. Kroening, and T. Wahl. 2010. Dynamic cutoff detection in parameterized concurrent programs. In Proceedings of the 22nd International Conference on Computer Aided Verification (CAV’10). 645--659. Google ScholarDigital Library
- R. M. Karp and R. E. Miller. 1969. Parallel program schemata. Journal of Computer and System Sciences 3, 2, 147--195. Google ScholarDigital Library
- J. Kloos, R. Majumdar, F. Niksic, and R. Piskac. 2013. Incremental, inductive coverability. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV’13). 158--173. Google ScholarDigital Library
- M. Leuschel and H. Lehmann. 2000. Coverability of reset Petri nets and other well-structured transition systems by partial deduction. In Computational Logic—CL 2000. Lecture Notes in Computer Science, Vol. 1861. Springer, 101--115. Google ScholarDigital Library
- S. Lu, S. Park, E. Seo, and Y. Zhou. 2008. Learning from mistakes: A comprehensive study on real world concurrency bug characteristics. In Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS XIII). 329--339. Google ScholarDigital Library
- R. Meyer and T. Strazny. 2010. Petruchio: From dynamic networks to nets. In Proceedings of the 22nd International Conference on Computer Aided Verification (CAV’10). 175--179. Google ScholarDigital Library
- S. S. Owicki. 1975. Axiomatic Proof Techniques for Parallel Programs. Outstanding Dissertations in the Computer Sciences. Garland Publishing, New York, NY. Google ScholarDigital Library
- A. Pnueli, J. Xu, and L. D. Zuck. 2002. Liveness with (0,1,∞ )-counter abstraction. In Proceedings of the 14th International Conference on Computer Aided Verification (CAV’02). 107--122. Google ScholarDigital Library
- C. Rackoff. 1978. The covering and boundedness problems for vector addition systems. Theoretical Computer Science 6, 223--231.Google ScholarCross Ref
- P.-A. Reynier and F. Servais. 2011. Minimal coverability set for Petri nets: Karp and Miller algorithm with pruning. In Applications and Theory of Petri Nets. Lecture Notes in Computer Science, Vol. 6709. Springer, 69--88. Google ScholarDigital Library
- P. Schnoebelen. 2010. Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets. In Proceedings of the 35th International Conference on Mathematical Foundations of Computer Science (MFCS’10). 616--628. Google ScholarDigital Library
- A. Valmari and H. Hansen. 2012. Old and new algorithms for minimal coverability sets. In Application and Theory of Petri Nets. Lecture Notes in Computer Science, Vol. 7347. Springer, 208--227. Google ScholarDigital Library
- D. Zufferey, T. Wies, and T. A. Henzinger. 2012. Ideal abstractions for well-structured transition systems. In Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’12). 445--460. Google ScholarDigital Library
Index Terms
- A Widening Approach to Multithreaded Program Verification
Recommendations
Parameterized verification of monotone information systems
AbstractIn this paper, we study the information system verification problem as a parameterized verification one. Informations systems are modeled as multi-parameterized systems in a formal language based on the Algebraic State-Transition Diagrams (ASTD) ...
Specifying multithreaded Java semantics for program verification
ICSE '02: Proceedings of the 24th International Conference on Software EngineeringThe Java programming language supports multithreading where the threads interact among themselves via read/write of shared data. Most current work on multithreaded Java program verification assumes a model of execution that is based on interleaving of ...
Modular verification of multithreaded programs
Multithreaded software systems are prone to errors due to the difficulty of reasoning about multiple interleaved threads operating on shared data. Static checkers that analyze a program's behavior over all execution paths and all thread interleavings ...
Comments