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{TSO}}_{\text{RMW}}\), 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{WAIT}}_{\text{RMW}}\) library. Underpinned by \(\text{RDMA}^{\text{WAIT}}_{\text{RMW}}\), 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{SC}}_{\text{RMW}}\), 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.