一句话：为共享变量并发提出基于轨迹的指称语义，在标准单变量原语下获得无循环程序的全抽象性，并机器化验证。
本文重新审视顺序一致性内存下并发语言的组合语义，目标是指称相等当且仅当代码片段在所有上下文中行为相同。Brookes 的经典指称语义依赖不实用的全内存原子读-改-写指令。作者针对仅含标准单变量原语的语言，提出基于轨迹的指称语义：轨迹记录程序写动作和环境预期的写，并用闭包算子实现抽象。论文证明其 adequacy；对无循环代码证明全抽象性；若加入全内存原子读，则含循环程序也全抽象。所有结果已在 Coq 中机器化验证。
We revisit the fundamental problem of defining a compositional semantics for a concurrent programming language under sequentially consistent memory with the aim of equating the denotations of pieces of code if and only if these pieces induce the same behavior under all program contexts. While the denotational semantics presented by Brookes [Information and Computation 127, 2 (1996)] has been considered a definitive solution, we observe that Brookes’s full abstraction result crucially relies on the availability of an impractical whole-memory atomic read-modify-write instruction. In contrast, we consider a language with standard primitives, which apply to a single variable. For that language, we propose an alternative denotational semantics based on traces that track program write actions together with the writes expected from the environment, and equipped with several closure operators to achieve necessary abstraction. We establish the adequacy of the semantics, and demonstrate full abstraction for the case that the analyzed code segment is loop-free. Furthermore, we show that by including a whole-memory atomic read in the language, one obtains full abstraction for programs with loops. To gain confidence, our results are fully mechanized in Coq.
@article{SvyatlovskiyML24,
title = {Compositional Semantics for Shared-Variable Concurrency},
author = {Mikhail Svyatlovskiy and Shai Mermelstein and Ori Lahav},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656399}
}