Repository logo
 

Bounding data races in space and time

Accepted version
Peer-reviewed

Type

Conference Object

Change log

Authors

Dolan, S 
Sivaramakrishnan, KC 

Abstract

© 2018 ACM. We propose a new semantics for shared-memory parallel programs that gives strong guarantees even in the presence of data races. Our local data race freedom property guarantees that all data-race-free portions of programs exhibit sequential semantics. We provide a straightforward operational semantics and an equivalent axiomatic model, and evaluate an implementation for the OCaml programming language. Our evaluation demonstrates that it is possible to balance a comprehensible memory model with a reasonable (no overhead on x86, ∼0.6% on ARM) sequential performance trade-off in a mainstream programming language.

Description

Keywords

weak memory models, operational semantics

Journal Title

ACM SIGPLAN Notices

Conference Name

PLDI '18: ACM SIGPLAN Conference on Programming Language Design and Implementation

Journal ISSN

1523-2867
1558-1160

Volume Title

53

Publisher

ACM
Sponsorship
Royal Commission for the Exhibition of 1851 (200684)