Algorithmic Structure in Weak Memory and RDMA Verification

Weak memory models invalidate many classical assumptions underlying program verification, giving rise to subtle and often infinite-state behaviours. In this talk, I present structural and algorithmic approaches to analysing such systems.

First, I discuss a game-theoretic formulation of concurrent programs under Total Store Order (TSO), separating program control from memory nondeterminism. This perspective yields finite-state behaviour for reachability and safety under adversarial scheduling, while natural fairness assumptions restore undecidability.

Second, I consider Remote Direct Memory Access (RDMA), a high-performance communication model with even more pronounced weak memory effects. Although reachability is undecidable, I show that robustness — equivalence with sequential consistency — is decidable via a normal form theorem for violations, leading to tight ExpSpace and PSpace complexity bounds.

The results illustrate how structural insights can clarify the algorithmic and complexity landscape of modern weak memory models.

Bio

Stephan Spengler is a PhD candidate in Computer Science at Uppsala University, working in the area of algorithmic verification of concurrent systems under weak memory models. His research focuses on structural and complexity-theoretic aspects of weak memory semantics, including game-theoretic formulations of TSO and verification problems for RDMA. Previously, he worked in combinatorial optimisation and graph theory, and he remains broadly interested in foundational questions in theoretical computer science, particularly the algorithmic structure and complexity of concurrent systems.