Efficient Processor Support for DRFx, a Memory Model with Exceptions
Sixteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2011), Newport Beach, California, March 5-11, 2011.
Abhayendra Singh, Daniel Marino, Satish Narayanasamy, Todd Millstein, Madanlal Musuvathi
A longstanding challenge of shared-memory concurrency is to provide
a memory model that allows for efficient implementation
while providing strong and simple guarantees to programmers. The
C++0x and Java memory models admit a wide variety of compiler
and hardware optimizations and provide sequentially consistent
(SC) semantics for data-race-free programs. However, they either
do not provide any semantics (C++0x) or provide a hard-tounderstand
semantics (Java) for racy programs, compromising the
safety and debuggability of such programs.
In earlier work we proposed the DRFx memory model, which
addresses this problem by dynamically detecting potential violations
of SC due to the interaction of compiler or hardware optimizations
with data races and halting execution upon detection. In
this paper, we present a detailed micro-architecture design for supporting
the DRFx memory model, formalize the design and prove
its correctness, and evaluate the design using a hardware simulator.
We describe a set of DRFx-compliant complexity-effective optimizations
which allow us to attain performance close to that of
TSO (Total Store Model) and DRF0 while providing strong guarantees
for all programs.
[PDF | Project Page]
Superseded by this paper.