Delay-Bounded Scheduling: A Canonical Characterization of Scheduler Nondeterminism

Share

Michael Emmi, Shaz Qadeer, Zvonimir Rakamaric. Microsoft Research Tech Report MSR-TR-2010-123, September, 2010.
[pdf] [bib]

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 buf fered 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.

Bibtex:

@techreport{msr-tr-2010-123,
  author = {Michael Emmi and Shaz Qadeer and Zvonimir Rakamari\'c},
  title = {Delay-Bounded Scheduling: {A} Canonical Characterization of
    Scheduler Nondeterminism},
  institution = {Microsoft Research},
  year = {2010},
  month = {September},
  number = {MSR-TR-2010-123},
}