{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:24:44Z","timestamp":1779074684590,"version":"3.51.4"},"reference-count":81,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/R032556\/1, EP\/V038915\/1, EP\/R025134\/2"],"award-info":[{"award-number":["EP\/R032556\/1, EP\/V038915\/1, EP\/R025134\/2"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","award":["DP190102142"],"award-info":[{"award-number":["DP190102142"]}],"id":[{"id":"10.13039\/501100000923","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":[[2022,10,31]]},"abstract":"<jats:p>Transactional memory (TM) is an intensively studied synchronisation paradigm with many proposed implementations in software and hardware, and combinations thereof. However, TM under relaxed memory, e.g., C11 (the 2011 C\/C++ standard) is still poorly understood, lacking rigorous foundations that support verifiable implementations. This paper addresses this gap by developing TMS2-ra, a relaxed operational TM specification. We integrate TMS2-ra with RC11 (the repaired C11 memory model that disallows load-buffering) to provide a formal semantics for TM libraries and their clients. We develop a logic, TARO, for verifying client programs that use TMS2-ra for synchronisation. We also show how TMS2-ra can be implemented by a C11 library, TML-ra, that uses relaxed and release-acquire atomics, yet guarantees the synchronisation properties required by TMS2-ra. We benchmark TML-ra and show that it outperforms its sequentially consistent counterpart in the STAMP benchmarks. Finally, we use a simulation-based verification technique to prove correctness of TML-ra. Our entire development is supported by the Isabelle\/HOL proof assistant.<\/jats:p>","DOI":"10.1145\/3563352","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"1817-1844","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Implementing and verifying release-acquire transactional memory in C11"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8813-780X","authenticated-orcid":false,"given":"Sadegh","family":"Dalvandi","sequence":"first","affiliation":[{"name":"University of Surrey, UK"}],"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, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314649"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"J. Alglave and P. Cousot. 2017. Ogre and Pythia: an invariance proof method for weak consistency models. In POPL G. Castagna and A. D. Gordon (Eds.). ACM 3\u201318. isbn:978-1-4503-4660-3 J. Alglave and P. Cousot. 2017. Ogre and Pythia: an invariance proof method for weak consistency models. In POPL G. Castagna and A. D. Gordon (Eds.). ACM 3\u201318. isbn:978-1-4503-4660-3","DOI":"10.1145\/3093333.3009883"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_2_1_4_1","volume-title":"Bouajjani and A. Silva (Eds.) (LNCS","volume":"49","author":"Armstrong A.","unstructured":"A. Armstrong and B. Dongol . 2017. Modularising Opacity Verification for Hybrid Transactional Memory. In FORTE, A . Bouajjani and A. Silva (Eds.) (LNCS , Vol. 10321). Springer, 33\u2013 49 . A. Armstrong and B. Dongol. 2017. Modularising Opacity Verification for Hybrid Transactional Memory. In FORTE, A. Bouajjani and A. Silva (Eds.) (LNCS, Vol. 10321). Springer, 33\u201349."},{"key":"e_1_2_1_5_1","volume-title":"Linearizability: A Sound and Complete Method","author":"Armstrong A.","year":"2017","unstructured":"A. Armstrong , B. Dongol , and S. Doherty . 2017 . Proving Opacity via Linearizability: A Sound and Complete Method . In FORTE, A. Bouajjani and A. Silva (Eds.) (LNCS, Vol. 10321). Springer, 50\u2013 66 . A. Armstrong, B. Dongol, and S. Doherty. 2017. Proving Opacity via Linearizability: A Sound and Complete Method. In FORTE, A. Bouajjani and A. Silva (Eds.) (LNCS, Vol. 10321). Springer, 50\u201366."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3332466.3374514"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.OPODIS.2021.30"},{"key":"e_1_2_1_8_1","first-page":"1","article-title":"2018","volume":"65","author":"Attiya H.","year":"2018","unstructured":"H. Attiya , A. Gotsman , S. Hans , and N. Rinetzky . 2018 . Characterizing Transactional Memory Consistency Conditions Using Observational Refinement. J. ACM , 65 , 1 ( 2018 ), 2:1\u20132:44. H. Attiya, A. Gotsman, S. Hans, and N. Rinetzky. 2018. Characterizing Transactional Memory Consistency Conditions Using Observational Refinement. J. ACM, 65, 1 (2018), 2:1\u20132:44.","journal-title":"Characterizing Transactional Memory Consistency Conditions Using Observational Refinement. J. ACM"},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","unstructured":"M. Batty A. F. Donaldson and J. Wickerson. 2016. Overhauling SC atomics in C11 and OpenCL. In POPL. ACM 634\u2013648. M. Batty A. F. Donaldson and J. Wickerson. 2016. Overhauling SC atomics in C11 and OpenCL. In POPL. ACM 634\u2013648.","DOI":"10.1145\/2914770.2837637"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"M. Batty S. Owens S. Sarkar P. Sewell and T. Weber. 2011. Mathematizing C++ concurrency. In POPL T. Ball and M. Sagiv (Eds.). ACM 55\u201366. isbn:978-1-4503-0490-0 M. Batty S. Owens S. Sarkar P. Sewell and T. Weber. 2011. Mathematizing C++ concurrency. In POPL T. Ball and M. Sagiv (Eds.). ACM 55\u201366. isbn:978-1-4503-0490-0","DOI":"10.1145\/1925844.1926394"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_4"},{"key":"e_1_2_1_12_1","first-page":"1","article-title":"2021","volume":"17","author":"Beillahi S. M.","year":"2021","unstructured":"S. M. Beillahi , A. Bouajjani , and C. Enea . 2021 . Robustness Against Transactional Causal Consistency. Log. Methods Comput. Sci. , 17 , 1 ( 2021 ), https:\/\/lmcs.episciences.org\/7149 S. M. Beillahi, A. Bouajjani, and C. Enea. 2021. Robustness Against Transactional Causal Consistency. Log. Methods Comput. Sci., 17, 1 (2021), https:\/\/lmcs.episciences.org\/7149","journal-title":"Robustness Against Transactional Causal Consistency. Log. Methods Comput. Sci."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_9"},{"key":"e_1_2_1_14_1","volume-title":"Sledgehammer: Judgement Day. In IJCAR (LNCS","author":"B\u00f6hme S.","year":"2010","unstructured":"S. B\u00f6hme and T. Nipkow . 2010 . Sledgehammer: Judgement Day. In IJCAR (LNCS , Vol. 6173). Springer, 107\u2013 121 . S. B\u00f6hme and T. Nipkow. 2010. Sledgehammer: Judgement Day. In IJCAR (LNCS, Vol. 6173). Springer, 107\u2013121."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1835698.1835703"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192373"},{"key":"e_1_2_1_17_1","volume-title":"std::atomic_compare_exchange. https:\/\/en.cppreference.com\/w\/cpp\/atomic\/atomic_compare_exchange Accessed","year":"2022","unstructured":"cppreference.com. 2022. std::atomic_compare_exchange. https:\/\/en.cppreference.com\/w\/cpp\/atomic\/atomic_compare_exchange Accessed 18 July , 2022 cppreference.com. 2022. std::atomic_compare_exchange. https:\/\/en.cppreference.com\/w\/cpp\/atomic\/atomic_compare_exchange Accessed 18 July, 2022"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"L. Dalessandro D. Dice M. L. Scott N. Shavit and M. F. Spear. 2010. Transactional Mutex Locks. In Euro-Par (2) (LNCS Vol. 6272). Springer 2\u201313. L. Dalessandro D. Dice M. L. Scott N. Shavit and M. F. Spear. 2010. Transactional Mutex Locks. In Euro-Par (2) (LNCS Vol. 6272). Springer 2\u201313.","DOI":"10.1007\/978-3-642-15291-7_2"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.11"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.4230\/DARTS.6.2.15"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437801.3441619"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6899919"},{"key":"#cr-split#-e_1_2_1_23_1.1","unstructured":"S. Dalvandi and B. Dongol. 2022. Implementing and Verifying Release-Acquire Transactional Memory (Extended Version). https:\/\/doi.org\/10.48550\/ARXIV.2208.00315 10.48550\/ARXIV.2208.00315"},{"key":"#cr-split#-e_1_2_1_23_1.2","doi-asserted-by":"crossref","unstructured":"S. Dalvandi and B. Dongol. 2022. Implementing and Verifying Release-Acquire Transactional Memory (Extended Version). https:\/\/doi.org\/10.48550\/ARXIV.2208.00315","DOI":"10.1145\/3563352"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-021-09610-2"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523451"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511663079"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-017-0433-3"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11864219_14"},{"key":"e_1_2_1_29_1","volume-title":"Pedone (Eds.) (LIPIcs","volume":"17","author":"Doherty S.","unstructured":"S. Doherty , B. Dongol , J. Derrick , G. Schellhorn , and H. Wehrheim . 2016. Proving Opacity of a Pessimistic STM. In OPODIS, P. Fatourou, E. Jim\u00e9nez, and F . Pedone (Eds.) (LIPIcs , Vol. 70). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 35:1\u201335: 17 . S. Doherty, B. Dongol, J. Derrick, G. Schellhorn, and H. Wehrheim. 2016. Proving Opacity of a Pessimistic STM. In OPODIS, P. Fatourou, E. Jim\u00e9nez, and F. Pedone (Eds.) (LIPIcs, Vol. 70). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 35:1\u201335:17."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98938-9_7"},{"key":"e_1_2_1_31_1","unstructured":"S. Doherty B. Dongol H. Wehrheim and J. Derrick. 2019. Verifying C11 programs operationally. In PPoPP Jeffrey K. Hollingsworth and Idit Keidar (Eds.). ACM 355\u2013365. isbn:978-1-4503-6225-2 S. Doherty B. Dongol H. Wehrheim and J. Derrick. 2019. Verifying C11 programs operationally. In PPoPP Jeffrey K. Hollingsworth and Idit Keidar (Eds.). ACM 355\u2013365. isbn:978-1-4503-6225-2"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0225-8"},{"key":"e_1_2_1_33_1","doi-asserted-by":"crossref","unstructured":"M. Doko and V. Vafeiadis. 2017. Tackling Real-Life Relaxed Concurrency with FSL++. In ESOP. 448\u2013475. M. Doko and V. Vafeiadis. 2017. Tackling Real-Life Relaxed Concurrency with FSL++. In ESOP. 448\u2013475.","DOI":"10.1007\/978-3-662-54434-1_17"},{"key":"e_1_2_1_34_1","unstructured":"S. Dolan KC Sivaramakrishnan and A. Madhavapeddy. 2018. Bounding Data Races in Space and Time. In PLDI (PLDI 2018). ACM New York NY USA. 242\u2013255. isbn:978-1-4503-5698-5 S. Dolan KC Sivaramakrishnan and A. Madhavapeddy. 2018. Bounding Data Races in Space and Time. In PLDI (PLDI 2018). ACM New York NY USA. 242\u2013255. isbn:978-1-4503-5698-5"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47846-3_17"},{"key":"e_1_2_1_36_1","first-page":"1","article-title":"2018. Transactions in relaxed memory architectures","volume":"2","author":"Dongol B.","unstructured":"B. Dongol , R. Jagadeesan , and J. Riely . 2018. Transactions in relaxed memory architectures . PACMPL , 2 , POPL (2018), 18: 1 \u2013 18 :29. B. Dongol, R. Jagadeesan, and J. Riely. 2018. Transactions in relaxed memory architectures. PACMPL, 2, POPL (2018), 18:1\u201318:29.","journal-title":"PACMPL"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293883.3295708"},{"key":"e_1_2_1_38_1","volume-title":"VMCAI (LNCS","volume":"204","author":"Dongol B.","unstructured":"B. Dongol , R. Jagadeesan , J. Riely , and A. Armstrong . 2018. On abstraction and compositionality for weak-memory linearisability . In VMCAI (LNCS , Vol. 10747). Springer, 183\u2013 204 . B. Dongol, R. Jagadeesan, J. Riely, and A. Armstrong. 2018. On abstraction and compositionality for weak-memory linearisability. In VMCAI (LNCS, Vol. 10747). Springer, 183\u2013204."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290373"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22012-8_36"},{"key":"e_1_2_1_41_1","doi-asserted-by":"crossref","unstructured":"R. Guerraoui and M. Kapalka. 2010. Principles of Transactional Memory. Morgan & Claypool Publishers. R. Guerraoui and M. Kapalka. 2010. Principles of Transactional Memory. Morgan & Claypool Publishers.","DOI":"10.1007\/978-3-031-02002-5"},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","unstructured":"M. He V. Vafeiadis S. Qin and J. F. Ferreira. 2016. Reasoning about Fences and Relaxed Atomics. In PDP. IEEE Computer Society 520\u2013527. isbn:978-1-4673-8776-7 M. He V. Vafeiadis S. Qin and J. F. Ferreira. 2016. Reasoning about Fences and Relaxed Atomics. In PDP. IEEE Computer Society 520\u2013527. isbn:978-1-4673-8776-7","DOI":"10.1109\/PDP.2016.103"},{"key":"e_1_2_1_43_1","volume-title":"Transactional Memory: Architectural Support for Lock-Free Data Structures","author":"Herlihy M.","year":"1993","unstructured":"M. Herlihy and J. E. B. Moss . 1993 . Transactional Memory: Architectural Support for Lock-Free Data Structures . In ISCA, A. J. Smith (Ed.). ACM , 289\u2013300. M. Herlihy and J. E. B. Moss. 1993. Transactional Memory: Architectural Support for Lock-Free Data Structures. In ISCA, A. J. Smith (Ed.). ACM, 289\u2013300."},{"key":"e_1_2_1_44_1","first-page":"3","article-title":"1990. Linearizability","volume":"12","author":"Herlihy M.","year":"1990","unstructured":"M. Herlihy and J. M. Wing . 1990. Linearizability : A Correctness Condition for Concurrent Objects. ACM TOPLAS , 12 , 3 ( 1990 ), 463\u2013492. M. Herlihy and J. M. Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. ACM TOPLAS, 12, 3 (1990), 463\u2013492.","journal-title":"A Correctness Condition for Concurrent Objects. ACM TOPLAS"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428262"},{"key":"e_1_2_1_46_1","first-page":"035","volume-title":"M\u00fcller (Ed.) (LIPIcs","volume":"29","author":"Kaiser J.-O.","unstructured":"J.-O. Kaiser , H.-H. Dang , D. D., O. Lahav , and V. Vafeiadis . 2017. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In ECOOP, P . M\u00fcller (Ed.) (LIPIcs , Vol. 74). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 17:1\u201317: 29 . isbn:978-3-95977- 035 - 034 J.-O. Kaiser, H.-H. Dang, D. D., O. Lahav, and V. Vafeiadis. 2017. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In ECOOP, P. M\u00fcller (Ed.) (LIPIcs, Vol. 74). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 17:1\u201317:29. isbn:978-3-95977-035-4"},{"key":"e_1_2_1_47_1","doi-asserted-by":"crossref","unstructured":"J. Kang C.-K. Hur O. Lahav V. Vafeiadis and D. Dreyer. 2017. A promising semantics for relaxed-memory concurrency. In POPL. ACM 175\u2013189. J. Kang C.-K. Hur O. Lahav V. Vafeiadis and D. Dreyer. 2017. A promising semantics for relaxed-memory concurrency. In POPL. ACM 175\u2013189.","DOI":"10.1145\/3093333.3009850"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_10"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_11"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485475"},{"key":"e_1_2_1_52_1","first-page":"47665","volume-title":"Speckmann (Eds.) (LNCS","volume":"323","author":"Lahav O.","unstructured":"O. Lahav and V. Vafeiadis . 2015. Owicki-Gries Reasoning for Weak Memory Models. In ICALP, M. M. Halld\u00f3rsson, K. Iwama, N. Kobayashi, and B . Speckmann (Eds.) (LNCS , Vol. 9135). Springer, 311\u2013 323 . isbn:978-3-662- 47665 - 47669 O. Lahav and V. Vafeiadis. 2015. Owicki-Gries Reasoning for Weak Memory Models. In ICALP, M. M. Halld\u00f3rsson, K. Iwama, N. Kobayashi, and B. Speckmann (Eds.) (LNCS, Vol. 9135). Springer, 311\u2013323. isbn:978-3-662-47665-9"},{"key":"e_1_2_1_53_1","doi-asserted-by":"crossref","unstructured":"O. Lahav V. Vafeiadis J. Kang C.-K. Hur and D. Dreyer. 2017. Repairing sequential consistency in C\/C++11. In PLDI. ACM 618\u2013632. O. Lahav V. Vafeiadis J. Kang C.-K. Hur and D. Dreyer. 2017. Repairing sequential consistency in C\/C++11. In PLDI. ACM 618\u2013632.","DOI":"10.1145\/3140587.3062352"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386010"},{"key":"e_1_2_1_56_1","unstructured":"M. Lesani V. Luchangco and M. Moir. 2012. Putting Opacity in Its Place. In WTTM. M. Lesani V. Luchangco and M. Moir. 2012. Putting Opacity in Its Place. In WTTM."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527324"},{"key":"e_1_2_1_58_1","unstructured":"N. A. Lynch. 1996. Distributed Algorithms. Morgan Kaufmann. isbn:1-55860-348-4 N. A. Lynch. 1996. Distributed Algorithms. Morgan Kaufmann. isbn:1-55860-348-4"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434285"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694393"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/IISWC.2008.4636089"},{"key":"e_1_2_1_62_1","first-page":"319","article-title":"1976","volume":"6","author":"Owicki S. S.","year":"1976","unstructured":"S. S. Owicki and D. Gries . 1976 . An Axiomatic Proof Technique for Parallel Programs I. Acta Inf. , 6 ( 1976 ), 319 \u2013 340 . S. S. Owicki and D. Gries. 1976. An Axiomatic Proof Technique for Parallel Programs I. Acta Inf., 6 (1976), 319\u2013340.","journal-title":"An Axiomatic Proof Technique for Parallel Programs I. Acta Inf."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_22"},{"key":"e_1_2_1_64_1","unstructured":"A. Podkopaev I. Sergey and A. Nanevski. 2016. Operational Aspects of C\/C++ Concurrency. CoRR abs\/1606.01400 (2016) arxiv:1606.01400. A. Podkopaev I. Sergey and A. Nanevski. 2016. Operational Aspects of C\/C++ Concurrency. CoRR abs\/1606.01400 (2016) arxiv:1606.01400."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290381"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_33"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-11245-5_1"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3382734.3405746"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4842-4932-1_8"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3465084.3467944"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/s004460050028"},{"key":"e_1_2_1_72_1","unstructured":"M. Spear H. Boehm V. Luchangco M. L. Scott and M. Wong. 2020. Transactional Memory Lite Support in C++. isocpp. M. Spear H. Boehm V. Luchangco M. L. Scott and M. Wong. 2020. Transactional Memory Lite Support in C++. isocpp."},{"key":"e_1_2_1_73_1","first-page":"89959","volume-title":"Beyer and M. Huisman (Eds.) (LNCS","volume":"209","author":"Summers A. J.","unstructured":"A. J. Summers and P. M\u00fcller . 2018. Automating Deductive Verification for Weak-Memory Programs. In TACAS, D . Beyer and M. Huisman (Eds.) (LNCS , Vol. 10805). Springer, 190\u2013 209 . isbn:978-3-319- 89959 - 89956 A. J. Summers and P. M\u00fcller. 2018. Automating Deductive Verification for Weak-Memory Programs. In TACAS, D. Beyer and M. Huisman (Eds.) (LNCS, Vol. 10805). Springer, 190\u2013209. isbn:978-3-319-89959-6"},{"key":"e_1_2_1_74_1","first-page":"89883","volume-title":"Ahmed (Ed.) (LNCS","volume":"384","author":"Svendsen K.","unstructured":"K. Svendsen , J. Pichon-Pharabod , M. Doko , O. Lahav , and V. Vafeiadis . 2018. A Separation Logic for a Promising Semantics. In ESOP, A . Ahmed (Ed.) (LNCS , Vol. 10801). Springer, 357\u2013 384 . isbn:978-3-319- 89883 - 89884 K. Svendsen, J. Pichon-Pharabod, M. Doko, O. Lahav, and V. Vafeiadis. 2018. A Separation Logic for a Promising Semantics. In ESOP, A. Ahmed (Ed.) (LNCS, Vol. 10801). Springer, 357\u2013384. isbn:978-3-319-89883-4"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737992"},{"key":"e_1_2_1_76_1","doi-asserted-by":"crossref","unstructured":"A. Turon V. Vafeiadis and D. Dreyer. 2014. GPS: navigating weak memory with ghosts protocols and separation. In OOPSLA A. P. Black and T. D. Millstein (Eds.). ACM 691\u2013707. isbn:978-1-4503-2585-1 A. Turon V. Vafeiadis and D. Dreyer. 2014. GPS: navigating weak memory with ghosts protocols and separation. In OOPSLA A. P. Black and T. D. Millstein (Eds.). ACM 691\u2013707. isbn:978-1-4503-2585-1","DOI":"10.1145\/2660193.2660243"},{"key":"e_1_2_1_77_1","doi-asserted-by":"crossref","unstructured":"V. Vafeiadis and C. Narayan. 2013. Relaxed separation logic: A program logic for C11 concurrency. In OOPSLA. 867\u2013884. V. Vafeiadis and C. Narayan. 2013. Relaxed separation logic: A program logic for C11 concurrency. In OOPSLA. 867\u2013884.","DOI":"10.1145\/2544173.2509532"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_13"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.21"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/3328796"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563352","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563352","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:02:33Z","timestamp":1750186953000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563352"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":81,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563352"],"URL":"https:\/\/doi.org\/10.1145\/3563352","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}