---
_id: '6426'
abstract:
- lang: eng
  text: Synchronous programs are easy to specify because the side effects of an operation
    are finished by the time the invocation of the operation returns to the caller.
    Asynchronous programs, on the other hand, are difficult to specify because there
    are side effects due to pending computation scheduled as a result of the invocation
    of an operation. They are also difficult to verify because of the large number
    of possible interleavings of concurrent asynchronous computation threads. We show
    that specifications and correctness proofs for asynchronous programs can be structured
    by introducing the fiction, for proof purposes, that intermediate, non-quiescent
    states of asynchronous operations can be ignored. Then, the task of specification
    becomes relatively simple and the task of verification can be naturally decomposed
    into smaller sub-tasks. The sub-tasks iteratively summarize, guided by the structure
    of an asynchronous program, the atomic effect of non-atomic operations and the
    synchronous effect of asynchronous operations. This structuring of specifications
    and proofs corresponds to the introduction of multiple layers of stepwise refinement
    for asynchronous programs. We present the first proof rule, called synchronization,
    to reduce asynchronous invocations on a lower layer to synchronous invocations
    on a higher layer. We implemented our proof method in CIVL and evaluated it on
    a collection of benchmark programs.
alternative_title:
- IST Austria Technical Report
author:
- 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: Bernhard
  full_name: Kragl, Bernhard
  id: 320FC952-F248-11E8-B48F-1D18A9856A87
  last_name: Kragl
  orcid: 0000-0001-7745-9117
- first_name: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
citation:
  ama: Henzinger TA, Kragl B, Qadeer S. <i>Synchronizing the Asynchronous</i>. IST
    Austria; 2017. doi:<a href="https://doi.org/10.15479/AT:IST-2018-853-v2-2">10.15479/AT:IST-2018-853-v2-2</a>
  apa: Henzinger, T. A., Kragl, B., &#38; Qadeer, S. (2017). <i>Synchronizing the
    asynchronous</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2018-853-v2-2">https://doi.org/10.15479/AT:IST-2018-853-v2-2</a>
  chicago: Henzinger, Thomas A, Bernhard Kragl, and Shaz Qadeer. <i>Synchronizing
    the Asynchronous</i>. IST Austria, 2017. <a href="https://doi.org/10.15479/AT:IST-2018-853-v2-2">https://doi.org/10.15479/AT:IST-2018-853-v2-2</a>.
  ieee: T. A. Henzinger, B. Kragl, and S. Qadeer, <i>Synchronizing the asynchronous</i>.
    IST Austria, 2017.
  ista: Henzinger TA, Kragl B, Qadeer S. 2017. Synchronizing the asynchronous, IST
    Austria, 28p.
  mla: Henzinger, Thomas A., et al. <i>Synchronizing the Asynchronous</i>. IST Austria,
    2017, doi:<a href="https://doi.org/10.15479/AT:IST-2018-853-v2-2">10.15479/AT:IST-2018-853-v2-2</a>.
  short: T.A. Henzinger, B. Kragl, S. Qadeer, Synchronizing the Asynchronous, IST
    Austria, 2017.
date_created: 2019-05-13T08:15:55Z
date_published: 2017-08-04T00:00:00Z
date_updated: 2025-04-15T08:11:53Z
day: '04'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2018-853-v2-2
file:
- access_level: open_access
  checksum: b48d42725182d7ca10107a118815f4cf
  content_type: application/pdf
  creator: dernst
  date_created: 2019-05-13T08:14:44Z
  date_updated: 2020-07-14T12:47:30Z
  file_id: '6431'
  file_name: main(1).pdf
  file_size: 971347
  relation: main_file
file_date_updated: 2020-07-14T12:47:30Z
has_accepted_license: '1'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: '28'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
related_material:
  record:
  - id: '133'
    relation: later_version
    status: public
status: public
title: Synchronizing the asynchronous
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2017'
...