A Lower Bound on Resource Verification

May 17, 2011

Alexander Malkis


A Lower Bound on Resource Verification

Time:   11:00am
Location:   Meeting room 302 (Mountain View), level 3

In multi-threaded programs data is often separated into lock-protected resources. Properties of those resources are typically verified by modular, Owicki-Gries-like methods. The Owicki-Gries proof structure follows the program syntax in an intuitive, cheap and easily implementable and extendable manner (Concurrent Separation Logic, Chalice, VCC, RGSep, …). Alas, some properties do not admit this proof structure. So far nothing was known about the boundary between properties that do have this proof structure and properties that don’t have it. We will characterize a class of properties that do admit an Owicki-Gries proof structure, showing what properties are always cheaply provable and a worst-case approximation inherent to the Owicki-Gries method.