eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-05-11
9361
1
17
10.4230/DagSemProc.09361.1
article
09361 Abstracts Collection – Design and Validation of Concurrent Systems
Flanagan, Cormac
Graf, Susanne
Parthasarathy, Madhusan
Quadeer, Shaz
The Dagstuhl Seminar 09361
``Design and Validation of Concurrent Systems'' was held
in Schloss Dagstuhl~--~Leibniz Center for Informatics
from August 30 to September 4, 2009.
During the seminar, participants presented their current
research, and ongoing work and open problems were discussed.
This paper reviews the seminar topics and goals, and provides abstracts of
the presentations given during the seminar.
Links to extended abstracts or full papers are provided, if available.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol09361/DagSemProc.09361.1/DagSemProc.09361.1.pdf
Concurrency
Specification
Programming
Verification
Validation
Testing
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-05-11
9361
1
0
10.4230/DagSemProc.09361.2
article
Verifying Optimistic Concurrency: Prophecy Variables and Backward Reasoning
Tasiran, Serdar
Sezgin, Ali
Quadeer, Shaz
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.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol09361/DagSemProc.09361.2/DagSemProc.09361.2.pdf
Concurrency
Program Verification
Static Analysis