一句话：用异步博弈语义为并发分离逻辑建立异步可靠性定理，并解释其常规可靠性及无数据竞争。
并发分离逻辑（CSL）用于共享内存与锁的并发命令式程序规约。本文受异步博弈语义启发，给出一种并发、交互式的逻辑解释：对每个程序 C 构造状态层与指令/锁层的一对异步迁移系统，刻画 C 与环境或 frame 交互时的操作行为。论文证明，Γ⊢{P}C{Q} 的每个推导树 π 都定义了一个在这两个异步语义下获胜的异步策略。由此得到 CSL 的异步可靠性定理：从有状态语义到无状态语义的典范映射满足基本纤维化性质。作者主张这为 CSL 的通常可靠性定理，包括无数据竞争，提供了清晰的概念性解释。
Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks. In this paper, we develop a concurrent and interactive account of the logic inspired by asynchronous game semantics. To every program C, we associate a pair of asynchronous transition systems [C]S and [C]L which describe the operational behavior of the Code when confronted to its Environment or Frame --- both at the level of machine states (S) and of machine instructions and locks (L). We then establish that every derivation tree π of a judgment Γ ⊢ {P}C{Q} defines a winning and asynchronous strategy [π]Sep with respect to both asynchronous semantics [C]S and [C]L. From this, we deduce an asynchronous soundness theorem for CSL, which states that the canonical map ℒ: [C]S~[C]L, from the stateful semantics [C]S to the stateless semantics [C]L satisfies a basic fibrational property. We advocate that this provides a clean and conceptual explanation for the usual soundness theorem of CSL, including the absence of data races.
DOI 原文 ·
@inproceedings{paperbot4353,
title = {An Asynchronous Soundness Theorem for Concurrent Separation Logic},
author = {Paul-André Melliès and Léo Stefanesco},
booktitle = {LICS},
year = {2018},
doi = {10.1145/3209108.3209116}
}