{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:49:03Z","timestamp":1780994943005,"version":"3.54.1"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nd\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>\n            <jats:italic toggle=\"yes\">Trace theory<\/jats:italic>\n            (formulated by Mazurkiewicz in 1987) is a principled framework for defining equivalence relations for concurrent program runs based on a commutativity relation over the set of atomic steps taken by individual program threads. Its simplicity, elegance, and algorithmic efficiency makes it useful in many different contexts including program verification and testing. It is well-understood that the larger the equivalence classes are, the more benefits they would bring to the algorithms and applications that use them. In this paper, we study relaxations of trace equivalence with the goal of maintaining its algorithmic advantages.\n          <\/jats:p>\n          <jats:p>\n            We first prove that the largest appropriate relaxation of trace equivalence, an equivalence relation that preserves the order of steps taken by each thread\n            <jats:italic toggle=\"yes\">and<\/jats:italic>\n            what write operation each read operation observes, does not yield efficient algorithms. Specifically, we prove a\n            <jats:italic toggle=\"yes\">linear space lower bound<\/jats:italic>\n            for the problem of checking, in a streaming setting, if two arbitrary steps of a concurrent program run are\n            <jats:italic toggle=\"yes\">causally concurrent<\/jats:italic>\n            (i.e. they can be reordered in an equivalent run) or\n            <jats:italic toggle=\"yes\">causally ordered<\/jats:italic>\n            (i.e. they always appear in the same order in all equivalent runs). The same problem can be decided in\n            <jats:italic toggle=\"yes\">constant space<\/jats:italic>\n            for trace equivalence. Next, we propose a new commutativity-based notion of equivalence called\n            <jats:italic toggle=\"yes\">grain equivalence<\/jats:italic>\n            that is strictly more relaxed than trace equivalence, and yet yields a constant space algorithm for the same problem. This notion of equivalence uses commutativity of\n            <jats:italic toggle=\"yes\">grains<\/jats:italic>\n            , which are sequences of atomic steps, in addition to the standard commutativity from trace theory. We study the two distinct cases when the grains are contiguous subwords of the input program run and when they are not, formulate the precise definition of causal concurrency in each case, and show that they can be decided in\n            <jats:italic toggle=\"yes\">constant space<\/jats:italic>\n            , despite being strict relaxations of the notion of causal concurrency based on trace equivalence.\n          <\/jats:p>","DOI":"10.1145\/3632873","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"911-941","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Coarser Equivalences for Causal Concurrency"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9005-2653","authenticated-orcid":false,"given":"Azadeh","family":"Farzan","sequence":"first","affiliation":[{"name":"University of Toronto, Toronto, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7610-0660","authenticated-orcid":false,"given":"Umang","family":"Mathur","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360576"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_16"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632915"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60246-1_149"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158119"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360550"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660211"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/554921"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837650"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250762"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","unstructured":"Azadeh Farzan. 2023. Commutativity in automated verification. In LICS. 1\u20137. https:\/\/doi.org\/10.1109\/LICS56636.2023.10175734 10.1109\/LICS56636.2023.10175734","DOI":"10.1109\/LICS56636.2023.10175734"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523727"},{"key":"e_1_3_1_14_1","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1007\/11817963_30","volume-title":"Computer Aided Verification","author":"Farzan Azadeh","year":"2006","unstructured":"Azadeh Farzan, P. Madhusudan. 2006. Causal Atomicity. In Computer Aided Verification, Thomas Ball, Robert B. Jones. Springer Berlin Heidelberg, Berlin, Heidelberg, 315\u2013328."},{"key":"e_1_3_1_15_1","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/978-3-540-70545-1_8","volume-title":"Computer Aided Verification","author":"Farzan Azadeh","year":"2008","unstructured":"Azadeh Farzan, P. Madhusudan. 2008. Monitoring Atomicity in Concurrent Programs. In Computer Aided Verification. Aarti Gupta, Sharad Malik. Springer Berlin Heidelberg, Berlin, Heidelberg, 52\u201365."},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393651"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_21"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2208.12117"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_11"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371081"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542490"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375618"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/2367430.2367439"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/181014.181328"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794279614"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56922-7_36"},{"key":"e_1_3_1_29_1","unstructured":"Michel Hack. 1976. Petri net language. Massachusetts Institute of Technology"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180225"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.96"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594315"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2000.1727"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1006\/jpdc.1999.1574"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276516"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90054-J"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062374"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236025"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00120-3"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498711"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2021.16"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-019-00347-1"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276515"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434317"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373376.3378475"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/25542.25553"},{"key":"e_1_3_1_49_1","doi-asserted-by":"crossref","unstructured":"Robin Milner. 1980. A calculus of communicating systems. Springer.","DOI":"10.1007\/3-540-10235-3"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371085"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192385"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44881-0_35"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/1986308.1986334"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2555243.2555262"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57182-5_59"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/11494881_14"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103702"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882300"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3426182.3426185"},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591291"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591291"},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_17"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.09.023"},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17906-2_31"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632873","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632873","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:07:40Z","timestamp":1751659660000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632873"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":63,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632873"],"URL":"https:\/\/doi.org\/10.1145\/3632873","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}