Jeffrey, Alan and Riely, James - On Thin Air Reads: Towards an Event Structures Model of Relaxed Memory

lmcs:3804 - Logical Methods in Computer Science, March 29, 2019, Volume 15, Issue 1
On Thin Air Reads: Towards an Event Structures Model of Relaxed Memory

Authors: Jeffrey, Alan and Riely, James

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.

Source :
DOI : 10.23638/LMCS-15(1:33)2019
Volume: Volume 15, Issue 1
Published on: March 29, 2019
Submitted on: July 20, 2017
Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science