skip to main content
article

Exploiting purity for atomicity

Published: 01 July 2004 Publication History

Abstract

The notion that certain procedures are atomic is a fundamental correctness property of many multithreaded software systems. A procedure is atomic if for every execution there is an equivalent serial execution in which the actions performed by any thread while executing the atomic procedure are not interleaved with actions of other threads. Several existing tools verify atomicity by using commutativity of actions to show that every execution reduces to a corresponding serial execution. However, experiments with these tools have highlighted a number of interesting procedures that, while intuitively atomic, are not reducible.In this paper, we exploit the notion of pure code blocks to verify the atomicity of such irreducible procedures. If a pure block terminates normally, then its evaluation does not change the program state, and hence these evaluation steps can be removed from the program trace before reduction. We develop a static analysis for atomicity based on this insight, and we illustrate this analysis on a number of interesting examples that could not be verified using earlier tools based purely on reduction. The techniques developed in this paper may also be applicable in other approaches for verifying atomicity, such as model checking and dynamic analysis.

References

[1]
M. P. Atkinson, K. J. Chisholm, and W. P. Cockshott. PS-Algol: an Algol with a persistent heap. ACM SIGPLAN Notices, 17(7):24--31, 1981.
[2]
M. P. Atkinson and D. Morrison. Procedures as persistent data objects. ACM Transactions on Programming Languages and Systems, 7(4):539--559, 1985.
[3]
R.-J. Back. A method for refining atomicity in parallel algorithms. In PARLE 89: Parallel Architectures and Languages Europe, volume 366 of Lecture Notes in Computer Science, pages 199--216. Springer-Verlag, 1989.
[4]
C. Boyapati and M. Rinard. A parameterized type system for race-free Java programs. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications, pages 56--69, 2001.
[5]
D. Bruening. Systematic testing of multithreaded Java programs. Master's thesis, Massachusetts Institute of Technology, 1999.
[6]
E. Cohen and L. Lamport. Reduction in TLA. In Proceedings of the International Conference on Concurrency Theory, volume 1466 of Lecture Notes in Computer Science, pages 317--331. Springer-Verlag, 1998.
[7]
X. Deng, M. Dwyer, J. Hatcliff, and M. Mizuno. Invariant-based specification, synthesis, and verification of synchronization in concurrent programs. In International Conference on Software Engineering, pages 442--452, 2002.
[8]
T. W. Doeppner, Jr. Parallel program correctness through refinement. In Proceedings of the ACM Symposium on the Principles of Programming Languages, pages 155--169, 1977.
[9]
J. L. Eppinger, L. B. Mummert, and A. Z. Spector. Camelot and Avalon: A Distributed Transaction Facility. Morgan Kaufmann, 1991.
[10]
C. Flanagan. Verifying commit-atomicity using model-checking. In SPIN 2004: 11th International SPIN Workshop on Model Checking of Software, pages 252--266, 2004.
[11]
C. Flanagan and S. N. Freund. Type-based race detection for Java. In Proceedings of the ACMConference on Programming Language Design and Implementation, pages 219--232, 2000.
[12]
C. Flanagan and S. N. Freund. Atomizer: A dynamic atomicity checker for multithreaded programs. In Proceedings of the ACM Symposium on the Principles of Programming Languages, pages 256--267, 2004.
[13]
C. Flanagan, S. N. Freund, and S. Qadeer. Exploiting purity for atomicity. Technical Note 04-02, Williams College, 2004.
[14]
C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In Proceedings of the ACM Conference on Programming Language Design and Implementation, pages 234--245, 2002.
[15]
C. Flanagan and S. Qadeer. Transactions for software model checking. In Proceedings of the Workshop on Software Model Checking, 2003.
[16]
C. Flanagan and S. Qadeer. A type and effect system for atomicity. In Proceedings of the ACMConference on Programming Language Design and Implementation, pages 338--349, 2003.
[17]
C. Flanagan and S. Qadeer. Types for atomicity. In Proceedings of the ACM Workshop on Types in Language Design and Implementation, pages 1--12, 2003.
[18]
S. N. Freund and S. Qadeer. Checking concise specifications for multithreaded software. In Journal of Object Technology, 2004. (to appear). A preliminary version appeared in Workshop on Formal Techniques for Java-like Programs, 2003.
[19]
P. Godefroid. Using partial orders to improve automatic verification methods. In Proceedings of the IEEE Conference on Computer Aided Verification, pages 176--185, 1991.
[20]
D. Grossman. Type-safe multithreading in Cyclone. In Proceedings of the ACM Workshop on Types in Language Design and Implementation, pages 13--25, 2003.
[21]
T. L. Harris and K. Fraser. Language support for lightweight transactions. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications, pages 388--402, 2003.
[22]
J. Hatcliff, Robby, and M. B. Dwyer. Verifying atomicity specifications for concurrent object-oriented software using model-checking. In Proceedings of the International Conference on Verification, Model Checking and Abstract Interpretation, pages 175--190, 2004.
[23]
M. P. Herlihy and J. M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems, 12(3):463--492, 1990.
[24]
C. A. R. Hoare. Towards a theory of parallel programming. In Operating Systems Techniques, volume 9 of A.P.I.C. Studies in Data Processing, pages 61--71. Academic Press, 1972.
[25]
L. Lamport and F. B. Schneider. Pretending atomicity. Research Report 44, DEC Systems Research Center, 1989.
[26]
R. J. Lipton. Reduction: A method of proving properties of parallel programs. Communications of the ACM, 18(12):717--721, 1975.
[27]
B. Liskov, D. Curtis, P. Johnson, and R. Scheifler. Implementation of Argus. In Proceedings of the Symposium on Operating Systems Principles, pages 111--122, 1987.
[28]
D. B. Lomet. Process structuring, synchronization, and recovery using atomic actions. Language Design for Reliable Software, pages 128--137, 1977.
[29]
J. Misra. A Discipline of Multiprogramming: Programming Theory for Distributed Applications. Springer-Verlag, 2001.
[30]
F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer, 1999.
[31]
C. Papadimitriou. The theory of database concurrency control. Computer Science Press, 1986.
[32]
D. Peled. Combining partial order reductions with on-the-fly model checking. In D. Dill, editor, CAV 94: Computer Aided Verification, Lecture Notes in Computer Science 818, pages 377--390. Springer-Verlag, 1994.
[33]
S. Qadeer, S. K. Rajamani, and J. Rehof. Summarizing procedures in concurrent programs. In Proceedings of the ACM Symposium on the Principles of Programming Languages, pages 245--255, 2004.
[34]
Robby, E. Rodriguez, M. B. Dwyer, and J. Hatcliff. Checking strong specifications using an extensible software model checking framework. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 404--420, 2004.
[35]
D. C. Schmidt and T. H. Harrison. Double-checked locking - a optimization pattern for efficiently initializing and accessing thread-safe objects. In R. Martin, F. Buschmann, and D. Riehle, editors, Pattern Languages of Program Design 3. Addison-Wesley, 1997.
[36]
N. Sterling. WARLOCK -- a static data race analysis tool. In USENIX Technical Conference Proceedings, pages 97--106, Winter 1993.
[37]
S. D. Stoller. Model-checking multi-threaded distributed Java programs. In Workshop on Model Checking and Software Verification, pages 224--244, 2000.
[38]
L. Wang and S. D. Stoller. Run-time analysis for atomicity. In Proceedings of the Workshop on Runtime Verification, volume 89(2) of Electronic Notes in Computer Science. Elsevier, 2003.
[39]
A. Welc, S. Jagannathan, and A. L. Hosking. Transactional monitors for concurrent objects. In Proceedings of the 18th European Conference on Object-Oriented Programming, 2004.

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGSOFT Software Engineering Notes
ACM SIGSOFT Software Engineering Notes  Volume 29, Issue 4
July 2004
284 pages
ISSN:0163-5948
DOI:10.1145/1013886
Issue’s Table of Contents
  • cover image ACM Conferences
    ISSTA '04: Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis
    July 2004
    294 pages
    ISBN:1581138202
    DOI:10.1145/1007512
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: 01 July 2004
Published in SIGSOFT Volume 29, Issue 4

Check for updates

Author Tags

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

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)1
  • Downloads (Last 6 weeks)0
Reflects downloads up to 22 Feb 2025

Other Metrics

Citations

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media