{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:24:47Z","timestamp":1779074687968,"version":"3.51.4"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["851811"],"award-info":[{"award-number":["851811"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003977","name":"Israel Science Foundation","doi-asserted-by":"publisher","award":["814\/22"],"award-info":[{"award-number":["814\/22"]}],"id":[{"id":"10.13039\/501100003977","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"publisher","award":["MR\/V024299\/1"],"award-info":[{"award-number":["MR\/V024299\/1"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,10,8]]},"abstract":"<jats:p>Remote direct memory access (RDMA) is a modern technology enabling networked machines to exchange information without involving the operating system of either side, and thus significantly speeding up data transfer in computer clusters. While RDMA is extensively used in practice and studied in various research papers, a formal underlying model specifying the allowed behaviours of concurrent RDMA programs running in modern multicore architectures is still missing. This paper aims to close this gap and provide semantic foundations of RDMA on x86-TSO machines. We propose three equivalent formal models, two operational models in different levels of abstraction and one declarative model, and prove that the three characterisations are equivalent. To gain confidence in the proposed semantics, the more concrete operational model has been reviewed by NVIDIA experts, a major vendor of RDMA systems, and we have empirically validated the declarative formalisation on various subtle litmus tests by extensive testing. We believe that this work is a necessary initial step for formally addressing RDMA-based systems by proposing language-level models, verifying their mapping to hardware, and developing reasoning techniques for concurrent RDMA programs.<\/jats:p>","DOI":"10.1145\/3689781","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"1982-2009","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4667-7266","authenticated-orcid":false,"given":"Guillaume","family":"Ambal","sequence":"first","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0446-3507","authenticated-orcid":false,"given":"Brijesh","family":"Dongol","sequence":"additional","affiliation":[{"name":"University of Surrey, Guildford, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2159-9046","authenticated-orcid":false,"given":"Haggai","family":"Eran","sequence":"additional","affiliation":[{"name":"NVIDIA, Haifa, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3173-8636","authenticated-orcid":false,"given":"Vasileios","family":"Klimis","sequence":"additional","affiliation":[{"name":"Queen Mary University of London, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4305-6998","authenticated-orcid":false,"given":"Ori","family":"Lahav","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2319-3242","authenticated-orcid":false,"given":"Azalea","family":"Raad","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_1_2_1","article-title":"Deciding Reachability under Persistent X86-TSO","volume":"5","author":"Abdulla Parosh Aziz","year":"2021","unstructured":"Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. 2021. Deciding Reachability under Persistent X86-TSO. Proc. ACM Program. Lang. 5, POPL, Article 56 (Jan. 2021), 32 pages. https:\/\/doi.org\/10.1145\/3434337 10.1145\/3434337","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_3_1","first-page":"308","volume-title":"Proceedings of the 24th European Symposium on Programming on Programming Languages and Systems - Volume 9032","author":"Abdulla Parosh Aziz","year":"2015","unstructured":"Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Tuan-Phong Ngo. 2015. The Best of Both Worlds: Trading Efficiency and Optimality in Fence Insertion for TSO. In Proceedings of the 24th European Symposium on Programming on Programming Languages and Systems - Volume 9032. Springer-Verlag New York, Inc., New York, NY, USA, 308\u2013332. https:\/\/doi.org\/10.1007\/978-3-662-46669-8_13 10.1007\/978-3-662-46669-8_13"},{"key":"e_1_3_1_4_1","first-page":"409","volume-title":"Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, PODC 2019, Toronto, ON, Canada, July 29 - August 2, 2019","author":"Aguilera Marcos K.","year":"2019","unstructured":"Marcos K. Aguilera, Naama Ben-David, Rachid Guerraoui, Virendra J. Marathe, and Igor Zablotchi. 2019. The Impact of RDMA on Agreement. In Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, PODC 2019, Toronto, ON, Canada, July 29 - August 2, 2019, Peter Robinson and Faith Ellen (Eds.). ACM, 409\u2013418. https:\/\/doi.org\/10.1145\/3293611.3331601 10.1145\/3293611.3331601"},{"issue":"2","key":"e_1_3_1_5_1","first-page":"8:1","article-title":"Armed Cats: Formal Concurrency Modelling at Arm","volume":"43","author":"Alglave Jade","year":"2021","unstructured":"Jade Alglave, Will Deacon, Richard Grisenthwaite, Antoine Hacquard, and Luc Maranget. 2021. Armed Cats: Formal Concurrency Modelling at Arm. ACM Trans. Program. Lang. Syst. 43, 2 (2021), 8:1\u20138:54. https:\/\/doi.org\/10.1145\/3458926 10.1145\/3458926","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2","key":"e_1_3_1_6_1","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1145\/3296957.3177156","article-title":"Frightening Small Children and Disconcerting Grown-Ups: Concurrency in the Linux Kernel","volume":"53","author":"Alglave Jade","year":"2018","unstructured":"Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and Alan Stern. 2018. Frightening Small Children and Disconcerting Grown-Ups: Concurrency in the Linux Kernel. SIGPLAN Not. 53, 2 (March 2018), 405\u2013418. https:\/\/doi.org\/10.1145\/3296957.3177156 10.1145\/3296957.3177156","journal-title":"SIGPLAN Not."},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_1_8_1","unstructured":"Guillaume Ambal Brijesh Dongol Haggai Eran Vasileios Klimis Ori Lahav and Azalea Raad. 2024a. Extended Version. https:\/\/www.soundandcomplete.org\/papers\/OOPSLA2024\/RDMA\/rdma-extended.pdf"},{"key":"e_1_3_1_9_1","unstructured":"Guillaume Ambal Brijesh Dongol Haggai Eran Vasileios Klimis Ori Lahav and Azalea Raad. 2024b. Project page for Semantics of Remote Direct Memory Access. https:\/\/www.soundandcomplete.org\/papers\/OOPSLA2024\/RDMA"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/305278"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_1_12_1","article-title":"A Formalization of Java\u2019s Concurrent Access Modes","volume":"3","author":"Bender John","year":"2019","unstructured":"John Bender and Jens Palsberg. 2019. A Formalization of Java\u2019s Concurrent Access Modes. Proc. ACM Program. Lang. 3, OOPSLA, Article 142 (Oct. 2019), 28 pages. https:\/\/doi.org\/10.1145\/3360568 10.1145\/3360568","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_9"},{"key":"e_1_3_1_14_1","doi-asserted-by":"crossref","unstructured":"M. S. Birrittella M. Debbage R. Huggahalli J. Kunz T. Lovett T. Rimmer K. D. Underwood and R. C. Zak. 2015. Intel OmniPath Architecture: Enabling scalable high performance fabrics. In 2015 IEEE 23rd Annual Symposium on High-Performance Interconnects (HOTI) (HOTI 2015). 1\u20139. https:\/\/doi.org\/10.1109\/HOTI.2015.22 10.1109\/HOTI.2015.22","DOI":"10.1109\/HOTI.2015.22"},{"key":"e_1_3_1_15_1","first-page":"533","volume-title":"ESOP 2013 (LNCS, Vol. 7792)","author":"Bouajjani Ahmed","year":"2013","unstructured":"Ahmed Bouajjani, Egor Derevenetc, and Roland Meyer. 2013. Checking and Enforcing Robustness against TSO. In ESOP 2013 (LNCS, Vol. 7792). Springer, 533\u2013553. https:\/\/doi.org\/10.1007\/978-3-642-37036-6_29 10.1007\/978-3-642-37036-6_29"},{"key":"e_1_3_1_16_1","article-title":"Grounding Thin-Air Reads with Event Structures","volume":"3","author":"Chakraborty Soham","year":"2019","unstructured":"Soham Chakraborty and Viktor Vafeiadis. 2019. Grounding Thin-Air Reads with Event Structures. Proc. ACM Program. Lang. 3, POPL, Article 70 (Jan. 2019), 28 pages. https:\/\/doi.org\/10.1145\/3290383 10.1145\/3290383","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454027"},{"issue":"10","key":"e_1_3_1_18_1","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1145\/3022671.2984033","article-title":"Modeling and Analysis of Remote Memory Access Programming","volume":"51","author":"Dan Andrei Marian","year":"2016","unstructured":"Andrei Marian Dan, Patrick Lam, Torsten Hoefler, and Martin Vechev. 2016. Modeling and Analysis of Remote Memory Access Programming. SIGPLAN Not. 51, 10 (oct 2016), 129\u2013144. https:\/\/doi.org\/10.1145\/3022671.2984033 10.1145\/3022671.2984033","journal-title":"SIGPLAN Not."},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/40.671404"},{"key":"e_1_3_1_20_1","first-page":"608","volume-title":"Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (St. Petersburg, FL, USA) (POPL \u201916)","author":"Flur Shaked","year":"2016","unstructured":"Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. 2016. Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (St. Petersburg, FL, USA) (POPL \u201916). Association for Computing Machinery, New York, NY, USA, 608\u2013621. https:\/\/doi.org\/10.1145\/2837614.2837615 10.1145\/2837614.2837615"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3264413"},{"key":"e_1_3_1_22_1","unstructured":"IBTA. 2022. InfiniBand Architecture Specification Volume 1 Release 1.6. https:\/\/www.infinibandta.org\/ibta-specification\/."},{"key":"e_1_3_1_23_1","unstructured":"InfiniBand Trade Association (IBTA). 2018. The RoCE Initiative. https:\/\/www.infinibandta.org\/roce-initiative\/ (Accessed: July 2023)."},{"issue":"1","key":"e_1_3_1_24_1","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1145\/3093333.3009850","article-title":"A Promising Semantics for Relaxed- Memory Concurrency","volume":"52","author":"Kang Jeehoon","year":"2017","unstructured":"Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. 2017. A Promising Semantics for Relaxed- Memory Concurrency. SIGPLANNot. 52, 1 (Jan. 2017), 175\u2013189. https:\/\/doi.org\/10.1145\/3093333.3009850 10.1145\/3093333.3009850","journal-title":"SIGPLANNot"},{"key":"e_1_3_1_25_1","article-title":"Taming X86-TSO Persistency","volume":"5","author":"Khyzha Artem","year":"2021","unstructured":"Artem Khyzha and Ori Lahav. 2021. Taming X86-TSO Persistency. Proc. ACM Program. Lang. 5, POPL, Article 47 (Jan. 2021), 29 pages. https:\/\/doi.org\/10.1145\/3434328 10.1145\/3434328","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_26_1","article-title":"PerSeVerE: Persistency Semantics for Verification under Ext4","volume":"5","author":"Kokologiannakis Michalis","year":"2021","unstructured":"Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, and Viktor Vafeiadis. 2021. PerSeVerE: Persistency Semantics for Verification under Ext4. Proc. ACM Program. Lang. 5, POPL, Article 43 (jan 2021), 29 pages. https:\/\/doi.org\/10.1145\/3434324 10.1145\/3434324","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_27_1","first-page":"211","volume-title":"PLDI 2020","author":"Lahav Ori","year":"2020","unstructured":"Ori Lahav and Udi Boker. 2020. Decidable verification under a causally consistent shared memory. In PLDI 2020, Alastair F. Donaldson and Emina Torlak (Eds.). ACM, 211\u2013226. https:\/\/doi.org\/10.1145\/3385412.3385966 10.1145\/3385412.3385966"},{"issue":"1","key":"e_1_3_1_28_1","doi-asserted-by":"crossref","first-page":"649","DOI":"10.1145\/2914770.2837643","article-title":"Taming Release-Acquire Consistency","volume":"51","author":"Lahav Ori","year":"2016","unstructured":"Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis. 2016. Taming Release-Acquire Consistency. SIGPLAN Not. 51, 1 (Jan. 2016), 649\u2013662. https:\/\/doi.org\/10.1145\/2914770.2837643 10.1145\/2914770.2837643","journal-title":"SIGPLAN Not."},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386010"},{"key":"e_1_3_1_32_1","unstructured":"linux-rdma. 2018. RDMA core. https:\/\/github.com\/linux-rdma\/rdma-core\/ (Accessed: Jul. 2023)."},{"key":"e_1_3_1_33_1","first-page":"495","volume-title":"Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings (Lecture Notes in Computer Science, Vol. 7358)","author":"Mador-Haim Sela","year":"2012","unstructured":"Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, and Derek Williams. 2012. An Axiomatic Memory Model for PO WER Multiprocessors. In Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings (Lecture Notes in Computer Science, Vol. 7358), P. Madhusudan and Sanjit A. Seshia (Eds.). Springer, 495\u2013512. https:\/\/doi.org\/10.1007\/978-3-642-31424-7_36 10.1007\/978-3-642-31424-7_36"},{"key":"e_1_3_1_34_1","doi-asserted-by":"crossref","unstructured":"Jeremy Manson William Pugh and Sarita V. Adve. 2005. The Java Memory Model. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Long Beach California USA) (POPL \u201905). Association for Computing Machinery New York NY USA 378\u2013391. https:\/\/doi.org\/10.1145\/1040305.1040336 10.1145\/1040305.1040336","DOI":"10.1145\/1040305.1040336"},{"issue":"2","key":"e_1_3_1_35_1","first-page":"4:1","article-title":"Reconciling Event Structures with Modern Multiprocessors (Artifact)","volume":"6","author":"Moiseenko Evgenii","year":"2020","unstructured":"Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, and Viktor Vafeiadis. 2020. Reconciling Event Structures with Modern Multiprocessors (Artifact). Dagstuhl Artifacts Series 6, 2 (2020), 4:1\u20134:3. https:\/\/doi.org\/10.4230\/DARTS.6.2.4 10.4230\/DARTS.6.2.4","journal-title":"Dagstuhl Artifacts Series"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2983997"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2541940.2541965"},{"key":"e_1_3_1_38_1","unstructured":"NVIDIA Corporation. 2021. NVIDIA BlueField-2 DPU. https:\/\/www.nvidia.com\/content\/dam\/en-zz\/Solutions\/Data-Center\/documents\/datasheet-nvidia-bluefield-2-dpu.pdf (Accessed: Jul. 2023)."},{"key":"e_1_3_1_39_1","unstructured":"OpenFabrics. 2016. RDMA core. https:\/\/ofiwg.github.io\/libfabric\/ (Accessed: Jul. 2023)."},{"key":"e_1_3_1_40_1","unstructured":"PCI-SIG. 2022. PCI Express Base Specification Revision 6.0 Version 1.0. https:\/\/pcisig.com\/pci-express-6.0-specification."},{"key":"e_1_3_1_41_1","first-page":"622","volume-title":"Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (St. Petersburg, FL, USA) (POPL \u201916)","author":"Pichon-Pharabod Jean","year":"2016","unstructured":"Jean Pichon-Pharabod and Peter Sewell. 2016. A Concurrency Semantics for Relaxed Atomics That Permits Optimisation and Avoids Thin-Air Executions. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (St. Petersburg, FL, USA) (POPL \u201916). Association for Computing Machinery, New York, NY, USA, 622\u2013633. https:\/\/doi.org\/10.1145\/2837614.2837616 10.1145\/2837614.2837616"},{"key":"e_1_3_1_42_1","first-page":"22:1","volume-title":"31st European Conference on Object-Oriented Programming (ECOOP 2017) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 74)","author":"Podkopaev Anton","year":"2017","unstructured":"Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis. 2017. Promising Compilation to ARMv8 POP. In 31st European Conference on Object-Oriented Programming (ECOOP 2017) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 74), Peter M\u00fcller (Ed.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 22:1\u201322:28. https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2017.22 10.4230\/LIPIcs.ECOOP.2017.22"},{"key":"e_1_3_1_43_1","article-title":"Bridging the Gap Between Programming Languages and Hardware Weak Memory Models","volume":"3","author":"Podkopaev Anton","year":"2019","unstructured":"Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis. 2019. Bridging the Gap Between Programming Languages and Hardware Weak Memory Models. Proc. ACM Program. Lang. 3, POPL, Article 69 (Jan. 2019), 31 pages. https:\/\/doi.org\/10.1145\/3290382 10.1145\/3290382","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_44_1","article-title":"Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8","volume":"2","author":"Pulte Christopher","year":"2018","unstructured":"Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell. 2018. Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8. Proc. ACM Program. Lang. 2, POPL, Article 19 (Dec. 2018), 29 pages. https:\/\/doi.org\/10.1145\/3158107 10.1145\/3158107","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314624"},{"key":"e_1_3_1_46_1","doi-asserted-by":"crossref","first-page":"940","DOI":"10.1007\/978-3-319-89884-1_33","volume-title":"Programming Languages and Systems","author":"Raad Azalea","year":"2018","unstructured":"Azalea Raad, Ori Lahav, and Viktor Vafeiadis. 2018. On Parallel Snapshot Isolation and Release\/Acquire Consistency. In Programming Languages and Systems, Amal Ahmed (Ed.). Springer International Publishing, Cham, 940\u2013967."},{"key":"e_1_3_1_47_1","first-page":"1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Raad Azalea","year":"2019","unstructured":"Azalea Raad, Ori Lahav, and Viktor Vafeiadis. 2019a. On the Semantics of Snapshot Isolation. In Verification, Model Checking, and Abstract Interpretation, Constantin Enea and Ruzica Piskac (Eds.). Springer International Publishing, Cham, 1\u201323."},{"key":"e_1_3_1_48_1","article-title":"Persistent Owicki-Gries Reasoning: A Program Logic for Reasoning about Persistent Programs on Intel-X86","volume":"4","author":"Raad Azalea","year":"2020","unstructured":"Azalea Raad, Ori Lahav, and Viktor Vafeiadis. 2020a. Persistent Owicki-Gries Reasoning: A Program Logic for Reasoning about Persistent Programs on Intel-X86. Proc. ACM Program. Lang. 4, OOPSLA, Article 151 (nov 2020), 28 pages. https:\/\/doi.org\/10.1145\/3428219 10.1145\/3428219","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_49_1","article-title":"Extending Intel-X86 Consistency and Persistency: Formalising the Semantics of Intel-X86 Memory Types and Non-Temporal Stores","volume":"6","author":"Raad Azalea","year":"2022","unstructured":"Azalea Raad, Luc Maranget, and Viktor Vafeiadis. 2022. Extending Intel-X86 Consistency and Persistency: Formalising the Semantics of Intel-X86 Memory Types and Non-Temporal Stores. Proc. ACM Program. Lang. 6, POPL, Article 22 (jan 2022), 31 pages. https:\/\/doi.org\/10.1145\/3498683 10.1145\/3498683","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_50_1","article-title":"Persistence Semantics for Weak Memory: Integrating Epoch Persistency with the TSO Memory Model","volume":"2","author":"Raad Azalea","year":"2018","unstructured":"Azalea Raad and Viktor Vafeiadis. 2018. Persistence Semantics for Weak Memory: Integrating Epoch Persistency with the TSO Memory Model. Proc. ACM Program. Lang. 2, OOPSLA, Article 137 (Oct. 2018), 27 pages. https:\/\/doi.org\/10.1145\/3276507 10.1145\/3276507","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_51_1","article-title":"Persistency Semantics of the Intel-X86 Architecture","volume":"4","author":"Raad Azalea","year":"2020","unstructured":"Azalea Raad, John Wickerson, Gil Neiger, and Viktor Vafeiadis. 2020b. Persistency Semantics of the Intel-X86 Architecture. Proc. ACM Program. Lang. 4, POPL, Article 11 (Dec. 2020), 31 pages. https:\/\/doi.org\/10.1145\/3371079 10.1145\/3371079","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_52_1","article-title":"Weak Persistency Semantics from the Ground Up: Formalising the Persistency Semantics of ARMv8 and Transactional Models","volume":"3","author":"Raad Azalea","year":"2019","unstructured":"Azalea Raad, John Wickerson, and Viktor Vafeiadis. 2019b. Weak Persistency Semantics from the Ground Up: Formalising the Persistency Semantics of ARMv8 and Transactional Models. Proc. ACM Program. Lang. 3, OOPSLA, Article 135 (Oct. 2019), 27 pages. https:\/\/doi.org\/10.1145\/3360561 10.1145\/3360561","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_53_1","doi-asserted-by":"crossref","unstructured":"Renato J. Recio Paul R. Culley Dave Garcia Bernard Metzler and Jeff Hilland. 2007. A Remote Direct Memory Access Protocol Specification. RFC 5040. https:\/\/doi.org\/10.17487\/RFC5040 10.17487\/RFC5040","DOI":"10.17487\/rfc5040"},{"key":"e_1_3_1_54_1","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1145\/1993498.1993520","volume-title":"Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (San Jose, California, USA) (PLDI \u201911)","author":"Sarkar Susmit","year":"2011","unstructured":"Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams. 2011. Understanding POWER Multiprocessors. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (San Jose, California, USA) (PLDI \u201911). Association for Computing Machinery, New York, NY, USA, 175\u2013186. https:\/\/doi.org\/10.1145\/1993498.1993520 10.1145\/1993498.1993520"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_3_1_56_1","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1145\/3098583.3098588","volume-title":"Proceedings of the Workshop on Kernel-Bypass Networks (Los Angeles, CA, USA) (KBNets \u201917)","author":"Shpiner Alexander","year":"2017","unstructured":"Alexander Shpiner, Eitan Zahavi, Omar Dahley, Aviv Barnea, Rotem Damsker, Gennady Yekelis, Michael Zus, Eitan Kuta, and Dean Baram. 2017. RoCE Rocks without PFC: Detailed Evaluation. In Proceedings of the Workshop on Kernel-Bypass Networks (Los Angeles, CA, USA) (KBNets \u201917). Association for Computing Machinery, New York, NY, USA, 25\u201330. https:\/\/doi.org\/10.1145\/3098583.3098588 10.1145\/3098583.3098588"},{"key":"e_1_3_1_57_1","volume-title":"The SPARC Architecture Manual: Version 8","author":"SPARC","year":"1992","unstructured":"SPARC. 1992. The SPARC Architecture Manual: Version 8. Prentice-Hall, Inc., Upper Saddle River, NJ, USA."},{"key":"e_1_3_1_58_1","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1109\/HOTI.2019.00017","article-title":"Abstract - HOTI 2019: Compute Express Link","author":"Van Doren S.","year":"2019","unstructured":"S. Van Doren. 2019. Abstract - HOTI 2019: Compute Express Link. In 2019 IEEE Symposium on High-Performance Interconnects (HOTI) (HOTI 2019). 18-18. https:\/\/doi.org\/10.1109\/HOTI.2019.00017 10.1109\/HOTI.2019.00017","journal-title":"2019 IEEE Symposium on High-Performance Interconnects (HOTI) (HOTI 2019)"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815419"},{"key":"e_1_3_1_60_1","first-page":"21:1","volume-title":"34th European Conference on Object-Oriented Programming (ECOOP 2020) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 166)","author":"Xiong Shale","year":"2020","unstructured":"Shale Xiong, Andrea Cerone, Azalea Raad, and Philippa Gardner. 2020. Data Consistency in Transactional Storage Systems: A Centralised Semantics. In 34th European Conference on Object-Oriented Programming (ECOOP 2020) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 166), Robert Hirschfeld and Tobias Pape (Eds.). Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany, 21:1\u201321:31. https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2020.21 10.4230\/LIPIcs.ECOOP.2020.21"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2785956.2787484"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689781","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689781","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:08:48Z","timestamp":1770196128000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689781"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":60,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689781"],"URL":"https:\/\/doi.org\/10.1145\/3689781","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-05","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}