Distributed causal memory: Modular specification and verification in higher-order distributed separation logic

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

DOI

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.

Original languageEnglish
Article number42
JournalProceedings of the ACM on Programming Languages
Volume5
IssuePOPL
Number of pages29
DOIs
Publication statusPublished - Jan 2021

Bibliographical note

Funding Information:
This work was supported in part by a Villum Investigator grant (no. 25804), Center for Basic Research in Program Verification (CPV), from the VILLUM Foundation.

Publisher Copyright:
© 2021 Owner/Author.

Copyright:
Copyright 2021 Elsevier B.V., All rights reserved.

    Research areas

  • causal consistency, concurrency, Distributed systems, formal verification, higher-order logic, separation logic

See relations at Aarhus University Citationformats

ID: 208206280