Effects for cooperable and serializable threads
Jaeheon Yi, Cormac Flanagan · 2010
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 bi-modal sequential/multithreaded reasoning (depending on whether code is inside or outside an atomic block).