Further Reading on Local Reasoning and Separation Logic

The purpose of this page is just to point you to some relevant papers, should you be interested in delving into some of the further work on local reasoning and separation logic. I've broken the further work into categories:

Concurrency   Verification and Program Analysis   Footprints and the Frame Problem   Separation Logic for OO.   Talks   Other Interesting Papers  

Back to Local Reasoning Page  

 

Concurrency

Beginning. The place to get started is Some highlights: we can transfer portions of heap between processes, as in a resource manager or in efficient message passing; we can do modular reasoning in the presence of semaphores (e.g., split binary semaphores without maintaining a global invariant); we do parallel mergesort with no rely or guarantee conditions, the proven processes automatically mind their own business.

That paper grew out of a note from January 2002 which showed some modular reasoning about concurrency. At that time I had no model and was scared about soundness. Then John Reynolds showed surprising subtleties regarding soundness, and we were facing an extremely difficult problem in the semantics of concurrency. We needed expert help, and it arrived in Steve Brookes who rode in and saved the day (and the whole approach).

The next step adapted a nice idea of John Boyland to allow processes to share read permissions.

A highlight: a nice proof of the classic readers-and-writers program. In the original TCS paper I emphasized that proven programs are race-free, and Steve Brookes showed a theorem to that effect. Doug Lea then pointed us to a challenge, some extremely racy non-blocking algorithms. After a lot of discussion in the East London Massive, and some unsuccessful attempts, Matthew Parkinson finally gave a proof of such an algorithm. Of course, there is no conflict with the ``no races'' theorem: the concurrent separation logic just forces you to be explicit about granularity, by wrapping little critical sections around those portions of code considered atomic.

 

Rely/Guarantee meets Separation Logic. Interesting work is under way on combining ideas in concurrent separation logic with the rely/guarantee formalism pioneered by Cliff Jones. Two groups independently made very good steps in this direction in 2006.

The main interest in these approaches is that they try to merge the merits of rely/guarantee (good treatment of interference) and separation logic (good treatment of independence, avoidance of global states). It's early days yet for these approaches, but they appear to have promise.

 

More Work on Semantics. Speaking of granularity, partly spurred by the concurrent separation logic, John Reynolds has opened an attack on Dijkstra's old ``grain of time'' problem.

And Steve Brookes has also weighed in on the subject. It is rather amazing to me to see progress on such basic problems in the semantics of concurrency, many years after they arose.

A completely different kind of model was defined by Jonathan Hayman and Glynn Winskel, using Petri Nets.

Their model accounts for ``independence'' properties of proven programs in concurrent separation logic, and also is pertinent to the grain of time problem because of the good refinement properties that Petri nets (and other independence models) possess.

 

Further Remarks and Links related to Concurrency.

 

Program Verification and Analysis

News: Smallfoot. The goal of Smallfoot was to see if the simplicity of by-hand specs and proofs could be transferred to an automatic setting. Smallfoot is an assertion checker. It requires (lightweight) preconditions, postconditions and loop invariants to be given by the user. It uses its own toy programming language, designed to ease experimentation in the initial steps, rather than a real programming language. There are two main papers to look at: Smallfoot v0.1 was released in December of 2005.

Smallfoot-RG is an extention which uses the marriage or rely-guarantee and separation logic proposed by Parkinson and Vafeiadis to provide the first automatic verifications for (some properties of) some tricky concurrent algorithms.

 

Program Analysis. In 2005 we started working on program analysis using separation logic. The first step use Smallfoot's symbolic execution mechanism together with selected true impications to infer invariants via a fixed-point calculation, in the usual way of abstract interpretation.

Dino named this approach Space Invader (you can figure out what it stands for), and he has a SpaceInvader blog. (Closely related ideas were put forth independently in a paper of Magill et al. ) Anyhow, the point of this first Invader paper was to show a way of defining an abstract domain that has some of separation logic's modularity built in, as a springboard for further things. Here are some of the further things: Watch this space. There is more coming on program analysis.

Further Remarks and Links related to Verification and Analysis.

 

Footprints and the Frame Problem

The frame problem in AI is that, when specifying what changes, an inordinate amount of effort usually needs to be spent saying what doesn't change. These frame axioms (what doesn't change) distract from the real concern: what changes. For example, when say you increment location 10's contents, you intend that no other locations are altered, but it is a pain to say so explicitly. There are many, many papers on the frame problem int he AI literature. You can find them on search engines. I recommend, especially, papers of Reiter for their simplicity and clarity.

A POPL'01 paper and a CSL'01 paper described an approach to the frame problem for programs based on a connection between frame axioms and the notion of footprint : the cells a program accesses. We know that any cell outside the footprint will not change, so frame axioms describing this absence of change can be obtained for free, without explicitly stating them beforehand. A FOSSACS'02 paper went on to explain that, while separation logic gives a convenient way to exploit this fact, using the frame rule, it is in no way necessary: the frame axioms (invariants for cells outside the footprint) are just true, whether or not you employ separation logic to express them.

Several papers have taken these ideas further, and probed more deeply.

 

Alternative approaches to footprints/frames. One alternative has been put forth by Benton.

Benton considers a model that contradicts some of the underlying assumptions of the above work (namely, the frame property), and makes the support (or footprint) of an assertion explicit. He also uses a polymorphic interpretation of Hoare triples.

Another alternative is in work by Kassios.

His ``dynamic frames'' also allow the footprint (or, a collection of current or owned cells) to appear explicitly in specifications, rather than left implicit as in separation logic.

Finally, here is some very recent work with a very clear treatment of the issues involved.

These works identify locality properties related to those that underly separation logic (e.g., the ``frame property''): it is something like working in the target language of separation logic semantics, but not exactly...

 

Separation Logic and Object-Oriented Programming

A nod in the OO direction considered static modules (like single-instance classes). Then, Matthew Parkinson in his thesis, and in a paper with Gavin Bierman, took a major step forward, to handle a subset of Java. More recently, Parkinson has given an entertaining and radical position paper against the noion of class invariant, bolstered by simple solutions to some old conundrums

Next, Parkinson and Bierman have extended their work to account for inheritance

and a very similar solution was obtained in

The Parkinson-Bierman approach works by adding ``abstract predicates'' to separation logic. These predicates are logical cousins of type variabes, and their explanation of abstraction with them is somehow analogous to the treatments of classical abstract typesusing the polymorphic lambda-calculus, by Reynols, Mitchell and Plotkin. A foundational and powerful view of the mechanisms here was given in

Further works related to OO, Data Abstraction and Refinement.
Quite a lot is happening in this space, not all of which is explicitly presented in OO terms.

 

Random Further Reading

The following list collects a few pointers to other papers not listed above. It is intentionally incomplete and will be updated infrequently.

Back to Top