Diaframe: automated verification of fine-grained concurrent programs in Iris
Diaframe: automated verification of fine-grained concurrent programs in Iris
复制标题
Diaframe：Iris 中细粒度并发程序的自动验证
DOI：
10.1145/3519939.3523432
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
H. Geuvers
中科院分区：
文献类型：
--
作者：
Ike Mulder;Robbert Krebbers;H. Geuvers
细粒度的并发程序很难得到正确的，但在现代计算机中扮演着重要的角色。我们希望以一种值得信赖的方式，用最少的用户努力来证明这些程序的强大规范。在本文中，我们提出了Diaframe-细粒度并发程序的自动化和基础验证工具。Diaframe构建在Coq中用于高阶并发分离逻辑的Iris框架之上，该框架已经具有基本的可靠性证明和提供强规范的能力，但缺乏自动化。Diaframe为Iris配备了强大的自动化功能，使用了一种新颖的、可扩展的、目标导向的证明搜索策略，使用了线性逻辑编程和双溯因的思想。来自文献的24个示例的基准测试表明，Diaframe的证明负担与现有的非基础工具相比具有竞争力，而其表达性和可靠性保证更强。
Fine-grained concurrent programs are difficult to get right, yet play an important role in modern-day computers. We want to prove strong specifications of such programs, with minimal user effort, in a trustworthy way. In this paper, we present Diaframe—an automated and foundational verification tool for fine-grained concurrent programs. Diaframe is built on top of the Iris framework for higher-order concurrent separation logic in Coq, which already has a foundational soundness proof and the ability to give strong specifications, but lacks automation. Diaframe equips Iris with strong automation using a novel, extendable, goal-directed proof search strategy, using ideas from linear logic programming and bi-abduction. A benchmark of 24 examples from the literature shows that the proof burden of Diaframe is competitive with existing non-foundational tools, while its expressivity and soundness guarantees are stronger.
影响因子：
22.7
作者：
Gu, Ronghui;Shao, Zhong;Costanzo, David
通讯作者：
Costanzo, David