TY - GEN
T1 - Verifying a C Implementation of Derecho’s Coordination Mechanism Using VST and Coq
AU - Nagasamudram, Ramana
AU - Beringer, Lennart
AU - Birman, Ken
AU - Milano, Mae
AU - Naumann, David A.
N1 - Publisher Copyright:
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.
PY - 2024
Y1 - 2024
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85195517170&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85195517170&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-60698-4_6
DO - 10.1007/978-3-031-60698-4_6
M3 - Conference contribution
AN - SCOPUS:85195517170
SN - 9783031606977
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 99
EP - 117
BT - NASA Formal Methods - 16th International Symposium, NFM 2024, Proceedings
A2 - Benz, Nathaniel
A2 - Gopinath, Divya
A2 - Shi, Nija
T2 - 16th International Symposium on NASA Formal Methods, NFM 2024
Y2 - 4 June 2024 through 6 June 2024
ER -