article published yes Marek Chalupa author Krishnendu Chatterjee author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X Andreas Pavlogiannis author 49704004-F248-11E8-B48F-1D18A9856A870000-0002-8943-0722 Nishant Sinha author Kapil Vaidya author KrCh department POPL: Programming Languages Modern Graph Algorithmic Techniques in Formal Verification project Rigorous Systems Engineering project Quantitative Graph Games: Theory and Applications project 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 stateless 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 (Mazurkiewicz partitioning), with the goal of exploring only few representative traces from each class. We introduce a new equivalence on traces under sequential consistency semantics, which we call the observation 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 data-centric DPOR, based on the observation equivalence. https://research-explorer.ista.ac.at/download/10417/19716/2018_ACM_Chalupa.pdf application/pdfno Association for Computing Machinery2018Los Angeles, CA, United States eng 2475-1421 1610.0118810.1145/3158119 2POPL https://research-explorer.ista.ac.at/record/5448 https://research-explorer.ista.ac.at/record/5456 Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. 2018. Data-centric dynamic partial order reduction. Proceedings of the ACM on Programming Languages. 2(POPL), 31. M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Proceedings of the ACM on Programming Languages 2 (2018). Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. Data-centric dynamic partial order reduction. <i>Proceedings of the ACM on Programming Languages</i>. 2018;2(POPL). doi:<a href="https://doi.org/10.1145/3158119">10.1145/3158119</a> M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya, “Data-centric dynamic partial order reduction,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 2, no. POPL. Association for Computing Machinery, 2018. Chalupa, Marek, et al. “Data-Centric Dynamic Partial Order Reduction.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 2, no. POPL, 31, Association for Computing Machinery, 2018, doi:<a href="https://doi.org/10.1145/3158119">10.1145/3158119</a>. Chalupa, Marek, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. “Data-Centric Dynamic Partial Order Reduction.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2018. <a href="https://doi.org/10.1145/3158119">https://doi.org/10.1145/3158119</a>. Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., &#38; Vaidya, K. (2018). Data-centric dynamic partial order reduction. <i>Proceedings of the ACM on Programming Languages</i>. Los Angeles, CA, United States: Association for Computing Machinery. <a href="https://doi.org/10.1145/3158119">https://doi.org/10.1145/3158119</a> 104172021-12-05T23:01:49Z2025-05-20T09:45:10Z