一句话：首次在 Moggi 单子框架下为 RA 弱内存模型的函数式并发语言给出组合式指称语义，并验证程序变换。
本文为一种具备一等并行组合与共享内存操作的函数式语言提出组合式指称语义，其操作语义遵循 Release/Acquire（RA）弱内存模型。语义采用 Moggi 的单子方法，并以 Brookes 风格轨迹为基础：作者将 Brookes 的轨迹适配到 Kang 等人提出的 RA 基于视图的机器，并在 Brookes 的 mumble 与 stutter 闭包之外补充了 RA 特有的操作。这些补充操作提供了对轨迹更细致的理解，使轨迹与操作语义中的“中断执行”解耦。作者证明该指称语义是 adequate 的，并用其验证了若干有意义的程序变换。这是首个将弱内存模型置于 Moggi 标准单子方法之中、与其他编程效应同等对待的工作。
We present a compositional denotational semantics for a functional language with first-class parallel composition and shared-memory operations whose operational semantics follows the Release/Acquire weak memory model (RA). The semantics is formulated in Moggi’s monadic approach and is based on Brookes-style traces. To do so we adapt Brookes’s traces to view-based machine for RA by Kang et al., and supplement Brookes’s mumble and stutter closure operations with additional operations, specific to RA. The latter provides a more nuanced understanding of traces that uncouples them from operational interrupted executions. We show that our denotational semantics is adequate and use it to validate various program transformations of interest. This is the first work to put weak memory models on the same footing as many other programming effects in Moggi’s standard monadic approach.
@article{DvirKL25,
title = {A Brookes-Style Denotational Semantics for Release/Acquire Concurrency},
author = {Yotam Dvir and Ohad Kammar and Ori Lahav},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {47},
number = {2},
year = {2025},
doi = {10.1145/3715096}
}