Sciweavers

Share
ISSTA
2012
ACM

Cooperative types for controlling thread interference in Java

8 years 5 months ago
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 speciļ¬cations. 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...
Jaeheon Yi, Tim Disney, Stephen N. Freund, Cormac
Added 28 Sep 2012
Updated 28 Sep 2012
Type Journal
Year 2012
Where ISSTA
Authors Jaeheon Yi, Tim Disney, Stephen N. Freund, Cormac Flanagan
Comments (0)
books