Generalizing Reduction and Abstraction to Simplify Concurrent Programs: The QED Approach
Intervenant(s) : Serdar Tasiran (Koç University & Microsoft Research Center for Multi-Core Software Engineering)A key difficulty in concurrent program verification is the large number of interleavings of fine-grain actions. The typical correctness argument makes use of a separation of concerns. At each phase, one worries only about interference due to concurrency, or the sequential behavior of a code block. We present a proof system, QED, that builds on this intuition. In QED, we formulate semantic conditions under which actions commute, and a somewhat different notion of program abstraction. Commutativity checks between actions and abstraction checks are converted to verification conditions and are checked by the Z3 theorem prover. A key computational advantage is that QED proof steps have locally-checkable antecedents. QED proofs apply reduction and abstraction iteratively and transform a program to consist of larger-grain actions. We show that this approach greatly simplifies proofs of assertions, atomicity and linearizability, even in optimistically concurrent programs.
Serdar Tasiran received his BS in Electrical Engineering from Bilkent University in 1991, and his MS and PhD from UC Berkeley in Electrical Engineering and Computer Sciences in 1995 and 1998, respectively. He was a researcher at the Gigascale Systems Research Center , a multi-university, multi-company consortium until 2000. From 2000 to 2003, he was a research scientist at the Systems Research Center (part of DEC, Compaq and later HP Labs) in Palo Alto, CA. Since 2003, he has been at Koc University, Istanbul, Turkey. While at Koc University, he has had visiting appointments at MIT, EPFL, Microsoft Research, USA and India. His research interests are the specification, verification, performance estimation and optimization of concurrent systems.
Marc.Shapiro (at) null