{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:12:34Z","timestamp":1767928354276,"version":"3.49.0"},"reference-count":61,"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":[{"name":"NSF","award":["SHF 1901069, CCF 2007428"],"award-info":[{"award-number":["SHF 1901069, CCF 2007428"]}]},{"DOI":"10.13039\/100006785","name":"Google","doi-asserted-by":"publisher","award":["PhD Fellowship"],"award-info":[{"award-number":["PhD Fellowship"]}],"id":[{"id":"10.13039\/100006785","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>\n            Concurrent programs are notoriously hard to write correctly, as scheduling nondeterminism introduces subtle errors that are both hard to detect and to reproduce. The most common concurrency errors are (data) races, which occur when memory-conflicting actions are executed concurrently. Consequently, considerable effort has been made towards developing efficient techniques for race detection. The most common approach is dynamic race prediction: given an observed, race-free trace \u03c3 of a concurrent program, the task is to decide whether events of \u03c3 can be correctly reordered to a trace \u03c3\n            <jats:sup>*<\/jats:sup>\n            that witnesses a race hidden in \u03c3.\n          <\/jats:p>\n          <jats:p>\n            In this work we introduce the notion of sync(hronization)-preserving races. A sync-preserving race occurs in \u03c3 when there is a witness \u03c3\n            <jats:sup>*<\/jats:sup>\n            in which synchronization operations (e.g., acquisition and release of locks) appear in the same order as in \u03c3. This is a broad definition that strictly subsumes the famous notion of happens-before races. Our main results are as follows. First, we develop a sound and complete algorithm for predicting sync-preserving races. For moderate values of parameters like the number of threads, the algorithm runs in \u00d5(\n            <jats:italic>N<\/jats:italic>\n            ) time and space, where\n            <jats:italic>N<\/jats:italic>\n            is the length of the trace \u03c3. Second, we show that the problem has a \u03a9(\n            <jats:italic>N<\/jats:italic>\n            \/log\n            <jats:sup>2<\/jats:sup>\n            <jats:italic>N<\/jats:italic>\n            ) space lower bound, and thus our algorithm is essentially time and space optimal. Third, we show that predicting races with even just a single reversal of two sync operations is NP-complete and even W1-hard when parameterized by the number of threads. Thus, sync-preservation characterizes exactly the tractability boundary of race prediction, and our algorithm is nearly optimal for the tractable side. Our experiments show that our algorithm is fast in practice, while sync-preservation characterizes races often missed by state-of-the-art methods.\n          <\/jats:p>","DOI":"10.1145\/3434317","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T17:34:24Z","timestamp":1609781664000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":32,"title":["Optimal prediction of synchronization-preserving races"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7610-0660","authenticated-orcid":false,"given":"Umang","family":"Mathur","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8943-0722","authenticated-orcid":false,"given":"Andreas","family":"Pavlogiannis","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Deterministic Concurrency: A Clock-Synchronised Shared Memory Approach","author":"Aguado Joaqu\u00edn","year":"2018","unstructured":"Joaqu\u00edn Aguado , Michael Mendler , Marc Pouzet , Partha Roop , and Reinhard von Hanxleden . 2018 . Deterministic Concurrency: A Clock-Synchronised Shared Memory Approach . In Programming Languages and Systems, Amal Ahmed (Ed.). Springer International Publishing , Cham , 86-113. Joaqu\u00edn Aguado, Michael Mendler, Marc Pouzet, Partha Roop, and Reinhard von Hanxleden. 2018. Deterministic Concurrency: A Clock-Synchronised Shared Memory Approach. In Programming Languages and Systems, Amal Ahmed (Ed.). Springer International Publishing, Cham, 86-113."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1167473.1167488"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855591.1855595"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/2001252.2001255"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2414729.2414732"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806626"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368119"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512560"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45718-6_81"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815427"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/122759.122767"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-005-3861-2"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250762"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/838237.838485"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_14"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_21"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.84874"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542490"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375618"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360605"},{"key":"e_1_2_1_21_1","volume-title":"Bond","author":"Gen\u00e7 Kaan","year":"2020","unstructured":"Kaan Gen\u00e7 , Yufan Xu , and Michael D . Bond . 2020 . Personal Communication . ( 2020 ). Kaan Gen\u00e7, Yufan Xu, and Michael D. Bond. 2020. Personal Communication. ( 2020 )."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794279614"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290370"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594315"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984024"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276516"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522736"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062374"},{"key":"e_1_2_1_30_1","volume-title":"Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM 21, 7 (","author":"Lamport Leslie","year":"1978","unstructured":"Leslie Lamport . 1978. Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM 21, 7 ( July 1978 ), 558-565. Leslie Lamport. 1978. Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM 21, 7 ( July 1978 ), 558-565."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2931037.2931046"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1346281.1346323"},{"key":"e_1_2_1_33_1","unstructured":"Umang Mathur. 2020. RAPID. https:\/\/github.com\/umangm\/rapid Accessed: 2020-10-25.  Umang Mathur. 2020. RAPID. https:\/\/github.com\/umangm\/rapid Accessed: 2020-10-25."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276515"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394783"},{"key":"e_1_2_1_36_1","volume-title":"Optimal Prediction of Synchronization-Preserving Races. CoRR abs\/","author":"Mathur Umang","year":"2010","unstructured":"Umang Mathur , Andreas Pavlogiannis , and Mahesh Viswanathan . 2020b. Optimal Prediction of Synchronization-Preserving Races. CoRR abs\/ 2010 .16385 ( 2020 ). arXiv: 2010.16385 https:\/\/arxiv.org\/abs\/ 2010.16385 Umang Mathur, Andreas Pavlogiannis, and Mahesh Viswanathan. 2020b. Optimal Prediction of Synchronization-Preserving Races. CoRR abs\/ 2010.16385 ( 2020 ). arXiv: 2010.16385 https:\/\/arxiv.org\/abs\/ 2010.16385"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373376.3378475"},{"key":"e_1_2_1_38_1","first-page":"215","article-title":"Virtual Time and Global States of Distributed Systems","author":"Mattern Friedemann","year":"1988","unstructured":"Friedemann Mattern . 1988 . Virtual Time and Global States of Distributed Systems . In Parallel and Distributed Algorithms. North-Holland , 215 - 226 . Friedemann Mattern. 1988. Virtual Time and Global States of Distributed Systems. In Parallel and Distributed Algorithms. North-Holland, 215-226.","journal-title":"Parallel and Distributed Algorithms. North-Holland"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250738"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371085"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/781498.781529"},{"key":"e_1_2_1_42_1","volume-title":"Bond","author":"Roemer Jake","year":"2019","unstructured":"Jake Roemer and Michael D . Bond . 2019 . Online Set-Based Dynamic Analysis for Sound Predictive Race Detection. CoRR abs\/ 1907.08337 ( 2019 ). arXiv: 1907.08337 http:\/\/arxiv.org\/abs\/ 1907.08337 Jake Roemer and Michael D. Bond. 2019. Online Set-Based Dynamic Analysis for Sound Predictive Race Detection. CoRR abs\/ 1907.08337 ( 2019 ). arXiv: 1907.08337 http:\/\/arxiv.org\/abs\/ 1907.08337"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192385"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385993"},{"key":"e_1_2_1_45_1","unstructured":"Grigore Rosu. 2018. RV-Predict Runtime Verification. Accessed: 2018-04-01.  Grigore Rosu. 2018. RV-Predict Runtime Verification. Accessed: 2018-04-01."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/1986308.1986334"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/265924.265927"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/73141.74844"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375584"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/11494881_14"},{"key":"e_1_2_1_51_1","volume-title":"International Conference on Runtime Verification. Springer, 136-150","author":"\u015eerb\u0103nu\u0163\u0103 Traian Florin","year":"2012","unstructured":"Traian Florin \u015eerb\u0103nu\u0163\u0103 , Feng Chen , and Grigore Ro\u015fu . 2012 . Maximal causal models for sequentially consistent systems . In International Conference on Runtime Verification. Springer, 136-150 . Traian Florin \u015eerb\u0103nu\u0163\u0103, Feng Chen, and Grigore Ro\u015fu. 2012. Maximal causal models for sequentially consistent systems. In International Conference on Runtime Verification. Springer, 136-150."},{"key":"e_1_2_1_52_1","unstructured":"Ilya Sergey. 2019. What Does It Mean for a Program Analysis to Be Sound? https:\/\/blog.sigplan.org\/ 2019 \/08\/07\/what-does-itmean-for-a-program-analysis-to-be-sound\/  Ilya Sergey. 2019. What Does It Mean for a Program Analysis to Be Sound? https:\/\/blog.sigplan.org\/ 2019 \/08\/07\/what-does-itmean-for-a-program-analysis-to-be-sound\/"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103702"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/582034.582042"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882300"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/504282.504288"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_17"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10766-018-0579-5"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095810.1095832"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293883.3295731"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2009.56"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434317","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434317","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434317","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:35Z","timestamp":1750195475000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434317"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":61,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434317"],"URL":"https:\/\/doi.org\/10.1145\/3434317","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}