---
_id: '1338'
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 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.
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. <i>Formal Methods in System Design</i>. 2017;50(2-3):97-139.
    doi:<a href="https://doi.org/10.1007/s10703-016-0256-5">10.1007/s10703-016-0256-5</a>
  apa: Cerny, P., Clarke, E., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., Samanta,
    R., &#38; Tarrach, T. (2017). From non-preemptive to preemptive scheduling using
    synchronization synthesis. <i>Formal Methods in System Design</i>. Springer. <a
    href="https://doi.org/10.1007/s10703-016-0256-5">https://doi.org/10.1007/s10703-016-0256-5</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.” <i>Formal Methods in System Design</i>.
    Springer, 2017. <a href="https://doi.org/10.1007/s10703-016-0256-5">https://doi.org/10.1007/s10703-016-0256-5</a>.
  ieee: P. Cerny <i>et al.</i>, “From non-preemptive to preemptive scheduling using
    synchronization synthesis,” <i>Formal Methods in System Design</i>, vol. 50, no.
    2–3. Springer, pp. 97–139, 2017.
  ista: Cerny P, Clarke E, Henzinger TA, Radhakrishna A, Ryzhyk L, Samanta R, Tarrach
    T. 2017. From non-preemptive to preemptive scheduling using synchronization synthesis.
    Formal Methods in System Design. 50(2–3), 97–139.
  mla: Cerny, Pavol, et al. “From Non-Preemptive to Preemptive Scheduling Using Synchronization
    Synthesis.” <i>Formal Methods in System Design</i>, vol. 50, no. 2–3, Springer,
    2017, pp. 97–139, doi:<a href="https://doi.org/10.1007/s10703-016-0256-5">10.1007/s10703-016-0256-5</a>.
  short: P. Cerny, E. Clarke, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, R. Samanta,
    T. Tarrach, Formal Methods in System Design 50 (2017) 97–139.
date_created: 2018-12-11T11:51:27Z
date_published: 2017-06-01T00:00:00Z
date_updated: 2023-09-20T11:13:51Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/s10703-016-0256-5
ec_funded: 1
external_id:
  isi:
  - '000399888900001'
file:
- access_level: open_access
  checksum: 1163dfd997e8212c789525d4178b1653
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:13:05Z
  date_updated: 2020-07-14T12:44:44Z
  file_id: '4985'
  file_name: IST-2016-656-v1+1_s10703-016-0256-5.pdf
  file_size: 1416170
  relation: main_file
file_date_updated: 2020-07-14T12:44:44Z
has_accepted_license: '1'
intvolume: '        50'
isi: 1
issue: 2-3
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: 97 - 139
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
- _id: B67AFEDC-15C9-11EA-A837-991A96BB2854
  name: IST Austria Open Access Fund
publication: Formal Methods in System Design
publication_status: published
publisher: Springer
publist_id: '5929'
pubrep_id: '656'
quality_controlled: '1'
related_material:
  record:
  - id: '1729'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: From non-preemptive to preemptive scheduling using synchronization synthesis
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 50
year: '2017'
...
---
_id: '1130'
abstract:
- lang: eng
  text: "In this thesis we present a computer-aided programming approach to concurrency.
    Our approach helps the programmer by automatically fixing concurrency-related
    bugs, i.e. bugs that occur when the program is executed using an aggressive preemptive
    scheduler, but not when using a non-preemptive (cooperative) scheduler. Bugs are
    program behaviours that are incorrect w.r.t. a specification. We consider both
    user-provided explicit specifications in the form of assertion\r\nstatements in
    the code as well as an implicit specification. The implicit specification is inferred
    from the non-preemptive behaviour. Let us consider sequences of calls that the
    program makes to an external interface. The implicit 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 consider several
    semantics-preserving fixes that go beyond atomic sections typically explored in
    the synchronisation synthesis literature. Our synthesis is able to place locks,
    barriers and wait-signal statements and last, but not least reorder independent
    statements. The latter may be useful if a thread is released to early, e.g., before
    some initialisation is completed. We guarantee that our synthesis does not introduce
    deadlocks and that the synchronisation inserted is optimal w.r.t. a given objective
    function. We dub our solution trace-based synchronisation synthesis and it is
    loosely based on counterexample-guided inductive synthesis (CEGIS). The synthesis
    works by discovering a trace that is incorrect w.r.t. the specification and identifying
    ordering constraints crucial to trigger the specification violation. Synchronisation
    may be placed immediately (greedy approach) or delayed until all incorrect traces
    are found (non-greedy approach). For the non-greedy approach we construct a set
    of global constraints over synchronisation placements. Each model of the global
    constraints set corresponds to a correctness-ensuring synchronisation placement.
    The placement that is optimal w.r.t. the given objective function is chosen as
    the synchronisation solution. We evaluate our approach on a number of realistic
    (albeit simplified) Linux device-driver\r\nbenchmarks. The benchmarks are versions
    of the drivers with known concurrency-related bugs. For the experiments with an
    explicit specification we added assertions that would detect the bugs in the experiments.
    Device drivers lend themselves to implicit specification, where the device and
    the operating system are the external interfaces. Our experiments demonstrate
    that our synthesis method is precise and efficient. We implemented objective functions
    for coarse-grained and fine-grained locking and observed that different synchronisation
    placements are produced for our experiments, favouring e.g. a minimal number of
    synchronisation operations or maximum concurrency."
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Thorsten
  full_name: Tarrach, Thorsten
  id: 3D6E8F2C-F248-11E8-B48F-1D18A9856A87
  last_name: Tarrach
  orcid: 0000-0003-4409-8487
citation:
  ama: Tarrach T. Automatic synthesis of synchronisation primitives for concurrent
    programs. 2016. doi:<a href="https://doi.org/10.15479/at:ista:1130">10.15479/at:ista:1130</a>
  apa: Tarrach, T. (2016). <i>Automatic synthesis of synchronisation primitives for
    concurrent programs</i>. Institute of Science and Technology Austria. <a href="https://doi.org/10.15479/at:ista:1130">https://doi.org/10.15479/at:ista:1130</a>
  chicago: Tarrach, Thorsten. “Automatic Synthesis of Synchronisation Primitives for
    Concurrent Programs.” Institute of Science and Technology Austria, 2016. <a href="https://doi.org/10.15479/at:ista:1130">https://doi.org/10.15479/at:ista:1130</a>.
  ieee: T. Tarrach, “Automatic synthesis of synchronisation primitives for concurrent
    programs,” Institute of Science and Technology Austria, 2016.
  ista: Tarrach T. 2016. Automatic synthesis of synchronisation primitives for concurrent
    programs. Institute of Science and Technology Austria.
  mla: Tarrach, Thorsten. <i>Automatic Synthesis of Synchronisation Primitives for
    Concurrent Programs</i>. Institute of Science and Technology Austria, 2016, doi:<a
    href="https://doi.org/10.15479/at:ista:1130">10.15479/at:ista:1130</a>.
  short: T. Tarrach, Automatic Synthesis of Synchronisation Primitives for Concurrent
    Programs, Institute of Science and Technology Austria, 2016.
date_created: 2018-12-11T11:50:19Z
date_published: 2016-07-07T00:00:00Z
date_updated: 2023-09-07T11:57:01Z
day: '07'
ddc:
- '000'
degree_awarded: PhD
department:
- _id: ToHe
- _id: GradSch
doi: 10.15479/at:ista:1130
ec_funded: 1
file:
- access_level: open_access
  checksum: 319a506831650327e85376db41fc1094
  content_type: application/pdf
  creator: dernst
  date_created: 2021-02-22T11:39:32Z
  date_updated: 2021-02-22T11:39:32Z
  file_id: '9179'
  file_name: 2016_Tarrach_Thesis.pdf
  file_size: 1523935
  relation: main_file
  success: 1
- access_level: closed
  checksum: 39efcd789f0ad859ff15652cb7afc412
  content_type: application/pdf
  creator: cchlebak
  date_created: 2021-11-16T14:14:38Z
  date_updated: 2021-11-17T13:46:55Z
  file_id: '10296'
  file_name: 2016_Tarrach_Thesispdfa.pdf
  file_size: 1306068
  relation: main_file
file_date_updated: 2021-11-17T13:46:55Z
has_accepted_license: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://thorstent.github.io/theses/phd_thorsten_tarrach.pdf
month: '07'
oa: 1
oa_version: Published Version
page: '151'
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication_identifier:
  issn:
  - 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '6230'
related_material:
  record:
  - id: '1729'
    relation: part_of_dissertation
    status: public
  - id: '2218'
    relation: part_of_dissertation
    status: public
  - id: '2445'
    relation: part_of_dissertation
    status: public
status: public
supervisor:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
title: Automatic synthesis of synchronisation primitives for concurrent programs
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2016'
...
---
_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
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: 2023-09-20T11:13:50Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-319-21668-3_11
ec_funded: 1
file:
- access_level: local
  checksum: 6ff58ac220e2f20cb001ba35d4924495
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:08:53Z
  date_updated: 2020-07-14T12:45:13Z
  file_id: '4715'
  file_name: IST-2015-336-v1+1_long_version.pdf
  file_size: 481922
  relation: main_file
file_date_updated: 2020-07-14T12:45:13Z
has_accepted_license: '1'
intvolume: '      9207'
language:
- iso: eng
month: '07'
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: The Wittgenstein Prize
- _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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9207
year: '2015'
...
---
_id: '1992'
abstract:
- lang: eng
  text: "We present a method and a tool for generating succinct representations of
    sets of concurrent traces. We focus on trace sets that contain all correct or
    all incorrect permutations of events from a given trace. We represent trace sets
    as HB-Formulas that are Boolean combinations of happens-before constraints between
    events. To generate a representation of incorrect interleavings, our method iteratively
    explores interleavings that violate the specification and gathers generalizations
    of the discovered interleavings into an HB-Formula; its complement yields a representation
    of correct interleavings.\r\n\r\nWe claim that our trace set representations can
    drive diverse verification, fault localization, repair, and synthesis techniques
    for concurrent programs. We demonstrate this by using our tool in three case studies
    involving synchronization synthesis, bug summarization, and abstraction refinement
    based verification. In each case study, our initial experimental results have
    been promising.\r\n\r\nIn the first case study, we present an algorithm for inferring
    missing synchronization from an HB-Formula representing correct interleavings
    of a given trace. The algorithm applies rules to rewrite specific patterns in
    the HB-Formula into locks, barriers, and wait-notify constructs. In the second
    case study, we use an HB-Formula representing incorrect interleavings for bug
    summarization. While the HB-Formula itself is a concise counterexample summary,
    we present additional inference rules to help identify specific concurrency bugs
    such as data races, define-use order violations, and two-stage access bugs. In
    the final case study, we present a novel predicate learning procedure that uses
    HB-Formulas representing abstract counterexamples to accelerate counterexample-guided
    abstraction refinement (CEGAR). In each iteration of the CEGAR loop, the procedure
    refines the abstraction to eliminate multiple spurious abstract counterexamples
    drawn from the HB-Formula."
author:
- first_name: Ashutosh
  full_name: Gupta, Ashutosh
  id: 335E5684-F248-11E8-B48F-1D18A9856A87
  last_name: Gupta
- 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: 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: 'Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. Succinct representation
    of concurrent trace sets. In: ACM; 2015:433-444. doi:<a href="https://doi.org/10.1145/2676726.2677008">10.1145/2676726.2677008</a>'
  apa: 'Gupta, A., Henzinger, T. A., Radhakrishna, A., Samanta, R., &#38; Tarrach,
    T. (2015). Succinct representation of concurrent trace sets (pp. 433–444). Presented
    at the POPL: Principles of Programming Languages, Mumbai, India: ACM. <a href="https://doi.org/10.1145/2676726.2677008">https://doi.org/10.1145/2676726.2677008</a>'
  chicago: Gupta, Ashutosh, Thomas A Henzinger, Arjun Radhakrishna, Roopsha Samanta,
    and Thorsten Tarrach. “Succinct Representation of Concurrent Trace Sets,” 433–44.
    ACM, 2015. <a href="https://doi.org/10.1145/2676726.2677008">https://doi.org/10.1145/2676726.2677008</a>.
  ieee: 'A. Gupta, T. A. Henzinger, A. Radhakrishna, R. Samanta, and T. Tarrach, “Succinct
    representation of concurrent trace sets,” presented at the POPL: Principles of
    Programming Languages, Mumbai, India, 2015, pp. 433–444.'
  ista: 'Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. 2015. Succinct
    representation of concurrent trace sets. POPL: Principles of Programming Languages,
    433–444.'
  mla: Gupta, Ashutosh, et al. <i>Succinct Representation of Concurrent Trace Sets</i>.
    ACM, 2015, pp. 433–44, doi:<a href="https://doi.org/10.1145/2676726.2677008">10.1145/2676726.2677008</a>.
  short: A. Gupta, T.A. Henzinger, A. Radhakrishna, R. Samanta, T. Tarrach, in:, ACM,
    2015, pp. 433–444.
conference:
  end_date: 2015-01-17
  location: Mumbai, India
  name: 'POPL: Principles of Programming Languages'
  start_date: 2015-01-15
date_created: 2018-12-11T11:55:05Z
date_published: 2015-01-15T00:00:00Z
date_updated: 2021-01-12T06:54:33Z
day: '15'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1145/2676726.2677008
file:
- access_level: open_access
  checksum: f0d4395b600f410a191256ac0b73af32
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:17:56Z
  date_updated: 2020-07-14T12:45:22Z
  file_id: '5314'
  file_name: IST-2015-317-v1+1_author_version.pdf
  file_size: 399462
  relation: main_file
file_date_updated: 2020-07-14T12:45:22Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 433 - 444
publication_identifier:
  isbn:
  - 978-1-4503-3300-9
publication_status: published
publisher: ACM
publist_id: '5091'
pubrep_id: '317'
quality_controlled: '1'
scopus_import: 1
status: public
title: Succinct representation of concurrent trace sets
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '2218'
abstract:
- lang: eng
  text: While fixing concurrency bugs, program repair algorithms may introduce new
    concurrency bugs. We present an algorithm that avoids such regressions. The solution
    space is given by a set of program transformations we consider in the repair process.
    These include reordering of instructions within a thread and inserting atomic
    sections. The new algorithm learns a constraint on the space of candidate solutions,
    from both positive examples (error-free traces) and counterexamples (error traces).
    From each counterexample, the algorithm learns a constraint necessary to remove
    the errors. From each positive examples, it learns a constraint that is necessary
    in order to prevent the repair from turning the trace into an error trace. We
    implemented the algorithm and evaluated it on simplified Linux device drivers
    with known bugs.
alternative_title:
- LNCS
author:
- first_name: Pavol
  full_name: Cerny, Pavol
  last_name: Cerny
- 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: Thorsten
  full_name: Tarrach, Thorsten
  id: 3D6E8F2C-F248-11E8-B48F-1D18A9856A87
  last_name: Tarrach
  orcid: 0000-0003-4409-8487
citation:
  ama: 'Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. Regression-free
    synthesis for concurrency. In: Vol 8559. Springer; 2014:568-584. doi:<a href="https://doi.org/10.1007/978-3-319-08867-9_38">10.1007/978-3-319-08867-9_38</a>'
  apa: 'Cerny, P., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., &#38; Tarrach,
    T. (2014). Regression-free synthesis for concurrency (Vol. 8559, pp. 568–584).
    Presented at the CAV: Computer Aided Verification, Vienna, Austria: Springer.
    <a href="https://doi.org/10.1007/978-3-319-08867-9_38">https://doi.org/10.1007/978-3-319-08867-9_38</a>'
  chicago: Cerny, Pavol, Thomas A Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, and
    Thorsten Tarrach. “Regression-Free Synthesis for Concurrency,” 8559:568–84. Springer,
    2014. <a href="https://doi.org/10.1007/978-3-319-08867-9_38">https://doi.org/10.1007/978-3-319-08867-9_38</a>.
  ieee: 'P. Cerny, T. A. Henzinger, A. Radhakrishna, L. Ryzhyk, and T. Tarrach, “Regression-free
    synthesis for concurrency,” presented at the CAV: Computer Aided Verification,
    Vienna, Austria, 2014, vol. 8559, pp. 568–584.'
  ista: 'Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. 2014. Regression-free
    synthesis for concurrency. CAV: Computer Aided Verification, LNCS, vol. 8559,
    568–584.'
  mla: Cerny, Pavol, et al. <i>Regression-Free Synthesis for Concurrency</i>. Vol.
    8559, Springer, 2014, pp. 568–84, doi:<a href="https://doi.org/10.1007/978-3-319-08867-9_38">10.1007/978-3-319-08867-9_38</a>.
  short: P. Cerny, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, T. Tarrach, in:, Springer,
    2014, pp. 568–584.
conference:
  end_date: 2014-07-22
  location: Vienna, Austria
  name: 'CAV: Computer Aided Verification'
  start_date: 2014-07-18
date_created: 2018-12-11T11:56:23Z
date_published: 2014-07-22T00:00:00Z
date_updated: 2023-09-07T11:57:01Z
day: '22'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-319-08867-9_38
ec_funded: 1
file:
- access_level: open_access
  checksum: a631d3105509f239724644e77a1212e2
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:13:14Z
  date_updated: 2020-07-14T12:45:33Z
  file_id: '4995'
  file_name: IST-2014-297-v1+1_cav14-final.pdf
  file_size: 416732
  relation: main_file
- access_level: open_access
  checksum: f8b0f748cc9fa697ca992cc56c87bc4e
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:13:15Z
  date_updated: 2020-07-14T12:45:33Z
  file_id: '4996'
  file_name: IST-2014-297-v2+1_cav14-final2.pdf
  file_size: 616293
  relation: main_file
file_date_updated: 2020-07-14T12:45:33Z
has_accepted_license: '1'
intvolume: '      8559'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://link.springer.com/chapter/10.1007%2F978-3-319-08867-9_38
month: '07'
oa: 1
oa_version: Submitted Version
page: 568 - 584
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Moderne Concurrency Paradigms
publication_identifier:
  isbn:
  - 978-331908866-2
publication_status: published
publisher: Springer
publist_id: '4749'
pubrep_id: '297'
quality_controlled: '1'
related_material:
  record:
  - id: '1130'
    relation: dissertation_contains
    status: public
status: public
title: Regression-free synthesis for concurrency
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8559
year: '2014'
...
---
_id: '2445'
abstract:
- lang: eng
  text: We develop program synthesis techniques that can help programmers fix concurrency-related
    bugs. We make two new contributions to synthesis for concurrency, the first improving
    the efficiency of the synthesized code, and the second improving the efficiency
    of the synthesis procedure itself. The first contribution is to have the synthesis
    procedure explore a variety of (sequential) semantics-preserving program transformations.
    Classically, only one such transformation has been considered, namely, the insertion
    of synchronization primitives (such as locks). Based on common manual bug-fixing
    techniques used by Linux device-driver developers, we explore additional, more
    efficient transformations, such as the reordering of independent instructions.
    The second contribution is to speed up the counterexample-guided removal of concurrency
    bugs within the synthesis procedure by considering partial-order traces (instead
    of linear traces) as counterexamples. A partial-order error trace represents a
    set of linear (interleaved) traces of a concurrent program all of which lead to
    the same error. By eliminating a partial-order error trace, we eliminate in a
    single iteration of the synthesis procedure all linearizations of the partial-order
    trace. We evaluated our techniques on several simplified examples of real concurrency
    bugs that occurred in Linux device drivers.
alternative_title:
- LNCS
author:
- first_name: Pavol
  full_name: Cerny, Pavol
  id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
  last_name: Cerny
- 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: Thorsten
  full_name: Tarrach, Thorsten
  id: 3D6E8F2C-F248-11E8-B48F-1D18A9856A87
  last_name: Tarrach
  orcid: 0000-0003-4409-8487
citation:
  ama: 'Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. Efficient synthesis
    for concurrency by semantics-preserving transformations. In: Vol 8044. Springer;
    2013:951-967. doi:<a href="https://doi.org/10.1007/978-3-642-39799-8_68">10.1007/978-3-642-39799-8_68</a>'
  apa: 'Cerny, P., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., &#38; Tarrach,
    T. (2013). Efficient synthesis for concurrency by semantics-preserving transformations
    (Vol. 8044, pp. 951–967). Presented at the CAV: Computer Aided Verification, St.
    Petersburg, Russia: Springer. <a href="https://doi.org/10.1007/978-3-642-39799-8_68">https://doi.org/10.1007/978-3-642-39799-8_68</a>'
  chicago: Cerny, Pavol, Thomas A Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, and
    Thorsten Tarrach. “Efficient Synthesis for Concurrency by Semantics-Preserving
    Transformations,” 8044:951–67. Springer, 2013. <a href="https://doi.org/10.1007/978-3-642-39799-8_68">https://doi.org/10.1007/978-3-642-39799-8_68</a>.
  ieee: 'P. Cerny, T. A. Henzinger, A. Radhakrishna, L. Ryzhyk, and T. Tarrach, “Efficient
    synthesis for concurrency by semantics-preserving transformations,” presented
    at the CAV: Computer Aided Verification, St. Petersburg, Russia, 2013, vol. 8044,
    pp. 951–967.'
  ista: 'Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. 2013. Efficient
    synthesis for concurrency by semantics-preserving transformations. CAV: Computer
    Aided Verification, LNCS, vol. 8044, 951–967.'
  mla: Cerny, Pavol, et al. <i>Efficient Synthesis for Concurrency by Semantics-Preserving
    Transformations</i>. Vol. 8044, Springer, 2013, pp. 951–67, doi:<a href="https://doi.org/10.1007/978-3-642-39799-8_68">10.1007/978-3-642-39799-8_68</a>.
  short: P. Cerny, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, T. Tarrach, in:, Springer,
    2013, pp. 951–967.
conference:
  end_date: 2013-07-19
  location: St. Petersburg, Russia
  name: 'CAV: Computer Aided Verification'
  start_date: 2013-07-13
date_created: 2018-12-11T11:57:42Z
date_published: 2013-07-01T00:00:00Z
date_updated: 2023-09-07T11:57:01Z
day: '01'
ddc:
- '000'
- '004'
department:
- _id: ToHe
doi: 10.1007/978-3-642-39799-8_68
ec_funded: 1
file:
- access_level: open_access
  checksum: 70c70ca5487faba82262c63e1b678a27
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:15:37Z
  date_updated: 2020-07-14T12:45:40Z
  file_id: '5158'
  file_name: IST-2014-199-v1+1_cav2013-final.pdf
  file_size: 365548
  relation: main_file
file_date_updated: 2020-07-14T12:45:40Z
has_accepted_license: '1'
intvolume: '      8044'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 951 - 967
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _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: '4458'
pubrep_id: '199'
quality_controlled: '1'
related_material:
  record:
  - id: '1130'
    relation: dissertation_contains
    status: public
scopus_import: 1
status: public
title: Efficient synthesis for concurrency by semantics-preserving transformations
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8044
year: '2013'
...