Synchronizing the Asynchronous Conference Paper


Author(s): Kragl, Bernhard; Qadeer, Shaz; Henzinger, Thomas A
Title: Synchronizing the Asynchronous
Title Series: LIPIcs
Affiliation IST Austria
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.
Keywords: refinement; Synchronization; Concurrent Programs; asynchronous programs; deductive verification; mover types; atomic action; commutativity; Lipton reduction
Conference Title: CONCUR: International Conference on Concurrency Theory
Volume: 118
Conference Dates: September 4-7, 2018
Conference Location: Beijing, China
ISBN: 978-3-95977-087-3
Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik  
Location: Dagstuhl, Germany
Date Published: 2018-08-13
Start Page: 21:1
End Page: 21:17
Copyright Statement: Creative Commons Attribution 3.0 Unported (CC BY 3.0)
Sponsor: This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).
URL:
DOI: 10.4230/LIPIcs.CONCUR.2018.21
Open access: yes (repository)
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
  2. Bernhard Kragl
    5 Kragl
Related IST Austria Work