Specifying and Verifying RDMA Synchronisation (Extended Version)
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866914282801725440 |
|---|---|
| author | Ambal, Guillaume Stupple, Max Dongol, Brijesh Raad, Azalea |
| author_facet | Ambal, Guillaume Stupple, Max Dongol, Brijesh Raad, Azalea |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_14642 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Specifying and Verifying RDMA Synchronisation (Extended Version) Ambal, Guillaume Stupple, Max Dongol, Brijesh Raad, Azalea Distributed, Parallel, and Cluster Computing Logic in Computer Science Systems and Control 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. |
| title | Specifying and Verifying RDMA Synchronisation (Extended Version) |
| topic | Distributed, Parallel, and Cluster Computing Logic in Computer Science Systems and Control |
| url | https://arxiv.org/abs/2601.14642 |