Exploiting purity for atomicity

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: Malcolm Atkinson , Ken Chisholm , Paul Cockshott, PS-algol: an algol with a persistent heap, ACM SIGPLAN Notices, v.17 n.7, July 1982 [doi>10.1145/988376.988378]
• 2: Malcolm P. Atkinson , Ronald Morrison, Procedures as persistent data objects, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.4, p.539-559, Oct. 1985 [doi>10.1145/4472.4477]
• 3: Ralph-Johan Back, A Method for Refining Atomicity in Parallel Algorithms, Proceedings of the Parallel Architectures and Languages Europe, Volume II: Parallel Languages, p.199-216, June 12-16, 1989
• 4: Chandrasekhar Boyapati , Martin Rinard, A parameterized type system for race-free Java programs, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.56-69, October 14-18, 2001, Tampa Bay, FL, USA
• 5: D. Bruening. Systematic testing of multithreaded Java programs. Master's thesis, Massachusetts Institute of Technology, 1999.
• 6: Ernie Cohen , Leslie Lamport, Reduction in TLA, Proceedings of the 9th International Conference on Concurrency Theory, p.317-331, September 08-11, 1998
• 7: Xianghua Deng , Matthew B. Dwyer , John Hatcliff , Masaaki Mizuno, Invariant-based specification, synthesis, and verification of synchronization in concurrent programs, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581394]
• 8: Thomas W. Doeppner, Jr., Parallel program correctness through refinement, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.155-169, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512965]
• 9: Jeffrey L. Eppinger , Lily B. Mummert , Alfred Z. Spector, Camelot and Avalon: a distributed transaction facility, Morgan Kaufmann Publishers Inc., San Francisco, CA, 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: Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
• 12: Cormac Flanagan , Stephen N Freund, Atomizer: a dynamic atomicity checker for multithreaded programs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.256-267, January 14-16, 2004, Venice, Italy
• 13: C. Flanagan, S. N. Freund, and S. Qadeer. Exploiting purity for atomicity. Technical Note 04-02, Williams College, 2004.
• 14: 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
• 15: C. Flanagan and S. Qadeer. Transactions for software model checking. In Proceedings of the Workshop on Software Model Checking, 2003.
• 16: Cormac Flanagan , Shaz Qadeer, A type and effect system for atomicity, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 17: 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
• 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: Patrice Godefroid, Using Partial Orders to Improve Automatic Verification Methods, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.176-185, June 18-21, 1990
• 20: Dan Grossman, Type-safe multithreading in cyclone, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 21: Tim Harris , Keir Fraser, Language support for lightweight transactions, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA
• 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: Maurice P. Herlihy , Jeannette M. Wing, Linearizability: a correctness condition for concurrent objects, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.3, p.463-492, July 1990 [doi>10.1145/78969.78972]
• 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: Leslie Lamport , Fred B. Schneider, Pretending Atomicity, Cornell University, Ithaca, NY, 1989
• 26: 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]
• 27: B. Liskov , D. Curtis , P. Johnson , R. Scheifer, Implementation of Argus, Proceedings of the eleventh ACM Symposium on Operating systems principles, p.111-122, November 08-11, 1987, Austin, Texas, United States
• 28: D. B. Lomet, Process structuring, synchronization, and recovery using atomic actions, Proceedings of an ACM conference on Language design for reliable software, p.128-137, March 28-30, 1977, Raleigh, North Carolina
• 29: Jayadev Misra, A discipline of multiprogramming: programming theory for distributed applications, Springer-Verlag New York, Inc., Secaucus, NJ, 2001
• 30: Flemming Nielson , Hanne R. Nielson , Chris Hankin, Principles of Program Analysis, Springer-Verlag New York, Inc., Secaucus, NJ, 1999
• 31: Christos Papadimitriou, The theory of database concurrency control, Computer Science Press, Inc., New York, NY, 1986
• 32: Doron Peled, Combining Partial Order Reductions with On-the-fly Model-Checking, Proceedings of the 6th International Conference on Computer Aided Verification, p.377-390, June 21-23, 1994
• 33: Shaz Qadeer , Sriram K. Rajamani , Jakob Rehof, Summarizing procedures in concurrent programs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.245-255, January 14-16, 2004, Venice, Italy
• 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: Douglas C. Schmidt , Tim Harrison, Double-checked locking, Pattern languages of program design 3, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1997
• 36: N. Sterling. WARLOCK -- a static data race analysis tool. In USENIX Technical Conference Proceedings, pages 97--106, Winter 1993.
• 37: Scott D. Stoller, Model-Checking Multi-threaded Distributed Java Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.224-244, August 30-September 01, 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.

INDEX TERMS

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

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Reliability, Verification

Keywords:
atomicity, concurrent programs, purity, reduction