Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Verified High-Performance Composable Object Library for Remote Direct Memory Access (Extended Version)

Guillaume Ambal, George Hodgkins, Mark Madler, Gregory Chockler, Brijesh Dongol, Joseph Izraelevitz, Azalea Raad, Viktor Vafeiadis

TL;DR

The paper tackles the challenge of building verifiable, high-performance RDMA-based libraries by introducing LOCO, a library of composable, distributed objects, and Mowgli, a modular framework for formal verification across weak memory models. LOCO demonstrates how simple primitives (shared variables, barriers, and ring buffers) can be composed to implement higher-level services such as a linearisable key-value store and a distributed DC/DC controller, all with formal correctness proofs. The rdmawait memory model provides a robust foundation for reasoning about inter-node synchronization, while Mowgli enables locality-based proofs and compositional reasoning across multiple libraries and clients. Empirical results show LOCO can match or exceed OpenMPI performance in certain scenarios (notably ring buffers) while offering verified safety guarantees, underscoring the practical impact of combining formal methods with RDMA-based designs.

Abstract

Remote Direct Memory Access (RDMA) is a memory technology that allows remote devices to directly write to and read from each other's memory, bypassing components such as the CPU and operating system. This enables low-latency high-throughput networking, as required for many modern data centres, HPC applications and AI/ML workloads. However, baseline RDMA comprises a highly permissive weak memory model that is difficult to use in practice and has only recently been formalised. In this paper, we introduce the Library of Composable Objects (LOCO), a formally verified library for building multi-node objects on RDMA, filling the gap between shared memory and distributed system programming. LOCO objects are well-encapsulated and take advantage of the strong locality and the weak consistency characteristics of RDMA. They have performance comparable to custom RDMA systems (e.g. distributed maps), but with a far simpler programming model amenable to formal proofs of correctness. To support verification, we develop a novel modular declarative verification framework, called Mowgli, that is flexible enough to model multinode objects and is independent of a memory consistency model. We instantiate Mowgli with the RDMA memory model, and use it to verify correctness of LOCO libraries.

A Verified High-Performance Composable Object Library for Remote Direct Memory Access (Extended Version)

TL;DR

The paper tackles the challenge of building verifiable, high-performance RDMA-based libraries by introducing LOCO, a library of composable, distributed objects, and Mowgli, a modular framework for formal verification across weak memory models. LOCO demonstrates how simple primitives (shared variables, barriers, and ring buffers) can be composed to implement higher-level services such as a linearisable key-value store and a distributed DC/DC controller, all with formal correctness proofs. The rdmawait memory model provides a robust foundation for reasoning about inter-node synchronization, while Mowgli enables locality-based proofs and compositional reasoning across multiple libraries and clients. Empirical results show LOCO can match or exceed OpenMPI performance in certain scenarios (notably ring buffers) while offering verified safety guarantees, underscoring the practical impact of combining formal methods with RDMA-based designs.

Abstract

Remote Direct Memory Access (RDMA) is a memory technology that allows remote devices to directly write to and read from each other's memory, bypassing components such as the CPU and operating system. This enables low-latency high-throughput networking, as required for many modern data centres, HPC applications and AI/ML workloads. However, baseline RDMA comprises a highly permissive weak memory model that is difficult to use in practice and has only recently been formalised. In this paper, we introduce the Library of Composable Objects (LOCO), a formally verified library for building multi-node objects on RDMA, filling the gap between shared memory and distributed system programming. LOCO objects are well-encapsulated and take advantage of the strong locality and the weak consistency characteristics of RDMA. They have performance comparable to custom RDMA systems (e.g. distributed maps), but with a far simpler programming model amenable to formal proofs of correctness. To support verification, we develop a novel modular declarative verification framework, called Mowgli, that is flexible enough to model multinode objects and is independent of a memory consistency model. We instantiate Mowgli with the RDMA memory model, and use it to verify correctness of LOCO libraries.

Paper Structure

This paper contains 85 sections, 21 theorems, 42 equations, 25 figures.

Table of Contents

  1. Introduction
  2. LOCO
  3. MOWGLI
  4. Contributions
  5. Overview of LOCO and MOWGLI
  6. The rdmawait Memory Model
  7. LOCO Libraries
  8. Shared Variable Library (sv, \ref{['sec:brlib']})
  9. Barrier Library (bal, \ref{['sec:balib']})
  10. Ring Buffer Library (rbl, \ref{['sec:rblib']})
  11. Mixed-Size Writes (msw, \ref{['sec:msw']})
  12. LOCO API Example
  13. LOCO-Based Applications
  14. Towards a Modular Verification Framework for LOCO
  15. Lack of Causality
  16. ...and 70 more sections

Key Result

lemma 1

Given $\widetilde{\mathsf{p}}$ on library $L$ and a well-defined implementation $I$ of $L$, if $\langle{\widetilde{v}, G}\rangle \in \llbracket \llfloor \widetilde{\mathsf{p}} \rrfloor_{I} \rrbracket$ then there exists $\langle{\widetilde{v}, G'}\rangle \in \llbracket \widetilde{\mathsf{p}} \rrbrack

Figures (25)

  • Figure 1: Overview of proofs
  • Figure 2: Polling under rdmatso
  • Figure 3: Waiting under rdmawait
  • Figure 4: Preventing RDMA store buffering
  • Figure 5: Using $\mathtt{GF}_{\textsc{sv}\xspace}$
  • ...and 20 more figures

Theorems & Definitions (38)

  • definition 1
  • definition 2
  • definition 3
  • definition 4
  • definition 5
  • definition 6: sv-consistency
  • definition 7
  • definition 8
  • definition 9
  • lemma 1
  • ...and 28 more