Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
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?
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:
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:
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.
