---
OA_place: publisher
OA_type: gold
_id: '133'
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 computation threads. We present synchronization,
    a new proof rule that simplifies the verification of asynchronous programs by
    introducing the fiction, for proof purposes, that asynchronous operations complete
    synchronously. Synchronization summarizes an asynchronous computation as immediate
    atomic effect. Modular verification is enabled via pending asynchronous calls
    in atomic summaries, and a complementary proof rule that eliminates pending asynchronous
    calls when components and their specifications are composed. We evaluate synchronization
    in the context of a multi-layer refinement verification methodology on a collection
    of benchmark programs.
alternative_title:
- LIPIcs
article_number: '21'
article_processing_charge: No
author:
- 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
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  ama: 'Kragl B, Qadeer S, Henzinger TA. Synchronizing the asynchronous. In: Vol 118.
    Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2018. doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2018.21">10.4230/LIPIcs.CONCUR.2018.21</a>'
  apa: 'Kragl, B., Qadeer, S., &#38; Henzinger, T. A. (2018). Synchronizing the asynchronous
    (Vol. 118). Presented at the CONCUR: International Conference on Concurrency Theory,
    Beijing, China: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2018.21">https://doi.org/10.4230/LIPIcs.CONCUR.2018.21</a>'
  chicago: Kragl, Bernhard, Shaz Qadeer, and Thomas A Henzinger. “Synchronizing the
    Asynchronous,” Vol. 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.
    <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2018.21">https://doi.org/10.4230/LIPIcs.CONCUR.2018.21</a>.
  ieee: 'B. Kragl, S. Qadeer, and T. A. Henzinger, “Synchronizing the asynchronous,”
    presented at the CONCUR: International Conference on Concurrency Theory, Beijing,
    China, 2018, vol. 118.'
  ista: 'Kragl B, Qadeer S, Henzinger TA. 2018. Synchronizing the asynchronous. CONCUR:
    International Conference on Concurrency Theory, LIPIcs, vol. 118, 21.'
  mla: Kragl, Bernhard, et al. <i>Synchronizing the Asynchronous</i>. Vol. 118, 21,
    Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2018.21">10.4230/LIPIcs.CONCUR.2018.21</a>.
  short: B. Kragl, S. Qadeer, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, 2018.
conference:
  end_date: 2018-09-07
  location: Beijing, China
  name: 'CONCUR: International Conference on Concurrency Theory'
  start_date: 2018-09-04
date_created: 2018-12-11T11:44:48Z
date_published: 2018-08-13T00:00:00Z
date_updated: 2026-04-08T07:23:52Z
day: '13'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2018.21
extern: '1'
file:
- access_level: open_access
  checksum: c90895f4c5fafc18ddc54d1c8848077e
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:18:46Z
  date_updated: 2020-07-14T12:44:44Z
  file_id: '5368'
  file_name: IST-2018-853-v2+2_concur2018.pdf
  file_size: 745438
  relation: main_file
file_date_updated: 2020-07-14T12:44:44Z
has_accepted_license: '1'
intvolume: '       118'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Rigorous Systems Engineering
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Moderne Concurrency Paradigms
publication_identifier:
  issn:
  - 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '7790'
pubrep_id: '1039'
quality_controlled: '1'
related_material:
  record:
  - id: '6426'
    relation: earlier_version
    status: public
  - id: '8332'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: Synchronizing the asynchronous
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: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 118
year: '2018'
...