Search Results

Documents authored by Tasiran, Serdar


Document
Verifying Optimistic Concurrency: Prophecy Variables and Backward Reasoning

Authors: Serdar Tasiran, Ali Sezgin, and Shaz Quadeer

Published in: Dagstuhl Seminar Proceedings, Volume 9361, Design and Validation of Concurrent Systems (2010)


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.

Cite as

Serdar Tasiran, Ali Sezgin, and Shaz Quadeer. Verifying Optimistic Concurrency: Prophecy Variables and Backward Reasoning. In Design and Validation of Concurrent Systems. Dagstuhl Seminar Proceedings, Volume 9361, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{tasiran_et_al:DagSemProc.09361.2,
  author =	{Tasiran, Serdar and Sezgin, Ali and Quadeer, Shaz},
  title =	{{Verifying Optimistic Concurrency: Prophecy Variables and Backward Reasoning}},
  booktitle =	{Design and Validation of Concurrent Systems},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9361},
  editor =	{Cormac Flanagan and Madhusan Parthasarathy and Shaz Quadeer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09361.2},
  URN =		{urn:nbn:de:0030-drops-24306},
  doi =		{10.4230/DagSemProc.09361.2},
  annote =	{Keywords: Concurrency, Program Verification, Static Analysis}
}
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