Viktor Vafeiadis |
|
Viktor Vafeiadis |
|
My main research focus is the verification of intricate concurrent programs which execute in a shared memory paradigm. In doing the proofs, I prefer axiomatic techniques, in particular rely/guarantee and separation logic. Generally, I am also interested in programming languages, type systems, operational semantics, and compilers.
Matthew Parkinson and I are working on the combination of rely/guarantee reasoning and separation logic into a single system.
With the combination, we can encode all our earlier rely/guarantee and separation logic proofs. We can describe interference naturally (using a relation as in rely/guarantee), and where there is no interference, we can reason locally (as in separation logic). We need much less auxiliary state than is required by separation logic, and we can still reason cleanly about resource management (e.g. absence of memory leaks).
I have proved the linearisability and safety of the following algorithms, listed in rough order of the complexity of the proofs.
The proofs are hand-crafted and not machine-checked. I have not attempted proofs of liveness. I also have not proved absence of memory leaks (only applicable to the lock-coupling list algorithm).
This work started at a summer internship at Microsoft Research Cambridge under the supervision of Maurice Herlihy and Tony Hoare. There I proved the safety of the list algorithms mentioned above. The following paper summarises the proofs of these algorithms:
The accompanying hand-crafted formal proofs are available as
University of Cambridge Computer Laboratory technical report
UCAM-CL-TR-659.
The informal proof of the linearisability of contains, not included in the technical
report, is available as a pdf file.
After my internship, I proved the correctness of a few more algorithms, and used R-G to exploit some common design patterns found in these algorithms. The following draft paper describes how to prove the linearisabilty of lock-free algorithms that follow a common design pattern. It includes a proof of the elimination-based stack and a proof outline of RDCSS.