Delay-Bounded Scheduling

2011_POPL_eqr screenshot

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.

Citation

Michael Emmi, Shaz Qadeer, Zvonimir Rakamaric
Delay-Bounded Scheduling
Lecture Notes in Computer Science, 411--422, 2011.

BibTeX

@inproceedings{2011_POPL_eqr,
  title = {Delay-Bounded Scheduling},
  author = {Michael Emmi and Shaz Qadeer and Zvonimir Rakamaric},
  journal = {Lecture Notes in Computer Science},
  booktitle = {Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)},
  editor = {Thomas Ball and Mooly Sagiv},
  publisher = {ACM},
  pages = {411--422},
  year = {2011}
}