{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:04:07Z","timestamp":1767927847336,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":56,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T00:00:00Z","timestamp":1559952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,6,8]]},"DOI":"10.1145\/3314221.3314604","type":"proceedings-article","created":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:02:18Z","timestamp":1559941338000},"page":"126-141","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":26,"title":["Robustness against release\/acquire semantics"],"prefix":"10.1145","author":[{"given":"Ori","family":"Lahav","sequence":"first","affiliation":[{"name":"Tel Aviv University, Israel"}]},{"given":"Roy","family":"Margalit","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}]}],"member":"320","published-online":{"date-parts":[[2019,6,8]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"Ori Lahav and Roy Margalit. 2019. Supplementary material for this paper. https:\/\/www.cs.tau.ac.il\/~orilahav\/papers\/pldi19full.pdf  Ori Lahav and Roy Margalit. 2019. Supplementary material for this paper. https:\/\/www.cs.tau.ac.il\/~orilahav\/papers\/pldi19full.pdf"},{"key":"e_1_3_2_2_2_1","volume-title":"Mohamed Faouzi Atig, and Shankaranarayanan Krishna","author":"Abdulla Parosh Aziz","year":"2019","unstructured":"Parosh Aziz Abdulla , Jatin Arora , Mohamed Faouzi Atig, and Shankaranarayanan Krishna . 2019 . Verification of programs under the releaseacquire semantics. In PLDI ( to appear). Parosh Aziz Abdulla, Jatin Arora, Mohamed Faouzi Atig, and Shankaranarayanan Krishna. 2019. Verification of programs under the releaseacquire semantics. In PLDI (to appear)."},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276505"},{"key":"e_1_3_2_2_4_1","volume-title":"Magnus L\u00e5ng, and Tuan Phong Ngo.","author":"Abdulla Parosh Aziz","year":"2015","unstructured":"Parosh Aziz Abdulla , Mohamed Faouzi Atig , Magnus L\u00e5ng, and Tuan Phong Ngo. 2015 . Precise and sound automatic fence insertion procedure under PSO. In NETYS. Springer International Publishing , Cham, 32\u201347. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Magnus L\u00e5ng, and Tuan Phong Ngo. 2015. Precise and sound automatic fence insertion procedure under PSO. In NETYS. Springer International Publishing, Cham, 32\u201347."},{"key":"e_1_3_2_2_5_1","volume-title":"Mohamed Faouzi Atig, and Tuan-Phong Ngo","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 ESOP. Springer-Verlag New York , Inc., New York, 308\u2013332. 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 ESOP. Springer-Verlag New York, Inc., New York, 308\u2013332."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/325164.325100"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01784241"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2994593"},{"key":"e_1_3_2_2_9_1","volume-title":"Stability in weak memory models","author":"Alglave Jade","year":"2032","unstructured":"Jade Alglave and Luc Maranget . 2011. Stability in weak memory models . In CAV. Springer-Verlag , Berlin, Heidelberg , 50\u201366. http: \/\/dl.acm.org\/citation.cfm?id= 2032 305.2032311 Jade Alglave and Luc Maranget. 2011. Stability in weak memory models. In CAV. Springer-Verlag, Berlin, Heidelberg, 50\u201366. http: \/\/dl.acm.org\/citation.cfm?id=2032305.2032311"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706303"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_2"},{"key":"e_1_3_2_2_13_1","volume-title":"The problem of programming language concurrency semantics","author":"Batty Mark","unstructured":"Mark Batty , Kayvan Memarian , Kyndylan Nienhuis , Jean PichonPharabod , and Peter Sewell . 2015. The problem of programming language concurrency semantics . In ESOP. Springer , Berlin, Heidelberg , 283\u2013307. Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean PichonPharabod, and Peter Sewell. 2015. The problem of programming language concurrency semantics. In ESOP. Springer, Berlin, Heidelberg, 283\u2013307."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_2_2_15_1","first-page":"1","article-title":"Robustness against consistency models with atomic visibility. In CONCUR. Schloss Dagstuhl\u2013 Leibniz-Zentrum fuer Informatik, Dagstuhl","volume":"7","author":"Bernardi Giovanni","year":"2016","unstructured":"Giovanni Bernardi and Alexey Gotsman . 2016 . Robustness against consistency models with atomic visibility. In CONCUR. Schloss Dagstuhl\u2013 Leibniz-Zentrum fuer Informatik, Dagstuhl , Germany , 7 : 1 \u2013 7 :15. Giovanni Bernardi and Alexey Gotsman. 2016. Robustness against consistency models with atomic visibility. In CONCUR. Schloss Dagstuhl\u2013 Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 7:1\u20137:15.","journal-title":"Germany"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2247684.2247688"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_29"},{"key":"e_1_3_2_2_18_1","volume-title":"Suha Orhun Mutluergil, and Serdar Tasiran","author":"Bouajjani Ahmed","year":"2018","unstructured":"Ahmed Bouajjani , Constantin Enea , Suha Orhun Mutluergil, and Serdar Tasiran . 2018 . Reasoning about TSO programs using reduction and abstraction. In CAV. Springer , Cham, 336\u2013353. Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, and Serdar Tasiran. 2018. Reasoning about TSO programs using reduction and abstraction. In CAV. Springer, Cham, 336\u2013353."},{"key":"e_1_3_2_2_19_1","volume-title":"Deciding robustness against total store ordering","author":"Bouajjani Ahmed","unstructured":"Ahmed Bouajjani , Roland Meyer , and Eike M\u00f6hlmann . 2011. Deciding robustness against total store ordering . In ICALP. Springer, Berlin , Heidelberg , 428\u2013440. Ahmed Bouajjani, Roland Meyer, and Eike M\u00f6hlmann. 2011. Deciding robustness against total store ordering. In ICALP. Springer, Berlin, Heidelberg, 428\u2013440."},{"key":"e_1_3_2_2_20_1","volume-title":"PLDI","author":"Brutschy Lucas","unstructured":"Lucas Brutschy , Dimitar Dimitrov , Peter M\u00fcller , and Martin Vechev . 2018. Static serializability analysis for causal consistency . In PLDI . ACM , New York , 90\u2013104. Lucas Brutschy, Dimitar Dimitrov, Peter M\u00fcller, and Martin Vechev. 2018. Static serializability analysis for causal consistency. In PLDI. ACM, New York, 90\u2013104."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250737"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_12"},{"key":"e_1_3_2_2_23_1","volume-title":"Sound and complete monitoring of sequential consistency for relaxed memory models","author":"Burnim Jabob","unstructured":"Jabob Burnim , Koushik Sen , and Christos Stergiou . 2011. Sound and complete monitoring of sequential consistency for relaxed memory models . In TACAS. Springer , Berlin, Heidelberg , 11\u201325. Jabob Burnim, Koushik Sen, and Christos Stergiou. 2011. Sound and complete monitoring of sequential consistency for relaxed memory models. In TACAS. Springer, Berlin, Heidelberg, 11\u201325."},{"key":"e_1_3_2_2_25_1","volume-title":"Robustness against Power is PSpace-complete","author":"Derevenetc Egor","unstructured":"Egor Derevenetc and Roland Meyer . 2014. Robustness against Power is PSpace-complete . In ICALP. Springer , Berlin, Heidelberg , 158\u2013170. Egor Derevenetc and Roland Meyer. 2014. Robustness against Power is PSpace-complete. In ICALP. Springer, Berlin, Heidelberg, 158\u2013170."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2011.159"},{"key":"e_1_3_2_2_27_1","volume-title":"PPoPP","author":"Doherty Simon","unstructured":"Simon Doherty , Brijesh Dongol , Heike Wehrheim , and John Derrick . 2019. Verifying C11 programs operationally . In PPoPP . ACM , New York , 355\u2013365. Simon Doherty, Brijesh Dongol, Heike Wehrheim, and John Derrick. 2019. Verifying C11 programs operationally. In PPoPP. ACM, New York, 355\u2013365."},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1071610.1071615"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-7315(92)90052-O"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33651-5_3"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_2_2_32_1","volume-title":"The SPARC architecture manual (version 9)","author":"SPARC International Inc. 1994.","unstructured":"SPARC International Inc. 1994. The SPARC architecture manual (version 9) . Prentice-Hall, Inc. , Upper Saddle River, NJ, USA. SPARC International Inc. 1994. The SPARC architecture manual (version 9). Prentice-Hall, Inc., Upper Saddle River, NJ, USA."},{"key":"e_1_3_2_2_33_1","first-page":"1","article-title":"Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. In ECOOP. Schloss Dagstuhl\u2013 Leibniz-Zentrum fuer Informatik, Dagstuhl","volume":"17","author":"Kaiser Jan-Oliver","year":"2017","unstructured":"Jan-Oliver Kaiser , Hoang-Hai Dang , Derek Dreyer , Ori Lahav , and Viktor Vafeiadis . 2017 . Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. In ECOOP. Schloss Dagstuhl\u2013 Leibniz-Zentrum fuer Informatik, Dagstuhl , Germany , 17 : 1 \u2013 17 :29. Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. 2017. Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. In ECOOP. Schloss Dagstuhl\u2013 Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 17:1\u201317:29.","journal-title":"Germany"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158105"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.16"},{"key":"e_1_3_2_2_36_1","volume-title":"POPL","author":"Lahav Ori","unstructured":"Ori Lahav , Nick Giannarakis , and Viktor Vafeiadis . 2016. Taming release-acquire consistency . In POPL . ACM , New York , 649\u2013662. Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis. 2016. Taming release-acquire consistency. In POPL. ACM, New York, 649\u2013662."},{"key":"e_1_3_2_2_37_1","volume-title":"Owicki-Gries reasoning for weak memory models","author":"Lahav Ori","unstructured":"Ori Lahav and Viktor Vafeiadis . 2015. Owicki-Gries reasoning for weak memory models . In ICALP. Springer-Verlag , Berlin, Heidelberg , 311\u2013323. Ori Lahav and Viktor Vafeiadis. 2015. Owicki-Gries reasoning for weak memory models. In ICALP. Springer-Verlag, Berlin, Heidelberg, 311\u2013323."},{"key":"e_1_3_2_2_38_1","volume-title":"Explaining relaxed memory models with program transformations","author":"Lahav Ori","unstructured":"Ori Lahav and Viktor Vafeiadis . 2016. Explaining relaxed memory models with program transformations . In FM. Springer , Cham , 479\u2013495. Ori Lahav and Viktor Vafeiadis. 2016. Explaining relaxed memory models with program transformations. In FM. Springer, Cham, 479\u2013495."},{"key":"e_1_3_2_2_39_1","volume-title":"PLDI","author":"Lahav Ori","unstructured":"Ori Lahav , Viktor Vafeiadis , Jeehoon Kang , Chung-Kil Hur , and Derek Dreyer . 2017. Repairing sequential consistency in C\/C++11 . In PLDI . ACM , New York , 618\u2013632. Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. 2017. Repairing sequential consistency in C\/C++11. In PLDI. ACM, New York, 618\u2013632."},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_2_41_1","volume-title":"A verification-based approach to memory fence insertion in relaxed memory systems","author":"Linden Alexander","year":"2032","unstructured":"Alexander Linden and Pierre Wolper . 2011. A verification-based approach to memory fence insertion in relaxed memory systems . In SPIN. Springer-Verlag , Berlin, Heidelberg , 144\u2013160. http:\/\/dl.acm.org\/ citation.cfm?id= 2032 692.2032707 Alexander Linden and Pierre Wolper. 2011. A verification-based approach to memory fence insertion in relaxed memory systems. In SPIN. Springer-Verlag, Berlin, Heidelberg, 144\u2013160. http:\/\/dl.acm.org\/ citation.cfm?id=2032692.2032707"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_24"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254115"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_26"},{"key":"e_1_3_2_2_45_1","unstructured":"Luc Maranget Susmit Sarkar and Peter Sewell. 2012. A tutorial introduction to the ARM and POWER relaxed memory models. http:\/\/www.cl.cam.ac.uk\/~pes20\/ppc-supplemental\/test7.pdf .  Luc Maranget Susmit Sarkar and Peter Sewell. 2012. A tutorial introduction to the ARM and POWER relaxed memory models. http:\/\/www.cl.cam.ac.uk\/~pes20\/ppc-supplemental\/test7.pdf ."},{"key":"e_1_3_2_2_46_1","volume-title":"Pattern-based synthesis of synchronization for the C++ memory model","author":"Meshman Yuri","unstructured":"Yuri Meshman , Noam Rinetzky , and Eran Yahav . 2015. Pattern-based synthesis of synchronization for the C++ memory model . In FMCAD. FMCAD Inc , Austin, TX , 120\u2013127. http:\/\/dl.acm.org\/citation.cfm?id= 2893529.2893552 Yuri Meshman, Noam Rinetzky, and Eran Yahav. 2015. Pattern-based synthesis of synchronization for the C++ memory model. In FMCAD. FMCAD Inc, Austin, TX, 120\u2013127. http:\/\/dl.acm.org\/citation.cfm?id= 2893529.2893552"},{"key":"e_1_3_2_2_47_1","volume-title":"CONCUR","volume":"118","author":"Nagar Kartik","year":"2018","unstructured":"Kartik Nagar and Suresh Jagannathan . 2018 . Automated detection of serializability violations under weak consistency . In CONCUR 2018, Vol. 118 . Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 41:1\u201341:18. Kartik Nagar and Suresh Jagannathan. 2018. Automated detection of serializability violations under weak consistency. In CONCUR 2018, Vol. 118. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 41:1\u201341:18."},{"key":"e_1_3_2_2_48_1","volume-title":"OOPSLA","author":"Norris Brian","unstructured":"Brian Norris and Brian Demsky . 2013. CDSchecker: checking concurrent data structures written with C\/C++ atomics . In OOPSLA . ACM , New York , 131\u2013150. Brian Norris and Brian Demsky. 2013. CDSchecker: checking concurrent data structures written with C\/C++ atomics. In OOPSLA. ACM, New York, 131\u2013150."},{"key":"e_1_3_2_2_49_1","volume-title":"Reasoning about the implementation of concurrency abstractions on x86-TSO","author":"Owens Scott","unstructured":"Scott Owens . 2010. Reasoning about the implementation of concurrency abstractions on x86-TSO . In ECOOP. Springer-Verlag , Berlin, Heidelberg , 478\u2013503. Scott Owens. 2010. Reasoning about the implementation of concurrency abstractions on x86-TSO. In ECOOP. Springer-Verlag, Berlin, Heidelberg, 478\u2013503."},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/42190.42277"},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043592"},{"key":"e_1_3_2_2_53_1","volume-title":"A separation logic for a promising semantics","author":"Svendsen Kasper","unstructured":"Kasper Svendsen , Jean Pichon-Pharabod , Marko Doko , Ori Lahav , and Viktor Vafeiadis . 2018. A separation logic for a promising semantics . In ESOP. Springer International Publishing , Cham , 357\u2013384. Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, and Viktor Vafeiadis. 2018. A separation logic for a promising semantics. In ESOP. Springer International Publishing, Cham, 357\u2013384."},{"key":"e_1_3_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660243"},{"key":"e_1_3_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509532"},{"key":"e_1_3_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009838"},{"key":"e_1_3_2_2_57_1","volume-title":"Retrieved","author":"Williams Anthony","year":"2008","unstructured":"Anthony Williams . 2008 . Peterson\u2019s lock with C++0x atomics . Retrieved October 26, 2018 from https:\/\/www.justsoftwaresolutions.co. uk\/threading\/petersons_lock_with_C++0x_atomics.html Anthony Williams. 2008. Peterson\u2019s lock with C++0x atomics. Retrieved October 26, 2018 from https:\/\/www.justsoftwaresolutions.co. uk\/threading\/petersons_lock_with_C++0x_atomics.html"}],"event":{"name":"PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Phoenix AZ USA","acronym":"PLDI '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314604","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314604","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:22Z","timestamp":1750204402000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314604"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,8]]},"references-count":56,"alternative-id":["10.1145\/3314221.3314604","10.1145\/3314221"],"URL":"https:\/\/doi.org\/10.1145\/3314221.3314604","relation":{},"subject":[],"published":{"date-parts":[[2019,6,8]]},"assertion":[{"value":"2019-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}