A Verified High-Performance Composable Object Library for Remote Direct Memory Access
summary
LOCO is a verified C++ RDMA object library that implements ring buffers, barriers and a key‑value store atop a single-thread manager for hardware completion, and it claims performance that matches or beats specialized RDMA systems and Redis in benchmarks. A new declarative verification framework, Mowgli, plus a local‑soundness meta‑theorem lets implementations be proved correct against RDMA’s weak ordering without redoing whole‑system proofs. The team verifies many library layers and attributes improved latency to an optimized polling backend.
AI-written summary · about
chapters (9)
- 0:00RDMA introduction and challenges
- 3:58Problems with RDMA libraries
- 5:01Mowgli framework introduction
- 7:29Formalizing ring buffers
- 10:16Dependency cycles in execution
- 12:45Hardware behaviors in Mowgli
- 14:51Verifying implementations
- 17:44Results and contributions
- 18:47Q&A
related talks
28mLLOR: Automated Repair of OpenMP Programs
55m“A lock-free concurrency toolkit for deferred reclamation and optimistic speculation"
15mCosmo: A Concurrent Separation Logic for Multicore Ocaml
23mAn Operational Approach to Library Abstraction under Relaxed Memory Concurrency
55m “High Performance C++ Concurrent Transactional Data Structures"
19mVerifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
21mMechanized Verification of a Fine-Grained Concurrent Queue from Meta's Folly Libr