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.