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.

翻译：远程直接内存访问（RDMA）允许一台计算机直接读写远程计算机的内存，实现高吞吐、低延迟的数据传输。随着$\text{RDMA}^\text{TSO}$语义（描述基于TSO CPU的RDMA网络行为）的形式化，确保RDMA程序正确性才成为可能。然而，该语义目前缺乏远程同步的形式化定义，这意味着常见抽象（如锁）的实现无法被验证。本文通过提出$\text{RDMA}^{\text{TSO}}_{\text{RMW}}$——首个针对TSO架构的远程“读-修改-写”（RMW）指令语义模型，填补了这一空白。研究发现，远程RMW操作具有弱一致性，仅能保证相对于其他远程RMW操作的原子性。因此，我们以$\text{RDMA}^{\text{WAIT}}_{\text{RMW}}$库为基础，构建了一套可组合的同步抽象机制。基于$\text{RDMA}^{\text{WAIT}}_{\text{RMW}}$，我们进一步规范、实现并验证了适用于不同场景的三类远程锁。此外，我们提出了强RDMA模型$\text{RDMA}^{\text{SC}}_{\text{RMW}}$的概念，该模型类似于共享内存架构中的顺序一致性。我们开发的库与现有高性能库LOCO保持兼容，确保了可组合性与可验证性。