Verifying a C Implementation of Derecho’s Coordination Mechanism Using VST and Coq

Ramana Nagasamudram, Lennart Beringer, Ken Birman, Mae Milano, David A. Naumann

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

Derecho is a C++ framework for distributed programming leveraging high performance communication primitives such as RDMA. At its core is the shared state table (SST), a replicated data structure that supports efficient protocols for consensus and group membership. Our aim is to formalize the reasoning principles articulated by the designers, which focus on knowledge and monotonicity, as basis for highly assured high performance distributed applications. To this end we develop a high level model that exposes the SST principles in an application-friendly way. We use the model to specify and verify a re-implementation in C of the SST API. We validate the specifications by verifying simple applications that embody key parts of the Derecho protocols. The development is carried out using VST and Coq. This lays groundwork for verification of the full Derecho protocols and applications built on them.

Original languageEnglish
Title of host publicationNASA Formal Methods - 16th International Symposium, NFM 2024, Proceedings
EditorsNathaniel Benz, Divya Gopinath, Nija Shi
Pages99-117
Number of pages19
DOIs
StatePublished - 2024
Event16th International Symposium on NASA Formal Methods, NFM 2024 - Moffett Field, United States
Duration: 4 Jun 20246 Jun 2024

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume14627 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference16th International Symposium on NASA Formal Methods, NFM 2024
Country/TerritoryUnited States
CityMoffett Field
Period4/06/246/06/24

Fingerprint

Dive into the research topics of 'Verifying a C Implementation of Derecho’s Coordination Mechanism Using VST and Coq'. Together they form a unique fingerprint.

Cite this