Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
A calculus of atomic actions
Elmas T., Qadeer S., Tasiran S.  POPL 2009 (Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Savannah, GA, Jan 21-23, 2009)2-15.2008.Type:Proceedings
Date Reviewed: Mar 16 2009

Verification of partial correctness of shared-variable parallel programs is a very old subject. Nearly 35 years ago, Owicki and Gries proposed the first axiomatization of partial verification of parallel programs, using Hoare-style logic [1]. This and subsequent proposals to prove parallel program correctness brought out the complexity involved in proving parallel programs. All these proposals show that the correctness proofs require not only proof of correctness of sequential threads, but also proof of noninterference of the assertions used in the sequential proofs or the use of global invariants. Noninterference freedom proofs and global invariants are more difficult, which is probably why parallel program correctness is an academic exercise, restricted to a small class of interesting and well-known parallel programs.

With the recent significant advances in constraint solving and the emergence of powerful satisfiability modulo theories (SMT) solvers, this paper attempts to automate the age-old problem of partial correctness of multithreaded programs. The authors propose a new proof technique that cleverly combines the classical strategy of reduction with a relatively new abstraction technique. This technique can be iteratively applied to convert a fine-grained concurrent program into an almost sequential program that can then be easily proved. The proof technique is implemented in a tool called QED; QED provides a number of handy tactics for reducing the parallel programs to a set of constraints that are then solved using the state-of-the-art SMT solver Z3. The authors evaluated the tool on a number of small- to medium-sized multithreaded programs.

The paper is well written, has an illustrative introduction to the proposed methodology, and uses an interesting and nontrivial program. Examples are also given to explain the proposed method in further detail. The proof rules and tactic-based proof method are also explained well. In spite of the rich set of examples, the paper is so dense with technical material that beginners will initially have difficulty understanding it.

It is interesting to note that the verification technique proposed in this paper is in direct contrast to the correct-by-construction approach suggested several years ago for developing correct parallel programs; in the correct-by-construction approach, parallel programs are derived from coarse-grained programs, in a number of well-defined steps, using a set of correctness-preserving refinement rules.

Reviewer:  S. Ramesh Review #: CR136592 (1008-0812)
1) Owicki, S.; Gries, D. An axiomatic proof technique for parallel programs I. Acta lnformatica 6, (1976), 319–340.
Bookmark and Share
  Featured Reviewer  
 
Assertion Checkers (D.2.4 ... )
 
 
Correctness Proofs (D.2.4 ... )
 
 
Parallel Programming (D.1.3 ... )
 
 
Pre- And Post-Conditions (F.3.1 ... )
 
 
Concurrent Programming (D.1.3 )
 
 
Software/ Program Verification (D.2.4 )
 
Would you recommend this review?
yes
no
Other reviews under "Assertion Checkers": Date
Disjunctive program analysis for algebraic data types
Jensen T. ACM Transactions on Programming Languages and Systems 19(5): 751-803, 1997. Type: Article
Jun 1 1998
Efficient and effective array bound checking
Nguyen T., Irigoin F. ACM Transactions on Programming Languages and Systems 27(3): 527-570, 2005. Type: Article
Sep 2 2005
Improving application security with data flow assertions
Yip A., Wang X., Zeldovich N., Kaashoek M.  SOSP 2009 (Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, Big Sky, MT, Oct 11-14, 2009)291-304, 2009. Type: Proceedings
Jan 18 2010
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, Inc.®
Terms of Use
| Privacy Policy