Daniel Marino, Abhayendra Singh, Todd Millstein, Madanlal Musuvathi, and Satish Narayanasamy
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.
In International Conference on Programming Language Design and Implementation (PLDI).
Publisher Association for Computing Machinery, Inc.
Copyright © 2007 by the Association for Computing Machinery, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or firstname.lastname@example.org. The definitive version of this paper can be found at ACM’s Digital Library --http://www.acm.org/dl/.