一句话：用带证成关系的无混淆事件结构建模松弛内存，提出良证成配置以排除 thin-air reads，并证明 DRF 与 rely-guarantee 可靠性。
为建模松弛内存，论文提出一种建立在带 justification 关系的字母表上的无混淆事件结构。执行由 justified configuration 表示，其中每个读事件都有证成它的写事件；但仅 justification 允许导致 thin-air reads 的环，acyclic justification 又禁止编译器优化与动态调度产生的重排序。作者引入博弈式 well-justification 作为折中，证明良证成配置满足 DRF 定理：无数据竞争程序中所有良证成配置都顺序一致；并证明 rely-guarantee 推理对良证成配置可靠、对仅 justification 配置不可靠，良证成配置也类型安全。该方法仍不能验证独立读的交换，文中讨论可能的改进。
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.
@article{paperbot807,
title = {On Thin Air Reads: Towards an Event Structures Model of Relaxed Memory},
author = {Alan Jeffrey and James Riely},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 1},
year = {2019},
doi = {10.23638/lmcs-15(1:33)2019}
}