Ownership types and Separation Logic seem to have similar goals, control over ownership and aliasing. Perhaps, I should also add: the ability to write modular specifications.

What is known about the relationship between ownership types and Separation Logic?

  • $\begingroup$ Sounds vaguely familiar. $\endgroup$ Aug 28 '12 at 22:09
  • $\begingroup$ @DaveClarke: Does my answer make sense to you? You've done a lot of work on ownership, and I only did a little before switching to working on separation logic. $\endgroup$ Aug 30 '12 at 8:54
  • $\begingroup$ @NeelKrishnaswami: Your answer makes a lot of sense. I plan to fill in some gaps when I can find time. In any case, I'm not aware of any paper that does a significant comparison. $\endgroup$ Aug 30 '12 at 18:27

I recently finished writing a survey of Ownership Types and found very little that discusses the relationship between the two topics. The three closest papers I came across are the following, which curiously come from the same conference:

  • Yang Zhao and John Boyland. A fundamental permission interpretation for ownership types. In Second IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, June 17-19, 2008, Nanjing, China. IEEE Computer Society, 2008., pages 65–72.

  • Shuling Wang, Luís Soares Barbosa, and José Nuno Oliveira. A relational model for confined separation logic. In In Second IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, June 17-19, 2008, Nanjing, China. IEEE Computer Society, 2008., pages 263–270.

  • Shuling Wang and Zongyan Qiu. A generic model for confinement and its application. In In Second IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, June 17-19, 2008, Nanjing, China. IEEE Computer Society, 2008., pages 57–64.

The first paper encodes two styles of ownership types, namely owners-as-dominators and owners-as-locks, in terms of Boyland's fractional permissions, which are a capability system developed for reasoning about programs.

The second paper takes confinement ideas similar to those used in ownership types and adds them to separation logic.

The third paper has developed a semantic approach which is used to encode various confinement disciplines such as ownership types. I'm not sure whether their system covers separation logic as well, and I cannot access it at the moment. Their approach is rather ad hoc; it can be seen as a more formal and systematic to a paper I wrote a while ago with James Noble and others:

  • Towards a model of encapsulation James Noble, Robert Biddle, Ewan Tempero, Alex Potanin, Dave Clarke The First International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming (IWACO), 2003.

The way I understand the difference is that ownership types constrain the shape of the object graph, and substructural systems (like separation logic) manage permissions to access the heap.

In the original work on ownership types, the idea is to maintain the invariant of owners as dominators. An object $o$ is dominated by an object $d$, if every path from the root set to $o$ contains $d$. So $o$ is only reachable from $d$. So the system is designed so that class declarations are parameterized by their owners, and then this fact gives you a derived frame condition for $o$: its state cannot change unless a method on its owner $d$ is invoked.

In contrast, substructural systems like linear types and separation logic rely on the idea of resources. Each region of the heap is a resource, and if you don't possess the resource you can't touch it. This makes frame conditions very easy: they always hold.

One superficial difference (which nevertheless confused me for a long time) was that ownership types were types, and separation logic was a program logic. Luckily, while ownership types were born in a type-theoretic setting, people have applied these ideas to program logics as well.

The two main pieces of theoretical work I know on this are Kassios's work on dynamic frames, which Bannerjee and Naumann (and their students) systematically exploited in their work on regional logic.

As I understand it, their basic approach is to take Hoare logic, and then:

  1. Add a new type of region variables, which you use to associate objects and regions.
  2. Add an effect system to Hoare logic to track the regions reads and writes touch.
  3. Use the effects to determine if an assertion is frame-respecting or not. If it is, you can frame it, and if it isn't, you can't.

Each approach has benefits and weaknesses.

  • Ownership makes frame properties significantly less convenient to use than in substructural approaches, since you have to compute frame conditions.

  • On the other hand, algorithms on DAGs support prettier inductive proofs in an ownership style, since you can decouple the footprint from the pointer structure. In a separation-style spec, the natural thing is to give an inductive invariant on a spanning tree. But if the spanning tree the algorithm computes is ever different than the one your invariant has, you're in for a world of hurt.

My general sense is that separation is easier to use than ownership, since we need frame properties for nearly every command in an imperative program. (Dave Naumann argues that region logic is more amenable to automation, since the assertion logic remains plain old FOL, and so you can use off-the-shelf theorem provers and SMT solvers.)

EDIT: I just found the following paper by Matt Parkinson and Alex Summers, The Relationship between Separation Logic and Implicit Dynamic Frames, where they claim to give a logic unifying the two methods.

  • $\begingroup$ Thanks very much for your insights, Neel. However, I have been wondering about the relationship between the two paradigms, rather than the differences. So I am going to keep the question open for now. $\endgroup$
    – Uday Reddy
    Aug 29 '12 at 18:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.