一句话：提出 Iron，一种高阶并发分离逻辑，可精确推理动态线程间可转移资源及其义务，并在 Iris 模型与 Coq 中证明其可靠性。
在并发程序中，精确管理资源及其义务（如释放内存、关闭锁和释放文件句柄）十分困难，尤其是资源在线程间共享或动态转移时。本文提出 Iron，一种新高阶并发分离逻辑，支持对可在动态分配线程之间转移的资源进行精确推理。Iron 能验证将内存回收委托给 fork 线程等挑战性例子。作者在 Iris 基础逻辑之上定义 Iron 的模型来证明其可靠性，并证明内存资源被精确核算且不会泄漏；所有开发均在 Coq 证明助手中形式化。
Precise management of resources and the obligations they impose, such as the need to dispose of memory, close locks, and release file handles, is hard---especially in the presence of concurrency, when some resources are shared, and different threads operate on them concurrently. We present Iron, a novel higher-order concurrent separation logic that allows for precise reasoning about resources that are transferable among dynamically allocated threads. In particular, Iron can be used to show the correctness of challenging examples, where the reclamation of memory is delegated to a forked-off thread. We show soundness of Iron by means of a model of Iron, defined on top of the Iris base logic, and we use this model to prove that memory resources are accounted for precisely and not leaked. We have formalized all of the developments in the Coq proof assistant.
@article{paperbot628,
title = {Iron: managing obligations in higher-order concurrent separation logic},
author = {Aleš Bizjak and Daniel Gratzer and Robbert Krebbers and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290378}
}