一句话：在 Coq 中基于 Aneris 分布式分离逻辑与依赖分离协议，验证了可靠通信库及其上层 RPC 与复制键值存储组件。
本文针对分布式系统中可靠通信组件难以验证的问题，在类 OCaml 语言上基于 UDP 实现了一个可靠通信库，具有握手协议、双向通道以及重传/确认机制等典型特征。作者在 Aneris 分布式分离逻辑中验证该库，提出了一种新的证明模式——会话托管（session escrow）模式，它建立在已有 escrow 证明模式与依赖分离协议之上，而后者此前仅用于非分布式的并发场景。该库的规范使上层应用的推理得以简化：作者据此验证了一个远程过程调用（RPC）库，并进一步验证了带 leader-follower 的惰性复制键值存储及其客户端。整个开发高度模块化，每个组件都相对于其所用组件的规范（而非实现）进行验证，全部结果在 Coq 证明助手中机器化。
We present a foundationally verified implementation of a reliable communication library for asynchronous client-server communication, and a stack of formally verified components on top thereof. Our library is implemented in an OCaml-like language on top of UDP and features characteristic traits of existing protocols, such as a simple handshaking protocol, bidirectional channels, and retransmission/acknowledgement mechanisms. We verify the library in the Aneris distributed separation logic using a novel proof pattern---dubbed the session escrow pattern---based on the existing escrow proof pattern and the so-called dependent separation protocols, which hitherto have only been used in a non-distributed concurrent setting. We demonstrate how our specification of the reliable communication library simplifies formal reasoning about applications, such as a remote procedure call library, which we in turn use to verify a lazily replicated key-value store with leader-followers and clients thereof. Our development is highly modular---each component is verified relative to specifications of the components it uses (not the implementation). All our results are formalized in the Coq proof assistant.
@article{paperbot1924,
title = {Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols},
author = {Léon Gondelman and Jonas Kastberg Hinrichsen and Mário Pereira and Amin Timany and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {ICFP},
year = {2023},
doi = {10.1145/3607859}
}