Specifying and Verifying RDMA Synchronisation (Extended Version)

Abstract

Remote direct memory access (RDMA) allows a machine to directly read from and write to the memory of remote machine, enabling high-throughput, low-latency data transfer. Ensuring correctness of RDMA programs has only recently become possible with the formalisation of ${\text{RDMA}}^{\text{TSO}}$ semantics (describing the behaviour of RDMA networking over a TSO CPU). However, this semantics currently lacks a formalisation of remote synchronisation, meaning that the implementations of common abstractions such as locks cannot be verified. In this paper, we close this gap by presenting ${\text{RDMA}}_{\text{RMW}}^{\text{TSO}}$, the first semantics for remote `read-modify-write' (RMW) instructions over TSO. It turns out that remote RMW operations are weak and only ensure atomicity against other remote RMWs. We therefore build a set of composable synchronisation abstractions starting with the ${\text{RDMA}}_{\text{RMW}}^{\text{WAIT}}$ library. Underpinned by ${\text{RDMA}}_{\text{RMW}}^{\text{WAIT}}$, we then specify, implement and verify three classes of remote locks that are suitable for different scenarios. Additionally, we develop the notion of a strong RDMA model, ${\text{RDMA}}_{\text{RMW}}^{\text{SC}}$, which is akin to sequential consistency in shared memory architectures. Our libraries are built to be compatible with an existing set of high-performance libraries called LOCO, which ensures compositionality and verifiability.

95 pages, extended version of ESOP 2026 paper, replaced to fix a tikz opacity problem