Bounded partial-order reduction

Eliminating concurrency errors is increasingly important as systems rely more on parallelism for performance. Exhaus-tively exploring the state-space of a program’s thread in-terleavings finds concurrency errors and provides coverage guarantees, but suffers from exponential state-space explo-sion. Two prior approaches alleviate state-space explosion. (1) Dynamic partial-order reduction (DPOR) provides full coverage and explores only one interleaving of independent transitions. (2) Bounded search provides bounded coverage by enumerating interleavings that do not exceed a bound. In particular, we focus on preemption-bounding. Combin-ing partial-order reduction with preemption-bounding had remained an open problem. We show that preemption-bounded search explores th