论薄空气读：迈向宽松内存的事件结构模型
编程语言
2023-06-22 v6 计算机科学中的逻辑
摘要
为建模宽松内存，我们提出在带有论证关系的字母表上的无混淆事件结构。执行由论证配置建模，其中每个读事件有一个论证写事件。仅论证是太弱的标准，因为它允许导致所谓薄空气读（thin-air reads）的循环。非循环论证禁止此类循环，但也使由编译器优化和动态指令调度导致的事件重排序无效。我们提出基于类游戏模型的良论证（well-justification）概念，其采取中间立场。我们展示良论证配置满足 DRF 定理：在任何无数据竞争程序中，所有良论证配置都是顺序一致的。我们还展示依赖-保证（rely-guarantee）推理对良论证配置是可靠的，但对论证配置不可靠。例如，良论证配置是类型安全的。良论证允许许多但并非所有由宽松内存执行的重排序。特别地，它无法验证独立读的交换。我们讨论可能解决这些缺点的变体。
引用
@article{arxiv.1707.05881,
title = {On Thin Air Reads: Towards an Event Structures Model of Relaxed Memory},
author = {Alan Jeffrey and James Riely},
journal= {arXiv preprint arXiv:1707.05881},
year = {2023}
}