一句话：首次对因果一致分布式数据库实现进行模块化规约与验证，并在 Coq 中机器化证明。
本文关注如何对因果一致的分布式数据库实现进行模块化规约与验证，以支持客户端和服务器完整功能正确性的推理。作者在面向类 ML 语言、带网络原语的高阶分布式分离逻辑 Aneris 中，对数据库进行规约与推理，并利用其模块化规约与验证机制，使各组件仅依赖其他组件的规约而非实现进行独立验证。为说明规约可用性，论文证明了一组涉及因果依赖的小型合成示例，并验证了构建在该数据库之上的会话管理器库。所有结果均在 Coq 证明助手中基于 Aneris 逻辑的形式化完成。
We present the first specification and verification of an implementation of a causally-consistent distributed database that supports modular verification of full functional correctness properties of clients and servers. We specify and reason about the causally-consistent distributed database in Aneris, a higher-order distributed separation logic for an ML-like programming language with network primitives for programming distributed systems. We demonstrate that our specifications are useful, by proving the correctness of small, but tricky, synthetic examples involving causal dependency and by verifying a session manager library implemented on top of the distributed database. We use Aneris's facilities for modular specification and verification to obtain a highly modular development, where each component is verified in isolation, relying only on the specifications (not the implementations) of other components. We have used the Coq formalization of the Aneris logic to formalize all the results presented in the paper in the Coq proof assistant.
@article{paperbot1187,
title = {Distributed causal memory: modular specification and verification in higher-order distributed separation logic},
author = {Léon Gondelman and Simon Oddershede Gregersen and Abel Nieto and Amin Timany and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434323}
}