A Verified High-Performance Composable Object Library for Remote Direct Memory Access (Extended Version)
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866918159197405184 |
|---|---|
| author | Ambal, Guillaume Hodgkins, George Madler, Mark Chockler, Gregory Dongol, Brijesh Izraelevitz, Joseph Raad, Azalea Vafeiadis, Viktor |
| author_facet | Ambal, Guillaume Hodgkins, George Madler, Mark Chockler, Gregory Dongol, Brijesh Izraelevitz, Joseph Raad, Azalea Vafeiadis, Viktor |
| contents | Remote Direct Memory Access (RDMA) is a memory technology that allows remote devices to directly write to and read from each other's memory, bypassing components such as the CPU and operating system. This enables low-latency high-throughput networking, as required for many modern data centres, HPC applications and AI/ML workloads. However, baseline RDMA comprises a highly permissive weak memory model that is difficult to use in practice and has only recently been formalised. In this paper, we introduce the Library of Composable Objects (LOCO), a formally verified library for building multi-node objects on RDMA, filling the gap between shared memory and distributed system programming. LOCO objects are well-encapsulated and take advantage of the strong locality and the weak consistency characteristics of RDMA. They have performance comparable to custom RDMA systems (e.g. distributed maps), but with a far simpler programming model amenable to formal proofs of correctness. To support verification, we develop a novel modular declarative verification framework, called Mowgli, that is flexible enough to model multinode objects and is independent of a memory consistency model. We instantiate Mowgli with the RDMA memory model, and use it to verify correctness of LOCO libraries. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_10531 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Verified High-Performance Composable Object Library for Remote Direct Memory Access (Extended Version) Ambal, Guillaume Hodgkins, George Madler, Mark Chockler, Gregory Dongol, Brijesh Izraelevitz, Joseph Raad, Azalea Vafeiadis, Viktor Programming Languages Distributed, Parallel, and Cluster Computing Logic in Computer Science Systems and Control Remote Direct Memory Access (RDMA) is a memory technology that allows remote devices to directly write to and read from each other's memory, bypassing components such as the CPU and operating system. This enables low-latency high-throughput networking, as required for many modern data centres, HPC applications and AI/ML workloads. However, baseline RDMA comprises a highly permissive weak memory model that is difficult to use in practice and has only recently been formalised. In this paper, we introduce the Library of Composable Objects (LOCO), a formally verified library for building multi-node objects on RDMA, filling the gap between shared memory and distributed system programming. LOCO objects are well-encapsulated and take advantage of the strong locality and the weak consistency characteristics of RDMA. They have performance comparable to custom RDMA systems (e.g. distributed maps), but with a far simpler programming model amenable to formal proofs of correctness. To support verification, we develop a novel modular declarative verification framework, called Mowgli, that is flexible enough to model multinode objects and is independent of a memory consistency model. We instantiate Mowgli with the RDMA memory model, and use it to verify correctness of LOCO libraries. |
| title | A Verified High-Performance Composable Object Library for Remote Direct Memory Access (Extended Version) |
| topic | Programming Languages Distributed, Parallel, and Cluster Computing Logic in Computer Science Systems and Control |
| url | https://arxiv.org/abs/2510.10531 |