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 JunDisplayed time zone: Mountain Time (US & Canada) change
14:00 - 15:40 | |||
14:00 20mTalk | 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 20mTalk | Fixed Parameter Tractable Linearizability Monitoring PLDI Research Papers DOI Pre-print | ||
14:40 20mTalk | SuperCollider: Scalable and Effective Data Race Detection for CUDA PLDI Research Papers Mark Stephenson NVIDIA, Sana Damani NVIDIA, Mohamed Tarek Ibn Ziad NVIDIA, Anis Ladram NVIDIA, Michael Garland NVIDIA DOI | ||
15:00 20mTalk | Fast Atomicity Monitoring PLDI Research Papers DOI | ||