Assuring and evolving concurrent programs: annotations and policy

ABSTRACT

Assuring and evolving concurrent programs requires understanding the concurrency-related design decisions used in their implementation. In Java-style shared-memory programs, these decisions include which state is shared, how access to it is regulated, the roles of threads, and the policy that distinguishes desired concurrency from race conditions. These decisions rarely have purely local manifestations in code.In this paper, we use case studies from production Java code to explore the costs and benefits of a new annotation-based approach for expressing design intent. Our intent is both to assist in establishing "thread safety" attributes in code and to support tools that safely restructure code---for example, shifting critical section boundaries or splitting locks. The annotations we use express "mechanical" properties such as lock-state associations, uniqueness of references, and encapsulation of state into named aggregations. Our analyses revealed race conditions in our case study samples, drawn from open-source projects and library code.The novel technical features of this approach include (1) flexible encapsulation via aggregations of state that can cross object boundaries, (2) the association of locks with state aggregations, (3) policy descriptions for allowable method interleavings, and (4) the incremental process for inserting, validating, and exploiting annotations.

REFERENCES

• 1: Gregory R. Andrews , James R. McGraw, Language features for process interaction, Proceedings of an ACM conference on Language design for reliable software, p.114-127, March 28-30, 1977, Raleigh, North Carolina
• 2: Apache Software Foundation. Log4j project. http://jakarta.apache.org/log4j/docs/index.html. Current Jan. 2002.
• 3: David F. Bacon , Robert E. Strom , Ashis Tarafdar, Guava: a dialect of Java without data races, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.382-400, October 2000, Minneapolis, Minnesota, United States
• 4: Joshua Bloch, Effective Java programming language guide, Sun Microsystems, Inc., Mountain View, CA, 2001
• 5: J. Bloch. Proposed final draft, JSR-41: A simple assertion facility for the Java programming language. http://jcp.org/jsr/detail/41.jsp, June 2001. Current Jan. 2002.
• 6: Grady Booch , James Rumbaugh , Ivar Jacobson, The Unified Modeling Language user guide, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1999
• 7: 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
• 8: John Boyland, Alias burying: unique variables without destructive reads, Software—Practice & Experience, v.31 n.6, p.533-553, May 2001 [doi>10.1002/spe.370]
• 9: Roy H. Campbell , A. Nico Habermann, The specification of process synchronization by path expressions, Operating Systems, Proceedings of an International Symposium, p.89-102, April 23-25, 1974
• 10: Edwin C. Chan , John T. Boyland , William L. Scherlis, Promises: limited specifications for analysis and manipulation, Proceedings of the 20th international conference on Software engineering, p.167-176, April 19-25, 1998, Kyoto, Japan
• 11: David G. Clarke , John M. Potter , James Noble, Ownership types for flexible alias protection, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.48-64, October 18-22, 1998, Vancouver, British Columbia, Canada
• 12: Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
• 13: D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Research Report 159, Compaq SRC, Dec. 1998.
• 14: David Evans , John Guttag , James Horning , Yang Meng Tan, LCLint: a tool for using specifications to check code, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.87-96, December 06-09, 1994, New Orleans, Louisiana, United States
• 15: Cormac Flanagan , Martín Abadi, Object Types against Races, Proceedings of the 10th International Conference on Concurrency Theory, p.288-303, August 24-27, 1999
• 16: Cormac Flanagan , Martín Abadi, Types for Safe Locking, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.91-108, March 22-28, 1999
• 17: 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
• 18: Cormac Flanagan , Stephen N. Freund, Detecting race conditions in large programs, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.90-96, June 2001, Snowbird, Utah, United States [doi>10.1145/379605.379687]
• 19: David Garlan , Robert Monroe , David Wile, Acme: an architecture description interchange language, Proceedings of the 1997 conference of the Centre for Advanced Studies on Collaborative research, p.7, November 10-13, 1997, Toronto, Ontario, Canada
• 20: David K. Gifford , John M. Lucassen, Integrating functional and imperative programming, Proceedings of the 1986 ACM conference on LISP and functional programming, p.28-38, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319848]
• 21: A. Greenhouse. Bug 1507: Improper synchronization in AsyncAppender and Category causes race conditions. http://nagoya.apache.org/bugzilla/, Apr. 2001. Current Jan. 2002.
• 22: Aaron Greenhouse , John Boyland, An Object-Oriented Effects System, Proceedings of the 13th European Conference on Object-Oriented Programming, p.205-229, June 14-18, 1999
• 23: C. A. R. Hoare. Towards a theory of parallel programming. In C. A. R. Hoare and R. H. Perrot, editors, Oper. Syst. Techniques. Academic Press, 1971.
• 24: L. Lamport. The 'Hoare logic' of concurrent programs. Acta Inf., 14(1), 1980.
• 25: Doug Lea , Douglas Lea, Concurrent Programming in Java. Second Edition: Design Principles and Patterns, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 26: G. T. Leavens, A. L. Baker, and C. Ruby. JML: A notation for detailed design. In H. Kilov, B. Rumpe, and I. Simmonds, editors, Behavioral Specifications of Businesses and Systems. Kluwer, 1999.
• 27: K. Rustan M. Leino, Data groups: specifying the modification of extended state, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.144-153, October 18-22, 1998, Vancouver, British Columbia, Canada
• 28: K. R. M. Leino, G. Nelson, and J. B. Saxe. ESC/Java user's manual. Technical Note 2000-002, Compaq SRC, Oct. 2000.
• 29: Klaus-Peter Löhr, Concurrency annotations for reusable software, Communications of the ACM, v.36 n.9, p.81-89, Sept. 1993 [doi>10.1145/162685.162708]
• 30: J. M. Lucassen. Types and Effects: Towards the Integration of Functional and Imperative Programming. PhD thesis, MIT, Sept. 1987.
• 31: Bertrand Meyer, Object-oriented software construction (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1997
• 32: James Noble , David Holmes , John Potter, Exclusion for composite objects, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.13-28, October 2000, Minneapolis, Minnesota, United States
• 33: S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Inf., 6(4), 1976.
• 34: William L. Scherlis, Systematic Change of Data Representation: Program Manipulations and a Case Study, Proceedings of the 7th European Symposium on Programming: Programming Languages and Systems, p.252-266, March 28-April 04, 1998
• 35: Peter M. Schwarz , Alfred Z. Spector, Synchronizing shared abstract types, ACM Transactions on Computer Systems (TOCS), v.2 n.3, p.223-250, Aug. 1984 [doi>10.1145/989.1188]
• 36: Charles Simonyi , Martin Heller, The Hungarian revolution, BYTE, v.16 n.8, p.131-ff., Aug. 1991

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.0 General
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Evolutionary prototyping

General Terms:
Algorithms, Design, Performance