On the Verification Problem of Remote Direct Memory Access programs (Extended Version with Appendix)

TL;DR

This paper investigates the reachability and robustness of RDMA programs, proving undecidability in general for reachability and decidability for robustness, with precise complexity bounds.

Contribution

It establishes the undecidability of reachability in RDMA programs and provides a decision procedure for robustness with tight complexity bounds.

Findings

Reachability is undecidable for RDMA programs.

Robustness verification is decidable for RDMA programs.

Complexity bounds are EXPSPACE and PSPACE, and are proven optimal.

Abstract

Remote Direct Memory Access (RDMA) is a technology that allows direct memory access from the memory of one computer into that of another without involving either one's operating system. This enables high-throughput, low-latency networking, which is especially useful in massively parallel computer clusters. In this paper, we study the reachability and robustness problems for RDMA programs. We show that reachability is undecidable in general, even for a restricted fragment of the model. We then focus on robustness, which asks whether a program exhibits the same behaviours under the RDMA and sequential consistency (SC) semantics, and prove that this problem is decidable. Our central technical result establishes a normal form for robustness violations, showing that any non-robust program admits a violating execution of a specific form. We then leverage this normal form to obtain a decision procedure that reduces robustness to reachability in finite-state programs with counters, yielding an EXPSPACE upper bound in the general case, and a PSPACE upper bound in the absence of poll operations. Finally, we also show that both of these bounds are optimal.