{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:09:23Z","timestamp":1784200163275,"version":"3.55.0"},"reference-count":65,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["851811"],"award-info":[{"award-number":["851811"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003977","name":"Israel Science Foundation","doi-asserted-by":"publisher","award":["814\/22"],"award-info":[{"award-number":["814\/22"]}],"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":[[2025,6,10]]},"abstract":"<jats:p>\n                    Dynamic race detection is a highly effective runtime verification technique for identifying data races by instrumenting and monitoring concurrent program runs. However, standard dynamic race detection is incompatible with practical weak memory models; the added instrumentation introduces extra synchronization, which masks weakly consistent behaviors and inherently misses certain data races. In response, we propose to dynamically verify\n                    <jats:italic toggle=\"yes\">program robustness<\/jats:italic>\n                    \u2014a property ensuring that a program exhibits only strongly consistent behaviors. Building on an existing static decision procedure, we develop an algorithm for dynamic robustness verification under a C11-style memory model. The algorithm is based on \u201clocation clocks\u201d, a variant of vector clocks used in standard race detection. It allows effective and easy-to-apply defense against weak memory on a per-program basis, which can be combined with race detection that assumes strong consistency. We implement our algorithm in a tool, called RSan, and evaluate it across various settings. To our knowledge, this work is the first to propose and develop dynamic verification of robustness against weak memory models.\n                  <\/jats:p>","DOI":"10.1145\/3729277","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"675-698","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Dynamic Robustness Verification against Weak Memory"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7266-8681","authenticated-orcid":false,"given":"Roy","family":"Margalit","sequence":"first","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7905-9739","authenticated-orcid":false,"given":"Michalis","family":"Kokologiannakis","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7276-7644","authenticated-orcid":false,"given":"Shachar","family":"Itzhaky","sequence":"additional","affiliation":[{"name":"Technion, Haifa, 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, Tel Aviv, Israel"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65630-9_2"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360576"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26850-7_3"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_13"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2994593"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_6"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926394"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_17"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2019.30"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2247684.2247688"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375591"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806626"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_29"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_21"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22012-8_34"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250737"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1736020.1736040"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_12"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19835-9_3"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1073970.1073974"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43951-7_14"},{"key":"e_1_3_2_24_1","volume-title":"Cooperating sequential processes","author":"Dijkstra Edsger Wybe","year":"1965","unstructured":"Edsger Wybe Dijkstra. 1965. Cooperating sequential processes, Technical Report EWD-123. Technical Report. http:\/\/www.cs.utexas.edu\/~EWD\/transcriptions\/EWD01xx\/EWD123.html"},{"issue":"1","key":"e_1_3_2_25_1","first-page":"56","article-title":"Timestamps in message-passing systems that preserve the partial ordering. Proceedings of the 11th Australian","volume":"10","author":"Fidge C. J.","year":"1988","unstructured":"C. J. Fidge. 1988. Timestamps in message-passing systems that preserve the partial ordering. Proceedings of the 11th Australian Computer Science Conference 10, 1 (1988), 56\u201366. http:\/\/sky.scitech.qut.edu.au\/~fidgec\/Publications\/fidge88a.pdf","journal-title":"Computer Science Conference"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542490"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3575693.3575729"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_2_29_1","unstructured":"ISO\/IEC 14882:2011. 2011. Programming Language C++."},{"key":"e_1_3_2_30_1","unstructured":"ISO\/IEC 9899:2011. 2011. Programming Language C."},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2009.5160998"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062374"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","unstructured":"Michalis Kokologiannakis Ori Lahav Konstantinos Sagonas and Viktor Vafeiadis. 2017. Effective stateless model checking for C\/C++ concurrency. Proc. ACM Program. Lang. 2 POPL Article 17 (Dec. 2017) 32 pages. doi:10.1145\/3158105","DOI":"10.1145\/3158105"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-572494_4"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837643"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314604"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/7351.7352"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2442516.2442524"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009857"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314635"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22306-8_10"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_24"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254115"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","unstructured":"Lun Liu Todd Millstein and Madanlal Musuvathi. 2017. A volatile-by-default JVM for server applications. Proc. ACM Program. Lang. 1 OOPSLA Article 49 (Oct. 2017) 25 pages. doi:10.1145\/3133873","DOI":"10.1145\/3133873"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3462206"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446711"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018611"},{"key":"e_1_3_2_51_1","doi-asserted-by":"crossref","unstructured":"Roy Margalit Michalis Kokologiannakis Shachar Itzhaky and Ori Lahav. 2025a. Dynamic robustness verification against weak memory (extended version). arXiv:2504.15036 [cs.PL] https:\/\/arxiv.org\/abs\/2504.15036","DOI":"10.1145\/3729277"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","unstructured":"Roy Margalit Michalis Kokologiannakis Shachar Itzhaky and Ori Lahav. 2025b. Robustness sanitizer. doi:10.5281\/zenodo.15002568","DOI":"10.5281\/zenodo.15002568"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","unstructured":"Roy Margalit and Ori Lahav. 2021. Verifying observational robustness against a C11-style memory model. Proc. ACM Program. Lang. 5 POPL Article 4 (Jan. 2021) 33 pages. doi:10.1145\/3434285","DOI":"10.1145\/3434285"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993522"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3540250.3569450"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394783"},{"key":"e_1_3_2_57_1","first-page":"215","volume-title":"Proc. Workshop on Parallel and Distributed Algorithms","author":"Mattern Friedemann","year":"1989","unstructured":"Friedemann Mattern. 1989. Virtual time and global states of distributed systems. In Proc. Workshop on Parallel and Distributed Algorithms. North-Holland \/ Elsevier, 215\u2013226."},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","unstructured":"Kartik Nagar Anmol Sahoo Romit Roy Chowdhury and Suresh Jagannathan. 2024. Automated robustness cerification of concurrent data structure libraries against relaxed memory models. Proc. ACM Program. Lang. 8 OOPSLA2 Article 362 (Oct. 2024) 28 pages. doi:10.1145\/3689802","DOI":"10.1145\/3689802"},{"key":"e_1_3_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446748"},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371085"},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(81)90106-X"},{"key":"e_1_3_2_62_1","doi-asserted-by":"publisher","DOI":"10.5555\/1228965.1228969"},{"key":"e_1_3_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/265924.265927"},{"key":"e_1_3_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/1791194.1791203"},{"key":"e_1_3_2_65_1","unstructured":"ThreadSanitizer 2020. ThreadSanitizer manual. Retrieved March 2024 from https:\/\/github.com\/google\/sanitizers\/wiki\/ThreadSanitizerCppManual"},{"key":"e_1_3_2_66_1","doi-asserted-by":"publisher","DOI":"10.1504\/IJHPCN.2017.086532"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729277","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:09:40Z","timestamp":1784196580000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729277"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":65,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729277"],"URL":"https:\/\/doi.org\/10.1145\/3729277","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}