A type and effect system for atomicity

9 years 3 months ago
A type and effect system for atomicity
Ensuring the correctness of multithreaded programs is difficult, due to the potential for unexpected and nondeterministic interactions between threads. Previous work addressed this problem by devising tools for detecting race conditions, a situation where two threads simultaneously access the same data variable, and at least one of the accesses is a write. However, verifying the absence of such simultaneous-access race conditions is neither necessary nor sufficient to ensure the absence of errors due to unexpected thread interactions. We propose that a stronger non-interference property is required, namely atomicity. Atomic methods can be assumed to execute serially, without interleaved steps of other threads. Thus, atomic methods are amenable to sequential reasoning techniques, which significantly simplifies both formal and informal reasoning about program correctness. This paper presents a type system for specifying and verifying the atomicity of methods in multithreaded Java pro...
Cormac Flanagan, Shaz Qadeer
Added 05 Jul 2010
Updated 05 Jul 2010
Type Conference
Year 2003
Where PLDI
Authors Cormac Flanagan, Shaz Qadeer
Comments (0)