Abstract:
In the 1970s Hoare, and then Owicki and Gries, described proof rules for conditional critical regions and monitors, which allowed for pleasantly simple specifications and proofs of shared-variable concurrent programs. Although simple, the proof rules suffered from several limitations; in particular, their reliance on statically-enforceable anti-aliasing restrictions renders them inapplicable in the presence of pointers.
In this talk we revisit the approach from the perspective of "separation logic", an extension of Hoare's logic to mutable data structures. Separation logic's semantics is based on a primitive notion of heap partitioning, which is used to interpret a connective, the separating conjunction, that supports reasoning about non-interference patterns that change over time. With the separating conjunction we can at once handle many simple examples where a linked data structure is used to represent a resource, as well as subtler examples where a pointer is transferred from one process to another or between a process and a resource. In the latter cases reasoning about dynamically evolving heap partitions allows "memory ownership transfer" to be tracked in the logic. We give examples of ownership transfer inspired by buffered inter-process communication and by memory management.
This talk builds on recent work of Reynolds, O'Hearn and Yang on reasoning about pointer data structures.
Host: John Reynolds
Dr. O'Hearn and his colleague, Cristiano Calcagno, will be at Carnegie Mellon on Thursday, March 28th and Friday, March 29th. If you wish to talk with them, contact Rae Graham (raeg@cs.cmu.edu) on extension 8-4740.
Principles of Programming Seminars