Using Eclipse to demonstrate positive static assurance of Java program concurrency design intent

ABSTRACT

Assuring and evolving concurrent programs requires understanding the concurrency-related design decisions used in their implementation. Source code often does not reveal these design decisions because they may not have purely local manifestations in the code, or because they cannot be inferred from code. As a result, this design intent is usually not expressed, and it is therefore generally infeasible to assure that concurrent programs are free of race conditions.We describe a prototype Eclipse-based tool developed as part of research toward a practicable approach to capturing and assuring design intent. Through the use of annotations and composable static analyses we can help assure consistency of code and intent as both evolve. The dominant design consideration for the tool is the principle of "early gratification"---some assurance can be obtained with minimal or no annotation effort, and additional increments of annotation or other effort are rewarded with additional increments of assurance.

REFERENCES

• 1: 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
• 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: 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
• 4: 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
• 5: Aaron Greenhouse , William L. Scherlis , Thomas Gross, A programmer-oriented approach to safe concurrency, 2003
• 6: 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
• 7: 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]