一句话：在 Iris 中为线性化的上下文精化与逻辑原子性证明开发可扩展的 Coq 自动化，显著减少证明工作量。
并发分离逻辑可验证细粒度无锁并发程序，线性化是其正确性黄金标准。上下文精化与逻辑原子性等组合式方法虽能模块化证明线性化，但 Iris、FCSL、Voila 等工具仍需大量交互式证明。本文为 Iris 中的这两类方法开发证明自动化，核心是一组由程序与逻辑状态共同指导应用的证明规则，可形成有效搜索策略：简单例子全自动证明，复杂例子尽量减少回溯以与交互式 tactic 协作。作者在 Coq 中扩展并泛化 Diaframe，2.0 版可扩展支持不同程序验证风格，并以模块实现上述两种策略。评估表明，该自动化减少了两种方法的证明工作量。
Recent advances in concurrent separation logic enabled the formal verification of increasingly sophisticated fine-grained ( i.e. , lock-free) concurrent programs. For such programs, the golden standard of correctness is linearizability , which expresses that concurrent executions always behave as some valid sequence of sequential executions. Compositional approaches to linearizability (such as contextual refinement and logical atomicity) make it possible to prove linearizability of whole programs or compound data structures ( e.g. , a ticket lock) using proofs of linearizability of their individual components ( e.g. , a counter). While powerful, these approaches are also laborious—state-of-the-art tools such as Iris, FCSL, and Voila all require a form of interactive proof. This paper develops proof automation for contextual refinement and logical atomicity in Iris. The key ingredient of our proof automation is a collection of proof rules whose application is directed by both the program and the logical state. This gives rise to effective proof search strategies that can prove linearizability of simple examples fully automatically. For more complex examples, we ensure the proof automation cooperates well with interactive proof tactics by minimizing the use of backtracking. We implement our proof automation in Coq by extending and generalizing Diaframe, a proof automation extension for Iris. While the old version (Diaframe 1.0) was limited to ordinary Hoare triples, the new version (Diaframe 2.0) is extensible in its support for program verification styles: our proof search strategies for contextual refinement and logical atomicity are implemented as modules for Diaframe 2.0. We evaluate our proof automation on a set of existing benchmarks and novel proofs, showing that it provides significant reduction of proof work for both approaches to linearizability.
@article{paperbot2042,
title = {Proof Automation for Linearizability in Separation Logic},
author = {Ike Mulder and Robbert Krebbers},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA1},
year = {2023},
doi = {10.1145/3586043}
}