Trustworthy Systems

From non-preemptive to preemptive scheduling using synchronization synthesis

Authors

Pavol Cerny, Edmund Clarke, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta and Thorsten Tarrach

University of Colorado Boulder

Carnegie Mellon University

IST Austria

University of Pennsylvania

NICTA

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.

BibTeX Entry

  @inproceedings{Cerny_CHRRST_15,
    address          = {San Francisco, USA},
    author           = {Cerny, Pavol and Clarke, Edmund and Henzinger, Thomas and Radhakrishna, Arjun and Ryzhyk, Leonid and
                        Samanta, Roopsha and Tarrach, Thorsten},
    booktitle        = { International Conference on Computer Aided Verification},
    keywords         = {synthesis for concurrency, computer-aided programming, device drivers},
    month            = jul,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8582.pdf},
    slides           = {https://trustworthy.systems/publications/nicta_slides/8582.pdf},
    title            = {From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis},
    year             = {2015}
  }

Download