Cooperative types for controlling thread interference in Java

Multithreaded programs are notoriously prone to unintended interference between concurrent threads. To address this problem, we argue that yield annotations in the source code should document all thread interference, and we present a type system for verifying the absence of undocumented interference in Java programs. Under this type system, welltyped programs behave as if context switches occur only at yield annotations. Thus, well-typed programs can be understood using intuitive sequential reasoning, except where yield annotations remind the programmer to account for thread interference. Experimental results show that yield annotations describe thread interference more precisely than prior techniques based on method-level atomicity specifications. In particular, yield annotations reduce the number of interference points one must reason about by an order of magnitude. The type system is also more precise than prior methods targeting race freedom, and yield annotations highlight all k...

• Type: Journal
• Year: 2012
• Where: ISSTA
• Authors: Jaeheon Yi, Tim Disney, Stephen N. Freund, Cormac Flanagan
• Keywords: Context Switches, ISSTA 2012, Sequential Reasoning, Software Engineering, Unintended Interference