Wed 17 Jun 2026 14:00 - 14:20 at Flatirons 3 - Concurrency Chair(s): Shoaib Kamil

We study the estimation problem for concurrent programs: given a bounded program $P$, estimate the number of maximal Mazurkiewicz trace–equivalence classes induced by its interleavings. This quantity informs two practical questions for enumeration-based model checking: how long a model checking run is likely to take, and what fraction of the search space has been covered so far. We first show the counting problem is #P-hard even for restricted programs and, unless P = NP, inapproximable within any subexponential factor in polynomial time. Thus, we cannot expect efficient exact or randomized approximation algorithms. We give a Monte Carlo approach to find a polynomial-time unbiased estimator: we convert a stateless optimal DPOR algorithm into an unbiased estimator by viewing its exploration as a bounded-depth, bounded-width, tree whose leaves are the maximal Mazurkiewicz traces. A classical estimator by Knuth, when run on this tree, gives an unbiased estimation. In order to control the variance of the estimation, we apply stochastic enumeration by maintaining a small population of partial paths per depth whose evolution is coupled. We have implemented our estimator in the JMC model checker and evaluated it on shared-memory benchmarks. We find that with modest budgets, our estimator yields stable estimates—typically within a 20$%$ band—within a few hundred trials, even when the state space has $10^5–10^6$ classes. We also show how the same machinery estimates model-checking cost by weighting all explored traces, not only the maximal ones. Our algorithms provide the first provable poly-time unbiased estimators for counting Mazurkiewicz traces.

Wed 17 Jun

Displayed time zone: Mountain Time (US & Canada) change

14:00 - 15:40
ConcurrencyPLDI Research Papers at Flatirons 3
Chair(s): Shoaib Kamil Adobe
14:00
20m
Talk
State Space Estimation for DPOR-Based Model Checkers
PLDI Research Papers
A. R. Balasubramanian MPI-SWS, Mohammad Hossein Khoshechin Jorshari MPI-SWS, Rupak Majumdar MPI-SWS, Umang Mathur National University of Singapore, Minjian Zhang University of Illinois Urbana-Champaign
DOI Pre-print
14:20
20m
Talk
Fixed Parameter Tractable Linearizability Monitoring
PLDI Research Papers
Zheng Han Lee National University of Singapore, Umang Mathur National University of Singapore
DOI Pre-print
14:40
20m
Talk
SuperCollider: Scalable and Effective Data Race Detection for CUDA
PLDI Research Papers
DOI
15:00
20m
Talk
Fast Atomicity Monitoring
PLDI Research Papers
Hünkar Can Tunç Uber, Yifan Dong Aarhus University, Andreas Pavlogiannis Aarhus University
DOI