paperbot · PL 论文追踪

RSS

Grounding thin-air reads with event structures

POPL 3(POPL)2019
Soham Chakraborty, Viktor Vafeiadis

尚未生成 AI 速览(可能缺少 API key 或等待下次运行补跑)。

原文摘要(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 原文 ·

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}
}