The code of many colors: relating threads to code and shared state

ABSTRACT

We introduce a thread colors model as a way to express design intent concerning the relationships between threads, executable code, and shared state. By expressing the model as annotations in code, it is possible to formally link the model with source code and to analyze the consistency of model and code in a composable manner. By using annotations as cut-points, APIs can be annotated and compliance with library threading policies can be evaluated. This is illustrated using case study examples from published code that show how thread coloring models can assist in assuring policy compliance and in identifying concurrency errors.

REFERENCES

• 1: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 2: 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]
• 3: David Callahan , Jaspal Sublok, Static analysis of low-level synchronization, Proceedings of the 1988 ACM SIGPLAN and SIGOPS workshop on Parallel and distributed debugging, p.100-111, May 05-06, 1988, Madison, Wisconsin, United States
• 4: 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
• 5: 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
• 6: Manuel Fahndrich , Robert DeLine, Adoption and focus: practical linear types for imperative programming, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 7: 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
• 8: 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
• 9: 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
• 10: Aaron Greenhouse , William L. Scherlis, Assuring and evolving concurrent programs: annotations and policy, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581395]
• 11: Dan Grossman , Greg Morrisett , Steve Zdancewic, Syntactic type abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.6, p.1037-1080, Nov. 2000 [doi>10.1145/371880.371887]
• 12: Bug id 4138730: Provide apis in awt for porting multi-threaded guis to a single-threaded model. http://developer.java.sun.com/developer/bugParade/index.jshtml, 1998.
• 13: Bug id 4143834: Swing thread implementation causes notifier to lock. http://developer.java.sun.com/developer/bugParade/index.jshtml, 1998.
• 14: 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.
• 15: Gleb Naumovich , George S. Avrunin, A conservative data flow algorithm for detecting all pairs of statements that may happen in parallel, Proceedings of the 6th ACM SIGSOFT international symposium on Foundations of software engineering, p.24-34, November 01-05, 1998, Lake Buena Vista, Florida, United States
• 16: Gleb Naumovich , George S. Avrunin , Lori A. Clarke, Data flow analysis for checking properties of concurrent Java programs, Proceedings of the 21st international conference on Software engineering, p.399-410, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302663]
• 17: Gleb Naumovich , George S. Avrunin , Lori A. Clarke, An efficient algorithm for computing MHP information for concurrent Java programs, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.338-354, September 06-10, 1999, Toulouse, France
• 18: T. Perry. Blue panels with swing FIXED.http://lists.apple.com/mhonarc/java-dev/msg16355.html.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Tools; Methodologies (e.g., object-oriented, structured)
      D.2.5 Testing and Debugging

General Terms:
Design, Reliability

Keywords:
Java, design intent, multi-threaded programming, race conditions