Earlier Version

Synchronizing the asynchronous

T.A. Henzinger, B. Kragl, S. Qadeer, Synchronizing the Asynchronous, IST Austria, 2017.

Download
OA 971.35 KB

Technical Report | Published | English
Department
Series Title
IST Austria Technical Report
Abstract
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
2017-08-04
Page
28
ISSN
IST-REx-ID

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.
Main File(s)
File Name
971.35 KB
Access Level
OA Open Access
Last Uploaded
2019-05-13T08:14:44Z


Material in IST:
Later Version

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar