This page contains some links, and some remarks, on a developing line of work on what I call local reasoning, and a formalism that John Reynolds has dubbed separation logic (separation logic supports local reasoning). It's purpose is to give some context for people wanting to learn about the work.
Getting Started: Early Days
People and Project Links: East London Massive Smallfoot SpaceInvader Blog SLAyer
Further Reading:
Concurrency
Program Verification and Analysis
Semantics of Local Action
Data Abstraction
News
M Parkinson, R Bornat and P O'Hearn
POPL 2007
C Calcagno, D Distefano, P O'Hearn and H Yang. In 13th SAS, LNCS 4134,
182-203, 2006
J Berdine, B Cook, D Distefano and P O'Hearn. In 18th CAV, LNCS 4144,
pp386-400, 2006
D Distefano, P O'Hearn and H Yang. In 12th TACAS, LNCS 3920, pp287-302, 2006.
East London Massive
The London Separation Logic Community (aka, East London Massive)
has weekly meetings, which involve discussions that run 4-5 hours,
often prefixed by lunch and postfixed by further discussions in the pub.
Currently we are
Josh Berdine
Richard Bornat
Cristiano Calcagno
Aziem Chawdhary
Byron Cook
Dino Distefano
Akbar Hussein
Ivana Mijajlovic
Peter O'Hearn
Matthew Parkinson
Abhishek Thakur
Hongseok Yang
In actuality, the Massive has spread beyond East London. Some have moved, even outside of London, and others have joined. But the spirit is the same.
Lately, we have been consorting with Terminator. Check out this Microsoft Research News article on Taking on the Halting Problem . It has an interview with Byron, who is a Visiting Professor at Queen Mary. We count him as a member of the Massive and, conversely, I've joined up with Terminator; too cool!
The Massive is keen on automatic program verification (static analysis) these days. SpaceInvader is a tool being developed in Ldn, SLAyer is being developed at Microsoft, and there is lots of collaboration and idea-sharing between them.
Some Pics:
Terminator visits London ,
Beat Juggling
,
A party ,
A comic
Early Days
The best starting point for reading is
Reynolds's survey paper from LICS'02.
Besides that, though,
when understanding a subect it
is helpful
(and not emphasized enough in CS) to have a picture of the development
of ideas,
and in this account of the early days I will lead up to Reynolds's paper,
gradually.
An important precursor of separation logic was the logic of bunched implications (BI) introduced by David Pym and I in a short paper in 1999.
A major step forward was made by John Reynolds, who originated a ``separation logic'' for talking about heap data structures. Reynolds showed how the separating conjunction (the heap composition primitive) could be used to short-circuit the potentially global effect of aliasing, thereby leading to much simplified program proofs. Here is Reynolds's original paper.
These two lines were brought together in
I am often asked: how are BI and separation logic related, are they the same thing? There are two parts to the answer. First, separation logic is a formalism of program dynamics, based on Hoare triples, where there are no Hoare triples in BI. So, for this part of the answer separation logic is an extension of BI. Second, separation logic has been based on particular storage models while, as Pym has emphasized, BI can be understood more generally in terms of resource and it's model theory which is inspired by a primitive of resource composition. The heap models of separation logic are specific BI models, and furthermore not all BI models are about separation. So, for this second part to the answer, the relation is like that of First-order logic (which is generic) to Peano Arithmetic (a specific theory); the pre- and postconditions of separation logic form a specialization of BI.
After these first papers came one which concentrated on what I call local reasoning. See in particular the thought experiment involving the ``small axioms'', and an example showing why one can't avoid the notorious frame problem in program specification. A followup investigates the semantic basis of the ``frame rule'', for a concrete operational semantics.
The basic idea of local reasoning was already touched upon in the POPL'01 paper, and pointed at in previous work of Richard Bornat; it fully crystallized in discussions with Hongseok Yang leading up to the CSL'01 paper. During these discussions Yang came up with examples of ``within data structure'' locality, which went beyond the ``between data structure'' locality that had been displayed in the POPL'01 paper. This showed that the formalism could be used to concentrate on ``local surgeries'' that worked on small areas of a data structure, to be later glued together using the frame rule. Several examples were produced (using varieties of trees), before Yang settled on using the Schorr-Waite graph marking algorithm to illustrate his points.
Finally, Reynolds's paper from his LICS'02 invited lecture charts developments in separation logic up to May 2002, which represents a natural end-point to the early days.
Category theory (Day's construction); Reynolds-Oles functor-category semantics (extension of a command); Relevant logic (bunches, monoidal semantics); Linear logic and Syntactic Control of Interference; Bornat's work on proving pointer programs in traditional Hoare logic (non-locality the major problem; spatial separation the answer)
This project draws on ideas that go back some way; some of the territory was mapped out in this talk.Further Reading: Concurrency Program Verification and Analysis Semantics of Local Action Data Abstraction