---
_id: '1338'
abstract:
- lang: eng
text: 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.
article_processing_charge: No
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- first_name: Edmund
full_name: Clarke, Edmund
last_name: Clarke
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
- first_name: Leonid
full_name: Ryzhyk, Leonid
last_name: Ryzhyk
- first_name: Roopsha
full_name: Samanta, Roopsha
id: 3D2AAC08-F248-11E8-B48F-1D18A9856A87
last_name: Samanta
- first_name: Thorsten
full_name: Tarrach, Thorsten
id: 3D6E8F2C-F248-11E8-B48F-1D18A9856A87
last_name: Tarrach
orcid: 0000-0003-4409-8487
citation:
ama: Cerny P, Clarke E, Henzinger TA, et al. From non-preemptive to preemptive scheduling
using synchronization synthesis. Formal Methods in System Design. 2017;50(2-3):97-139.
doi:10.1007/s10703-016-0256-5
apa: Cerny, P., Clarke, E., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., Samanta,
R., & Tarrach, T. (2017). From non-preemptive to preemptive scheduling using
synchronization synthesis. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-016-0256-5
chicago: Cerny, Pavol, Edmund Clarke, Thomas A Henzinger, Arjun Radhakrishna, Leonid
Ryzhyk, Roopsha Samanta, and Thorsten Tarrach. “From Non-Preemptive to Preemptive
Scheduling Using Synchronization Synthesis.” Formal Methods in System Design.
Springer, 2017. https://doi.org/10.1007/s10703-016-0256-5.
ieee: P. Cerny et al., “From non-preemptive to preemptive scheduling using
synchronization synthesis,” Formal Methods in System Design, vol. 50, no.
2–3. Springer, pp. 97–139, 2017.
ista: Cerny P, Clarke E, Henzinger TA, Radhakrishna A, Ryzhyk L, Samanta R, Tarrach
T. 2017. From non-preemptive to preemptive scheduling using synchronization synthesis.
Formal Methods in System Design. 50(2–3), 97–139.
mla: Cerny, Pavol, et al. “From Non-Preemptive to Preemptive Scheduling Using Synchronization
Synthesis.” Formal Methods in System Design, vol. 50, no. 2–3, Springer,
2017, pp. 97–139, doi:10.1007/s10703-016-0256-5.
short: P. Cerny, E. Clarke, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, R. Samanta,
T. Tarrach, Formal Methods in System Design 50 (2017) 97–139.
corr_author: '1'
date_created: 2018-12-11T11:51:27Z
date_published: 2017-06-01T00:00:00Z
date_updated: 2025-09-23T08:54:01Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/s10703-016-0256-5
ec_funded: 1
external_id:
isi:
- '000399888900001'
pmid:
- '28490835'
file:
- access_level: open_access
checksum: 1163dfd997e8212c789525d4178b1653
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:13:05Z
date_updated: 2020-07-14T12:44:44Z
file_id: '4985'
file_name: IST-2016-656-v1+1_s10703-016-0256-5.pdf
file_size: 1416170
relation: main_file
file_date_updated: 2020-07-14T12:44:44Z
has_accepted_license: '1'
intvolume: ' 50'
isi: 1
issue: 2-3
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: 97 - 139
pmid: 1
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
- _id: B67AFEDC-15C9-11EA-A837-991A96BB2854
name: IST Austria Open Access Fund
publication: Formal Methods in System Design
publication_status: published
publisher: Springer
publist_id: '5929'
pubrep_id: '656'
quality_controlled: '1'
related_material:
record:
- id: '1729'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: From non-preemptive to preemptive scheduling using synchronization synthesis
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 50
year: '2017'
...