paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Grounding thin-air reads with event structures

用事件结构为 thin-air reads 奠定基础
POPL 3(POPL)2019匹配度 2/10 · 该论文属于并发内存模型与形式语义,讨论了事件结构和 promising 语义,与用户关注的 PL 理论有一定关联;但它不涉及 LLM/Agent、静态分析、浮点程序分析或贝叶斯程序分析,也不属于画像中的核心交叉方向。引用 59 inbox
Soham Chakraborty, Viktor Vafeiadis
crossref: 2026-09-10

AI 速览

一句话:提出基于事件结构的并发内存语义,禁止 thin-air reads,并证明其与 promising 语义等价且更易扩展。

定义编程语言并发语义的核心挑战在于:既允许高效编译到现有硬件架构,又禁止程序读到 thin-air values(程序中不出现的值)。Kang 等人在 POPL'17 提出的 promising 语义是重大突破,但该语义过于复杂,并包含难以修复的缺陷和限制。本文提出一种基于事件结构的替代方案。作者证明该语义满足标准结果:DRF 定理、实现正确性与优化正确性,并建立其与 Kang 等人语义之间的形式联系。此外,该语义更易适配:作者将其扩展到 promising 语义不支持的 SC accesses 等特性,并排除了一些可疑行为。

问题
如何在并发语言语义中允许面向现有硬件的高效编译,同时禁止程序读取程序中不存在的 thin-air values。
方法
基于事件结构给出替代并发语义,并证明其标准元理论结果及与 promising 语义的形式联系。
评估
通过形式化证明 DRF 定理、实现与优化正确性、与 Kang 等人语义的形式连接,并展示对 SC 访问等特性的扩展。
原文摘要(Abstract)

The key challenge in defining the concurrency semantics of a programming language is how to enable the most efficient compilation to existing hardware architectures, and yet forbid programs from reading thin-air values, i.e., ones that do not appear in the program. At POPL'17, Kang et al. achieved a major breakthrough by introducing the `promising' semantics that came with results showing that it was a good candidate solution to the problem. Unfortunately, however, the promising semantics is rather complicated, and due to its complexity it contains some flaws and limitations that are very hard to address. In response, we present an alternative solution to this problem based on event structures. We show that it is indeed a solution by establishing the standard results about the semantics (DRF theorems, implementation and optimization correctness) as well as a formal connection to the semantics of Kang et al. Further, we show that it is easier to adapt, by extending the semantics to cover features (such as SC accesses) that are not supported by Kang et al. and to rule out some dubious behaviors admitted by the promising semantics.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot631,
  title = {Grounding thin-air reads with event structures},
  author = {Soham Chakraborty and Viktor Vafeiadis},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
  number = {POPL},
  year = {2019},
  doi = {10.1145/3290383}
}