{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:10:46Z","timestamp":1775790646716,"version":"3.50.1"},"publisher-location":"Cham","reference-count":73,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031911170","type":"print"},{"value":"9783031911187","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Remote Direct Memory Access (RDMA) is a modern technology enabling high-performance inter-node communication. Despite its widespread adoption, theoretical understanding of permissible behaviours remains limited, as RDMA follows a very weak memory model. This paper addresses the challenge of establishing sufficient conditions for RDMA robustness. We introduce a set of straightforward criteria that, when met, guarantee sequential consistency and mitigate potential issues arising from weak memory behaviours in RDMA applications. Notably, when restricted to a tree topology, these conditions become even more relaxed, significantly reducing the need for synchronisation primitives. This work provides developers with practical guidelines to ensure the reliability and correctness of their RDMA-based systems.<\/jats:p>","DOI":"10.1007\/978-3-031-91118-7_3","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:17:45Z","timestamp":1746001065000},"page":"56-87","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Sufficient Conditions for Robustness of RDMA Programs"],"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\/0000-0003-4305-6998","authenticated-orcid":false,"given":"Ori","family":"Lahav","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":[[2025,5,1]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., L\u00e5ng, M., Ngo, T.P.: Precise and sound automatic fence insertion procedure under PSO. In: NETYS. pp. 32\u201347. Springer International Publishing, Cham (2015)","DOI":"10.1007\/978-3-319-26850-7_3"},{"key":"3_CR2","doi-asserted-by":"publisher","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: Proceedings of the 24th European Symposium on Programming on Programming Languages and Systems - Volume 9032. pp. 308\u2013332. Springer-Verlag New York, Inc., New York, NY, USA (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_13, http:\/\/dx.doi.org\/10.1007\/978-3-662-46669-8_13","DOI":"10.1007\/978-3-662-46669-8_13"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Adve, S.V., Hill, M.D.: Weak ordering\u2014a new definition. In: ISCA. pp. 2\u201314. ACM, New York (1990). https:\/\/doi.org\/10.1145\/325164.325100, http:\/\/doi.acm.org\/10.1145\/325164.325100","DOI":"10.1145\/325164.325100"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Aguilera, M.K., Ben-David, N., Guerraoui, R., Marathe, V.J., Zablotchi, I.: The impact of RDMA on agreement. In: Robinson, P., Ellen, F. (eds.) Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, PODC 2019, Toronto, ON, Canada, July 29 - August 2, 2019. pp. 409\u2013418. ACM (2019). https:\/\/doi.org\/10.1145\/3293611.3331601, https:\/\/doi.org\/10.1145\/3293611.3331601","DOI":"10.1145\/3293611.3331601"},{"key":"3_CR5","doi-asserted-by":"publisher","unstructured":"Alglave, J., Deacon, W., Grisenthwaite, R., Hacquard, A., Maranget, L.: Armed cats: Formal concurrency modelling at arm. ACM Trans. Program. Lang. Syst. 43(2), 8:1\u20138:54 (2021). https:\/\/doi.org\/10.1145\/3458926, https:\/\/doi.org\/10.1145\/3458926","DOI":"10.1145\/3458926"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Alglave, J., Kroening, D., Nimal, V., Poetzl, D.: Don\u2019t sit on the fence: a static analysis approach to automatic fence insertion. ACM Trans. Program. Lang. Syst. 39(2), 6:1\u20136:38 (May 2017). https:\/\/doi.org\/10.1145\/2994593, http:\/\/doi.acm.org\/10.1145\/2994593","DOI":"10.1145\/2994593"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Alglave, J., Maranget, L.: Stability in weak memory models. In: CAV. pp. 50\u201366. Springer-Verlag, Berlin, Heidelberg (2011), http:\/\/dl.acm.org\/citation.cfm?id=2032305.2032311","DOI":"10.1007\/978-3-642-22110-1_6"},{"key":"3_CR8","doi-asserted-by":"publisher","unstructured":"Alglave, J., Maranget, L., McKenney, P.E., Parri, A., Stern, A.: Frightening small children and disconcerting grown-ups: Concurrency in the linux kernel. SIGPLAN Not. 53(2), 405-418 (Mar 2018). https:\/\/doi.org\/10.1145\/3296957.3177156, https:\/\/doi.org\/10.1145\/3296957.3177156","DOI":"10.1145\/3296957.3177156"},{"key":"3_CR9","doi-asserted-by":"publisher","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36(2) (Jul 2014). https:\/\/doi.org\/10.1145\/2627752, https:\/\/doi.org\/10.1145\/2627752","DOI":"10.1145\/2627752"},{"key":"3_CR10","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) (Oct 2024). https:\/\/doi.org\/10.1145\/3689781, https:\/\/doi.org\/10.1145\/3689781","DOI":"10.1145\/3689781"},{"key":"3_CR11","unstructured":"Ambal, G., Lahav, O., Raad, A.: Extended version (2025), https:\/\/www.soundandcomplete.org\/papers\/ESOP2025\/RDMA\/"},{"key":"3_CR12","doi-asserted-by":"publisher","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing c++ concurrency. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 55\u201366. POPL \u201911, ACM, New York, NY, USA (2011). https:\/\/doi.org\/10.1145\/1926385.1926394, http:\/\/doi.acm.org\/10.1145\/1926385.1926394","DOI":"10.1145\/1926385.1926394"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Beillahi, S.M., Bouajjani, A., Enea, C.: Checking robustness against snapshot isolation. In: Computer Aided Verification. pp. 286\u2013304. Springer International Publishing, Cham (2019)","DOI":"10.1007\/978-3-030-25543-5_17"},{"key":"3_CR14","doi-asserted-by":"publisher","unstructured":"Beillahi, S.M., Bouajjani, A., Enea, C.: Robustness against transactional causal consistency. In: CONCUR 2019. vol.\u00a0140, pp. 30:1\u201330:18. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2019). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2019.30","DOI":"10.4230\/LIPIcs.CONCUR.2019.30"},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"Bender, J., Palsberg, J.: A formalization of java\u2019s concurrent access modes. Proc. ACM Program. Lang. 3(OOPSLA) (Oct 2019). https:\/\/doi.org\/10.1145\/3360568, https:\/\/doi.org\/10.1145\/3360568","DOI":"10.1145\/3360568"},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"Bernardi, G., Gotsman, A.: Robustness against consistency models with atomic visibility. In: CONCUR. pp. 7:1\u20137:15. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2016). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2016.7, http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2016\/6165","DOI":"10.4230\/LIPIcs.CONCUR.2016.7"},{"key":"3_CR17","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_CR18","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: ESOP. pp. 533\u2013553. Springer-Verlag, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_29, http:\/\/dx.doi.org\/10.1007\/978-3-642-37036-6_29","DOI":"10.1007\/978-3-642-37036-6_29"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Enea, C., Mutluergil, S.O., Tasiran, S.: Reasoning about TSO programs using reduction and abstraction. In: CAV. pp. 336\u2013353. Springer, Cham (2018)","DOI":"10.1007\/978-3-319-96142-2_21"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Meyer, R., M\u00f6hlmann, E.: Deciding robustness against total store ordering. In: ICALP. pp. 428\u2013440. Springer, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-22012-8_34"},{"key":"3_CR21","doi-asserted-by":"publisher","unstructured":"Brutschy, L., Dimitrov, D., M\u00fcller, P., Vechev, M.: Static serializability analysis for causal consistency. In: PLDI. pp. 90\u2013104. ACM, New York (2018). https:\/\/doi.org\/10.1145\/3192366.3192415, http:\/\/doi.acm.org\/10.1145\/3192366.3192415","DOI":"10.1145\/3192366.3192415"},{"key":"3_CR22","doi-asserted-by":"publisher","unstructured":"Burckhardt, S., Alur, R., Martin, M.M.K.: CheckFence: Checking consistency of concurrent data types on relaxed memory models. In: PLDI. pp. 12\u201321. ACM, New York (2007). https:\/\/doi.org\/10.1145\/1250734.1250737, http:\/\/doi.acm.org\/10.1145\/1250734.1250737","DOI":"10.1145\/1250734.1250737"},{"key":"3_CR23","doi-asserted-by":"publisher","unstructured":"Burckhardt, S., Musuvathi, M.: Effective program verification for relaxed memory models. In: CAV. pp. 107\u2013120. Springer-Verlag, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_12, http:\/\/dx.doi.org\/10.1007\/978-3-540-70545-1_12","DOI":"10.1007\/978-3-540-70545-1_12"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Burnim, J., Sen, K., Stergiou, C.: Sound and complete monitoring of sequential consistency for relaxed memory models. In: TACAS. pp. 11\u201325. Springer, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-19835-9_3"},{"key":"3_CR25","doi-asserted-by":"publisher","unstructured":"Chakraborty, S., Vafeiadis, V.: Grounding thin-air reads with event structures. Proc. ACM Program. Lang. 3(POPL) (Jan 2019). https:\/\/doi.org\/10.1145\/3290383, https:\/\/doi.org\/10.1145\/3290383","DOI":"10.1145\/3290383"},{"key":"3_CR26","doi-asserted-by":"publisher","unstructured":"Cho, K., Lee, S.H., Raad, A., Kang, J.: 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. p. 16-31. PLDI 2021, Association for Computing Machinery, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3453483.3454027, https:\/\/doi.org\/10.1145\/3453483.3454027","DOI":"10.1145\/3453483.3454027"},{"key":"3_CR27","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-144 (oct 2016). https:\/\/doi.org\/10.1145\/3022671.2984033, https:\/\/doi.org\/10.1145\/3022671.2984033","DOI":"10.1145\/3022671.2984033"},{"key":"3_CR28","unstructured":"Derevenetc, E.: Robustness against relaxed memory models. Ph.D. thesis, University of Kaiserslautern (2015), http:\/\/kluedo.ub.uni-kl.de\/frontdoor\/index\/index\/docId\/4074"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Derevenetc, E., Meyer, R.: Robustness against Power is PSpace-complete. In: ICALP. pp. 158\u2013170. Springer, Berlin, Heidelberg (2014)","DOI":"10.1007\/978-3-662-43951-7_14"},{"key":"3_CR30","doi-asserted-by":"publisher","unstructured":"Fekete, A., Liarokapis, D., O\u2019Neil, E., O\u2019Neil, P., Shasha, D.: Making snapshot isolation serializable. ACM Trans. Database Syst. 30(2), 492\u2013528 (Jun 2005). https:\/\/doi.org\/10.1145\/1071610.1071615, http:\/\/doi.acm.org\/10.1145\/1071610.1071615","DOI":"10.1145\/1071610.1071615"},{"key":"3_CR31","doi-asserted-by":"publisher","unstructured":"Flur, S., Gray, K.E., Pulte, C., Sarkar, S., Sezgin, A., Maranget, L., Deacon, W., Sewell, P.: Modelling the armv8 architecture, operationally: Concurrency and isa. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 608-621. POPL \u201916, Association for Computing Machinery, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2837614.2837615, https:\/\/doi.org\/10.1145\/2837614.2837615","DOI":"10.1145\/2837614.2837615"},{"key":"3_CR32","doi-asserted-by":"publisher","unstructured":"Gerstenberger, R., Besta, M., Hoefler, T.: Enabling highly scalable remote memory access programming with mpi-3 one sided. Commun. ACM 61(10), 106-113 (sep 2018). https:\/\/doi.org\/10.1145\/3264413, https:\/\/doi.org\/10.1145\/3264413","DOI":"10.1145\/3264413"},{"key":"3_CR33","doi-asserted-by":"publisher","unstructured":"Gharachorloo, K., Adve, S.V., Gupta, A., Hennessy, J.L., Hill, M.D.: Programming for different memory consistency models. Journal of Parallel and Distributed Computing 15(4), 399 \u2013 407 (1992). https:\/\/doi.org\/10.1016\/0743-7315(92)90052-O, http:\/\/www.sciencedirect.com\/science\/article\/pii\/074373159290052O","DOI":"10.1016\/0743-7315(92)90052-O"},{"key":"3_CR34","doi-asserted-by":"publisher","unstructured":"Gorjiara, H., Luo, W., Lee, A., Xu, G.H., Demsky, B.: Checking robustness to weak persistency models. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. p. 490-505. PLDI 2022, Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3519939.3523723, https:\/\/doi.org\/10.1145\/3519939.3523723","DOI":"10.1145\/3519939.3523723"},{"key":"3_CR35","doi-asserted-by":"publisher","unstructured":"Gotsman, A., Musuvathi, M., Yang, H.: Show no weakness: sequentially consistent specifications of TSO libraries. In: DISC. pp. 31\u201345. Springer-Verlag, Berlin, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33651-5_3, http:\/\/dx.doi.org\/10.1007\/978-3-642-33651-5_3","DOI":"10.1007\/978-3-642-33651-5_3"},{"key":"3_CR36","unstructured":"Inc., S.I.: The SPARC architecture manual (version 9). Prentice-Hall, Inc., Upper Saddle River, NJ, USA (1994)"},{"key":"3_CR37","doi-asserted-by":"publisher","unstructured":"Kang, J., Hur, C.K., Lahav, O., Vafeiadis, V., Dreyer, D.: A promising semantics for relaxed-memory concurrency. SIGPLAN Not. 52(1), 175-189 (Jan 2017). https:\/\/doi.org\/10.1145\/3093333.3009850, https:\/\/doi.org\/10.1145\/3093333.3009850","DOI":"10.1145\/3093333.3009850"},{"key":"3_CR38","doi-asserted-by":"publisher","unstructured":"Khyzha, A., Lahav, O.: Taming x86-tso persistency. Proc. ACM Program. Lang. 5(POPL) (Jan 2021). https:\/\/doi.org\/10.1145\/3434328, https:\/\/doi.org\/10.1145\/3434328","DOI":"10.1145\/3434328"},{"key":"3_CR39","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Kaysin, I., Raad, A., Vafeiadis, V.: Persevere: Persistency semantics for verification under ext4. Proc. ACM Program. Lang. 5(POPL) (jan 2021). https:\/\/doi.org\/10.1145\/3434324, https:\/\/doi.org\/10.1145\/3434324","DOI":"10.1145\/3434324"},{"key":"3_CR40","doi-asserted-by":"publisher","unstructured":"Lahav, O., Giannarakis, N., Vafeiadis, V.: Taming release-acquire consistency. SIGPLAN Not. 51(1), 649-662 (Jan 2016). https:\/\/doi.org\/10.1145\/2914770.2837643, https:\/\/doi.org\/10.1145\/2914770.2837643","DOI":"10.1145\/2914770.2837643"},{"key":"3_CR41","doi-asserted-by":"publisher","unstructured":"Lahav, O., Margalit, R.: Robustness against release\/acquire semantics. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. p. 126-141. PLDI 2019, Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3314221.3314604, https:\/\/doi.org\/10.1145\/3314221.3314604","DOI":"10.1145\/3314221.3314604"},{"key":"3_CR42","doi-asserted-by":"publisher","unstructured":"Lahav, O., Vafeiadis, V., Kang, J., Hur, C.K., Dreyer, D.: Repairing sequential consistency in c\/c++11. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. p. 618-632. PLDI 2017, Association for Computing Machinery, New York, NY, USA (2017). https:\/\/doi.org\/10.1145\/3062341.3062352, https:\/\/doi.org\/10.1145\/3062341.3062352","DOI":"10.1145\/3062341.3062352"},{"key":"3_CR43","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_CR44","doi-asserted-by":"publisher","unstructured":"Lee, S.H., Cho, M., Podkopaev, A., Chakraborty, S., Hur, C.K., Lahav, O., Vafeiadis, V.: Promising 2.0: Global optimizations in relaxed memory concurrency. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. p. 362-376. PLDI 2020, Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3385412.3386010, https:\/\/doi.org\/10.1145\/3385412.3386010","DOI":"10.1145\/3385412.3386010"},{"key":"3_CR45","doi-asserted-by":"crossref","unstructured":"Linden, A., Wolper, P.: A verification-based approach to memory fence insertion in relaxed memory systems. In: SPIN. pp. 144\u2013160. Springer-Verlag, Berlin, Heidelberg (2011), http:\/\/dl.acm.org\/citation.cfm?id=2032692.2032707","DOI":"10.1007\/978-3-642-22306-8_10"},{"key":"3_CR46","doi-asserted-by":"publisher","unstructured":"Linden, A., Wolper, P.: A verification-based approach to memory fence insertion in PSO memory systems. In: TACAS. pp. 339\u2013353. Springer-Verlag, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_24, http:\/\/dx.doi.org\/10.1007\/978-3-642-36742-7_24","DOI":"10.1007\/978-3-642-36742-7_24"},{"key":"3_CR47","doi-asserted-by":"publisher","unstructured":"Liu, F., Nedev, N., Prisadnikov, N., Vechev, M., Yahav, E.: Dynamic synthesis for relaxed memory models. In: PLDI. pp. 429\u2013440. ACM, New York (2012). https:\/\/doi.org\/10.1145\/2254064.2254115, http:\/\/doi.acm.org\/10.1145\/2254064.2254115","DOI":"10.1145\/2254064.2254115"},{"key":"3_CR48","doi-asserted-by":"publisher","unstructured":"Mador-Haim, S., Maranget, L., Sarkar, S., Memarian, K., Alglave, J., Owens, S., Alur, R., Martin, M.M.K., Sewell, P., Williams, D.: An axiomatic memory model for POWER multiprocessors. In: Madhusudan, P., Seshia, S.A. (eds.) Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings. Lecture Notes in Computer Science, vol.\u00a07358, pp. 495\u2013512. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_36","DOI":"10.1007\/978-3-642-31424-7_36"},{"key":"3_CR49","doi-asserted-by":"publisher","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The java memory model. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 378-391. POPL \u201905, Association for Computing Machinery, New York, NY, USA (2005). https:\/\/doi.org\/10.1145\/1040305.1040336, https:\/\/doi.org\/10.1145\/1040305.1040336","DOI":"10.1145\/1040305.1040336"},{"key":"3_CR50","doi-asserted-by":"publisher","unstructured":"Margalit, R., Lahav, O.: Verifying observational robustness against a c11-style memory model. Proc. ACM Program. Lang. 5(POPL) (Jan 2021). https:\/\/doi.org\/10.1145\/3434285, https:\/\/doi.org\/10.1145\/3434285","DOI":"10.1145\/3434285"},{"key":"3_CR51","doi-asserted-by":"publisher","unstructured":"Moiseenko, E., Podkopaev, A., Lahav, O., Melkonian, O., Vafeiadis, V.: Reconciling Event Structures with Modern Multiprocessors (Artifact). Dagstuhl Artifacts Series 6(2), 4:1\u20134:3 (2020). https:\/\/doi.org\/10.4230\/DARTS.6.2.4, https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2020\/13201","DOI":"10.4230\/DARTS.6.2.4"},{"key":"3_CR52","doi-asserted-by":"publisher","unstructured":"Nagar, K., Jagannathan, S.: Automated detection of serializability violations under weak consistency. In: CONCUR 2018. vol.\u00a0118, pp. 41:1\u201341:18. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2018). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2018.41, http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2018\/9579","DOI":"10.4230\/LIPIcs.CONCUR.2018.41"},{"key":"3_CR53","doi-asserted-by":"publisher","unstructured":"Nienhuis, K., Memarian, K., Sewell, P.: 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. p. 111-128. OOPSLA 2016, Association for Computing Machinery, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2983990.2983997, https:\/\/doi.org\/10.1145\/2983990.2983997","DOI":"10.1145\/2983990.2983997"},{"key":"3_CR54","doi-asserted-by":"crossref","unstructured":"Owens, S.: Reasoning about the implementation of concurrency abstractions on x86-TSO. In: ECOOP. pp. 478\u2013503. Springer-Verlag, Berlin, Heidelberg (2010)","DOI":"10.1007\/978-3-642-14107-2_23"},{"key":"3_CR55","doi-asserted-by":"publisher","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: TPHOLs. pp. 391\u2013407. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_27","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"3_CR56","doi-asserted-by":"publisher","unstructured":"Pichon-Pharabod, J., Sewell, P.: 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. p. 622-633. POPL \u201916, Association for Computing Machinery, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2837614.2837616, https:\/\/doi.org\/10.1145\/2837614.2837616","DOI":"10.1145\/2837614.2837616"},{"key":"3_CR57","doi-asserted-by":"publisher","unstructured":"Podkopaev, A., Lahav, O., Vafeiadis, V.: Promising Compilation to ARMv8 POP. In: M\u00fcller, P. (ed.) 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a074, pp. 22:1\u201322:28. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2017). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2017.22, http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2017\/7266","DOI":"10.4230\/LIPIcs.ECOOP.2017.22"},{"key":"3_CR58","doi-asserted-by":"publisher","unstructured":"Podkopaev, A., Lahav, O., Vafeiadis, V.: Bridging the gap between programming languages and hardware weak memory models. Proc. ACM Program. Lang. 3(POPL), 69:1\u201369:31 (Jan 2019). https:\/\/doi.org\/10.1145\/3290382, http:\/\/doi.acm.org\/10.1145\/3290382","DOI":"10.1145\/3290382"},{"key":"3_CR59","doi-asserted-by":"publisher","unstructured":"Pulte, C., Flur, S., Deacon, W., French, J., Sarkar, S., Sewell, P.: Simplifying arm concurrency: Multicopy-atomic axiomatic and operational models for armv8. Proc. ACM Program. Lang. 2(POPL), 19:1\u201319:29 (Dec 2018). https:\/\/doi.org\/10.1145\/3158107, http:\/\/doi.acm.org\/10.1145\/3158107","DOI":"10.1145\/3158107"},{"key":"3_CR60","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_CR61","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_CR62","doi-asserted-by":"publisher","unstructured":"Raad, A., Lahav, O., Vafeiadis, V.: Persistent owicki-gries reasoning: A program logic for reasoning about persistent programs on intel-x86. Proc. ACM Program. Lang. 4(OOPSLA) (nov 2020). https:\/\/doi.org\/10.1145\/3428219, https:\/\/doi.org\/10.1145\/3428219","DOI":"10.1145\/3428219"},{"key":"3_CR63","doi-asserted-by":"publisher","unstructured":"Raad, A., Maranget, L., Vafeiadis, V.: Extending intel-x86 consistency and persistency: Formalising the semantics of intel-x86 memory types and non-temporal stores. Proc. ACM Program. Lang. 6(POPL) (jan 2022). https:\/\/doi.org\/10.1145\/3498683, https:\/\/doi.org\/10.1145\/3498683","DOI":"10.1145\/3498683"},{"key":"3_CR64","doi-asserted-by":"publisher","unstructured":"Raad, A., Vafeiadis, V.: Persistence semantics for weak memory: Integrating epoch persistency with the tso memory model. Proc. ACM Program. Lang. 2(OOPSLA), 137:1\u2013137:27 (Oct 2018). https:\/\/doi.org\/10.1145\/3276507, http:\/\/doi.acm.org\/10.1145\/3276507","DOI":"10.1145\/3276507"},{"key":"3_CR65","doi-asserted-by":"publisher","unstructured":"Raad, A., Wickerson, J., Neiger, G., Vafeiadis, V.: Persistency semantics of the intel-x86 architecture. Proc. ACM Program. Lang. 4(POPL) (Dec 2020). https:\/\/doi.org\/10.1145\/3371079, https:\/\/doi.org\/10.1145\/3371079","DOI":"10.1145\/3371079"},{"key":"3_CR66","doi-asserted-by":"publisher","unstructured":"Raad, A., Wickerson, J., Vafeiadis, V.: Weak persistency semantics from the ground up: Formalising the persistency semantics of armv8 and transactional models. Proc. ACM Program. Lang. 3(OOPSLA), 135:1\u2013135:27 (Oct 2019). https:\/\/doi.org\/10.1145\/3360561, http:\/\/doi.acm.org\/10.1145\/3360561","DOI":"10.1145\/3360561"},{"key":"3_CR67","doi-asserted-by":"publisher","unstructured":"Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding power multiprocessors. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. p. 175-186. PLDI \u201911, Association for Computing Machinery, New York, NY, USA (2011). https:\/\/doi.org\/10.1145\/1993498.1993520, https:\/\/doi.org\/10.1145\/1993498.1993520","DOI":"10.1145\/1993498.1993520"},{"key":"3_CR68","doi-asserted-by":"publisher","unstructured":"Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: X86-TSO: A rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun. ACM 53(7), 89\u201397 (Jul 2010). https:\/\/doi.org\/10.1145\/1785414.1785443, http:\/\/doi.acm.org\/10.1145\/1785414.1785443","DOI":"10.1145\/1785414.1785443"},{"key":"3_CR69","doi-asserted-by":"publisher","unstructured":"Shpiner, A., Zahavi, E., Dahley, O., Barnea, A., Damsker, R., Yekelis, G., Zus, M., Kuta, E., Baram, D.: Roce rocks without pfc: Detailed evaluation. In: Proceedings of the Workshop on Kernel-Bypass Networks. p. 25-30. KBNets \u201917, Association for Computing Machinery, New York, NY, USA (2017). https:\/\/doi.org\/10.1145\/3098583.3098588, https:\/\/doi.org\/10.1145\/3098583.3098588","DOI":"10.1145\/3098583.3098588"},{"key":"3_CR70","doi-asserted-by":"publisher","unstructured":"Vindum, S.F., Birkedal, L.: Spirea: A mechanized concurrent separation logic for weak persistent memory. Proc. ACM Program. Lang. 7(OOPSLA2), 632\u2013657 (2023). https:\/\/doi.org\/10.1145\/3622820, https:\/\/doi.org\/10.1145\/3622820","DOI":"10.1145\/3622820"},{"key":"3_CR71","doi-asserted-by":"publisher","unstructured":"Wei, X., Shi, J., Chen, Y., Chen, R., Chen, H.: Fast in-memory transaction processing using rdma and htm. In: Proceedings of the 25th Symposium on Operating Systems Principles. p. 87-104. SOSP \u201915, Association for Computing Machinery, New York, NY, USA (2015). https:\/\/doi.org\/10.1145\/2815400.2815419, https:\/\/doi.org\/10.1145\/2815400.2815419","DOI":"10.1145\/2815400.2815419"},{"key":"3_CR72","doi-asserted-by":"publisher","unstructured":"Xiong, S., Cerone, A., Raad, A., Gardner, P.: Data Consistency in Transactional Storage Systems: A Centralised Semantics. In: Hirschfeld, R., Pape, T. (eds.) 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0166, pp. 21:1\u201321:31. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2020). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2020.21, https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2020\/13178","DOI":"10.4230\/LIPIcs.ECOOP.2020.21"},{"key":"3_CR73","doi-asserted-by":"publisher","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. In: Proceedings of the 2015 ACM Conference on Special Interest Group on Data Communication. p. 523-536. SIGCOMM \u201915, Association for Computing Machinery, New York, NY, USA (2015). https:\/\/doi.org\/10.1145\/2785956.2787484, https:\/\/doi.org\/10.1145\/2785956.2787484","DOI":"10.1145\/2785956.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-031-91118-7_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:17:52Z","timestamp":1746001072000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-91118-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031911170","9783031911187"],"references-count":73,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-91118-7_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","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":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}