{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T12:47:08Z","timestamp":1770382028156,"version":"3.49.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001824","name":"Czech Science Foundation","doi-asserted-by":"crossref","award":["GBP202\/12\/G061"],"award-info":[{"award-number":["GBP202\/12\/G061"]}],"id":[{"id":"10.13039\/501100001824","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["P23499- N23, S11407-N23"],"award-info":[{"award-number":["P23499- N23, S11407-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["279307: Graph Games"],"award-info":[{"award-number":["279307: Graph Games"]}],"id":[{"id":"10.13039\/501100000781","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":[[2018,1]]},"abstract":"<jats:p>\n            We present a new dynamic partial-order reduction method for stateless model checking of concurrent programs. A common approach for exploring program behaviors relies on enumerating the traces of the program, without storing the visited states (aka\n            <jats:italic>stateless<\/jats:italic>\n            exploration). As the number of distinct traces grows exponentially, dynamic partial-order reduction (DPOR) techniques have been successfully used to partition the space of traces into equivalence classes (\n            <jats:italic>Mazurkiewicz<\/jats:italic>\n            partitioning), with the goal of exploring only few representative traces from each class.\n          <\/jats:p>\n          <jats:p>\n            We introduce a new equivalence on traces under sequential consistency semantics, which we call the\n            <jats:italic>observation<\/jats:italic>\n            equivalence. Two traces are observationally equivalent if every read event observes the same write event in both traces. While the traditional Mazurkiewicz equivalence is control-centric, our new definition is data-centric. We show that our observation equivalence is coarser than the Mazurkiewicz equivalence, and in many cases even exponentially coarser. We devise a DPOR exploration of the trace space, called\n            <jats:italic>data-centric<\/jats:italic>\n            DPOR, based on the observation equivalence.\n          <\/jats:p>\n          <jats:p>\n            <jats:list>\n              <jats:list-item>\n                <jats:p>\n                  For acyclic architectures, our algorithm is guaranteed to explore\n                  <jats:italic>exactly<\/jats:italic>\n                  one representative trace from each observation class, while spending polynomial time per class. Hence, our algorithm is\n                  <jats:italic>optimal<\/jats:italic>\n                  wrt the observation equivalence, and in several cases explores exponentially fewer traces than\n                  <jats:italic>any<\/jats:italic>\n                  enumerative method based on the Mazurkiewicz equivalence.\n                <\/jats:p>\n              <\/jats:list-item>\n              <jats:list-item>\n                <jats:p>For cyclic architectures, we consider an equivalence between traces which is finer than the observation equivalence; but coarser than the Mazurkiewicz equivalence, and in some cases is exponentially coarser. Our data-centric DPOR algorithm remains optimal under this trace equivalence.<\/jats:p>\n              <\/jats:list-item>\n            <\/jats:list>\n          <\/jats:p>\n          <jats:p>Finally, we perform a basic experimental comparison between the existing Mazurkiewicz-based DPOR and our data-centric DPOR on a set of academic benchmarks. Our results show a significant reduction in both running time and the number of explored equivalence classes.<\/jats:p>","DOI":"10.1145\/3158119","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":49,"title":["Data-centric dynamic partial order reduction"],"prefix":"10.1145","volume":"2","author":[{"given":"Marek","family":"Chalupa","sequence":"first","affiliation":[{"name":"Masaryk University, Czechia"}]},{"given":"Krishnendu","family":"Chatterjee","sequence":"additional","affiliation":[{"name":"IST Austria, Austria"}]},{"given":"Andreas","family":"Pavlogiannis","sequence":"additional","affiliation":[{"name":"IST Austria, Austria"}]},{"given":"Nishant","family":"Sinha","sequence":"additional","affiliation":[{"name":"Kena Labs, India"}]},{"given":"Kapil","family":"Vaidya","sequence":"additional","affiliation":[{"name":"IIT Bombay, India"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535845"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_28"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958083"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_42"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/SWAT.1973.14"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050035"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_2_9_1","volume-title":"Peled","author":"Clarke Edmund M.","year":"1999","unstructured":"Edmund M. Clarke , Jr., Orna Grumberg , and Doron A . Peled . 1999 a. Model Checking. MIT Press , Cambridge, MA, USA. Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. 1999a. Model Checking. MIT Press, Cambridge, MA, USA."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814297"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103693"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_14"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_2_2_14_1","volume-title":"Johnson","author":"Garey Michael R.","year":"1979","unstructured":"Michael R. Garey and David S . Johnson . 1979 . Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman & Co. , New York, NY, USA. Michael R. Garey and David S. Johnson. 1979. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman & Co., New York, NY, USA."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-1489-x"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384077"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737975"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2351676.2351698"},{"key":"e_1_2_2_21_1","doi-asserted-by":"crossref","unstructured":"Vineet Kahlon Chao Wang and Aarti Gupta. 2009. Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique. In CAV.  Vineet Kahlon Chao Wang and Aarti Gupta. 2009. Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique. In CAV.","DOI":"10.1007\/978-3-642-02658-4_31"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90054-J"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0078-9"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12029-9_22"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_2_2_28_1","volume-title":"CHESS: A systematic testing tool for concurrent software. Technical Report.","author":"Madan Musuvathi Tom Ball","year":"2007","unstructured":"Tom Ball Madan Musuvathi , Shaz Qadeer . 2007 . CHESS: A systematic testing tool for concurrent software. Technical Report. Tom Ball Madan Musuvathi, Shaz Qadeer. 2007. CHESS: A systematic testing tool for concurrent software. Technical Report."},{"key":"e_1_2_2_29_1","unstructured":"Friedemann Mattern. 1989. Virtual Time and Global States of Distributed Systems. In Parallel and Distributed Algorithms. North-Holland 215\u2013226.  Friedemann Mattern. 1989. Virtual Time and Global States of Distributed Systems. In Parallel and Distributed Algorithms. North-Holland 215\u2013226."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17906-2_30"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384314"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273442.1250785"},{"key":"e_1_2_2_33_1","volume-title":"Piramanayagam Arumuga Nainar, and Iulian Neamtiu","author":"Musuvathi Madanlal","year":"2008","unstructured":"Madanlal Musuvathi , Shaz Qadeer , Thomas Ball , Gerard Basler , Piramanayagam Arumuga Nainar, and Iulian Neamtiu . 2008 . Finding and Reproducing Heisenbugs in Concurrent Programs. In OSDI. Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. 2008. Finding and Reproducing Heisenbugs in Concurrent Programs. In OSDI."},{"key":"e_1_2_2_34_1","doi-asserted-by":"crossref","unstructured":"Doron Peled. 1993. All from One One for All: On Model Checking Using Representatives. In CAV.  Doron Peled. 1993. All from One One for All: On Model Checking Using Representatives. In CAV.","DOI":"10.1007\/3-540-56922-7_34"},{"key":"e_1_2_2_36_1","unstructured":"C\u00e9sar Rodr\u00edguez Marcelo Sousa Subodh Sharma and Daniel Kroening. 2015. Unfolding-based Partial Order Reduction. In CONCUR.  C\u00e9sar Rodr\u00edguez Marcelo Sousa Subodh Sharma and Daniel Kroening. 2015. Unfolding-based Partial Order Reduction. In CONCUR."},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2012.18"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693017_25"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70889-6_13"},{"key":"e_1_2_2_40_1","doi-asserted-by":"crossref","unstructured":"Samira Tasharofi Rajesh K. Karmani Steven Lauterburg Axel Legay Darko Marinov and Gul Agha. 2012. TransDPOR: A Novel Dynamic Partial-order Reduction Technique for Testing Actor Programs. In FMOODS\/FORTE.  Samira Tasharofi Rajesh K. Karmani Steven Lauterburg Axel Legay Darko Marinov and Gul Agha. 2012. TransDPOR: A Novel Dynamic Partial-order Reduction Technique for Testing Actor Programs. In FMOODS\/FORTE.","DOI":"10.1007\/978-3-642-30793-5_14"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-53863-1_36"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_29"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158119","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158119","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158119"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":40,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158119"],"URL":"https:\/\/doi.org\/10.1145\/3158119","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}