Types for atomicity

Ensuring the correctness of multithreaded programs is difficult, due to the potential for unexpected and nondeterministic interactions between threads. Previous work has 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, the absence of 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 the atomicity of code blocks, and we present a type system for specifying and verifying such atomicity properties. The type system allows statement blocks and functions to be annotated with the keyword atomic. If the program type checks, then the type system guarantees that for any arbitrarily-interleaved program execution, there is a corresponding execution with equivalent behavior in which the instructions of ...

• Type: Conference
• Year: 2003
• Where: TLDI
• Authors: Cormac Flanagan, Shaz Qadeer
• Keywords: Atomic Block, Formal Methods, Race Conditions, TLDI 2003, Type Systems