{"ID":2856733,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2510.10531","arxiv_id":"2510.10531","title":"A Verified High-Performance Composable Object Library for Remote Direct Memory Access (Extended Version)","abstract":"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.","short_abstract":"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/M...","url_abs":"https://arxiv.org/abs/2510.10531","url_pdf":"https://arxiv.org/pdf/2510.10531v1","authors":"[\"Guillaume Ambal\",\"George Hodgkins\",\"Mark Madler\",\"Gregory Chockler\",\"Brijesh Dongol\",\"Joseph Izraelevitz\",\"Azalea Raad\",\"Viktor Vafeiadis\"]","published":"2025-10-12T10:12:16Z","proceeding":"cs.PL","tasks":"[\"cs.PL\",\"cs.DC\",\"cs.LO\",\"eess.SY\"]","methods":"[]","has_code":false}