Earlier Version

Synchronizing the asynchronous

Henzinger TA, Kragl B, Qadeer S. 2017. Synchronizing the asynchronous, IST Austria, 28p.

OA main(1).pdf 971.35 KB

Technical Report | Published | English
Series Title
IST Austria Technical Report
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.
Publishing Year
Date Published

Cite this

Henzinger TA, Kragl B, Qadeer S. Synchronizing the Asynchronous. IST Austria; 2017. doi:10.15479/AT:IST-2018-853-v2-2
Henzinger, T. A., Kragl, B., & Qadeer, S. (2017). Synchronizing the asynchronous. IST Austria. https://doi.org/10.15479/AT:IST-2018-853-v2-2
Henzinger, Thomas A, Bernhard Kragl, and Shaz Qadeer. Synchronizing the Asynchronous. IST Austria, 2017. https://doi.org/10.15479/AT:IST-2018-853-v2-2.
T. A. Henzinger, B. Kragl, and S. Qadeer, Synchronizing the asynchronous. IST Austria, 2017.
Henzinger TA, Kragl B, Qadeer S. 2017. Synchronizing the asynchronous, IST Austria, 28p.
Henzinger, Thomas A., et al. Synchronizing the Asynchronous. IST Austria, 2017, doi:10.15479/AT:IST-2018-853-v2-2.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]
Main File(s)
File Name
main(1).pdf 971.35 KB
Access Level
OA Open Access
Date Uploaded
MD5 Checksum

Material in ISTA:
Later Version


Marked Publications

Open Data ISTA Research Explorer

Search this title in

Google Scholar