一句话：提出经形式化验证的 RDMA 多节点可组合对象库 LOCO，并给出内存模型无关的模块化验证框架 Mowgli。
RDMA 允许远程设备绕过 CPU 与操作系统直接读写彼此内存，是数据中心、HPC 与 AI/ML 负载所需低延迟高吞吐网络的基础。但 RDMA 的弱内存模型极为宽松、难以使用，且直到近期才被形式化。本文提出 LOCO（Library of Composable Objects），一个用于在 RDMA 上构建多节点对象的形式化验证库，填补共享内存与分布式系统编程之间的空白。LOCO 对象封装良好，充分利用 RDMA 的强局部性与弱一致性，性能可与定制 RDMA 系统（如分布式 map）相当，但编程模型更简单且可进行形式化正确性证明。为支持验证，作者开发了模块化声明式验证框架 Mowgli，可建模多节点对象且独立于内存一致性模型，并以 RDMA 内存模型实例化，用于验证 LOCO 库的正确性。
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.
@article{AmbalHMCDIRV26,
title = {A Verified High-Performance Composable Object Library for Remote Direct Memory Access},
author = {Guillaume Ambal and George Hodgkins and Mark Madler and Gregory Chockler and Brijesh Dongol and Joseph Izraelevitz and Azalea Raad and Viktor Vafeiadis},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776713}
}