@article{mowgli,
author = {Ambal, Guillaume and Hodgkins, George and Madler, Mark and Chockler, Gregory and Dongol, Brijesh and Izraelevitz, Joseph and Raad, Azalea and Vafeiadis, Viktor},
title = {A Verified High-Performance Composable Object Library for Remote Direct Memory Access},
year = {2026},
issue_date = {January 2026},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {10},
number = {POPL},
url = {https://doi.org/10.1145/3776713},
doi = {10.1145/3776713},
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.},
journal = {Proc. ACM Program. Lang.},
month = jan,
articleno = {71},
numpages = {32},
keywords = {Declarative Semantics, Distributed Computing, RDMA, Verification}
}