Types for Precise Thread Interference

Jaeheon Yi, Tim Disney, Stephen Freund and Cormac Flanagan

Abstract

Interference between concurrent threads may potentially occur at any program point, and programmers use a variety of synchronization idioms such as locks, barriers, etc, to restrict where interference may actually occur. The resulting actual interference points are typically never documented and must be manually reconstructed as the first step in any subsequent programming task (code review, refactoring, etc).

This paper proposes explicitly specifying actual interference points in the program source code presents a type and effect system for verifying the correctness of these interference specifications.

Experimental results on a variety of Java benchmarks show that this approach provides a significant improvement over prior systems based on method-level atomicity specifications. In particular, it reduces the number of interference points one must consider from several hundred points per thousand lines of code to roughly 13 per thousand lines of code. Explicit interference points also highlight all known concurrency defects in these benchmarks.

Full paper

Slides

o

Presented at FOOL 2011; Sunday, 23 October 2011; Portland, Oregon, USA