article

From non-preemptive to preemptive scheduling using synchronization synthesis

Authors:

Edmund M. Clarke,

Thomas A. Henzinger,

Arjun Radhakrishna,

Roopsha Samanta,

Thorsten TarrachAuthors Info & Claims

Formal Methods in System Design, Volume 50, Issue 2-3

Pages 97 - 139

https://doi.org/10.1007/s10703-016-0256-5

Published: 01 June 2017 Publication History

Abstract

We present a computer-aided programming approach to concurrency. The approach allows programmers to program assuming a friendly, non-preemptive scheduler, and our synthesis procedure inserts synchronization to ensure that the final program works even with a preemptive scheduler. The correctness specification is implicit, inferred from the non-preemptive behavior. Let us consider sequences of calls that the program makes to an external interface. The specification requires that any such sequence produced under a preemptive scheduler should be included in the set of sequences produced under a non-preemptive scheduler. We guarantee that our synthesis does not introduce deadlocks and that the synchronization inserted is optimal w.r.t. a given objective function. The solution is based on a finitary abstraction, an algorithm for bounded language inclusion modulo an independence relation, and generation of a set of global constraints over synchronization placements. Each model of the global constraints set corresponds to a correctness-ensuring synchronization placement. The placement that is optimal w.r.t. the given objective function is chosen as the synchronization solution. We apply the approach to device-driver programming, where the driver threads call the software interface of the device and the API provided by the operating system. Our experiments demonstrate that our synthesis method is precise and efficient. The implicit specification helped us find one concurrency bug previously missed when model-checking using an explicit, user-provided specification. We implemented objective functions for coarse-grained and fine-grained locking and observed that different synchronization placements are produced for our experiments, favoring a minimal number of synchronization operations or maximum concurrency, respectively.

References

[1]

Alglave J, Kroening D, Nimal V, Poetzl D (2014) Don't sit on the fence--a static analysis approach to automatic fence insertion. In: CAV, pp 508---524

Digital Library

[2]

Bertoni A, Mauri G, Sabadini N (1982) Equivalence and membership problems for regular trace languages. In: Automata, languages and programming. Springer, Heidelberg, pp 61---71

Digital Library

[3]

Bloem R, Hofferek G, Könighofer B, Könighofer R, Außerlechner S, Spörk R (2014) Synthesis of synchronization using uninterpreted functions. In: FMCAD, pp 35---42

Digital Library

[4]

Černý P, Clarke EM, Henzinger TA, Radhakrishna A, Ryzhyk L, Samanta R, Tarrach T (2013) From non-preemptive to preemptive scheduling using synchronization synthesis. In: CAV, pp 180---197. https://github.com/thorstent/Liss

[5]

Černý P, Henzinger T, Radhakrishna A, Ryzhyk L, Tarrach T (2013) Efficient synthesis for concurrency by semantics-preserving transformations. In: CAV, pp 951---967

[6]

Černý P, Henzinger T, Radhakrishna A, Ryzhyk L, Tarrach T (2014) Regression-free synthesis for concurrency. In: CAV, pp 568---584. https://github.com/thorstent/ConRepair

Digital Library

[7]

Černý P, Clarke EM, Henzinger TA, Radhakrishna A, Ryzhyk L, Samanta R, Tarrach T (2015) Optimizing solution quality in synchronization synthesis. ArXiv e-prints. ArXiv:1511.07163

[8]

Cherem S, Chilimbi T, Gulwani S (2008) Inferring locks for atomic sections. In: PLDI, pp 304---315

Digital Library

[9]

Clarke EM, Emerson EA (1982) Design and synthesis of synchronization skeletons using branching time temporal logic. Springer, Berlin

[10]

Clarke E, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: TACAS, pp 168---176. http://www.cprover.org/cbmc/

[11]

De Wulf M, Doyen L, Henzinger TA, Raskin JF (2006) Antichains: a new algorithm for checking universality of finite automata. In: CAV. Springer, Heidelberg, pp 17---30

Digital Library

[12]

Deshmukh J, Ramalingam G, Ranganath V, Vaswani K (2010) Logical concurrency control from sequential proofs. In: Programming languages and systems. Springer, Heidelberg, pp 226---245

Digital Library

[13]

Eswaran KP, Gray JN, Lorie RA, Traiger IL (1976) The notions of consistency and predicate locks in a database system. Commun ACM 19(11):624---633

Digital Library

[14]

Flanagan C, Qadeer S (2003) Types for atomicity. In: ACM SIGPLAN notices, vol 38. ACM, New York, pp 1---12

Digital Library

[15]

Gupta A, Henzinger T, Radhakrishna A, Samanta R, Tarrach T (2015) Succinct representation of concurrent trace sets. In: POPL15, pp 433---444

Digital Library

[16]

Herlihy MP, Wing JM (1990) Linearizability: a correctness condition for concurrent objects. ACM Trans Progr Lang Syst (TOPLAS) 12(3):463---492

Digital Library

[17]

Jin G, Zhang W, Deng D, Liblit B, Lu S (2012) Automated concurrency-bug fixing. In: OSDI, pp 221---236

Digital Library

[18]

Khoshnood S, Kusano M, Wang C (2015) ConcBugAssist: constraint solving for diagnosis and repair of concurrency bugs. In: International symposium on software testing and analysis

Digital Library

[19]

Memcached distributed memory object caching system. http://memcached.org. Accessed 01 Jul 2015

[20]

Papadimitriou C (1986) The theory of database concurrency control. Computer Science Press, Rockville

Digital Library

[21]

Ryzhyk L, Chubb P, Kuz I, Heiser G (2009) Dingo: Taming device drivers. In: Eurosys

Digital Library

[22]

Sadowski C, Yi J (2010) User evaluation of correctness conditions: a case study of cooperability. In: PLATEAU, pp 2:1---2:6

Digital Library

[23]

Solar-Lezama A, Jones C, Bodík R (2008) Sketching concurrent data structures. In: PLDI, pp 136---148

Digital Library

[24]

Vechev M, Yahav E, Yorsh G (2010) Abstraction-guided synthesis of synchronization. In: POPL, pp 327---338

Digital Library

[25]

Vechev MT, Yahav E, Raman R, Sarkar V (2010) Automatic verification of determinism for structured parallel programs. In: SAS, pp 455---471

Digital Library

[26]

Yi J, Flanagan C (2010) Effects for cooperable and serializable threads. In: Proceedings of the 5th ACM SIGPLAN workshop on types in language design and implementation. ACM, New York, pp 3---14

Digital Library

Cited By

Houshmand FLesani MVora K(2021)Grafs: declarative graph analyticsProceedings of the ACM on Programming Languages10.1145/34735885:ICFP(1-32)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473588
Fellner ATarrach TWeissenbacher G(2020)Language Inclusion for Finite Prime Event StructuresVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-39322-9_15(314-336)Online publication date: 16-Jan-2020
https://dl.acm.org/doi/10.1007/978-3-030-39322-9_15
Bouajjani AEnea CLahiri S(2019)Abstract semantic diffing of evolving concurrent programsFormal Methods in System Design10.1007/s10703-018-0322-254:1(4-26)Online publication date: 1-Aug-2019
https://dl.acm.org/doi/10.1007/s10703-018-0322-2

From non-preemptive to preemptive scheduling using synchronization synthesis

Recommendations

Preemptive and non-preemptive scheduling on two unrelated parallel machines
Abstract
In this paper, for the problem of minimizing the makespan on two unrelated parallel machines we compare the quality of preemptive and non-preemptive schedules. It is known that there exists an optimal preemptive schedule with at most two ...
From preemptive to non-preemptive speed-scaling scheduling

We are given a set of jobs, each one specified by its release date, its deadline and its processing volume (work), and a single (or a set of) speed-scalable processor(s). We adopt the standard model in speed-scaling in which if a processor runs at speed ...
Preemptive Hadoop Jobs Scheduling under a Deadline
SKG '12: Proceedings of the 2012 Eighth International Conference on Semantics, Knowledge and Grids

MapReduce has become the dominant programming model in a cloud-based data processing environment, such as Hadoop. First In First Out (FIFO) is the default job scheduling policy of Hadoop, but it cannot guarantee that the job will be completed by a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Methods in System Design

Formal Methods in System Design Volume 50, Issue 2-3

June 2017

256 pages

ISSN:0925-9856

Issue’s Table of Contents

Copyright © Copyright © 2017 Springer Science+Business Media New York.

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 June 2017

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Houshmand FLesani MVora K(2021)Grafs: declarative graph analyticsProceedings of the ACM on Programming Languages10.1145/34735885:ICFP(1-32)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473588
Fellner ATarrach TWeissenbacher G(2020)Language Inclusion for Finite Prime Event StructuresVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-39322-9_15(314-336)Online publication date: 16-Jan-2020
https://dl.acm.org/doi/10.1007/978-3-030-39322-9_15
Bouajjani AEnea CLahiri S(2019)Abstract semantic diffing of evolving concurrent programsFormal Methods in System Design10.1007/s10703-018-0322-254:1(4-26)Online publication date: 1-Aug-2019
https://dl.acm.org/doi/10.1007/s10703-018-0322-2

View Options

View options

Get Access

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

Media

Figures

Other

Tables

View Issue’s Table of Contents