Effects for cooperable and serializable threads

Reasoning about the correctness of multithreaded programs is complicated by the potential for unexpected interference between threads. Previous work on controlling thread interference focused on verifying race freedom and/or atomicity. Unfortunately, race freedom is insufficient to prevent unintended thread interference. The notion of atomic blocks provides more semantic guarantees, but offers limited benefits for non-atomic code and it requires bimodal sequential/multithreaded reasoning (depending on whether code is inside or outside an atomic block). This paper proposes an alternative strategy that uses yield annotations to control thread interference, and we present an effect system for verifying the correctness of these yield annotations. The effect system guarantees that for any preemptively-scheduled execution of a well-formed program, there is a corresponding cooperative execution with equivalent behavior in which context switches happen only at yield annotations. This effect...

• Type: Conference
• Year: 2010
• Where: TLDI
• Authors: Jaeheon Yi, Cormac Flanagan
• Keywords: Bimodal Sequential/multithreaded Reasoning, Cooperative Reasoning, Formal Methods, TLDI 2010, Unintended Thread Interference