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.

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.