---
res:
  bibo_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.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Pavol
      foaf_name: Cerny, Pavol
      foaf_surname: Cerny
      foaf_workInfoHomepage: http://www.librecat.org/personId=4DCBEFFE-F248-11E8-B48F-1D18A9856A87
  - foaf_Person:
      foaf_givenName: Edmund
      foaf_name: Clarke, Edmund
      foaf_surname: Clarke
  - foaf_Person:
      foaf_givenName: Thomas A
      foaf_name: Henzinger, Thomas A
      foaf_surname: Henzinger
      foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
    orcid: 0000−0002−2985−7724
  - foaf_Person:
      foaf_givenName: Arjun
      foaf_name: Radhakrishna, Arjun
      foaf_surname: Radhakrishna
      foaf_workInfoHomepage: http://www.librecat.org/personId=3B51CAC4-F248-11E8-B48F-1D18A9856A87
  - foaf_Person:
      foaf_givenName: Leonid
      foaf_name: Ryzhyk, Leonid
      foaf_surname: Ryzhyk
  - foaf_Person:
      foaf_givenName: Roopsha
      foaf_name: Samanta, Roopsha
      foaf_surname: Samanta
      foaf_workInfoHomepage: http://www.librecat.org/personId=3D2AAC08-F248-11E8-B48F-1D18A9856A87
  - foaf_Person:
      foaf_givenName: Thorsten
      foaf_name: Tarrach, Thorsten
      foaf_surname: Tarrach
      foaf_workInfoHomepage: http://www.librecat.org/personId=3D6E8F2C-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0003-4409-8487
  bibo_doi: 10.1007/s10703-016-0256-5
  bibo_issue: 2-3
  bibo_volume: 50
  dct_date: 2017^xs_gYear
  dct_identifier:
  - UT:000399888900001
  dct_language: eng
  dct_publisher: Springer@
  dct_title: From non-preemptive to preemptive scheduling using synchronization synthesis@
  fabio_hasPubmedId: '28490835'
...