DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2015.483

Rely/Guarantee Reasoning for Asynchronous Programs

Authors: Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, and Viktor Vafeiadis

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract

Asynchronous programming has become ubiquitous in smartphone and web application development, as well as in the development of server-side and system applications. Many of the uses of asynchrony can be modeled by extending programming languages with asynchronous procedure calls - procedures not executed immediately, but stored and selected for execution at a later point by a non-deterministic scheduler. Asynchronous calls induce a flow of control that is difficult to reason about, which in turn makes formal verification of asynchronous programs challenging. In response, we take a rely/guarantee approach: Each asynchronous procedure is verified separately with respect to its rely and guarantee predicates; the correctness of the whole program then follows from the natural conditions the rely/guarantee predicates have to satisfy. In this way, the verification of asynchronous programs is modularly decomposed into the more usual verification of sequential programs with synchronous calls. For the sequential program verification we use Hoare-style deductive reasoning, which we demonstrate on several simplified examples. These examples were inspired from programs written in C using the popular Libevent library; they are manually annotated and verified within the state-of-the-art Frama-C platform.

Cite as

Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, and Viktor Vafeiadis. Rely/Guarantee Reasoning for Asynchronous Programs. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 483-496, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{gavran_et_al:LIPIcs.CONCUR.2015.483,
  author =	{Gavran, Ivan and Niksic, Filip and Kanade, Aditya and Majumdar, Rupak and Vafeiadis, Viktor},
  title =	{{Rely/Guarantee Reasoning for Asynchronous Programs}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{483--496},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.483},
  URN =		{urn:nbn:de:0030-drops-53902},
  doi =		{10.4230/LIPIcs.CONCUR.2015.483},
  annote =	{Keywords: Asynchronous programs, rely/guarantee reasoning}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2012.522

Static Analysis for Checking Data Format Compatibility of Programs

Authors: Pranavadatta Devaki and Aditya Kanade

Published in: LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)

Abstract

Large software systems are developed by composing multiple programs. If the programs manipulate and exchange complex data, such as network packets or files, it is essential to establish that they follow compatible data formats. Most of the complexity of data formats is associated with the headers. In this paper, we address compatibility of programs operating over headers of network packets, files, images, etc. As format specifications are rarely available, we infer the format associated with headers by a program as a set of guarded layouts. In terms of these formats, we define and check compatibility of (a) producer-consumer programs and (b) different versions of producer (or consumer) programs. A compatible producer-consumer pair is free of type mismatches and logical incompatibilities such as the consumer rejecting valid outputs generated by the producer. A backward compatible producer (resp. consumer) is guaranteed to be compatible with consumers (resp. producers) that were compatible with its older version. With our prototype tool, we identified 5 known bugs and 1 potential bug in (a) sender-receiver modules of Linux network drivers of 3 vendors and (b) different versions of a TIFF image library.

Cite as

Pranavadatta Devaki and Aditya Kanade. Static Analysis for Checking Data Format Compatibility of Programs. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 522-533, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{devaki_et_al:LIPIcs.FSTTCS.2012.522,
  author =	{Devaki, Pranavadatta and Kanade, Aditya},
  title =	{{Static Analysis for Checking Data Format Compatibility of Programs}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{522--533},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.522},
  URN =		{urn:nbn:de:0030-drops-38862},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.522},
  annote =	{Keywords: Data format compatibility, producer-consumer/version-related programs}
}

Search Results

Documents authored by Kanade, Aditya

Rely/Guarantee Reasoning for Asynchronous Programs

Abstract

Cite as

Static Analysis for Checking Data Format Compatibility of Programs

Abstract

Cite as

Thanks for your feedback!

Could not send message