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 -
On Thin Air Reads: Towards an Event Structures Model of Relaxed Memory

Authors: Alan Jeffrey ; James Riely ORCID-iD

    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

    Linked data

    Source : ScholeXplorer IsCitedBy ARXIV 1911.06567
    Source : ScholeXplorer IsCitedBy DOI 10.4230/lipics.ecoop.2020.5
    Source : ScholeXplorer IsCitedBy DOI 10.48550/arxiv.1911.06567
    • 10.48550/arxiv.1911.06567
    • 10.4230/lipics.ecoop.2020.5
    • 1911.06567
    Reconciling Event Structures with Modern Multiprocessors
    Moiseenko, E. ; Podkopaev, A. ; Lahav, O. ; Melkonian, O. ; Vafeiadis, V. ;

    5 Documents citing this article

    Consultation statistics

    This page has been seen 1747 times.
    This article's PDF has been downloaded 386 times.