Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic

Jun 15 11:00 ₂₀₂₁

Abstract: In this presentation we are going to talk about modular specification and verification of causally-consistent distributed database, a data structure that guarantees causal consistency among replicas of the database.

With causal consistency, different replicas can observe different data on the same key, yet it is guaranteed that all data are observed in a causally related order: if a node {$N$} observes an update {$X$} originating at node {$M$}, then node {$N$} must have also observed the effects of any other update {$Y$} that took place on node {$M$} before {$X$}. Causal consistency can, for instance, be used to ensure in a distributed messaging application that a reply to a message is never seen before the message itself.

We will see how one can specify and verify a concrete implementation of such a distributed data structure in a way that supports modular verification of full functional correctness properties of clients and servers. Our approach is conducted using Aneris, a higher-order distributed separation logic for an ML-like programming language with network primitives for programming distributed systems. All the results of that work are formalized in the Coq proof assistant using the Aneris/Iris infrastructure and are presented in the paper.