Title: On Thin Air Reads: Towards an Event Structures Model of Relaxed Memory,
Abstract: To model relaxed memory, we propose confusion-free event structures over an
alphabet with a justification relation. Executions are modeled by justified
configurations, where every read event has a justifying write event.
Justification alone is too weak a criterion, since it allows cycles of the kind
that result in so-called thin-air reads. Acyclic justification forbids such
cycles, but also invalidates event reorderings that result from compiler
optimizations and dynamic instruction scheduling. We propose the notion of
well-justification, based on a game-like model, which strikes a middle ground.
We show that well-justified configurations satisfy the DRF theorem: in any
data-race free program, all well-justified configurations are sequentially
consistent. We also show that rely-guarantee reasoning is sound for
well-justified configurations, but not for justified configurations. For
example, well-justified configurations are type-safe.
Well-justification allows many, but not all reorderings performed by relaxed
memory. In particular, it fails to validate the commutation of independent
reads. We discuss variations that may address these shortcomings.