Extended sequential reasoning for data-race-free programs
Laura Effinger-Dean, Hans‐J. Boehm, Dhruva R. Chakrabarti, Pramod G. Joisha · 2011
Most multithreaded programming languages prohibit or discourage data races. By avoiding data races, we are guaranteed that variables accessed within a synchronization-free code region cannot be modified by other threads, allowing us to reason about such code regions as though they were single-threaded. However, such single-threaded reasoning is not limited to synchronization-free regions. We present a simple characterization of extended interference-free regions in which variables cannot be modified by other threads.