License
when quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-24306
URL: http://drops.dagstuhl.de/opus/volltexte/2010/2430/

Tasiran, Serdar ; Sezgin, Ali ; Quadeer, Shaz

Verifying Optimistic Concurrency: Prophecy Variables and Backward Reasoning

pdf-format:
Dokument 1.pdf (371 KB)


Abstract

Several static proof systems have been developed over the years for verifying shared-memory multithreaded programs. These proof systems make use of auxiliary variables to express mutual exclusion or non-interference among shared variable accesses. Typically, the values of these variables summarize the past of the program execution; consequently, they are known as history variables. Prophecy variables, on the other hand, are the temporal dual of history variables and their values summarize the future of the program execution. In this paper, we show that prophecy variables are useful for locally constructing proofs of systems with optimistic concurrency. To enable the fullest use of prophecy variables in proof construction, we introduce tressa annotations, as the dual of the well-known assert annotations. A tressa claim states a condition for reverse reachability from an end state of the program, much like an assert claim states a condition for forward reachability from the initial state of the program. We present the proof rules and the notion of correctness of a program for two-way reasoning in a static setting: forward in time for assert claims, backward in time for tressa claims. Even though the interaction between the two is non-trivial, the formalization is intuitive and accessible. We demonstrate how to verify implementations based on optimistic concurrency which is a programming paradigm that allows conflicts to be handled after they occur. We have incorporated our proof rules into the QED verifier and have used our implementation to verify a handful of small but sophisticated algorithms. Our experience shows that the proof steps and annotations follow closely the intuition of the programmer, making the proof itself a natural extension of implementation.

BibTeX - Entry

@InProceedings{tasiran_et_al:DSP:2010:2430,
  author =	{Serdar Tasiran and Ali Sezgin and Shaz Quadeer},
  title =	{Verifying Optimistic Concurrency: Prophecy Variables and Backward Reasoning},
  booktitle =	{Design and Validation of Concurrent Systems},
  year =	{2010},
  editor =	{Cormac Flanagan and Madhusan Parthasarathy and Shaz Quadeer},
  number =	{09361},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2430},
  annote =	{Keywords: Concurrency, Program Verification, Static Analysis}
}

Keywords: Concurrency, Program Verification, Static Analysis
Seminar: 09361 - Design and Validation of Concurrent Systems
Issue date: 2010
Date of publication: 11.05.2010


DROPS-Home | Fulltext Search | Imprint Published by LZI