一句话：提出从抽象分离逻辑规约推导交互迹的自由定理，并证明逻辑原子并发规约蕴含线性化。
分离逻辑中带有抽象谓词的规约直观上限制了客户端与库之间的调用方式，即规定了二者交互迹上的协议，但这一直觉此前缺乏形式化。本文将其形式化，并给出从抽象分离逻辑规约推导交互迹“自由定理”的一般方法，展示多个例子。特别地，作者证明：并发模块操作的逻辑原子（logically atomic）并发分离逻辑规约蕴含该操作是可线性化的（linearizable）。所有结果均在 Coq 证明助手内、基于高阶并发分离逻辑框架 Iris 机械化验证。
Separation logic specifications with abstract predicates intuitively enforce a discipline that constrains when and how calls may be made between a client and a library. Thus a separation logic specification of a library intuitively enforces a protocol on the trace of interactions between a client and the library. We show how to formalize this intuition and demonstrate how to derive "free theorems" about such interaction traces from abstract separation logic specifications. We present several examples of free theorems. In particular, we prove that a so-called logically atomic concurrent separation logic specification of a concurrent module operation implies that the operation is linearizable. All the results presented in this paper have been mechanized and formally proved in the Coq proof assistant using the Iris higher-order concurrent separation logic framework.
@article{paperbot1135,
title = {Theorems for free from separation logic specifications},
author = {Lars Birkedal and Thomas Dinsdale-Young and Armaël Guéneau and Guilhem Jaber and Kasper Svendsen and Nikos Tzevelekos},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {ICFP},
year = {2021},
doi = {10.1145/3473586}
}