Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures
Authors: 
Guillaume Ambal, Brijesh Dongol, 
Haggai Eran, Vasileios Klimis, 
Ori Lahav, 
Azalea RaadAuthors Info & Claims
Article No.: 341, Pages 1982 - 2009
Abstract
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.
References
[1]
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 (2021), Article 56, Jan., 32 pages. https://doi.org/10.1145/3434337
[2]
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–332. isbn:978-3-662-46668-1 https://doi.org/10.1007/978-3-662-46669-8_13
[3]
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–418. https://doi.org/10.1145/3293611.3331601
[4]
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–8:54. https://doi.org/10.1145/3458926
[5]
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 (2018), March, 405–418. issn:0362-1340 https://doi.org/10.1145/3296957.3177156
[6]
Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory. ACM Trans. Program. Lang. Syst., 36, 2 (2014), 7:1–7:74. https://doi.org/10.1145/2627752
[7]
Guillaume Ambal, Brijesh Dongol, Haggai Eran, Vasileios Klimis, Ori Lahav, and Azalea Raad. 2024. Extended Version. https://www.soundandcomplete.org/papers/OOPSLA2024/RDMA/rdma-extended.pdf
[8]
Guillaume Ambal, Brijesh Dongol, Haggai Eran, Vasileios Klimis, Ori Lahav, and Azalea Raad. 2024. Project page for Semantics of Remote Direct Memory Access. https://www.soundandcomplete.org/papers/OOPSLA2024/RDMA
[9]
Don Anderson. 1999. FireWire system architecture (2nd ed.): IEEE 1394a. Addison-Wesley Longman Publishing Co., Inc., USA. isbn:0201485354
[10]
Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ Concurrency. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’11). ACM, New York, NY, USA. 55–66. isbn:978-1-4503-0490-0 https://doi.org/10.1145/1926385.1926394
[11]
John Bender and Jens Palsberg. 2019. A Formalization of Java’s Concurrent Access Modes. Proc. ACM Program. Lang., 3, OOPSLA (2019), Article 142, Oct., 28 pages. https://doi.org/10.1145/3360568
[12]
Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, and John Wickerson. 2022. View-Based Owicki–Gries Reasoning for Persistent x86-TSO. In Programming Languages and Systems, Ilya Sergey (Ed.). Springer International Publishing, Cham. 234–261. isbn:978-3-030-99336-8
[13]
M. S. Birrittella, M. Debbage, R. Huggahalli, J. Kunz, T. Lovett, T. Rimmer, K. D. Underwood, and R. C. Zak. 2015. Intel Omni-Path Architecture: Enabling scalable, high performance fabrics. In 2015 IEEE 23rd Annual Symposium on High-Performance Interconnects (HOTI) (HOTI 2015). 1–9. issn:1550-4794 https://doi.org/10.1109/HOTI.2015.22
[14]
Ahmed Bouajjani, Egor Derevenetc, and Roland Meyer. 2013. Checking and Enforcing Robustness against TSO. In ESOP 2013 (LNCS, Vol. 7792). Springer, 533–553. https://doi.org/10.1007/978-3-642-37036-6_29
[15]
Soham Chakraborty and Viktor Vafeiadis. 2019. Grounding Thin-Air Reads with Event Structures. Proc. ACM Program. Lang., 3, POPL (2019), Article 70, Jan., 28 pages. https://doi.org/10.1145/3290383
[16]
Kyeongmin Cho, Sung-Hwan Lee, Azalea Raad, and Jeehoon Kang. 2021. Revamping Hardware Persistency Models: View-Based and Axiomatic Persistency Models for Intel-X86 and Armv8. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2021). Association for Computing Machinery, New York, NY, USA. 16–31. isbn:9781450383912 https://doi.org/10.1145/3453483.3454027
[17]
Andrei Marian Dan, Patrick Lam, Torsten Hoefler, and Martin Vechev. 2016. Modeling and Analysis of Remote Memory Access Programming. SIGPLAN Not., 51, 10 (2016), oct, 129–144. issn:0362-1340 https://doi.org/10.1145/3022671.2984033
[18]
D. Dunning, G. Regnier, G. McAlpine, D. Cameron, B. Shubert, F. Berry, A.M. Merritt, E. Gronke, and C. Dodd. 1998. The Virtual Interface Architecture. IEEE Micro, 18, 2 (1998), 66–76. https://doi.org/10.1109/40.671404
[19]
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 (POPL ’16). Association for Computing Machinery, New York, NY, USA. 608–621. isbn:9781450335492 https://doi.org/10.1145/2837614.2837615
[20]
Robert Gerstenberger, Maciej Besta, and Torsten Hoefler. 2018. Enabling Highly Scalable Remote Memory Access Programming with MPI-3 One Sided. Commun. ACM, 61, 10 (2018), sep, 106–113. issn:0001-0782 https://doi.org/10.1145/3264413
[21]
IBTA. 2022. InfiniBand Architecture Specification Volume 1 Release 1.6. https://www.infinibandta.org/ibta-specification/
[22]
InfiniBand Trade Association (IBTA). 2018. The RoCE Initiative. https://www.infinibandta.org/roce-initiative/ (Accessed: July 2023)
[23]
Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. 2017. A Promising Semantics for Relaxed-Memory Concurrency. SIGPLAN Not., 52, 1 (2017), Jan., 175–189. issn:0362-1340 https://doi.org/10.1145/3093333.3009850
[24]
Artem Khyzha and Ori Lahav. 2021. Taming X86-TSO Persistency. Proc. ACM Program. Lang., 5, POPL (2021), Article 47, Jan., 29 pages. https://doi.org/10.1145/3434328
[25]
Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, and Viktor Vafeiadis. 2021. PerSeVerE: Persistency Semantics for Verification under Ext4. Proc. ACM Program. Lang., 5, POPL (2021), Article 43, jan, 29 pages. https://doi.org/10.1145/3434324
[26]
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–226. https://doi.org/10.1145/3385412.3385966
[27]
Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis. 2016. Taming Release-Acquire Consistency. SIGPLAN Not., 51, 1 (2016), Jan., 649–662. issn:0362-1340 https://doi.org/10.1145/2914770.2837643
[28]
Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. 2017. Repairing Sequential Consistency in C/C++11. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). Association for Computing Machinery, New York, NY, USA. 618–632. isbn:9781450349888 https://doi.org/10.1145/3062341.3062352
[29]
Leslie Lamport. 1979. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Trans. Computers, 28, 9 (1979), Sept., 690–691. https://doi.org/10.1109/TC.1979.1675439
[30]
Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, and Viktor Vafeiadis. 2020. Promising 2.0: Global Optimizations in Relaxed Memory Concurrency. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020). Association for Computing Machinery, New York, NY, USA. 362–376. isbn:9781450376136 https://doi.org/10.1145/3385412.3386010
[31]
linux-rdma. 2018. RDMA core. https://github.com/linux-rdma/rdma-core/ (Accessed: Jul. 2023)
[32]
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 POWER Multiprocessors. In Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, P. Madhusudan and Sanjit A. Seshia (Eds.) (Lecture Notes in Computer Science, Vol. 7358). Springer, 495–512. https://doi.org/10.1007/978-3-642-31424-7_36
[33]
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 (POPL ’05). Association for Computing Machinery, New York, NY, USA. 378–391. isbn:158113830X https://doi.org/10.1145/1040305.1040336
[34]
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–4:3. issn:2509-8195 https://doi.org/10.4230/DARTS.6.2.4
[35]
Kyndylan Nienhuis, Kayvan Memarian, and Peter Sewell. 2016. An Operational Semantics for C/C++11 Concurrency. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2016). Association for Computing Machinery, New York, NY, USA. 111–128. isbn:9781450344449 https://doi.org/10.1145/2983990.2983997
[36]
Stanko Novakovic, Alexandros Daglis, Edouard Bugnion, Babak Falsafi, and Boris Grot. 2014. Scale-out NUMA. In Proceedings of the 19th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS ’14). Association for Computing Machinery, New York, NY, USA. 3–18. isbn:9781450323055 https://doi.org/10.1145/2541940.2541965
[37]
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)
[38]
OpenFabrics. 2016. RDMA core. https://ofiwg.github.io/libfabric/ (Accessed: Jul. 2023)
[39]
PCI-SIG. 2022. PCI Express Base Specification Revision 6.0 Version 1.0. https://pcisig.com/pci-express-6.0-specification
[40]
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 (POPL ’16). Association for Computing Machinery, New York, NY, USA. 622–633. isbn:9781450335492 https://doi.org/10.1145/2837614.2837616
[41]
Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis. 2017. Promising Compilation to ARMv8 POP. In 31st European Conference on Object-Oriented Programming (ECOOP 2017), Peter Müller (Ed.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 74). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. 22:1–22:28. isbn:978-3-95977-035-4 issn:1868-8969 https://doi.org/10.4230/LIPIcs.ECOOP.2017.22
[42]
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 (2019), Article 69, Jan., 31 pages. issn:2475-1421 https://doi.org/10.1145/3290382
[43]
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 (2018), Article 19, Dec., 29 pages. issn:2475-1421 https://doi.org/10.1145/3158107
[44]
Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan Lee, and Chung-Kil Hur. 2019. Promising-ARM/RISC-V: A Simpler and Faster Operational Concurrency Model. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2019). Association for Computing Machinery, New York, NY, USA. 1–15. isbn:9781450367127 https://doi.org/10.1145/3314221.3314624
[45]
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–967. isbn:978-3-319-89884-1
[46]
Azalea Raad, Ori Lahav, and Viktor Vafeiadis. 2019. On the Semantics of Snapshot Isolation. In Verification, Model Checking, and Abstract Interpretation, Constantin Enea and Ruzica Piskac (Eds.). Springer International Publishing, Cham. 1–23. isbn:978-3-030-11245-5
[47]
Azalea Raad, Ori Lahav, and Viktor Vafeiadis. 2020. Persistent Owicki-Gries Reasoning: A Program Logic for Reasoning about Persistent Programs on Intel-X86. Proc. ACM Program. Lang., 4, OOPSLA (2020), Article 151, nov, 28 pages. https://doi.org/10.1145/3428219
[48]
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 (2022), Article 22, jan, 31 pages. https://doi.org/10.1145/3498683
[49]
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 (2018), Article 137, Oct., 27 pages. issn:2475-1421 https://doi.org/10.1145/3276507
[50]
Azalea Raad, John Wickerson, Gil Neiger, and Viktor Vafeiadis. 2020. Persistency Semantics of the Intel-X86 Architecture. Proc. ACM Program. Lang., 4, POPL (2020), Article 11, Dec., 31 pages. https://doi.org/10.1145/3371079
[51]
Azalea Raad, John Wickerson, and Viktor Vafeiadis. 2019. Weak Persistency Semantics from the Ground Up: Formalising the Persistency Semantics of ARMv8 and Transactional Models. Proc. ACM Program. Lang., 3, OOPSLA (2019), Article 135, Oct., 27 pages. issn:2475-1421 https://doi.org/10.1145/3360561
[52]
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
[53]
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 (PLDI ’11). Association for Computing Machinery, New York, NY, USA. 175–186. isbn:9781450306638 https://doi.org/10.1145/1993498.1993520
[54]
Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen. 2010. X86-TSO: A Rigorous and Usable Programmer’s Model for x86 Multiprocessors. Commun. ACM, 53, 7 (2010), July, 89–97. issn:0001-0782 https://doi.org/10.1145/1785414.1785443
[55]
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 (KBNets ’17). Association for Computing Machinery, New York, NY, USA. 25–30. isbn:9781450350532 https://doi.org/10.1145/3098583.3098588
[56]
SPARC. 1992. The SPARC Architecture Manual: Version 8. Prentice-Hall, Inc., Upper Saddle River, NJ, USA. isbn:0-13-825001-4
[57]
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
[58]
Xingda Wei, Jiaxin Shi, Yanzhe Chen, Rong Chen, and Haibo Chen. 2015. Fast In-Memory Transaction Processing Using RDMA and HTM. In Proceedings of the 25th Symposium on Operating Systems Principles (SOSP ’15). Association for Computing Machinery, New York, NY, USA. 87–104. isbn:9781450338349 https://doi.org/10.1145/2815400.2815419
[59]
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), Robert Hirschfeld and Tobias Pape (Eds.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 166). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 21:1–21:31. isbn:978-3-95977-154-2 issn:1868-8969 https://doi.org/10.4230/LIPIcs.ECOOP.2020.21
[60]
Yibo Zhu, Haggai Eran, Daniel Firestone, Chuanxiong Guo, Marina Lipshteyn, Yehonatan Liron, Jitendra Padhye, Shachar Raindel, Mohamad Haj Yahia, and Ming Zhang. 2015. Congestion Control for Large-Scale RDMA Deployments. In Proceedings of the 2015 ACM Conference on Special Interest Group on Data Communication (SIGCOMM ’15). Association for Computing Machinery, New York, NY, USA. 523–536. isbn:9781450335423 https://doi.org/10.1145/2785956.2787484
Index Terms
- Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures
Recommendations
Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model
Emerging non-volatile memory (NVM) technologies promise the durability of disks with the performance of volatile memory (RAM). To describe the persistency guarantees of NVM, several memory persistency models have been proposed in the literature. However, ...
An operational semantics for ZCCS
ICFEM '97: Proceedings of the 1st International Conference on Formal Engineering MethodsG. Bruns (1995) has proposed a version of value-passing CCS in which an agent language, based on that proposed by Milner, is augmented with a rich data language. The data language can be used to describe sets, tuples and sequences etc. constructed from ...
Relaxed memory models: an operational approach
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesMemory models define an interface between programs written in some language and their implementation, determining which behaviour the memory (and thus a program) is allowed to have in a given model. A minimal guarantee memory models should provide to ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2024
2691 pages
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 08 October 2024
Published in PACMPL Volume 8, Issue OOPSLA2
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
- European Research Council
- Israel Science Foundation
- UK Research and Innovation
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 141Total Downloads
- Downloads (Last 12 months)141
- Downloads (Last 6 weeks)69
Reflects downloads up to 21 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in