[pl-seminar] [Fwd: RE: getting state rate at Doubletree Hotel]

[Thomas Reps <reps@xxxxxxxxxxx>]

Shaz Qadeer will be visiting on Friday, August 7 to serve on Nick Kidd's
dissertation committee.  He will give an informal whiteboard
presentation at 4 PM in 3310 CS on the following material.

======================================================
A Calculus of Atomic Actions

Shaz Qadeer
Microsoft Research

 We present a proof calculus and method for the static verification
  of assertions and procedure specifications in shared-memory
  concurrent programs. The key idea in our approach is to use
  atomicity as a proof tool and to simplify the verification of
  assertions by rewriting programs to consist of larger atomic
  actions. We propose a novel, iterative proof style in which
  alternating use of abstraction and reduction is exploited to compute
  larger atomic code blocks in a sound manner.  This makes possible
  the verification of assertions in the transformed program by simple
  sequential reasoning within atomic blocks, or significantly
  simplified application of existing concurrent program verification
  techniques such as the Owicki-Gries or rely-guarantee methods. Our
  method facilitates a clean separation of concerns where at each
  phase of the proof, the user worries only about only either the sequential
  properties or the concurrency control mechanisms in the
  program. We implemented our method in a tool called QED. We
  demonstrate the simplicity and effectiveness of our approach on a
  number of benchmarks including ones with intricate concurrency
  protocols.