From non-preemptive to preemptive scheduling using synchronization synthesis Conference Paper

Author(s): Cerný, Pavol; Clarke, Edmund M; Henzinger, Thomas A; Radhakrishna, Arjun; Ryzhyk, Leonid; Samanta, Roopsha; Tarrach, Thorsten
Title: From non-preemptive to preemptive scheduling using synchronization synthesis
Title Series: LNCS
Affiliation IST Austria
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 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.
Conference Title: CAV: Computer Aided Verification
Volume: 9207
Conference Dates: July 21 - 24, 2015
Conference Location: San Francisco, CA, USA
Publisher: Springer  
Date Published: 2015-07-01
Start Page: 180
End Page: 197
DOI: 10.1007/978-3-319-21668-3_11
Notes: This research was supported in part by the European Research Council (ERC) under grant 267989 (QUAREM), by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), by NSF under award CCF 1421752 and the Expeditions award CCF 1138996, by the Simons Foundation, and by a gift from the Intel Corporation.
Open access: yes (repository)
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work