A Separation Logic for a Promising Semantics
A Separation Logic for a Promising Semantics
复制标题
有前途语义的分离逻辑
DOI：
10.1007/978-3-319-89884-1_13
复制
发表时间：
2018
影响因子：
--
通讯作者：
Viktor Vafeiadis
中科院分区：
文献类型：
--
作者：
Kasper Svendsen;Jean Pichon;Marko Doko;O. Lahav;Viktor Vafeiadis
我们提出了 SLR，这是第一个用于在弱内存模型下推理并发程序的表达性程序逻辑，解决了无中生有的问题。我们的逻辑包括现有逻辑（例如 RSL 和 GPS）中的标准功能，这些功能以前已知只有在更强的内存模型下才有效：（1）分离，（2）每个位置不变量，（3）通过释放-获取同步进行所有权转移，以及用于推理（4）不存在凭空行为和（5）一致性的新功能。该逻辑在 Kang 等人最近的“有前途”的记忆模型上被证明是合理的，他们使用了一种截然不同的论据来证明更简单的记忆模型的逻辑健全性。
We present SLR, the first expressive program logic for reasoning about concurrent programs under a weak memory model addressing the out-of-thin-air problem. Our logic includes the standard features from existing logics, such as RSL and GPS, that were previously known to be sound only under stronger memory models: (1) separation, (2) per-location invariants, and (3) ownership transfer via release-acquire synchronisation—as well as novel features for reasoning about (4) the absence of out-of-thin-air behaviours and (5) coherence. The logic is proved sound over the recent “promising” memory model of Kang et al., using a substantially different argument to soundness proofs of logics for simpler memory models.