ON THIN AIR READS: TOWARDS AN EVENT STRUCTURES MODEL OF RELAXED MEMORY
ON THIN AIR READS: TOWARDS AN EVENT STRUCTURES MODEL OF RELAXED MEMORY
复制标题
DOI：
10.23638/lmcs-15(1:33)2019
复制
发表时间：
2019-01-01
影响因子：
0.6
通讯作者：
Riely, James
中科院分区：
文献类型：
--
作者：
Jeffrey, Alan;Riely, James
为了模拟放松的记忆，我们提出了具有对齐关系的字母表上的无混淆事件结构。执行由合理配置建模，其中每个读事件都有一个合理的写事件。理由本身是一个太弱的标准，因为它允许导致所谓的稀薄空气阅读的那种循环。非循环调整禁止这样的循环，但也会使由编译器优化和动态指令调度产生的事件重新排序无效。基于一个类似博弈的模型，我们提出了良正配置的概念，证明了良正配置满足DRF定理：在任何无数据竞争的程序中，所有良正配置都是顺序一致的。我们还表明，依赖-保证推理对于合理的配置是合理的，但对于合理的配置是错误的。例如，对齐良好的配置是类型安全的。对齐良好的配置允许由放松的内存执行许多(但不是所有)重新排序。特别是，它无法验证独立读取的换流。我们将讨论可能解决这些缺点的各种变化。
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.