skip to main content
10.1145/1007512.1007543acmconferencesArticle/Chapter ViewAbstractPublication PagesisstaConference Proceedingsconference-collections
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.

Cited By

View all
  • (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
  • (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)Atomicity Checking in Linear Time using Vector ClocksProceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3373376.3378475(183-199)Online publication date: 9-Mar-2020
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

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
  • 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
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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 July 2004

Permissions

Request permissions for this article.

Check for updates

Author Tags

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

Qualifiers

  • Article

Conference

ISSTA04
Sponsor:

Acceptance Rates

Overall Acceptance Rate 58 of 213 submissions, 27%

Upcoming Conference

ISSTA '25

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

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

Other Metrics

Citations

Cited By

View all
  • (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
  • (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)Atomicity Checking in Linear Time using Vector ClocksProceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3373376.3378475(183-199)Online publication date: 9-Mar-2020
  • (2018)VerifiedFTACM SIGPLAN Notices10.1145/3200691.317851453:1(354-367)Online publication date: 10-Feb-2018
  • (2018)VerifiedFTProceedings of the 23rd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming10.1145/3178487.3178514(354-367)Online publication date: 10-Feb-2018
  • (2011)JPure:Proceedings of the 20th international conference on Compiler construction: part of the joint European conferences on theory and practice of software10.5555/1987237.1987247(104-123)Online publication date: 26-Mar-2011
  • (2011)NDSeqProceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/1993498.1993545(401-414)Online publication date: 4-Jun-2011
  • (2011)NDSeqACM SIGPLAN Notices10.1145/1993316.199354546:6(401-414)Online publication date: 4-Jun-2011
  • (2011)JPure: A Modular Purity System for JavaCompiler Construction10.1007/978-3-642-19861-8_7(104-123)Online publication date: 2011
  • (2006)Types for safe lockingACM Transactions on Programming Languages and Systems10.1145/1119479.111948028:2(207-255)Online publication date: 1-Mar-2006
  • 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

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media