Assuring and evolving concurrent programs: annotations and policy

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