Synchronizing the Asynchronous

Kragl, Bernhard and Qadeer, Shaz and Henzinger, Thomas A (2018) Synchronizing the Asynchronous. In: CONCUR: International Conference on Concurrency Theory , September 4-7, 2018, Beijing, China.

This is the latest version of this item.

[img] Text
concur2018.pdf - Published Version
Available under License Creative Commons Attribution.
[IST-2018-853-v2+2]
Download (727Kb)
Official URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2018.21

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 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.

Item Type: Conference or Workshop Item (Paper)
Subjects: 000 Computer science, knowledge & general works > 000 Computer science, knowledge & systems
Research Group: Henzinger Group
Depositing User: Bernhard Kragl
Date Deposited: 14 Aug 2018 13:03
Last Modified: 27 Sep 2018 15:21
URI: https://repository.ist.ac.at/id/eprint/1039

Available Versions of this Item

Actions (login required)

View Item View Item