International Conference on Programming Language Design and Implementation (PLDI). June 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.