research-article

Delay-bounded scheduling

Authors:

Zvonimir RakamarićAuthors Info & Claims

ACM SIGPLAN Notices, Volume 46, Issue 1

Pages 411 - 422

https://doi.org/10.1145/1925844.1926432

Published: 26 January 2011 Publication History

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.

Supplementary Material

MP4 File (37-mpeg-4.mp4)

Download
389.16 MB

References

[1]

M. Abadi and L. Lamport. The existence of refinement mappings. Theor. Comput. Sci., 82 (2): 253--284, 1991.

Digital Library

[2]

M. F. Atig, A. Bouajjani, and S. Qadeer. Context-bounded analysis for concurrent programs with dynamic creation of threads. In TACAS '09: Proc. 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 5505 of LNCS, pages 107--123. Springer, 2009.

Digital Library

[3]

T. Ball, S. Burckhardt, K. E. Coons, M. Musuvathi, and S. Qadeer. Preemption sealing for efficient concurrency testing. In TACAS '10: Proc. 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 6015 of LNCS, pages 420--434. Springer, 2010.

Digital Library

[4]

M. Barnett and K. R. M. Leino. Weakest-precondition of unstructured programs. In PASTE '05: Proc. ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, pages 82--87. ACM, 2005.

Digital Library

[5]

A. Bouajjani and R. Majumdar. Personal communication, July 2010.

[6]

S. Burckhardt and M. Musuvathi. Personal communication, November 2010.

[7]

S. Burckhardt, P. Kothari, M. Musuvathi, and S. Nagarakatte. A randomized scheduler with probabilistic guarantees of finding bugs. In ASPLOS '10: Proc. 15th International Conference on Architectural Support for Programming Languages and Operating Systems, pages 167--178. ACM, 2010.

Digital Library

[8]

E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs, volume 131 of LNCS, pages 52--71. Springer, 1981.

Digital Library

[9]

J. Corbet, A. Rubini, and G. Kroah-Hartman. Linux Device Drivers. O'Reilly Media, Inc., 3rd edition, 2005.

Digital Library

[10]

L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS '08: Proc. 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 4963 of LNCS, pages 337--340. Springer, 2008.

Digital Library

[11]

R. DeLine and K. R. M. Leino. BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research, 2005.

[12]

O. Edelstein, E. Farchi, E. Goldin, Y. Nir, G. Ratsaby, and S. Ur. Framework for testing multi-threaded Java programs. Concurrency and Computation: Practice and Experience, 15 (3--5): 485--499, 2003.

[13]

M. Emmi, S. Qadeer, and Z. Rakamarić. Delay-bounded scheduling: A canonical characterization of scheduler nondeterminism. Technical Report MSR-TR-2010-123, Microsoft Research, 2010. http://research.microsoft.com/apps/pubs/?id=138569.

[14]

P. Ganty and R. Majumdar. Algorithmic verification of asynchronous programs. CoRR, abs/1011.0551, 2010. http://arxiv.org/abs/1011.0551.

Digital Library

[15]

J. J. Garrett. Ajax: A new approach to web applications, February 2005. http://www.adaptivepath.com/ideas/essays/archives/000385.php.

[16]

N. Ghafari, A. J. Hu, and Z. Rakamarić. Context-bounded translations for concurrent software: An empirical evaluation. In SPIN '10: Proc. 17th International Workshop on Model Checking Software, volume 6349 of LNCS, pages 227--244. Springer, 2010.

Digital Library

[17]

P. Godefroid. Model checking for programming languages using VeriSoft. In POPL '97: Proc. 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 174--186. ACM, 1997.

Digital Library

[18]

J. L. Hill, R. Szewczyk, A. Woo, S. Hollar, D. E. Culler, and K. S. J. Pister. System architecture directions for networked sensors. In ASPLOS '00: Proc. 9th International Conference on Architectural Support for Programming Languages and Operating Systems, pages 93--104. ACM, 2000.

Digital Library

[19]

R. Jhala and R. Majumdar. Interprocedural analysis of asynchronous programs. In POPL '07: Proc. 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 339--350. ACM, 2007.

Digital Library

[20]

P. Joshi, M. Naik, C.-S. Park, and K. Sen. CalFuzzer: An extensible active testing framework for concurrent programs. In CAV '09: Proc. 21st International Conference on Computer Aided Verification, volume 5643 of LNCS, pages 675--681. Springer, 2009.

Digital Library

[21]

N. Kidd, S. Jagannathan, and J. Vitek. One stack to run them all: Reducing concurrent analysis to sequential analysis under priority scheduling. In SPIN '10: Proc. 17th International Workshop on Model Checking Software, volume 6349 of LNCS, pages 245--261. Springer, 2010.

Digital Library

[22]

E. Kohler, R. Morris, B. Chen, J. Jannotti, and M. F. Kaashoek. The Click modular router. ACM Trans. Comput. Syst., 18 (3): 263--297, 2000.

Digital Library

[23]

S. La Torre, P. Madhusudan, and G. Parlato. Reducing context-bounded concurrent reachability to sequential reachability. In CAV '09: Proc. 21st International Conference on Computer Aided Verification, volume 5643 of LNCS, pages 477--492. Springer, 2009.

Digital Library

[24]

S. La Torre, P. Madhusudan, and G. Parlato. Model-checking parameterized concurrent programs using linear interfaces. In CAV '10: Proc. 22nd International Conference on Computer Aided Verification, volume 6174 of LNCS, pages 629--644. Springer, 2010.

Digital Library

[25]

S. La Torre, P. Madhusudan, and G. Parlato. Sequentializing parameterized programs, 2010. Under submission.

[26]

S. K. Lahiri, S. Qadeer, and Z. Rakamarić. Static and precise detection of concurrency errors in systems code using SMT solvers. In CAV '09: Proc. 21st International Conference on Computer Aided Verification, volume 5643 of LNCS, pages 509--524. Springer, 2009.

Digital Library

[27]

A. Lal and T. W. Reps. Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods in System Design, 35 (1): 73--97, 2009.

Digital Library

[28]

L. Lamport. Proving the correctness of multiprocess programs. IEEE Trans. Software Eng., 3 (2): 125--143, 1977.

Digital Library

[29]

M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In PLDI '07: Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 446--455. ACM, 2007.

Digital Library

[30]

M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. A. Nainar, and I. Neamtiu. Finding and reproducing Heisenbugs in concurrent programs. In OSDI '08: Proc. 8th USENIX Symposium on Operating Systems Design and Implementation, pages 267--280. USENIX Association, 2008.

Digital Library

[31]

W. Oney. Programming the Microsoft Windows Driver Model. Microsoft Press, 2nd edition, 2002.

Digital Library

[32]

V. S. Pai, P. Druschel, and W. Zwaenepoel. Flash: An efficient and portable web server. In USENIX '99: Proc. General Track of the USENIX Annual Technical Conference, pages 199--212. USENIX, 1999.

Digital Library

[33]

C. H. Papadimitriou. Computational Complexity. Addison Wesley, 1993.

[34]

S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. In TACAS '05: Proc. 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 3440 of LNCS, pages 93--107. Springer, 2005.

Digital Library

[35]

S. Qadeer and D. Wu. KISS: Keep it simple and sequential. In PLDI '04: Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 14--24. ACM, 2004.

Digital Library

[36]

G. Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst., 22 (2): 416--430, 2000.

Digital Library

[37]

K. Sen and M. Viswanathan. Model checking multithreaded programs with asynchronous atomic methods. In CAV '06: Proc. 18th International Conference on Computer Aided Verification, volume 4144 of LNCS, pages 300--314. Springer, 2006.

Digital Library

Cited By

Chen DJiang YXu CMa X(2021)On interleaving space exploration of multi-threaded programsFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-020-9501-615:4Online publication date: 1-Aug-2021
https://dl.acm.org/doi/10.1007/s11704-020-9501-6
Johnson AWahl T(2021)Delay-Bounded Scheduling Without Delay!Computer Aided Verification10.1007/978-3-030-81685-8_18(380-402)Online publication date: 15-Jul-2021
https://doi.org/10.1007/978-3-030-81685-8_18
Abdulla PAtig MGodbole AKrishna SVafeiadis V(2021)The Decidability of Verification under PS 2.0Programming Languages and Systems10.1007/978-3-030-72019-3_1(1-29)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72019-3_1
Show More Cited By

Index Terms

Delay-bounded scheduling

Recommendations

Delay-bounded scheduling
POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

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 ...
Exploiting synchronization in the analysis of shared-memory asynchronous programs
SPIN 2014: Proceedings of the 2014 International SPIN Symposium on Model Checking of Software

As asynchronous programming becomes more mainstream, program analyses capable of automatically uncovering programming errors are increasingly in demand. Since asynchronous program analysis is computationally costly, current approaches sacrifice ...
Asynchronous programs with prioritized task-buffers
FSE '12: Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering

We consider the algorithmic analysis of asynchronous software systems as a means for building reliable software. A key challenge in designing such analyses is identifying a concurrency model which does not extraneously introduce behaviors infeasible in ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 46, Issue 1

POPL '11

January 2011

624 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1925844

Issue’s Table of Contents

POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2011
652 pages
ISBN:9781450304900
DOI:10.1145/1926385
General Chair:
Thomas Ball
Microsoft Research, USA
,
Program Chair:
Mooly Sagiv
Tel Aviv University, Israel

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 January 2011

Published in SIGPLAN Volume 46, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

136
Total Citations
View Citations
712
Total Downloads

Downloads (Last 12 months)28
Downloads (Last 6 weeks)1

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Chen DJiang YXu CMa X(2021)On interleaving space exploration of multi-threaded programsFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-020-9501-615:4Online publication date: 1-Aug-2021
https://dl.acm.org/doi/10.1007/s11704-020-9501-6
Johnson AWahl T(2021)Delay-Bounded Scheduling Without Delay!Computer Aided Verification10.1007/978-3-030-81685-8_18(380-402)Online publication date: 15-Jul-2021
https://doi.org/10.1007/978-3-030-81685-8_18
Abdulla PAtig MGodbole AKrishna SVafeiadis V(2021)The Decidability of Verification under PS 2.0Programming Languages and Systems10.1007/978-3-030-72019-3_1(1-29)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72019-3_1
Liu PWahl TLal A(2019)Verifying Asynchronous Event-Driven Programs Using Partial Abstract TransformersComputer Aided Verification10.1007/978-3-030-25543-5_22(386-404)Online publication date: 12-Jul-2019
https://doi.org/10.1007/978-3-030-25543-5_22
Bouajjani AEnea CMukund MRoy R(2019)On Verifying TSO Robustness for Event-Driven Asynchronous ProgramsNetworked Systems10.1007/978-3-030-05529-5_15(225-239)Online publication date: 5-Jan-2019
https://doi.org/10.1007/978-3-030-05529-5_15
Bouajjani AEmmi MEnea COzkan BTasiran S(2017)Verifying Robustness of Event-Driven Asynchronous Programs Against ConcurrencyProgramming Languages and Systems10.1007/978-3-662-54434-1_7(170-200)Online publication date: 25-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54434-1_7
Tomasco EInverso OFischer BTorre SParlato G(2015)Verifying Concurrent Programs by Memory UnwindingProceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 903510.1007/978-3-662-46681-0_52(551-565)Online publication date: 11-Apr-2015
https://dl.acm.org/doi/10.1007/978-3-662-46681-0_52
Souza SSouza PBrito MSimao AZaluska E(2015)Empirical evaluation of a new composite approach to the coverage criteria and reachability testing of concurrent programsSoftware Testing, Verification & Reliability10.1002/stvr.156825:3(310-332)Online publication date: 1-May-2015
https://dl.acm.org/doi/10.1002/stvr.1568
Thomson PDonaldson ABetts A(2014)Concurrency testing using schedule boundingACM SIGPLAN Notices10.1145/2692916.255526049:8(15-28)Online publication date: 6-Feb-2014
https://dl.acm.org/doi/10.1145/2692916.2555260
Inverso OTomasco EFischer BLa Torre SParlato G(2014)Bounded Model Checking of Multi-threaded C Programs via Lazy SequentializationProceedings of the 16th International Conference on Computer Aided Verification - Volume 855910.1007/978-3-319-08867-9_39(585-602)Online publication date: 18-Jul-2014
https://dl.acm.org/doi/10.1007/978-3-319-08867-9_39
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents