一句话：提出连接图抽象，用分离逻辑证明无死锁与无内存泄漏，并在 Coq 中机械化，首次为高阶二元会话类型语言提供机械化证明。
本文提出“连接图”这一抽象表示，用于刻画并发交互实体（如线程、通道）的拓扑结构，从而封装关于无死锁推理的通用原则。连接图以顶点、边及带标签（表示交互协议）为参数。作者采用进度与保持（progress and preservation）风格证明无死锁和无内存泄漏，并以分离逻辑作为元理论工具，子结构化地处理连接图的边与标签。为局部证明保持性，提炼出保持连接图非环性的通用分离逻辑图变换规则；为局部证明全局进度，引入针对非环连接图的等待归纳原理。所有结果在 Coq 中机械化，并实例化到高阶二元会话类型语言，获得首个无死锁与无泄漏的机械化证明。
We introduce the notion of a connectivity graph —an abstract representation of the topology of concurrently interacting entities, which allows us to encapsulate generic principles of reasoning about deadlock freedom . Connectivity graphs are parametric in their vertices (representing entities like threads and channels) and their edges (representing references between entities) with labels (representing interaction protocols). We prove deadlock and memory leak freedom in the style of progress and preservation and use separation logic as a meta theoretic tool to treat connectivity graph edges and labels substructurally. To prove preservation locally, we distill generic separation logic rules for local graph transformations that preserve acyclicity of the connectivity graph. To prove global progress locally, we introduce a waiting induction principle for acyclic connectivity graphs. We mechanize our results in Coq, and instantiate our method with a higher-order binary session-typed language to obtain the first mechanized proof of deadlock and leak freedom.
@article{paperbot1552,
title = {Connectivity graphs: a method for proving deadlock freedom based on separation logic},
author = {Jules Jacobs and Stephanie Balzer and Robbert Krebbers},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498662}
}