一句话：为 x86-TSO 上的 RDMA 并发程序提出三个等价形式模型，填补语义基础空白。
论文解决 RDMA 虽有广泛实践与研究但缺少规定现代多核架构上并发 RDMA 程序允许行为的形式模型的问题。作者在 x86-TSO 机器上建立 RDMA 的语义基础，提出三个等价形式模型：两个不同抽象层次的操作式模型和一个声明式模型，并证明三者等价。为增强可信度，更具体的操作式模型经 NVIDIA 专家审阅，声明式形式化则通过大量微妙 litmus 测试进行经验验证。该工作为基于 RDMA 的系统提供语言级模型、验证其硬件映射以及开发并发 RDMA 程序推理技术迈出必要的第一步。
Remote direct memory access (RDMA) is a modern technology enabling networked machines to exchange information without involving the operating system of either side, and thus significantly speeding up data transfer in computer clusters. While RDMA is extensively used in practice and studied in various research papers, a formal underlying model specifying the allowed behaviours of concurrent RDMA programs running in modern multicore architectures is still missing. This paper aims to close this gap and provide semantic foundations of RDMA on x86-TSO machines. We propose three equivalent formal models, two operational models in different levels of abstraction and one declarative model, and prove that the three characterisations are equivalent. To gain confidence in the proposed semantics, the more concrete operational model has been reviewed by NVIDIA experts, a major vendor of RDMA systems, and we have empirically validated the declarative formalisation on various subtle litmus tests by extensive testing. We believe that this work is a necessary initial step for formally addressing RDMA-based systems by proposing language-level models, verifying their mapping to hardware, and developing reasoning techniques for concurrent RDMA programs.
@article{AmbalDEK0R24,
title = {Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures},
author = {Guillaume Ambal and Brijesh Dongol and Haggai Eran and Vasileios Klimis and Ori Lahav and Azalea Raad},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689781}
}