Sufficient Conditions for Robustness of RDMA Programs
Abstract
Remote Direct Memory Access (RDMA) is a modern technology enabling high-performance inter-node communication. Despite its widespread adoption, theoretical understanding of permissible behaviours remains limited, as RDMA follows a very weak memory model. This paper addresses the challenge of establishing sufficient conditions for RDMA robustness. We introduce a set of straightforward criteria that, when met, guarantee sequential consistency and mitigate potential issues arising from weak memory behaviours in RDMA applications. Notably, when restricted to a tree topology, these conditions become even more relaxed, significantly reducing the need for synchronisation primitives. This work provides developers with practical guidelines to ensure the reliability and correctness of their RDMA-based systems.
Paper
-
Sufficient Conditions for Robustness of RDMA Programs, ESOP 2025
Guillaume Ambal, Ori Lahav and Azalea Raad
[Paper] [Extended Version]
People
- Guillaume Ambal (Imperial College London)
- Ori Lahav (Tel Aviv University)
- Azalea Raad (Imperial College London)