May 17, 2011
Alexander Malkis
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.