eTX 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.