---
res:
  bibo_abstract:
  - "We present an algorithmic method for the synthesis of concurrent programs that
    are optimal with respect to quantitative performance measures. The input consists
    of a sequential sketch, that is, a program that does not contain synchronization
    constructs, and of a parametric performance model that assigns costs to actions
    such as locking, context switching, and idling. The quantitative synthesis problem
    is to automatically introduce synchronization constructs into the sequential sketch
    so that both correctness is guaranteed and worst-case (or average-case) performance
    is optimized. Correctness is formalized as race freedom or linearizability.\r\n\r\nWe
    show that for worst-case performance, the problem can be modeled\r\nas a 2-player
    graph game with quantitative (limit-average) objectives, and\r\nfor average-case
    performance, as a 2 1/2 -player graph game (with probabilistic transitions). In
    both cases, the optimal correct program is derived from an optimal strategy in
    the corresponding quantitative game. We prove that the respective game problems
    are computationally expensive (NP-complete), and present several techniques that
    overcome the theoretical difficulty in cases of concurrent programs of practical
    interest.\r\n\r\nWe have implemented a prototype tool and used it for the automatic
    syn- thesis of programs that access a concurrent list. For certain parameter val-
    ues, our method automatically synthesizes various classical synchronization schemes
    for implementing a concurrent list, such as fine-grained locking or a lazy algorithm.
    For other parameter values, a new, hybrid synchronization style is synthesized,
    which uses both the lazy approach and coarse-grained locks (instead of standard
    fine-grained locks). The trade-off occurs because while fine-grained locking tends
    to decrease the cost that is due to waiting for locks, it increases cache size
    requirements.@eng"
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Krishnendu
      foaf_name: Chatterjee, Krishnendu
      foaf_surname: Chatterjee
      foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-4561-241X
  - 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: 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: Rohit
      foaf_name: Singh, Rohit
      foaf_surname: Singh
  bibo_doi: 10.15479/AT:IST-2010-0004
  dct_date: 2010^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/2664-1690
  dct_language: eng
  dct_publisher: IST Austria@
  dct_title: Quantitative synthesis for concurrent programs@
...