{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:53:49Z","timestamp":1781855629815,"version":"3.54.5"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100003977","name":"Israel Science Foundation","doi-asserted-by":"publisher","award":["5166651"],"award-info":[{"award-number":["5166651"]}],"id":[{"id":"10.13039\/501100003977","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":[[2021,1,4]]},"abstract":"<jats:p>We study the problem of verifying the robustness of concurrent programs against a C11-style memory model that includes relaxed accesses and release\/acquire accesses and fences, and show that this verification problem can be reduced to a standard reachability problem under sequential consistency. We further observe that existing robustness notions do not allow the verification of programs that use speculative reads as in the sequence lock mechanism, and introduce a novel \"observational robustness\" property that fills this gap. In turn, we show how to soundly check for observational robustness. We have implemented our method and applied it to several challenging concurrent algorithms, demonstrating the applicability of our approach. To the best of our knowledge, this is the first method for verifying robustness against a programming language concurrency model that includes relaxed accesses and release\/acquire fences.<\/jats:p>","DOI":"10.1145\/3434285","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T12:34:24Z","timestamp":1609763664000},"page":"1-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Verifying observational robustness against a c11-style memory model"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7266-8681","authenticated-orcid":false,"given":"Roy","family":"Margalit","sequence":"first","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4305-6998","authenticated-orcid":false,"given":"Ori","family":"Lahav","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221"},{"key":"e_1_2_1_2_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. 2015b. Precise and sound automatic fence insertion procedure under PSO. In NETYS. Springer International Publishing, Cham, 32-47."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_13"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/325164.325100"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2994593"},{"key":"e_1_2_1_6_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-66. http:\/\/dl.acm.org\/citation.cfm?id= 2032305. 2032311"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706303"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_2"},{"key":"e_1_2_1_10_1","volume-title":"Atomic usage examples. Retrieved june 08","author":"Bahmann Helge","year":"2020","unstructured":"Helge Bahmann and Tim Blechmann. 2012. Atomic usage examples. Retrieved june 08, 2020 from https:\/\/www.boost.org\/ doc\/libs\/1_55_0\/doc\/html\/atomic\/usage_examples.html"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926394"},{"key":"e_1_2_1_12_1","volume-title":"Computer Aided Verification","author":"Beillahi Sidi Mohamed","unstructured":"Sidi Mohamed Beillahi, Ahmed Bouajjani, and Constantin Enea. 2019a. Checking robustness against snapshot isolation. In Computer Aided Verification. Springer International Publishing, Cham, 286-304."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2247684.2247688"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2618128.2618134"},{"key":"e_1_2_1_17_1","volume-title":"P0982R1: Weaken release sequences","author":"Boehm J","unstructured":"Hans-J Boehm, Olivier Giroux, and Viktor Vafeiades. 2018. P0982R1: Weaken release sequences. http:\/\/www.openstd.org\/jtc1\/sc22\/wg21\/docs\/papers\/2018\/p0982r1.html. Accessed: 2020-05-27."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_29"},{"key":"e_1_2_1_19_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-353."},{"key":"e_1_2_1_20_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-440."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192415"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250737"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_12"},{"key":"e_1_2_1_24_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-25."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1073970.1073974"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.11"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371102"},{"key":"e_1_2_1_28_1","unstructured":"Egor Derevenetc. 2015. Robustness against relaxed memory models. Ph.D. Dissertation. University of Kaiserslautern. http:\/\/kluedo.ub.uni-kl.de\/frontdoor\/index\/index\/docId\/4074"},{"key":"e_1_2_1_29_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-170."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293883.3295702"},{"key":"e_1_2_1_31_1","volume-title":"Tackling real-life relaxed concurrency with FSL++","author":"Doko Marko","unstructured":"Marko Doko and Viktor Vafeiadis. 2017. Tackling real-life relaxed concurrency with FSL++. In ESOP. Springer Berlin Heidelberg, Berlin, Heidelberg, 448-475."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1071610.1071615"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837615"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-7315(92)90052-O"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33651-5_3"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_37_1","volume-title":"Retrieved","author":"Kang Jeehoon","year":"2018","unstructured":"Jeehoon Kang. 2018. Deque proof. Retrieved June 11, 2020 from https:\/\/github.com\/jeehoonkang\/crossbeam-rfcs\/blob\/dequeproof\/text\/2018-01-07-deque-proof.md"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158105"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314604"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_1_42_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-160. http:\/\/dl.acm.org\/citation.cfm?id= 2032692. 2032707"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_24"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254115"},{"key":"e_1_2_1_45_1","doi-asserted-by":"crossref","unstructured":"Roy Margalit and Ori Lahav. 2020. Verifying observational robustness against a C11-style memory model. https: \/\/www.cs.tau.ac.il\/~orilahav\/papers\/popl21_robustness_full.pdf (full version of this paper).","DOI":"10.1145\/3434285"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR"},{"key":"e_1_2_1_47_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-503."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290382"},{"key":"e_1_2_1_49_1","first-page":"213","volume-title":"Retrieved","year":"2020","unstructured":"Rust. 2020. std::sync::Arc. Retrieved June 11, 2020 from https:\/\/doc.rust-lang.org\/src\/alloc\/sync.rs.html# 213-216"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3079856.3080206"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509532"},{"key":"e_1_2_1_52_1","volume-title":"Retrieved","author":"Dmitriy V'","year":"2008","unstructured":"Dmitriy V' jukov. 2008. C+ + atomics and memory ordering. Retrieved June 23, 2020 from https:\/\/bartoszmilewski.com\/ 2008 \/12\/01\/c-atomics-and-memory-ordering\/#comment-111"},{"key":"e_1_2_1_53_1","volume-title":"Retrieved","author":"Dmitriy V'","year":"2013","unstructured":"Dmitriy V' jukov. 2013. Relacy race detector. Retrieved July 06, 2020 from http:\/\/www.1024cores.net\/home\/relacy-racedetector"},{"key":"e_1_2_1_54_1","volume-title":"Retrieved","author":"Williams Anthony","year":"2008","unstructured":"Anthony Williams. 2008. Peterson's lock with C++0x atomics. Retrieved October 26, 2018 from https:\/\/www. justsoftwaresolutions.co.uk\/threading\/petersons_lock_with_C+ +0x_atomics.html"},{"key":"e_1_2_1_55_1","volume-title":"Retrieved","author":"Williams Anthony","year":"2010","unstructured":"Anthony Williams. 2010. Implementing Dekker's algorithm with fences. Retrieved June 08, 2020 from https:\/\/www. justsoftwaresolutions.co.uk\/threading\/implementing_dekkers_algorithm_with_fences.html"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434285","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434285","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:26:29Z","timestamp":1781853989000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434285"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":55,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434285"],"URL":"https:\/\/doi.org\/10.1145\/3434285","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}