Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA(…)
summary
Claims a first formal semantics for RDMA on x86‑TSO: three equivalent models (two operational at different abstraction levels, one declarative), with a machine‑checked style paper proof of equivalence. Implements a concrete operational model reviewed by NVIDIA experts and validates the declarative model by running litmus tests on InfiniBand and RoCE hardware. Finds no forbidden hardware behaviors and shows many weak reorderings occur under stress; poll synchronisation and explicit waits are required to prevent surprising reordering.
AI-written summary · about
chapters (11)
- 0:00RDMA introduction and motivation
- 2:07Low-latency RDMA communication
- 4:56RDMA reordering explained
- 7:05RDMA threads and nodes interactions
- 8:50Formal RDMA semantics models
- 12:01Testing RDMA on hardware
- 13:25Summary of RDMA semantics
- 14:07Future RDMA applications
- 15:13RDMA error handling
- 16:17Dynamic RDMA node changes
- 17:02Equivalence proof of RDMA semantics
related talks
18mRDMA is Turing complete, we just did not know it yet!
12mPreview: Networking
28mPersistent Memory plus RDMA, new age remote device
14mUnderstanding RDMA Microarchitecture Resources for Performance Isolation
12mCharacterizing and Optimizing Remote Persistent Memory with RDMA and NVM
18mFileMR: Rethinking RDMA Networking for Scalable Persistent Memory
15mSecuring RDMA for High-Performance Datacenter Storage Systems
23mTeRM: Extending RDMA-Attached Memory with SSD