arxiv: 2605.10631 · v1 · submitted 2026-05-11 · 💻 cs.LO

Recognition: no theorem link

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

Parosh Aziz Abdulla , Mohamed Faouzi Atig , Govind Rajanbabu , Stephan Spengler

Authors on Pith no claims yet

Pith reviewed 2026-05-12 05:17 UTC · model grok-4.3

classification 💻 cs.LO

keywords RDMAremote direct memory accessrobustnesssequential consistencyreachabilityundecidabilityverificationcomplexity

0 comments

The pith

RDMA programs have undecidable reachability but decidable robustness to sequential consistency.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that determining whether an RDMA program can reach a particular state is undecidable, even when restricted to simple fragments of the model. It then proves that checking robustness, which asks if the program exhibits exactly the same behaviors under RDMA as under sequential consistency, is decidable. The central technical step is a normal form result establishing that any robustness violation admits an execution of a specific restricted shape. This normal form reduces the robustness question to reachability in finite-state programs equipped with counters. The reduction yields an EXPSPACE decision procedure in the general case and a PSPACE procedure when poll operations are absent, with both bounds shown to be tight.

Core claim

Reachability is undecidable for RDMA programs even in restricted fragments. Robustness is decidable because any non-robust program admits a violating execution of a specific normal form; this form allows reduction of robustness to reachability in finite-state programs with counters, producing an EXPSPACE upper bound in general and a PSPACE upper bound without poll operations, with matching lower bounds.

What carries the argument

The normal form for robustness violations, which forces any violating execution into a specific restricted shape that can be checked via reachability in counter programs.

Load-bearing premise

The operational semantics used for RDMA operations correctly capture all possible behaviors of actual hardware without omitting cases that would require separate handling.

What would settle it

A concrete RDMA program with a robustness violation whose shortest violating execution fails to match the normal form would refute the central technical result.

Figures

Figures reproduced from arXiv: 2605.10631 by Govind Rajanbabu, Mohamed Faouzi Atig, Parosh Aziz Abdulla, Stephan Spengler.

**Figure 1.** Figure 1: The PCP program. The idea is that process P1 guesses a solution of PCP, which is a sequence of indices i1, i2, . . . , ik, and sends the guessed indices to both P2 and P3. For each received index i, process P2 (P3) sends the letters of ui (vi) to process P4. Process P4 checks that the sequences of letters received from P2 and P3 are identical. In order to implement this idea, we need to ensure that the s… view at source ↗

**Figure 2.** Figure 2: Message loss due to unsynchronised reads. [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗

**Figure 3.** Figure 3: The Alternating Bit Protocol [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗

**Figure 4.** Figure 4: The relations ippo and oppo as subsets of po [PITH_FULL_IMAGE:figures/full_fig_p009_4.png] view at source ↗

**Figure 5.** Figure 5: The RDMA code fragment corresponding to VASS transitions incrementing (left) and decrementing (right) a counter c. More precisely, for each transition t = (q, c, j, q′ ) ∈ T, the leader uses the code fragment given in [PITH_FULL_IMAGE:figures/full_fig_p019_5.png] view at source ↗

**Figure 6.** Figure 6: Nodes, variables, processes and data flow in the RDMA program. [PITH_FULL_IMAGE:figures/full_fig_p023_6.png] view at source ↗

**Figure 7.** Figure 7: Process P1 1: ( 2: B1 + B2 + · · · + BN 3: x1 := ⊥ 4: assume(f1 = ⊤) 5: assume(f1 = ⊥) 6: f1 := ⊤ 7: assume(x1 = ⊥) 8: ) + 9: assume(x1 = #) 10: assume(f1 = ⊥) 11: y¯1 := # (a) main routine 1: assume(x1 = i) 2: y¯1 := ui,1 3: g¯1 := ⊤ 4: y¯1 := ui,2 5: g¯1 := ⊤ . . . . . . y¯1 := ui,|ui| g¯1 := ⊤ (b) subroutine Bi [PITH_FULL_IMAGE:figures/full_fig_p023_7.png] view at source ↗

**Figure 8.** Figure 8: Process P2 [PITH_FULL_IMAGE:figures/full_fig_p023_8.png] view at source ↗

**Figure 9.** Figure 9: Process P3 1: ( 2: Dσ1 + Dσ2 + · · · + Dσ|Σ| 3: y1 := ⊥ 4: assume(g1 = ⊥) 5: assume(g1 = ⊤) 6: g1 := ⊥ 7: assume(y1 = ⊥) 8: y2 := ⊥ 9: assume(g2 = ⊥) 10: assume(g2 = ⊤) 11: g2 := ⊥ 12: assume(y2 = ⊥) 13: ) + 14: assume(y1 = #) 15: assume(g1 = ⊥) 16: assume(y2 = #) 17: assume(g2 = ⊥) (a) main routine 1: assume(y1 = σ) 2: assume(y2 = σ) (b) subroutine Dσ [PITH_FULL_IMAGE:figures/full_fig_p024_9.png] view at source ↗

**Figure 10.** Figure 10: Process P4 [PITH_FULL_IMAGE:figures/full_fig_p024_10.png] view at source ↗

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

RDMA robustness is decidable with tight EXPSPACE/PSPACE bounds via a normal-form reduction to counter machines.

read the letter

The main thing to know is that the paper shows the robustness problem for RDMA programs is decidable, with matching EXPSPACE and PSPACE complexity bounds obtained by reducing to counter-machine reachability after establishing a normal form for violations. They first prove reachability undecidable even in a restricted fragment, which sets up the focus on robustness as the practical question worth solving. The normal form is the central technical step, and they use it to get a decision procedure plus optimality proofs for the bounds. That combination is what is actually new relative to earlier memory-model work. The paper does a clean job separating the undecidable general case from the decidable robustness case and showing how the normal form simplifies the search for violating executions. The reduction itself follows standard patterns but is applied specifically to RDMA operations like direct accesses and polls. The modeling assumptions and the completeness of the normal form are the places where a flaw could hide, but the abstract and claims give no sign of internal inconsistency or missing cases. The bounds being optimal is a positive sign that the reduction is tight rather than loose. One minor soft spot is that real hardware behavior might diverge from the operational semantics used, which could affect how far the decision procedure transfers to practice, though that is a common modeling issue rather than a logical gap. This paper is for researchers working on verification of relaxed-memory concurrent programs and high-performance networking. A reader who already knows counter-machine reachability and normal-form arguments in concurrency will get the most value and see exactly where the RDMA-specific contribution sits. It has enough formal grounding and non-trivial results to deserve a serious referee. I would send it out for peer review.

Referee Report

0 major / 1 minor

Summary. The paper studies verification of RDMA programs. It proves reachability is undecidable even for a restricted fragment. For robustness (whether RDMA executions match sequential consistency), it establishes a normal form for all violating executions, reduces the problem to reachability in finite-state counter machines, and derives tight EXPSPACE (general) and PSPACE (no poll operations) upper bounds that match lower bounds.

Significance. If the normal-form argument and reductions hold, the results supply the first decidability and tight complexity classification for robustness in RDMA, a practically important model for high-performance networking. The normal form is a reusable technical device, the reduction to known counter-machine problems is standard and clean, and the optimality proofs give a complete picture. These are genuine strengths for the verification community.

minor comments (1)

Abstract: a one-sentence description of the core RDMA operations (e.g., RDMA read/write, poll) would help readers immediately grasp the model without consulting the body.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary of our work on reachability and robustness for RDMA programs, and for recognizing the significance of the normal-form result and the tight complexity classification. The recommendation for minor revision is noted; however, the report contains no specific major comments or requested changes.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper establishes undecidability of reachability by reduction from a known undecidable problem, then derives a normal form for robustness violations directly from the RDMA operational semantics (showing every violating execution can be transformed into a specific shape), and finally reduces robustness checking to reachability in finite-state counter machines whose decidability and complexity are independently known. None of these steps is self-definitional, none renames a fitted parameter as a prediction, and no load-bearing premise rests on a self-citation chain; the normal form is proved rather than assumed, and the final bounds are obtained by standard complexity results external to the paper.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work relies on standard results from automata theory and complexity for the undecidability and upper-bound arguments; no new free parameters or invented entities are introduced in the abstract.

axioms (1)

standard math Standard undecidability of reachability in counter machines or similar models
Invoked to establish undecidability for the RDMA reachability problem

pith-pipeline@v0.9.0 · 5505 in / 1251 out tokens · 42104 ms · 2026-05-12T05:17:20.899611+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

27 extracted references · 27 canonical work pages

[1]

In: PLDI

Abdulla, P.A., Arora, J., Atig, M.F., Krishna, S.N.: Verification of programs under the release-acquire semantics. In: PLDI. pp. 1117–1132. ACM (2019). https: //doi.org/https://doi.org/10.1145/3314221.3314649

work page doi:10.1145/3314221.3314649 2019
[2]

In: NETYS

Abdulla, P.A., Atig, M.F., Bouajjani, A., Derevenetc, E., Leonardsson, C., Meyer, R.: On the state reachability problem for concurrent programs under power. In: NETYS. Lecture Notes in Computer Science, vol. 12129, pp. 47–59. Springer (2020). https://doi.org/https://doi.org/10.1007/978-3-030-67087-0_4

work page doi:10.1007/978-3-030-67087-0_4 2020
[3]

Abdulla, P.A., Atig, M.F., Bouajjani, A., Kumar, K.N., Saivasan, P.: Deciding reachability under persistent x86-tso. Proc. ACM Program. Lang.5(POPL), 1–32 (2021).https://doi.org/https://doi.org/10.1145/3434337

work page doi:10.1145/3434337 2021
[4]

Abdulla, P.A., Atig, M.F., Bouajjani, A., Kumar, K.N., Saivasan, P.: Verification under intel-x86 with persistency. Proc. ACM Program. Lang.8(PLDI), 1189–1212 (2024).https://doi.org/https://doi.org/10.1145/3656425

work page doi:10.1145/3656425 2024
[5]

In: CONCUR

Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: The benefits of duality in verifying concurrent programs under TSO. In: CONCUR. LIPIcs, vol. 59, pp. 5:1– 5:15. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik (2016).https://doi.org/ https://doi.org/10.4230/LIPIcs.CONCUR.2016.5

work page doi:10.4230/lipics.concur.2016.5 2016
[6]

In: ESOP

Abdulla, P.A., Atig, M.F., Godbole, A., Krishna, S., Vafeiadis, V.: The decidability of verification under PS 2.0. In: ESOP. Lecture Notes in Computer Science, vol. 12648, pp. 1–29. Springer (2021). https://doi.org/https://doi.org/10.26226/ morressier.604907f41a80aac83ca25d26

work page 2021
[7]

In: NETYS

Abdulla, P.A., Atig, M.F., Kara, A., Rezine, O.: Verification of buffered dy- namic register automata. In: NETYS. Lecture Notes in Computer Science, vol. 9466, pp. 15–31. Springer (2015). https://doi.org/https://doi.org/10. 1007/978-3-319-26850-7_2

work page 2015
[8]

In: ESOP

Abdulla, P.A., Atig, M.F., Phong, N.T.: The best of both worlds: Trading efficiency and optimality in fence insertion for TSO. In: ESOP. Lecture Notes in Computer Science, vol. 9032, pp. 308–332. Springer (2015). https://doi.org/https://doi. org/10.1007/978-3-662-46669-8_13

work page doi:10.1007/978-3-662-46669-8_13 2015
[9]

Ambal, G., Dongol, B., Eran, H., Klimis, V., Lahav, O., Raad, A.: Semantics of remote direct memory access: Operational and declarative models of RDMA on TSO architectures. Proc. ACM Program. Lang.8(OOPSLA2), 1982–2009 (2024). https://doi.org/https://doi.org/10.1145/3689781

work page doi:10.1145/3689781 1982
[10]

In: ESOP (1)

Ambal, G., Lahav, O., Raad, A.: Sufficient conditions for robustness of RDMA programs. In: ESOP (1). Lecture Notes in Computer Science, vol. 15694, pp. 56–87. Springer (2025). https://doi.org/https://doi.org/10.1007/ 978-3-031-91118-7_3

work page 2025
[11]

In: POPL

Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: POPL. pp. 7–18. ACM (2010). https: //doi.org/https://doi.org/10.1145/1706299.1706303

work page doi:10.1145/1706299.1706303 2010
[12]

Lecture Notes in Computer Science, vol

Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: What’s decidable about weak memory models? In: ESOP. Lecture Notes in Computer Science, vol. 7211, pp. 26–46. Springer (2012). https://doi.org/https://doi.org/10. 1007/978-3-642-28869-2_2

work page 2012
[13]

In: ESOP

Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: ESOP. Lecture Notes in Computer Science, vol. 7792, pp. 533–553. Springer (2013).https://doi.org/https://doi.org/10.1007/978-3-642-37036-6_29 22 P.A. Abdulla, M.F. Atig, G. Rajanbabu, S. Spengler

work page doi:10.1007/978-3-642-37036-6_29 2013
[14]

In: Software Engineering

Bouajjani, A., Derevenetc, E., Meyer, R.: Robustness against relaxed memory models. In: Software Engineering. LNI, vol. P-227, pp. 85–86. GI (2014), https: //dl.gi.de/handle/20.500.12116/30973

work page 2014
[15]

In: Aceto, L., Henzinger, M., Sgall, J

Bouajjani, A., Meyer, R., M¨ ohlmann, E.: Deciding robustness against total store ordering. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzer- land, July 4-8, 2011, Proceedings, Part II. Lecture Notes in Computer Science, vol. 6756, pp. 428–440. Springer (2011). ...

work page 2011
[16]

In: FSTTCS

Calin, G., Derevenetc, E., Majumdar, R., Meyer, R.: A theory of partitioned global address spaces. In: FSTTCS. LIPIcs, vol. 24, pp. 127–139. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik (2013).https://doi.org/https://doi.org/10. 4230/LIPIcs.FSTTCS.2013.127

work page 2013
[17]

Cheng, A., Esparza, J., Palsberg, J.: Complexity results for 1-safe nets. Theor. Comput. Sci.147(1&2), 117–136 (1995). https://doi.org/https://doi.org/10. 1016/0304-3975(94)00231-7

work page 1995
[18]

In: OOPSLA

Dan, A.M., Lam, P., Hoefler, T., Vechev, M.T.: Modeling and analysis of remote memory access programming. In: OOPSLA. pp. 129–144. ACM (2016). https: //doi.org/https://doi.org/10.1145/2983990.2984033

work page doi:10.1145/2983990.2984033 2016
[19]

Derevenetc, E.: Robustness against Relaxed Memory Models. Ph.D. thesis, Uni- versity of Kaiserslautern (2015), https://nbn-resolving.org/urn:nbn:de:hbz: 386-kluedo-40743

work page 2015
[20]

In: ICALP (2)

Derevenetc, E., Meyer, R.: Robustness against power is pspace-complete. In: ICALP (2). Lecture Notes in Computer Science, vol. 8573, pp. 158–170. Springer (2014). https://doi.org/https://doi.org/10.1007/978-3-662-43951-7_14

work page doi:10.1007/978-3-662-43951-7_14 2014
[21]

Hopcroft, J.E., Pansiot, J.: On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci.8, 135–159 (1979). https://doi.org/https: //doi.org/10.1016/0304-3975(79)90041-0

work page doi:10.1016/0304-3975(79)90041-0 1979
[22]

Lahav, O., Boker, U.: What’s decidable about causally consistent shared memory? ACM Trans. Program. Lang. Syst.44(2), 8:1–8:55 (2022). https://doi.org/https: //doi.org/10.1145/3505273

work page doi:10.1145/3505273 2022
[23]

Research report (Yale University

Lipton, R.J.: The reachability problem requires exponential space. Research report (Yale University. Department of Computer Science), Department of Computer Sci- ence, Yale University (1976), https://books.google.de/books?id=7iSbGwAACAAJ

work page 1976
[24]

Bulletin of the American Mathematical Society52(4), 264–268 (1946)

Post, E.L.: A variant of a recursively unsolvable problem. Bulletin of the American Mathematical Society52(4), 264–268 (1946). https://doi.org/https://doi.org/ 10.1090/S0002-9904-1946-08555-9

work page doi:10.1090/s0002-9904-1946-08555-9 1946
[25]

Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci.6, 223–231 (1978). https://doi.org/https://doi.org/10. 1016/0304-3975(78)90036-1

work page 1978
[26]

In: TACAS (3)

Singh, A.K., Lahav, O.: Decidable verification under localized release-acquire concurrency. In: TACAS (3). Lecture Notes in Computer Science, vol. 14572, pp. 235–254. Springer (2024). https://doi.org/https://doi.org/10.1007/ 978-3-031-57256-2_12

work page 2024
[27]

Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM32(3), 733–749 (Jul 1985). https://doi.org/https://doi.org/10.1145/ 3828.3837 On the Verification Problem of RDMA programs 23 A Program Code for the Undecidability Proof This section holds the full program code for each of the processes in the reduction from PCP to R...

work page arXiv 1985