DRFx: A Simple and Efficient Memory Model for Concurrent Programming Languages
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2010), Toronto, Canada, June 6-10, 2010.
Daniel Marino, Abhayendra Singh, Todd Millstein, Madanlal Musuvathi, Satish Narayanasamy
The most intuitive memory model for shared-memory
multithreaded programming is sequential consistency (SC), but it
disallows the use of many compiler and hardware optimizations thereby
impacting performance. Data-race-free (DRF) models, such as the
proposed C++0x memory model, guarantee SC execution for data-race-free
programs. But these models provide no guarantee at all for racy
programs, compromising the safety and debuggability of such
programs. To address the safety issue, the Java memory model, which is
also based on the DRF model, provides a weak semantics for racy
executions. However, this semantics is subtle and complex, making it
difficult for programmers to reason about their programs and for
compiler writers to ensure the correctness of compiler optimizations.
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 SC
violations can be detected in hardware through a lightweight form of
conflict detection. Furthermore, our model safely allows aggressive
compiler and hardware optimizations within compiler-designated program
regions. We formalize our memory model, prove several properties about
this model, describe a compiler and hardware design suitable for DRFx,
and evaluate the performance overhead due to our compiler and hardware
requirements.
[PDF | Project Page]
Superseded by this paper.