Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

We present a proof calculus and method for the static verification of assertions and procedure specifications in shared-memory concurrent programs. The key idea in our approach is to use atomicity as a proof tool and to simplify the verification of assertions by rewriting programs to consist of larger atomic actions. We propose a novel, iterative proof style in which alternating use of abstraction and reduction is exploited to compute larger atomic code blocks in a sound manner. This makes possible the verification of assertions in the transformed program by simple sequential reasoning within atomic blocks, or significantly simplified application of existing concurrent program verification techniques such as the Owicki-Gries or rely-guarantee methods. Our method facilitates a clean separation of concerns where at each phase of the proof, the user worries only about only either the sequential properties or the concurrency control mechanisms in the program. We implemented our method in a tool called QED. We demonstrate the simplicity and effectiveness of our approach on a number of benchmarks including ones with intricate concurrency protocols.

REFERENCES

• 1: E. A. Ashcroft. Proving assertions about parallel programs. J. Comput. Syst. Sci., 10(1):110--135, 1975.
• 2: M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino. Boogie: A modular reusable verifier for object-oriented programs. FMCO '05: 4th International Symposium on Formal Methods for Components and Objects, pages 364--387, 2005.
• 3: Stephen Brookes, A semantics for concurrent separation logic, Theoretical Computer Science, v.375 n.1-3, p.227-270, April, 2007 [doi>10.1016/j.tcs.2006.12.034]
• 4: Joey W. Coleman , Cliff B. Jones, A Structural Proof of the Soundness of Rely/guarantee Rules, Journal of Logic and Computation, v.17 n.4, p.807-841, August 2007 [doi>10.1093/logcom/exm030]
• 5: Frank S. de Boer , Ulrich Hannemann , Willem P. de Roever, A Compositional Proof System for Shared Variable Concurrency, Proceedings of the 4th International Symposium of Formal Methods Europe on Industrial Applications and Strengthened Foundations of Formal Methods, p.515-532, September 15-19, 1997
• 6: L. M. de Moura and N. Björner. Z3: An efficient SMT solver. In TACAS '08: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 4963 of Lecture Notes in Computer Science, pages 337--340. Springer, 2008.
• 7: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 8: T. Elmas, S. Qadeer, and S. Tasiran. A calculus of atomic actions. Technical Report MSR-TR-2008-99, Microsoft Research, 2008.
• 9: Tayfun Elmas , Serdar Tasiran , Shaz Qadeer, VYRD: verifYing concurrent programs by runtime refinement-violation detection, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 10: Cormac Flanagan , Stephen N. Freund , Shaz Qadeer, Exploiting Purity for Atomicity, IEEE Transactions on Software Engineering, v.31 n.4, p.275-291, April 2005 [doi>10.1109/TSE.2005.47]
• 11: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 12: Cormac Flanagan , Shaz Qadeer, Types for atomicity, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 13: S. Freund and S. Qadeer. Checking concise specifications for multithreaded software. Journal of Object Technology, 3(6):81--101, 2004.
• 14: Maurice Herlihy , Victor Luchangco , Mark Moir, Obstruction-Free Synchronization: Double-Ended Queues as an Example, Proceedings of the 23rd International Conference on Distributed Computing Systems, p.522, May 19-22, 2003
• 15: Bart Jacobs , Jan Smans , Frank Piessens , Wolfram Schulte, A Simple Sequential Reasoning Approach for Sound Modular Verification of Mainstream Multithreaded Programs, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.9, p.23-47, June, 2007 [doi>10.1016/j.entcs.2007.04.005]
• 16: C. B. Jones. Development Methods for Computer Programs including a Notion of Interference. PhD thesis, Oxford University, June 1981.
• 17: Leslie Lamport, A new solution of Dijkstra's concurrent programming problem, Communications of the ACM, v.17 n.8, p.453-455, Aug. 1974 [doi>10.1145/361082.361093]
• 18: Richard J. Lipton, Reduction: a method of proving properties of parallel programs, Communications of the ACM, v.18 n.12, p.717-721, Dec. 1975 [doi>10.1145/361227.361234]
• 19: Maged M. Michael, Hazard Pointers: Safe Memory Reclamation for Lock-Free Objects, IEEE Transactions on Parallel and Distributed Systems, v.15 n.6, p.491-504, June 2004 [doi>10.1109/TPDS.2004.8]
• 20: Peter W. O'Hearn , Hongseok Yang , John C. Reynolds, Separation and information hiding, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.268-280, January 14-16, 2004, Venice, Italy
• 21: Susan Owicki , David Gries, Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, v.19 n.5, p.279-285, May 1976 [doi>10.1145/360051.360224]
• 22: Matthew Parkinson , Richard Bornat , Peter O'Hearn, Modular verification of a non-blocking stack, ACM SIGPLAN Notices, v.42 n.1, January 2007
• 23: Liqiang Wang , Scott D. Stoller, Static analysis of atomicity for programs with non-blocking synchronization, Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 15-17, 2005, Chicago, IL, USA [doi>10.1145/1065944.1065953]
• 24: Liqiang Wang , Scott D. Stoller, Runtime Analysis of Atomicity for Multithreaded Programs, IEEE Transactions on Software Engineering, v.32 n.2, p.93-110, February 2006 [doi>10.1109/TSE.2006.1599419]
• 25: Q. Xu, W. P. de Roever, and J. He. The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing, 9(2):149--174, 1997.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Assertion checkers

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming
          Subjects: Parallel programming
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods; Correctness proofs

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification; Invariants; Pre- and post-conditions; Assertions

General Terms:
Languages, Theory, Verification

Keywords:
abstraction, atomicity, concurrent programs, reduction