A Programmer-Oriented Approach to Safe Concurrency
Abstract
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, and the policy that distinguishes desired concurrency from race conditions. Source code often does not reveal these design decisions because they rarely have purely local manifestations or because they cannot be inferred from code. Many programmers believe it is too difficult to explicate the models in ordinary practice. 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. This thesis is about a practicable approach to capturing and expressing design intent, and, through the use of annotations and composable static analyses, assuring consistency of code and intent as both evolve. We use case studies to explore the costs and benefits of a new annotation-based approach for expressing design intent. Our annotations express mechanical properties that programmers must already be considering, such as lock state associations. Our analyses reveal race conditions in a variety of case study samples. We developed a prototype tool that embodies static analysis techniques for assuring consistency between code and models (expressed as code annotations). The novel technical features of this approach include (1) regions as flexible aggregations of state that can cross object boundaries, (2) a region-based object-oriented effects system; (3) analysis to track the association of locks with regions, (4) policy descriptions for allowable method interleavings, and (5) an incremental process for inserting, validating, and exploiting annotations.
Document Details
- Document Type
- Technical Report
- Publication Date
- May 01, 2003
- Accession Number
- ADA461080
Entities
People
- Aaron Greenhouse
Organizations
- Carnegie Mellon University