skip to main content
research-article

A calculus of atomic actions

Published: 21 January 2009 Publication History

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]
S. Brookes. A semantics for concurrent separation logic. Theor. Comput. Sci., 375(1-3):227--270, 2007.
[4]
J. W. Coleman and C. B. Jones. Guaranteeing the soundness of rely/guarantee rules. Journal of Logic and Computation, 17(4):807--841, 2007.
[5]
F. S. de Boer, U. Hannemann, and W.-P. de Roever. A compositional proof system for shared variable concurrency. In FME'97: 4th International Symposium of Formal Methods Europe, volume 1313, pages 515--532. Springer-Verlag, 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]
E. W. Dijkstra. A Discipline of Programming. Prentice Hall PTR, Upper Saddle River, NJ, USA, 1997.
[8]
T. Elmas, S. Qadeer, and S. Tasiran. A calculus of atomic actions. Technical Report MSR-TR-2008-99, Microsoft Research, 2008.
[9]
T. Elmas, S. Tasiran, and S. Qadeer. VYRD: Verifying concurrent programs by runtime refinement-violation detection. In PLDI '05: Proceedings of the 2005 ACM SIGPLAN conference on Programming Language Design and Implementation, pages 27--37, New York, NY, USA, 2005. ACM Press.
[10]
C. Flanagan, S. N. Freund, and S. Qadeer. Exploiting purity for atomicity. IEEE Trans. Softw. Eng., 31(4):275--291, 2005.
[11]
C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In PLDI '02: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, pages 234--245, New York, NY, USA, 2002. ACM Press.
[12]
C. Flanagan and S. Qadeer. Types for atomicity. In TLDI '03: Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Language Design and Implementation, pages 1--12, New York, NY, USA, 2003. ACM.
[13]
S. Freund and S. Qadeer. Checking concise specifications for multithreaded software. Journal of Object Technology, 3(6):81--101, 2004.
[14]
M. Herlihy, V. Luchangco, and M. Moir. Obstruction-free synchronization: Double-ended queues as an example. In ICDCS '03: Proceedings of the 23rd International Conference on Distributed Computing Systems, pages 522--529, Washington, DC, USA, 2003. IEEE Computer Society.
[15]
B. Jacobs, J. Smans, F. Piessens, and W. Schulte. A simple sequential reasoning approach for sound modular verification of mainstream multithreaded programs. Electron. Notes Theor. Comput. Sci., 174(9):23--47, 2007.
[16]
C. B. Jones. Development Methods for Computer Programs including a Notion of Interference. PhD thesis, Oxford University, June 1981.
[17]
L. Lamport. A new solution of Dijkstra's concurrent programming problem. Commun. ACM, 17(8):453--455, 1974.
[18]
R. J. Lipton. Reduction: a method of proving properties of parallel programs. Commun. ACM, 18(12):717--721, 1975.
[19]
M. M. Michael. Hazard pointers: Safe memory reclamation for lock-free objects. IEEE Trans. Parallel Distrib. Syst., 15(6):491--504, 2004.
[20]
P. W. O'Hearn, H. Yang, and J. C. Reynolds. Separation and information hiding. In POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 268--280, New York, NY, USA, 2004. ACM.
[21]
S. Owicki and D. Gries. Verifying properties of parallel programs: an axiomatic approach. Commun. ACM, 19(5):279--285, 1976.
[22]
M. Parkinson, R. Bornat, and P. O'Hearn. Modular verification of a non-blocking stack. SIGPLAN Not., 42(1):297--302, 2007.
[23]
L. Wang and S. D. Stoller. Static analysis for programs with non-blocking synchronization. In PPoPP '05: Proceedings of the ACM SIGPLAN 2005 Symposium on Principles and Practice of Parallel Programming, pages 61--71. ACM Press, June 2005.
[24]
L. Wang and S. D. Stoller. Runtime analysis of atomicity for multi-threaded programs. IEEE Transactions on Software Engineering, 32:93--110, Feb. 2006.
[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.

Cited By

View all
  • (2023)Smart Contract Parallel Execution with Fine-Grained State Accesses2023 IEEE 43rd International Conference on Distributed Computing Systems (ICDCS)10.1109/ICDCS57875.2023.00068(841-852)Online publication date: Jul-2023
  • (2022)Armada: Automated Verification of Concurrent Code with Sound Semantic ExtensibilityACM Transactions on Programming Languages and Systems10.1145/350249144:2(1-39)Online publication date: 27-May-2022
  • (2022)Software & System Verification with KIVThe Logic of Software. A Tasting Menu of Formal Methods10.1007/978-3-031-08166-8_20(408-436)Online publication date: 4-Jul-2022
  • Show More Cited By

Recommendations

Reviews

Ramesh S

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. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 44, Issue 1
POPL '09
January 2009
453 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1594834
Issue’s Table of Contents
  • cover image ACM Conferences
    POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
    January 2009
    464 pages
    ISBN:9781605583792
    DOI:10.1145/1480881
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: 21 January 2009
Published in SIGPLAN Volume 44, Issue 1

Check for updates

Author Tags

  1. abstraction
  2. atomicity
  3. concurrent programs
  4. reduction

Qualifiers

  • Research-article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)28
  • Downloads (Last 6 weeks)0
Reflects downloads up to 09 Jan 2025

Other Metrics

Citations

Cited By

View all
  • (2023)Smart Contract Parallel Execution with Fine-Grained State Accesses2023 IEEE 43rd International Conference on Distributed Computing Systems (ICDCS)10.1109/ICDCS57875.2023.00068(841-852)Online publication date: Jul-2023
  • (2022)Armada: Automated Verification of Concurrent Code with Sound Semantic ExtensibilityACM Transactions on Programming Languages and Systems10.1145/350249144:2(1-39)Online publication date: 27-May-2022
  • (2022)Software & System Verification with KIVThe Logic of Software. A Tasting Menu of Formal Methods10.1007/978-3-031-08166-8_20(408-436)Online publication date: 4-Jul-2022
  • (2021)Flashix: Modular Verification of a Concurrent and Crash-Safe Flash File SystemLogic, Computation and Rigorous Methods10.1007/978-3-030-76020-5_14(239-265)Online publication date: 4-Jun-2021
  • (2020)Armada: low-effort verification of high-performance concurrent programsProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3385412.3385971(197-210)Online publication date: 11-Jun-2020
  • (2020)Adding Concurrency to a Sequential Refinement TowerRigorous State-Based Methods10.1007/978-3-030-48077-6_2(6-23)Online publication date: 22-May-2020
  • (2019)Reductions for safety proofsProceedings of the ACM on Programming Languages10.1145/33710814:POPL(1-28)Online publication date: 20-Dec-2019
  • (2019)Pretend synchrony: synchronous verification of asynchronous distributed programsProceedings of the ACM on Programming Languages10.1145/32903723:POPL(1-30)Online publication date: 2-Jan-2019
  • (2019)A mechanized refinement proof of the Chase---Lev deque using a proof systemComputing10.1007/s00607-018-0635-4101:1(59-74)Online publication date: 1-Jan-2019
  • (2019)Automated Hypersafety VerificationComputer Aided Verification10.1007/978-3-030-25540-4_11(200-218)Online publication date: 12-Jul-2019
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media