23/06/2021

Modular Data-Race-Freedom Guarantees in the Promising Semantics

Minki Cho, Sung-Hwan Lee, Chung-Kil Hur, Ori Lahav

Keywords: Relaxed Memory Concurrency, Operational Semantics, Compiler Optimizations, Data Race Freedom

Abstract: Local data-race-freedom guarantees, ensuring strong semantics for locations accessed by non-racy instructions, provide a fruitful methodology for modular reasoning in relaxed memory concurrency. We observe that standard compiler optimizations are in inherent conflict with such guarantees in general fully-relaxed memory models. Nevertheless, for a certain strengthening of the promising model by Lee et al. that only excludes relaxed RMW-store reorderings, we establish multiple useful local data-racefreedom guarantees that enhance the programmability aspect of the model.We also demonstrate that the performance price of forbidding these reorderings is insignificant. To the best of our knowledge, these results are the first to identify a model that includes the standard concurrency constructs, supports the efficient mapping of relaxed reads and writes to plain hardware loads and stores, and yet validates several local data-race-freedom guarantees. To gain confidence, our results are fully mechanized in Coq.

The video of this talk cannot be embedded. You can watch it here:
https://slideslive.com/38956307
(Link will open in new window)
 0
 0
 0
 0
This is an embedded video. Talk and the respective paper are published at PLDI 2021 virtual conference. If you are one of the authors of the paper and want to manage your upload, see the question "My papertalk has been externally embedded..." in the FAQ section.

Comments

Post Comment
no comments yet
code of conduct: tbd

Similar Papers