John Reynolds

Carnegie-Mellon University

John C. Reynolds gave a brief presentation on Separation logic, an extension of Hoare logic for reasoning about shared mutable data structres that was discovered independently by him and Peter O'Hearn. A simple example of the advantage of the logic is the invariant of a program for in-place reversal of a list. In Hoare logic, one would have to write Exists x,y. list x i and list y j and compose(reflect(y),x) = x0 and forall k. reachable i k and reachable j k implies k = nil where list x i asserts that i is a list representing the sequence x, and the final conjunct asserts that only nil is reachable from both i and j, i.e. that the lists i and j do not share storage. In separation logic, however, one can write Exists x,y. (list x i * list y j) and compose(reflect(y),x) = x0 where * is a "separating conjunction" that asserts that its components hold for disjoint areas of storage. A central feature of the logic is the "frame rule": {p}c{q} ----------- when c assigns to no variable free in r. {p*r}c{q*r} Using this rule, one can limit the proof of a program fragment c to a specification {p]c{q} that only describes the storage actually used by c, and then infer that c will leave unchanged any property r of a disjoint storage area. The setting of separation logic is a low-level imperative programming language without garbage collection. All proofs preclude any dereferencing of dangling pointers. It is also possible to prove the absence of memory leaks, say by proving {p and empty}c{q and empty} where empty asserts that the heap storage is empty. The accomplishments of separation logic include the specification and (manual) proof of the Schorr-Waite marking algorithm and the Cheney copying garbage collector, as well as numerous simpler programs. There is also an extension of the logic to shared- variable concurrency which is capable of treating, for example, processes that communicate storage ownership through a shared buffer, or concurrent quicksort. A further extension permits read-only sharing via Boyland's fractional permissions. Reynolds refused to claim that any problems were "nearly solved" (since such a claim once boomeranged on him). As unsolved problems, he mentioned data structures with rich sharing, such as cyclic graphs, the need to move towards richer programming languages, and the need for automation. He provided the following list of researchers in the area: London: Peter O'Hearn Richard Bornat Samin Ishtiaq Cris Calcagno Josh Berdine Ivana Mijajlovic Dino DeStefano Cambridge (UK): Matthew Parkinson Gavin Bierman Copenhagen: Lars Birkedal Noah Torp-Smith Bodil Biering Seoul: Hong Seok Yang Pittsburgh: John Reynolds Aleks Nanevski