一句话：提出 Simuliris，首个在公平调度下证明利用未定义行为的并发程序变换保持终止的模拟技术。
现代编译器常利用源程序无数据竞争这一假设来合法化并发程序变换，但验证这类优化的正确性很困难。已有工作要么未证明变换保持终止，要么把所有同步操作视为外部函数，无法围绕它们重排指令。Simuliris 用所有权模块化推理编译器对行为良好程序的假设，把并发分离逻辑引入程序变换验证，并用 framing 与 coinduction 做线程局部证明。它基于 Coq 中 Iris 的非 step-indexed 变体，语言无关。作者在涉及数据竞争 UB 的标准优化上展示有效性，并实例化到 Rust 的 Stacked Borrows 语义，将基于类型的别名优化证明推广到并发。
Today’s compilers employ a variety of non-trivial optimizations to achieve good performance. One key trick compilers use to justify transformations of concurrent programs is to assume that the source program has no data races : if it does, they cause the program to have undefined behavior (UB) and give the compiler free rein. However, verifying correctness of optimizations that exploit this assumption is a non-trivial problem. In particular, prior work either has not proven that such optimizations preserve program termination (particularly non-obvious when considering optimizations that move instructions out of loop bodies), or has treated all synchronization operations as external functions (losing the ability to reorder instructions around them). In this work we present Simuliris , the first simulation technique to establish termination preservation (under a fair scheduler) for a range of concurrent program transformations that exploit UB in the source language. Simuliris is based on the idea of using ownership to reason modularly about the assumptions the compiler makes about programs with well-defined behavior. This brings the benefits of concurrent separation logics to the space of verifying program transformations: we can combine powerful reasoning techniques such as framing and coinduction to perform thread-local proofs of non-trivial concurrent program optimizations. Simuliris is built on a (non-step-indexed) variant of the Coq-based Iris framework, and is thus not tied to a particular language. In addition to demonstrating the effectiveness of Simuliris on standard compiler optimizations involving data race UB, we also instantiate it with Jung et al.’s Stacked Borrows semantics for Rust and generalize their proofs of interesting type-based aliasing optimizations to account for concurrency.
@article{paperbot1554,
title = {Simuliris: a separation logic framework for verifying concurrent program optimizations},
author = {Lennard Gäher and Michael Sammler and Simon Spies and Ralf Jung and Hoang-Hai Dang and Robbert Krebbers and Jeehoon Kang and Derek Dreyer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498689}
}