{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T05:57:25Z","timestamp":1777874245026,"version":"3.51.4"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227195","type":"print"},{"value":"9783032227201","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-nc-nd\/4.0"},{"start":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T00:00:00Z","timestamp":1775779200000},"content-version":"vor","delay-in-days":99,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22720-1_3","type":"book-chapter","created":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T15:28:20Z","timestamp":1775748500000},"page":"42-71","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Specifying and Verifying RDMA Synchronisation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4667-7266","authenticated-orcid":false,"given":"Guillaume","family":"Ambal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-5603-7585","authenticated-orcid":false,"given":"Max","family":"Stupple","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0446-3507","authenticated-orcid":false,"given":"Brijesh","family":"Dongol","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2319-3242","authenticated-orcid":false,"given":"Azalea","family":"Raad","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,4,10]]},"reference":[{"key":"3_CR1","unstructured":"Aguilera, M.K., Ben-David, N., Guerraoui, R., Marathe, V.J., Xygkis, A., Zablotchi, I.: Microsecond consensus for microsecond applications. In: 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). pp. 599\u2013616. USENIX Association (Nov 2020), https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/aguilera"},{"key":"3_CR2","unstructured":"Alquraan, A., Udayashankar, S., Marathe, V., Wong, B., Al-Kiswany, S.: Lolkv: the logless, line the logless, linearizable, rdma-based key-value storage system arizable, rdma-based key-value storage system. In: Proceedings of the 21st USENIX Symposium on Networked Systems Design and Implementation. NSDI\u201924, USENIX Association, USA (2024)"},{"key":"3_CR3","doi-asserted-by":"publisher","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, https:\/\/doi.org\/10.1145\/3689781","DOI":"10.1145\/3689781"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Ambal, G., Hodgkins, G., Madler, M., Chockler, G., Dongol, B., Izraelevitz, J., Raad, A., Vafeiadis, V.: A verified high-performance composable object library for remote direct memory access. Proc. ACM Program. Lang. 10(POPL) (Jan 2026). https:\/\/doi.org\/10.1145\/3776713, https:\/\/doi.org\/10.1145\/3776713","DOI":"10.1145\/3776713"},{"key":"3_CR5","doi-asserted-by":"publisher","unstructured":"Ambal, G., Lahav, O., Raad, A.: Sufficient conditions for robustness of RDMA programs. In: Vafeiadis, V. (ed.) Programming Languages and Systems - 34th European Symposium on Programming, ESOP 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part I. Lecture Notes in Computer Science, vol. 15694, pp. 56\u201387. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-91118-7_3, https:\/\/doi.org\/10.1007\/978-3-031-91118-7_3","DOI":"10.1007\/978-3-031-91118-7_3"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Ambal, G., Stupple, M., Dongol, B., Raad, A.: Specifying and verifying rdma synchronisation (extended version) (2026), https:\/\/arxiv.org\/abs\/2601.14642","DOI":"10.1007\/978-3-032-22720-1_3"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"Baran, A., Nelson-Slivon, J., Tseng, L., Palmieri, R.: Alock: Asymmetric lock primitive for rdma systems. In: Proceedings of the 36th ACM Symposium on Parallelism in Algorithms and Architectures. p. 15\u201326. SPAA \u201924, Association for Computing Machinery, New York, NY, USA (2024). https:\/\/doi.org\/10.1145\/3626183.3659977, https:\/\/doi.org\/10.1145\/3626183.3659977","DOI":"10.1145\/3626183.3659977"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Bila, E.V., Dongol, B., Lahav, O., Raad, A., Wickerson, J.: View-based owicki\u2013gries reasoning for persistent x86-tso. In: Sergey, I. (ed.) Programming Languages and Systems. pp. 234\u2013261. Springer International Publishing, Cham (2022)","DOI":"10.1007\/978-3-030-99336-8_9"},{"key":"3_CR9","doi-asserted-by":"publisher","unstructured":"Blundell, C., Lewis, E.C., Martin, M.M.: Subtleties of transactional memory atomicity semantics. IEEE Computer Architecture Letters 5(2), 17\u201317 (2006). https:\/\/doi.org\/10.1109\/L-CA.2006.18","DOI":"10.1109\/L-CA.2006.18"},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Brock, B., Bulu\u00e7, A., Yelick, K.: Bcl: A cross-platform distributed data structures library. In: Proceedings of the 48th International Conference on Parallel Processing. ICPP \u201919, Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3337821.3337912, https:\/\/doi.org\/10.1145\/3337821.3337912","DOI":"10.1145\/3337821.3337912"},{"key":"3_CR11","doi-asserted-by":"publisher","unstructured":"Chong, N., Sorensen, T., Wickerson, J.: The semantics of transactions and weak memory in x86, power, arm, and C++. In: Foster, J.S., Grossman, D. (eds.) Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018. pp. 211\u2013225. ACM (2018). https:\/\/doi.org\/10.1145\/3192366.3192373, https:\/\/doi.org\/10.1145\/3192366.3192373","DOI":"10.1145\/3192366.3192373"},{"key":"3_CR12","unstructured":"Chung, Y., Zamanian, E.: Using RDMA for lock management. CoRR abs\/1507.03274 (2015), http:\/\/arxiv.org\/abs\/1507.03274"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"Dalvandi, S., Dongol, B.: Implementing and verifying release-acquire transactional memory in C11. Proc. ACM Program. Lang. 6(OOPSLA2), 1817\u20131844 (2022). https:\/\/doi.org\/10.1145\/3563352, https:\/\/doi.org\/10.1145\/3563352","DOI":"10.1145\/3563352"},{"key":"3_CR14","doi-asserted-by":"publisher","unstructured":"Dan, A.M., Lam, P., Hoefler, T., Vechev, M.: Modeling and analysis of remote memory access programming. SIGPLAN Not. 51(10), 129\u2013144 (oct 2016). https:\/\/doi.org\/10.1145\/3022671.2984033, https:\/\/doi.org\/10.1145\/3022671.2984033","DOI":"10.1145\/3022671.2984033"},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"Devarajan, H., Kougkas, A., Bateman, K., Sun, X.H.: Hcl: Distributing parallel data structures in extreme scales. In: 2020 IEEE International Conference on Cluster Computing (CLUSTER). pp. 248\u2013258 (2020). https:\/\/doi.org\/10.1109\/CLUSTER49012.2020.00035","DOI":"10.1109\/CLUSTER49012.2020.00035"},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"Devulapalli, A., Wyckoff, P.: Distributed queue-based locking using advanced network features. In: 34th International Conference on Parallel Processing (ICPP 2005), 14-17 June 2005, Oslo, Norway. pp. 408\u2013415. IEEE Computer Society (2005). https:\/\/doi.org\/10.1109\/ICPP.2005.34, https:\/\/doi.org\/10.1109\/ICPP.2005.34","DOI":"10.1109\/ICPP.2005.34"},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"Dongol, B., Jagadeesan, R., Riely, J.: Transactions in relaxed memory architectures. Proc. ACM Program. Lang. 2(POPL), 18:1\u201318:29 (2018). https:\/\/doi.org\/10.1145\/3158106, https:\/\/doi.org\/10.1145\/3158106","DOI":"10.1145\/3158106"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Gangidi, A., Miao, R., Zheng, S., Bondu, S.J., Goes, G., Morsy, H., Puri, R., Riftadi, M., Shetty, A.J., Yang, J., et\u00a0al.: Rdma over ethernet for distributed training at meta scale. In: Proceedings of the ACM SIGCOMM 2024 Conference. pp. 57\u201370 (2024)","DOI":"10.1145\/3651890.3672233"},{"key":"3_CR19","unstructured":"Gao, J., Wang, Q., Shu, J.: Shiftlock: Mitigate one-sided RDMA lock contention via handover. In: Gunawi, H.S., Tarasov, V. (eds.) 23rd USENIX Conference on File and Storage Technologies, FAST 2025, Santa Clara, CA, February 25-27, 2025. pp. 355\u2013372. USENIX Association (2025), https:\/\/www.usenix.org\/conference\/fast25\/presentation\/gao"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990). https:\/\/doi.org\/10.1145\/78969.78972, https:\/\/doi.org\/10.1145\/78969.78972","DOI":"10.1145\/78969.78972"},{"key":"3_CR21","unstructured":"Hodgkins, G., Madler, M., Izraelevitz, J.: Loco: Rethinking objects for network memory (2025), https:\/\/arxiv.org\/abs\/2503.19270"},{"key":"3_CR22","unstructured":"IBTA: Infiniband architecture specification volume 1 release 1.6. https:\/\/www.infinibandta.org\/ibta-specification\/ (2022)"},{"key":"3_CR23","doi-asserted-by":"publisher","unstructured":"Lahav, O., Dongol, B., Wehrheim, H.: Rely-guarantee reasoning for causally consistent shared memory. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13964, pp. 206\u2013229. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_11, https:\/\/doi.org\/10.1007\/978-3-031-37706-8_11","DOI":"10.1007\/978-3-031-37706-8_11"},{"key":"3_CR24","doi-asserted-by":"publisher","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers 28(9), 690\u2013691 (Sep 1979). https:\/\/doi.org\/10.1109\/TC.1979.1675439, http:\/\/dx.doi.org\/10.1109\/TC.1979.1675439","DOI":"10.1109\/TC.1979.1675439"},{"key":"3_CR25","unstructured":"Li, P., Hua, Y., Zuo, P., Chen, Z., Sheng, J.: ROLEX: A scalable RDMA-oriented learned Key-Value store for disaggregated memory systems. In: 21st USENIX Conference on File and Storage Technologies (FAST 23). pp. 99\u2013114. USENIX Association, Santa Clara, CA (Feb 2023), https:\/\/www.usenix.org\/conference\/fast23\/presentation\/li-pengfei"},{"key":"3_CR26","unstructured":"Lu, Y., Chen, G., Li, B., Tan, K., Xiong, Y., Cheng, P., Zhang, J., Chen, E., Moscibroda, T.: $$\\{$$Multi-Path$$\\}$$ transport for $$\\{$$RDMA$$\\}$$ in datacenters. In: 15th USENIX symposium on networked systems design and implementation (NSDI 18). pp. 357\u2013371 (2018)"},{"key":"3_CR27","doi-asserted-by":"publisher","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-tso. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Lecture Notes in Computer Science, vol.\u00a05674, pp. 391\u2013407. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_27, https:\/\/doi.org\/10.1007\/978-3-642-03359-9_27","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"3_CR28","doi-asserted-by":"publisher","unstructured":"Raad, A., Doko, M., Rozic, L., Lahav, O., Vafeiadis, V.: On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models. Proc. ACM Program. Lang. 3(POPL), 68:1\u201368:31 (2019). https:\/\/doi.org\/10.1145\/3290381, https:\/\/doi.org\/10.1145\/3290381","DOI":"10.1145\/3290381"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Raad, A., Lahav, O., Vafeiadis, V.: On parallel snapshot isolation and release\/acquire consistency. In: Ahmed, A. (ed.) Programming Languages and Systems. pp. 940\u2013967. Springer International Publishing, Cham (2018)","DOI":"10.1007\/978-3-319-89884-1_33"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Raad, A., Lahav, O., Vafeiadis, V.: On the semantics of snapshot isolation. In: Enea, C., Piskac, R. (eds.) Verification, Model Checking, and Abstract Interpretation. pp. 1\u201323. Springer International Publishing, Cham (2019)","DOI":"10.1007\/978-3-030-11245-5_1"},{"key":"3_CR31","doi-asserted-by":"publisher","unstructured":"Singh, A.K., Lahav, O.: An operational approach to library abstraction under relaxed memory concurrency. Proc. ACM Program. Lang. 7(POPL), 1542\u20131572 (2023). https:\/\/doi.org\/10.1145\/3571246, https:\/\/doi.org\/10.1145\/3571246","DOI":"10.1145\/3571246"},{"key":"3_CR32","doi-asserted-by":"publisher","unstructured":"Stefanesco, L., Raad, A., Vafeiadis, V.: Specifying and verifying persistent libraries. In: Weirich, S. (ed.) Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part II. Lecture Notes in Computer Science, vol. 14577, pp. 185\u2013211. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57267-8_8, https:\/\/doi.org\/10.1007\/978-3-031-57267-8_8","DOI":"10.1007\/978-3-031-57267-8_8"},{"key":"3_CR33","unstructured":"Wang, Z., Luo, L., Ning, Q., Zeng, C., Li, W., Wan, X., Xie, P., Feng, T., Cheng, K., Geng, X., et\u00a0al.: $$\\{$$SRNIC$$\\}$$: A scalable architecture for $$\\{$$RDMA$$\\}$$$$\\{$$NICs$$\\}$$. In: 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI 23). pp. 1\u201314 (2023)"},{"key":"3_CR34","doi-asserted-by":"publisher","unstructured":"Yoon, D.Y., Chowdhury, M., Mozafari, B.: Distributed lock management with RDMA: decentralization without starvation. In: Das, G., Jermaine, C.M., Bernstein, P.A. (eds.) Proceedings of the 2018 International Conference on Management of Data, SIGMOD Conference 2018, Houston, TX, USA, June 10-15, 2018. pp. 1571\u20131586. ACM (2018). https:\/\/doi.org\/10.1145\/3183713.3196890, https:\/\/doi.org\/10.1145\/3183713.3196890","DOI":"10.1145\/3183713.3196890"},{"key":"3_CR35","doi-asserted-by":"crossref","unstructured":"Zhu, Y., Eran, H., Firestone, D., Guo, C., Lipshteyn, M., Liron, Y., Padhye, J., Raindel, S., Yahia, M.H., Zhang, M.: Congestion control for large-scale rdma deployments. ACM SIGCOMM Computer Communication Review 45(4), 523\u2013536 (2015)","DOI":"10.1145\/2829988.2787484"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22720-1_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T19:24:11Z","timestamp":1777577051000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22720-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227195","9783032227201"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22720-1_3","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":"10 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","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":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}