{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:03:14Z","timestamp":1784793794056,"version":"3.55.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325181","type":"print"},{"value":"9783032325198","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>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\u2019s operating system. This enables high-throughput, low-latency networking, which is especially useful in massively parallel computer clusters.<\/jats:p>\n                  <jats:p>\n                    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\n                    <jats:sc>ExpSpace<\/jats:sc>\n                    upper bound in the general case, and a\n                    <jats:sc>PSpace<\/jats:sc>\n                    upper bound in the absence of poll operations. Finally, we also show that both of these bounds are optimal.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32519-8_6","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:18:29Z","timestamp":1784791109000},"page":"113-135","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["On the\u00a0Verification Problem of\u00a0Remote Direct Memory Access Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6832-6611","authenticated-orcid":false,"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8229-3481","authenticated-orcid":false,"given":"Mohamed Faouzi","family":"Atig","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1634-5893","authenticated-orcid":false,"given":"Govind","family":"Rajanbabu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-5722-8843","authenticated-orcid":false,"given":"Stephan","family":"Spengler","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Arora, J., Atig, M.F., Krishna, S.N.: Verification of programs under the release-acquire semantics. In: PLDI, pp. 1117\u20131132. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314649","DOI":"10.1145\/3314221.3314649"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-030-67087-0_4","volume-title":"Networked Systems","author":"PA Abdulla","year":"2021","unstructured":"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: Georgiou, C., Majumdar, R. (eds.) NETYS 2020. LNCS, vol. 12129, pp. 47\u201359. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-67087-0_4"},{"key":"6_CR3","doi-asserted-by":"publisher","unstructured":"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\u201332 (2021). https:\/\/doi.org\/10.1145\/3434337","DOI":"10.1145\/3434337"},{"key":"6_CR4","doi-asserted-by":"publisher","unstructured":"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\u20131212 (2024). https:\/\/doi.org\/10.1145\/3656425","DOI":"10.1145\/3656425"},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"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.\u00a059, pp. 5:1\u20135:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2016.5","DOI":"10.4230\/LIPIcs.CONCUR.2016.5"},{"key":"6_CR6","doi-asserted-by":"publisher","unstructured":"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\u201329. Springer, Cham (2021). https:\/\/doi.org\/10.26226\/morressier.604907f41a80aac83ca25d26","DOI":"10.26226\/morressier.604907f41a80aac83ca25d26"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-319-26850-7_2","volume-title":"Networked Systems","author":"PA Abdulla","year":"2015","unstructured":"Abdulla, P.A., Atig, M.F., Kara, A., Rezine, O.: Verification of buffered dynamic register automata. In: Bouajjani, A., Fauconnier, H. (eds.) NETYS 2015. LNCS, vol. 9466, pp. 15\u201331. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-26850-7_2"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-662-46669-8_13","volume-title":"Programming Languages and Systems","author":"PA Abdulla","year":"2015","unstructured":"Abdulla, P.A., Atig, M.F., Ngo, T.-P.: The best of both worlds: trading efficiency and optimality in fence insertion for TSO. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 308\u2013332. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_13"},{"key":"6_CR9","unstructured":"Abdulla, P.A., Atig, M.F., Rajanbabu, G., Spengler, S.: On the verification problem of remote direct memory access programs (extended version with appendix) (2026). https:\/\/arxiv.org\/abs\/2605.10631"},{"issue":"OOPSLA2","key":"6_CR10","doi-asserted-by":"publisher","first-page":"1982","DOI":"10.1145\/3689781","volume":"8","author":"G Ambal","year":"2024","unstructured":"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\u20132009 (2024). https:\/\/doi.org\/10.1145\/3689781","journal-title":"Proc. ACM Program. Lang."},{"key":"6_CR11","doi-asserted-by":"publisher","unstructured":"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\u201387. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-91118-7_3","DOI":"10.1007\/978-3-031-91118-7_3"},{"key":"6_CR12","doi-asserted-by":"publisher","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: POPL, pp. 7\u201318. ACM (2010). https:\/\/doi.org\/10.1145\/1706299.1706303","DOI":"10.1145\/1706299.1706303"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-642-28869-2_2","volume-title":"Programming Languages and Systems","author":"MF Atig","year":"2012","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: What\u2019s decidable about weak memory models? In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 26\u201346. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_2"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/978-3-642-37036-6_29","volume-title":"Programming Languages and Systems","author":"A Bouajjani","year":"2013","unstructured":"Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 533\u2013553. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_29"},{"key":"6_CR15","unstructured":"Bouajjani, A., Derevenetc, E., Meyer, R.: Robustness against relaxed memory models. In: Software Engineering. LNI, vol. P-227, pp. 85\u201386. GI (2014). https:\/\/dl.gi.de\/handle\/20.500.12116\/30973"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-642-22012-8_34","volume-title":"Automata, Languages and Programming","author":"A Bouajjani","year":"2011","unstructured":"Bouajjani, A., Meyer, R., M\u00f6hlmann, E.: Deciding robustness against total store ordering. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011. LNCS, vol. 6756, pp. 428\u2013440. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22012-8_34"},{"key":"6_CR17","doi-asserted-by":"publisher","unstructured":"Calin, G., Derevenetc, E., Majumdar, R., Meyer, R.: A theory of partitioned global address spaces. In: FSTTCS. LIPIcs, vol. 24, pp. 127\u2013139. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2013). https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2013.127","DOI":"10.4230\/LIPIcs.FSTTCS.2013.127"},{"issue":"1&2","key":"6_CR18","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/0304-3975(94)00231-7","volume":"147","author":"A Cheng","year":"1995","unstructured":"Cheng, A., Esparza, J., Palsberg, J.: Complexity results for 1-safe nets. Theor. Comput. Sci. 147(1&2), 117\u2013136 (1995). https:\/\/doi.org\/10.1016\/0304-3975(94)00231-7","journal-title":"Theor. Comput. Sci."},{"key":"6_CR19","doi-asserted-by":"publisher","unstructured":"Dan, A.M., Lam, P., Hoefler, T., Vechev, M.T.: Modeling and analysis of remote memory access programming. In: OOPSLA, pp. 129\u2013144. ACM (2016). https:\/\/doi.org\/10.1145\/2983990.2984033","DOI":"10.1145\/2983990.2984033"},{"key":"6_CR20","unstructured":"Derevenetc, E.: Robustness against Relaxed Memory Models. Ph.D. thesis, University of Kaiserslautern (2015). https:\/\/nbn-resolving.org\/urn:nbn:de:hbz:386-kluedo-40743"},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-662-43951-7_14","volume-title":"Automata, Languages, and Programming","author":"E Derevenetc","year":"2014","unstructured":"Derevenetc, E., Meyer, R.: Robustness against power is PSpace-complete. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014. LNCS, vol. 8573, pp. 158\u2013170. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-43951-7_14"},{"key":"6_CR22","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0304-3975(79)90041-0","volume":"8","author":"JE Hopcroft","year":"1979","unstructured":"Hopcroft, J.E., Pansiot, J.: On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci. 8, 135\u2013159 (1979). https:\/\/doi.org\/10.1016\/0304-3975(79)90041-0","journal-title":"Theor. Comput. Sci."},{"key":"6_CR23","doi-asserted-by":"publisher","unstructured":"Lahav, O., Boker, U.: What\u2019s decidable about causally consistent shared memory? ACM Trans. Program. Lang. Syst. 44(2), 8:1\u20138:55 (2022). https:\/\/doi.org\/10.1145\/3505273","DOI":"10.1145\/3505273"},{"key":"6_CR24","unstructured":"Lipton, R.J.: The reachability problem requires exponential space. Research report (Yale University. Department of Computer Science), Department of Computer Science, Yale University (1976). https:\/\/books.google.de\/books?id=7iSbGwAACAAJ"},{"issue":"4","key":"6_CR25","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1090\/S0002-9904-1946-08555-9","volume":"52","author":"EL Post","year":"1946","unstructured":"Post, E.L.: A variant of a recursively unsolvable problem. Bull. Am. Math. Soc. 52(4), 264\u2013268 (1946). https:\/\/doi.org\/10.1090\/S0002-9904-1946-08555-9","journal-title":"Bull. Am. Math. Soc."},{"key":"6_CR26","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(78)90036-1","volume":"6","author":"C Rackoff","year":"1978","unstructured":"Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6, 223\u2013231 (1978). https:\/\/doi.org\/10.1016\/0304-3975(78)90036-1","journal-title":"Theor. Comput. Sci."},{"key":"6_CR27","doi-asserted-by":"publisher","unstructured":"Singh, A.K., Lahav, O.: Decidable verification under localized release-acquire concurrency. In: TACAS (3). Lecture Notes in Computer Science, vol. 14572, pp. 235\u2013254. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_12","DOI":"10.1007\/978-3-031-57256-2_12"},{"issue":"3","key":"6_CR28","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733\u2013749 (1985). https:\/\/doi.org\/10.1145\/3828.3837","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32519-8_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:18:31Z","timestamp":1784791111000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32519-8_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325181","9783032325198"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32519-8_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"Our prototype, along with the litmus tests used, is publicly available at\n                      \n                      .","order":2,"name":"Ethics","label":"Data-Availability Statement","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}