Algorithmic Structure in Weak Memory
and RDMA Verification





Stephan Spengler
Uppsala University, Sweden
10.03.2026

Introduction

Sequential Consistency

Total Store Order

TSO Games

Process Syntax


P ::= skip
    | P1 ; P2
    | P1 + P2
    | P*
    | x := v
    | assume(x == v)
    | mfence

Total Store Order Semantics

TSO Games

  • turn-based two-player game
  • process player: executes instructions
  • update player: updates buffer messages

  • reachability game: process player tries to reach target state(s)
  • safety game: process player tries to avoid target state(s)

TSO Games - Example 1

TSO Games - Example 1

TSO Games - Example 2

TSO Games - Example 2

Observations

  • process player: only plays in one process
  • update player: never updates any messages

  • analysis reduces to single-process programs
    • PSpace-complete

Adding Fairness

  • process player: only plays in one process

    Process Fairness:
    Every enabled process must eventually be executed.

  • update player: never updates any messages

    Update Fairness:
    Every buffer message must eventually be updated to the memory.

Update Fairness

Every buffer message must eventually be updated to the memory.

Show: TSO reachability games are undecidable
Idea: Reduction from Perfect Channel Systems
  • nondeterministic finite state automata augmented by FIFO channel
  • use TSO buffer to simulate channel
  • reduce PCS reachability (undecidable) to TSO reachability game
Perfect Channel System

Update Fairness - PCS Reduction

(
x := m1
x := m2
assume(y == m1)
assume(y == m2)
)*

((
assume(x == m1)
y := m1
)+(
assume(x == m2)
y := m2
))*
x = 0
y = 0
Memory

TSO Games with Fairness

  • Update Fairness:
    Every buffer message must eventually be updated to the memory.
    Theorem:
    Reachability games with update fairness are undecidable.
  • Process Fairness:
    Every enabled process must eventually be executed.
    Theorem:
    Safety games with process fairness are undecidable.

TSO Games - Conclusion

  • reachability and safety without fairness:
    • reduce to single-process programs → PSpace-complete
  • reachability with update fairness and safety with process fairness:
    • reduction from PCS reachability → undecidable
  • further work could consider other:
    • winning conditions
    • fairness conditions
    • memory models

Remote Direct Memory Access (RDMA)

Classical Data Flow

RDMA Data Flow

RDMA Queue Pairs

Ambal et al, 2024, Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures

RDMA Process Syntax


P ::= skip | P1 ; P2 | P1 + P2 | P*
    | x := vw | assume(x == vr)

    | x := y | y := x

    | rfence(n) | poll(n)

RDMA - Reachability


Show: RDMA reachability is undecidable
Idea: Reduction from Perfect Channel Systems
  • use RDMA queue pairs to simulate
    the channel
  • synchronisation (rfence, poll)
    not needed
Perfect Channel System

RDMA - Robustness


Robustness Problem:
Given an RDMA program,
for each execution of the program under RDMA semantics,
is there an execution of the program under SC semantics,
such that the behaviours are equivalent, meaning:
  • each read operation reads the same value
  • for each variable, all write operations are done in the same order

yes? → robust
no? → not robust

RDMA: Example Violation

x = 1
y = 0
Memory
y := w
z := x
x := 2
z = 0
w = 1
Memory

Normal Form Construction

  • requirement: minimal violation
    nrR(w, 1) lW(x, 2) nlR(x, 2) nrW(z, 2) nlW(y, 1)
  • identify and remove maximal event
    nrR(w, 1) nlR(x, 1) nrW(z, 1) nlW(y, 1)
  • order in a sequentially consistent way
    nrR(w, 1) nlW(y, 1) nlR(x, 1) nrW(z, 1)
  • reinsert maximal event
    nrR(w, 1) lW(x, 2) nlW(y, 1) nlR(x, 2) nrW(z, 2)
y := w
z := x
x := 2

Normal Form Structure

nrR(w, 1) lW(x, 2) nlR(x, 2) nrW(z, 2) nlW(y, 1) ⇓ nrR(w, 1) lW(x, 2) nlW(y, 1) nlR(x, 2) nrW(z, 2)

  • ⟨SC-consistent events⟩ ⟨maximal event⟩ ⟨SC-consistent events⟩
  • structured violation witness
  • greatly reduces search complexity
y := w
z := x
x := 2

Instrumentation

nrR(w, 1) lW(x, 2) nlW(y, 1) nlR(x, 2) nrW(z, 2)
  • instrumented program generates events in SC order
  • decides non-deterministically whether to put in 1st or 2nd part
    • preserves SC-consistency within parts
  • stops after guessing the maximal event
  • keeps track of:
    • RDMA-consistency
    • SC-consistency / violation
y := w
z := x
x := 2

Complexity Bounds


Theorem:
RDMA-robustness is ExpSpace-complete in the general case.


Theorem:
RDMA-robustness for programs without poll operations
is PSpace-complete.

Demo

Summary

Unifying Insights


  • Weak memory introduces new sources of nondeterminism.

  • Executions exhibit structural patterns.

  • Reduction to finite-state (or counter) systems.

Open Directions

  • Verification of parameterised RDMA programs
  • Synthesis under weak memory
  • Beyond RDMA: emerging hardware models
  • Optimisation-inspired abstractions
  • Quantitative aspects (cost, performance)

Key Takeaway



By identifying structural regularities in weak memory semantics, we can map precise decidability and complexity boundaries for modern concurrent systems.