Delay-Bounded Scheduling

Michael Emmi, Shaz Qadeer, and Zvonimir Rakamaric

Abstract

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.

Details

Publication typeTechReport
NumberMSR-TR-2010-123
> Publications > Delay-Bounded Scheduling