Title: A Verified High-Performance Composable Object Library for Remote Direct Memory Access (Extended Version) Show Chinese title

Title: 用于远程直接内存访问的经过验证的高性能可组合对象库（扩展版本）

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. Show Chinese abstract

Abstract: 远程直接内存访问（RDMA）是一种内存技术，允许远程设备直接写入和读取彼此的内存，绕过CPU和操作系统等组件。 这使得低延迟高吞吐量的网络成为可能，这是许多现代数据中心、高性能计算（HPC）应用和人工智能/机器学习（AI/ML）工作负载所要求的。 然而，基本的RDMA包含一个高度宽松的弱内存模型，在实践中难以使用，直到最近才被形式化。 在本文中，我们介绍了可组合对象库（LOCO），这是一个经过形式验证的库，用于在RDMA上构建多节点对象，填补了共享内存和分布式系统编程之间的空白。 LOCO对象具有良好的封装性，并利用了RDMA的强局部性和弱一致性特性。 它们的性能与定制的RDMA系统（例如分布式映射）相当，但编程模型要简单得多，适合进行正确性的形式证明。 为了支持验证，我们开发了一个新颖的模块化声明式验证框架，称为Mowgli，该框架足够灵活，可以建模多节点对象，并且独立于内存一致性模型。 我们将Mowgli实例化为RDMA内存模型，并用它来验证LOCO库的正确性。