Verifying concurrent systems is notoriously hard due to the inherent non-determinism in interprocess communication. Effective verification methods rely on dynamic partial order reduction (DPOR) techniques, which can reason about system correctness without exploring all concurrent traces explicitly. DPOR is traditionally based on the Mazurkiewicz equivalence, which distinguishes between traces based on the relative order of their conflicting events.
In this talk I will present the recently introduced Observation equivalence for DPOR. In contrast to reordering conflicting events, this equivalence is data centric: it distinguishes traces based on which write events are observed by which read events. This equivalence induces a partitioning that is exponentially coarser than the Mazurkiewicz partitioning without sacrificing completeness of bug finding. It also admits natural, efficient DPOR-like algorithms for exploring the partitioning optimally, leading to speedups over the standard methods. I will conclude with some new challenges posed by this data-centric view.
Stateless model-checking under the data-centric view