This program is tentative and subject to change.

Fri 25 Oct 2024 17:00 - 17:20 at San Gabriel - Memory Management and Analysis 2

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.

This program is tentative and subject to change.

Fri 25 Oct

Displayed time zone: Pacific Time (US & Canada) change

16:00 - 17:40
Memory Management and Analysis 2OOPSLA 2024 at San Gabriel
16:00
20m
Talk
Mark--Scavenge: Waiting for Trash to Take Itself Out
OOPSLA 2024
Jonas Norlinder Uppsala University, Erik Ă–sterlund Oracle, David Black-Schaffer Uppsala University, Tobias Wrigstad Uppsala University
16:20
20m
Talk
Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations
OOPSLA 2024
Luke Geeson University College London, James Brotherston , Wilco Dijkstra Arm Ltd, Alastair F. Donaldson Imperial College London, Lee Smith Arm, Tyler Sorensen University of California at Santa Cruz, John Wickerson Imperial College London
16:40
20m
Talk
PROMPT: A Fast and Extensible Memory Profiling Framework
OOPSLA 2024
Ziyang Xu Princeton University, Yebin Chon Princeton University, Yian Su Northwestern University, Zujun Tan Princeton University, USA, Sotiris Apostolakis Google, Simone Campanoni Northwestern University, David I. August Princeton University
17:00
20m
Talk
Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures
OOPSLA 2024
Guillaume Ambal , Brijesh Dongol University of Surrey, Haggai Eran NVIDIA, Vasileios Klimis Queen Mary University of London, Ori Lahav Tel Aviv University, Azalea Raad Imperial College London
17:20
20m
Talk
StarMalloc: Verifying a Modern, Hardened Memory Allocator
OOPSLA 2024
Antonin Reitz Inria, Aymeric Fromherz Inria, Jonathan Protzenko Microsoft Azure Research