Alan Jeffrey ; James Riely - 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 - https://doi.org/10.23638/LMCS-15(1:33)2019
On Thin Air Reads: Towards an Event Structures Model of Relaxed MemoryArticle

Authors: Alan Jeffrey ; James Riely ORCID

    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.


    Volume: Volume 15, Issue 1
    Published on: March 29, 2019
    Accepted on: March 8, 2019
    Submitted on: July 20, 2017
    Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science

    5 Documents citing this article

    Consultation statistics

    This page has been seen 2965 times.
    This article's PDF has been downloaded 488 times.