##
Peter O'Hearn

Queen Mary, University of London

###
Separation Logic for Shared-Variable Concurrency

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

POP Seminar

March 29, 2002

3:30 p.m.

Wean Hall 8220