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
Proceedings of the 38th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 411--422, doi:10.1145/1926385.1926432, 2011.
BibTeX
@inproceedings{2011_popl_eqr,
title = {Delay-Bounded Scheduling},
author = {Michael Emmi and Shaz Qadeer and Zvonimir Rakamaric},
booktitle = {Proceedings of the 38th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL)},
publisher = {ACM},
pages = {411--422},
doi = {10.1145/1926385.1926432},
year = {2011}
}
Acknowledgements
We thank Ahmed Bouajjani, Pierre Ganty, Rupak Majumdar, and Gennaro Parlato for providing helpful insight, and the anonymous reviewers for their numerous comments and suggestions.