On Thin Air Reads: Towards an Event Structures Model of Relaxed Memory

TL;DR

This paper introduces a new event structures model called well-justification for relaxed memory, balancing between overly weak and overly strict criteria, ensuring correctness and safety in concurrent executions.

Contribution

It proposes the well-justification concept, a middle ground model for relaxed memory that supports compiler optimizations while avoiding thin-air reads.

Findings

Well-justified configurations satisfy the DRF theorem.

Rely-guarantee reasoning is sound for well-justified configurations.

Type-safety is maintained in well-justified configurations.

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.