Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Pattern-based verification for multithreaded programs
Esparza J., Ganty P., Poch T. ACM Transactions on Programming Languages and Systems36 (3):1-29,2014.Type:Article
Date Reviewed: Nov 19 2014

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.

Reviewer:  Markus Wolf Review #: CR142953 (1502-0157)
Bookmark and Share
 
Software/ Program Verification (D.2.4 )
 
Would you recommend this review?
yes
no
Other reviews under "Software/Program Verification": Date
Verification of sequential and concurrent programs
Krzysztof R., Olderog E., Springer-Verlag New York, Inc., New York, NY, 1991. Type: Book (9780387975320)
Jul 1 1992
On verification of programs with goto statements
Lifschitz V. (ed) Information Processing Letters 18(4): 221-225, 1984. Type: Article
Mar 1 1985
The validation, verification and testing of software
Ince D. (ed), Oxford University Press, Inc., New York, NY, 1985. Type: Book (9789780198590040)
Sep 1 1987
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy