---
OA_place: repository
OA_type: green
_id: '1729'
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 such sequences produced under a non-preemptive scheduler. The solution
    is based on a finitary abstraction, an algorithm for bounded language inclusion
    modulo an independence relation, and rules for inserting synchronization. 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, and, since it
    does not require explicit specifications, is more practical than the conventional
    approach based on user-provided assertions.
alternative_title:
- LNCS
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. 2015;9207:180-197. doi:<a href="https://doi.org/10.1007/978-3-319-21668-3_11">10.1007/978-3-319-21668-3_11</a>
  apa: 'Cerny, P., Clarke, E., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., Samanta,
    R., &#38; Tarrach, T. (2015). From non-preemptive to preemptive scheduling using
    synchronization synthesis. Presented at the CAV: Computer Aided Verification,
    San Francisco, CA, United States: Springer. <a href="https://doi.org/10.1007/978-3-319-21668-3_11">https://doi.org/10.1007/978-3-319-21668-3_11</a>'
  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.” Lecture Notes in Computer Science.
    Springer, 2015. <a href="https://doi.org/10.1007/978-3-319-21668-3_11">https://doi.org/10.1007/978-3-319-21668-3_11</a>.
  ieee: P. Cerny <i>et al.</i>, “From non-preemptive to preemptive scheduling using
    synchronization synthesis,” vol. 9207. Springer, pp. 180–197, 2015.
  ista: Cerny P, Clarke E, Henzinger TA, Radhakrishna A, Ryzhyk L, Samanta R, Tarrach
    T. 2015. From non-preemptive to preemptive scheduling using synchronization synthesis.
    9207, 180–197.
  mla: Cerny, Pavol, et al. <i>From Non-Preemptive to Preemptive Scheduling Using
    Synchronization Synthesis</i>. Vol. 9207, Springer, 2015, pp. 180–97, doi:<a href="https://doi.org/10.1007/978-3-319-21668-3_11">10.1007/978-3-319-21668-3_11</a>.
  short: P. Cerny, E. Clarke, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, R. Samanta,
    T. Tarrach, 9207 (2015) 180–197.
conference:
  end_date: 2015-07-24
  location: San Francisco, CA, United States
  name: 'CAV: Computer Aided Verification'
  start_date: 2015-07-18
date_created: 2018-12-11T11:53:42Z
date_published: 2015-07-01T00:00:00Z
date_updated: 2025-09-23T08:54:01Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-319-21668-3_11
ec_funded: 1
external_id:
  isi:
  - '000491470400011'
file:
- access_level: open_access
  checksum: 6ff58ac220e2f20cb001ba35d4924495
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:08:53Z
  date_updated: 2025-06-26T07:12:35Z
  file_id: '4715'
  file_name: IST-2015-336-v1+1_long_version.pdf
  file_size: 481922
  relation: main_file
file_date_updated: 2025-06-26T07:12:35Z
has_accepted_license: '1'
intvolume: '      9207'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 180 - 197
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: Formal methods for the design and analysis of complex systems
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
publication_status: published
publisher: Springer
publist_id: '5398'
pubrep_id: '336'
quality_controlled: '1'
related_material:
  record:
  - id: '1130'
    relation: dissertation_contains
    status: public
  - id: '1338'
    relation: later_version
    status: public
scopus_import: '1'
series_title: Lecture Notes in Computer Science
status: public
title: From non-preemptive to preemptive scheduling using synchronization synthesis
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9207
year: '2015'
...