Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Local Reasoning and Separation Logic
[go: Go Back, main page]

Local Reasoning and Separation Logic

 
This page contains some links on separation logic and local reasoning (separation logic supports local reasoning). It's purpose is to give some context for people wanting to learn about the work. A good way to get started is to read Reynolds's survey paper from LICS'02 and the CSL'01 paper, together or in quick succession. When understanding a subect it is also helpful (and not emphasized enough in CS) to have a picture of the development of ideas. If you are interested in this sort of thing, go here for the early days.

People and Project Links:   East London Massive   Smallfoot   SpaceInvader Blog   SLAyer

Further Reading:   Early Days   Concurrency   Program Verification and Analysis   Footprints and the Frame Problem   SL for OOP

News

East London Massive

The East London Massive is a loose collective of people interested in program logic, semantics, and analysis. It started in London around the turn of the millenium, when we were working on the (at the time) new theory of separation logic at Queen Mary. The community then spread out to include friends in Cambridge and west London, as some of us left the East End and others joined. Currently, we are

Josh Berdine   Richard Bornat   James Brotherston   Cristiano Calcagno   Aziem Chawdhary   Byron Cook   Dino Distefano   Akbar Hussein   Ivana Filipovic   Peter O'Hearn   Matthew Parkinson   Hongseok Yang  

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. In a brilliant new development, jStar was born in 2008. Check it out.

The Massive has formed an allegiance with the Terminators. They are researching tools that automatically prove program termination (or find termination bugs). What a cool thing to try to do! 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. There is also a Scientific American Article on Terminator, and another in the Financial Times and a channel 9 interview . Way to go Byron!

Some Pics: Terminator visits London , Remix session , A party , A comic , Jamming , Harry Potter moment , Logicians? , A day at the office , Classical BI for Finance

Early Days

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.

BI had a general model theory oriented around ``resource composition''. It did not, though, have Hoare triples, and we did not (at that point) know how to construe heaps as models of BI. BI, though, it a general logic with a proof theory and model theory built up in the way of logicians. Pym has written a comprehensive monograph on BI. See the BI page for that and other papers.

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

One important point is that, armed with Pym's resource semantics, Ishtiaq and I were able to see how the ideas in Reynolds's paper could be reworked for a model that satisfied all the laws of classical (rather than intuitionistic) logic; this model also allowed for an account of memory disposal, and we were (surprisingly to us) now in the territory of "unsafe" low-level programming.

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.

When you see the CSL'01 or LICS'02 paper for the first time, it is possible to think: well, that was easy! (In a way, that's of course a good thing.) But, for a deeper understanding it helps a lot to consider what came before. For this, I recommend Proving Pointer Programs in Hoare Logic , by Richard Bornat. It shows various struggles, and points to previous work which is worth going back to check up on. It also has a very nice idea: Bornat reveals the relevant portion of storage in all his predicate definitions, which might be thought of as a precursor to the possible worlds in separation logic, and which could even be the basis of an approach to local reasoning without separation logic (see also remarks in the intro to Semantic Basis above).

Continuing... the basic idea of local reasoning was already touched upon in the POPL'01 paper, and pointed at in the previous work of 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.

 

Some Sources

It's always nice to acknowledge sources of inspiration. Here are some.

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  

Back to Top