[Proof Complexity] MIAO seminar Tue Mar 10 at 14:00 CET with Stephan Spengler: Algorithmic structure in weak memory and RDMA verification

[Jakob Nordström]

Dear all,

We are happy to announce that next Tuesday March 10 at 14:00 CET we will have the opportunity to listen to a seminar with Stephan Spengler from Uppsala University, who will give a talk titled "Algorithmic structure in weak memory and RDMA verification". You find the abstract at the bottom of this message.

We will run this as a MIAO hybrid seminar at the University of Copenhagen. Local participants are warmly welcome to the new location of the Algorithms and Complexity Section at Vibenshuset, Lyngbyvej 2, while other participants are equally warmly welcome to join virtually at https://lu-se.zoom.us/j/61925271827 . Please feel free to share this information with colleagues who you think might be interested. We are also hoping to record the seminar and post on the MIAO Research YouTube channel https://youtube.com/@MIAOresearch for people who would like to hear the talk but cannot attend.

More information about the MIAO seminar series can be found at https://jakobnordstrom.se/miao-seminars/ . If you do not wish to receive these announcements, or receive several copies of them, please send a message to jn at di.ku.dk<mailto:jn at di.ku.dk>.

Best regards,
Jakob Nordström

**********

Tuesday Mar 10 at 14:00 at the Algorithms and Complexity Section at the University of Copenhagen, Vibenshuset, Lyngbyvej 2, and on Zoom
Algorithmic structure in weak memory and RDMA verification
(Stephan Spengler, Uppsala University)

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.


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +45 28 78 38 11 / +46 70 742 21 98
https://jakobnordstrom.se