DRFx: A Simple and Efficient Memory Model for Concurrent Programming Languages - Singh, Abhayendra; Millstein, Todd; Musuvathi, Madanlal; Narayanasamy, Satish; Marino, Daniel; Musuvathi, Madan (International Conference on Programming Language Design and Implementation (PLDI)., 2010)
The most intuitive memory model for shared-memory multi-threaded programming is sequential consistency (SC), which requires that memory operations from all threads appear to occur in some global sequential order consistent with per-thread program order. But ensuring SC for all programs disallows the use of many compiler and hardware optimizations thereby impacting performance. Data-race-free models offer a compromise between programmer understanding and performance by guaranteeing SC execution for data-race-free programs while providing a weaker guarantee, or no guarantee at all, for other programs. While these models allow many optimizations, they require a programmer to know whether or not a program has a data race in order to understand its behavior. Unfortunately, data race errors are easy to make and hard to detect in general. We present the DRFx memory model, which is simple for programmers to understand and use while still supporting many common optimizations. We introduce a memory model (MM) exception which can be signaled to halt execution. If a program executes without throwing this exception, then DRFx guarantees that the execution is SC. If a program throws an MM exception during an execution, then DRFx guarantees that the program has a data race. We observe that conditions for an MM exception can be detected in hardware through lightweight conflict detection. Furthermore, our model safely allows aggressive compiler optimizations within compiler-designated program regions. We formalize our memory model, prove several theorems about its behavior, describe a compiler and hardware design suitable for DRFx, and evaluate the performance overhead due to our compiler and hardware requirements.