---
OA_place: publisher
OA_type: hybrid
_id: '10417'
abstract:
- lang: eng
  text: "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.\r\n\r\nWe
    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."
acknowledgement: "The research was partly supported by Austrian Science Fund (FWF)
  Grant No P23499- N23, FWF\r\nNFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant
  (279307: Graph Games), and Czech\r\nScience Foundation grant GBP202/12/G061."
article_number: '31'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Marek
  full_name: Chalupa, Marek
  last_name: Chalupa
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Andreas
  full_name: Pavlogiannis, Andreas
  id: 49704004-F248-11E8-B48F-1D18A9856A87
  last_name: Pavlogiannis
  orcid: 0000-0002-8943-0722
- first_name: Nishant
  full_name: Sinha, Nishant
  last_name: Sinha
- first_name: Kapil
  full_name: Vaidya, Kapil
  last_name: Vaidya
citation:
  ama: 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>
  apa: '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>'
  chicago: 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>.
  ieee: 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.
  ista: 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.
  mla: 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>.
  short: M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Proceedings
    of the ACM on Programming Languages 2 (2018).
conference:
  end_date: 2018-01-13
  location: Los Angeles, CA, United States
  name: 'POPL: Programming Languages'
  start_date: 2018-01-07
date_created: 2021-12-05T23:01:49Z
date_published: 2018-01-01T00:00:00Z
date_updated: 2025-05-20T09:45:10Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1145/3158119
ec_funded: 1
external_id:
  arxiv:
  - '1610.01188'
file:
- access_level: open_access
  checksum: b27ab1745f6dba2387deb785798a657c
  content_type: application/pdf
  creator: dernst
  date_created: 2025-05-20T09:44:47Z
  date_updated: 2025-05-20T09:44:47Z
  file_id: '19716'
  file_name: 2018_ACM_Chalupa.pdf
  file_size: 388891
  relation: main_file
  success: 1
file_date_updated: 2025-05-20T09:44:47Z
has_accepted_license: '1'
intvolume: '         2'
issue: POPL
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
  eissn:
  - 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
  record:
  - id: '5448'
    relation: earlier_version
    status: public
  - id: '5456'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: Data-centric dynamic partial order reduction
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 2
year: '2018'
...