1 Search Results for "Qadeer, Shaz"

Document
DOI: 10.4230/LIPIcs.CONCUR.2018.21
Synchronizing the Asynchronous

Authors: Bernhard Kragl, Shaz Qadeer, and Thomas A. Henzinger

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

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

Bernhard Kragl, Shaz Qadeer, and Thomas A. Henzinger. Synchronizing the Asynchronous. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{kragl_et_al:LIPIcs.CONCUR.2018.21,
  author =	{Kragl, Bernhard and Qadeer, Shaz and Henzinger, Thomas A.},
  title =	{{Synchronizing the Asynchronous}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{21:1--21:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.21},
  URN =		{urn:nbn:de:0030-drops-95591},
  doi =		{10.4230/LIPIcs.CONCUR.2018.21},
  annote =	{Keywords: concurrent programs, asynchronous programs, deductive verification, refinement, synchronization, mover types, atomic action, commutativity, Lipton reduction}
}
  • Refine by Author
  • 1 Henzinger, Thomas A.
  • 1 Kragl, Bernhard
  • 1 Qadeer, Shaz

  • Refine by Classification
  • 1 Software and its engineering → Formal software verification

  • Refine by Keyword
  • 1 Lipton reduction
  • 1 asynchronous programs
  • 1 atomic action
  • 1 commutativity
  • 1 concurrent programs
  • Show More...

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2018

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact