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.