Michael Emmi, Shaz Qadeer, and Zvonimir Rakamaric
We provide a new characterization of scheduling nondeterminism by allowing
deterministic schedulers to delay their next-scheduled task. In limiting the
delays an otherwise-deterministic scheduler is allowed, we discover
concurrency bugs efficiently---by exploring few schedules---and robustly---i.e.,
independent of the number of tasks, context switches, or buffered events.
Our characterization elegantly applies to any systematic exploration (e.g.,
testing, model checking) of concurrent programs with dynamic task-creation.
Additionally, we show that certain delaying schedulers admit efficient
reductions from concurrent to sequential program analysis.