<p>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:</p>

<ul>
<li><p>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. </p></li>
<li><p>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.</p></li>
<li><p>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.</p></li>
</ul>

<p>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. </p>

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

<p>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:</p>

<ul>
<li>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.</li>
</ul>

CC BY-SA 3.0
2012-10-13T19:58:46.360Z
2012-10-14T09:14:17.430Z
2012-10-14T09:14:17.430Z
Dave Clarke
<p>The way I understand the difference is that ownership types <em>constrain
the shape of the object graph</em>, and substructural systems (like
separation logic) <em>manage permissions to access the heap</em>.</p>

<p>In the original work on ownership types, the idea is to maintain the
invariant of <em>owners as dominators</em>. An object $o$ is <em>dominated</em> 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.</p>

<p>In contrast, substructural systems like linear types and separation
logic rely on the idea of <em>resources</em>. 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.</p>

<p>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.</p>

<p>The two main pieces of theoretical work I know on this are Kassios's
work on <a href="http://n.ethz.ch/~kassiosi/papers/fm06.pdf" rel="noreferrer"><em>dynamic frames</em></a>, which Bannerjee and Naumann (and their
students) systematically exploited in their work on <a href="http://www.cs.stevens.edu/~naumann/pub/BanerjeeEtalECOOP.pdf" rel="noreferrer"><em>regional logic</em></a>.</p>

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

<ol>
<li>Add a new type of region variables, which you use to associate objects and regions.</li>
<li>Add an effect system to Hoare logic to track the regions reads and writes touch.</li>
<li>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.</li>
</ol>

<p>Each approach has benefits and weaknesses.</p>

<ul>
<li><p>Ownership makes frame properties significantly less convenient to
use than in substructural approaches, since you have to compute frame
conditions.</p></li>
<li><p>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.</p></li>
</ul>

<p>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.)</p>

<p>EDIT: I just found the following paper by Matt Parkinson and Alex Summers, <a href="http://www.lmcs-online.org/ojs/viewarticle.php?id=1081&amp;layout=abstract" rel="noreferrer"><em>The Relationship between Separation Logic and Implicit Dynamic Frames</em></a>, where they claim to give a logic unifying the two methods. </p>

CC BY-SA 3.0
2012-08-29T18:51:26.013Z
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.
Uday Reddy
CC BY-SA 3.0
2012-08-29T06:53:11.057Z
2012-08-30T12:17:04.923Z
2012-08-30T12:17:04.923Z
Neel Krishnaswami
<p>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.</p>

<p>What is known about the relationship between ownership types and Separation Logic?</p>

CC BY-SA 3.0
2012-08-28T22:09:29.980Z
Sounds vaguely familiar.
Dave Clarke
CC BY-SA 3.0
2012-08-30T08:54:10.543Z
@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.
Neel Krishnaswami
CC BY-SA 3.0
2012-08-30T18:27:22.373Z
@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.
Dave Clarke
<pl.programming-languages><type-systems><object-oriented><program-logic>
Ownership types and Separation Logic
Uday Reddy
# Ownership types and Separation Logic

(Asked by: username_0 on 2012-08-28)

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?

**Tags:** pl.programming-languages, type-systems, object-oriented, program-logic

> **Comments:**
> **username_1**: Sounds vaguely familiar.  
> **username_2**: @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.  
> **username_1**: @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.  

---

## 2 answers

### Answer by username_1 on 2012-10-13. Score: 7 | Accepted answer

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, username_1
  The First International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming (IWACO), 2003.


---

### Answer by username_2 on 2012-08-29. Score: 9

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*](http://n.ethz.ch/~kassiosi/papers/fm06.pdf), which Bannerjee and Naumann (and their
students) systematically exploited in their work on [*regional logic*](http://www.cs.stevens.edu/~naumann/pub/BanerjeeEtalECOOP.pdf).

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*](http://www.lmcs-online.org/ojs/viewarticle.php?id=1081&layout=abstract), where they claim to give a logic unifying the two methods.

> **Comments:**
> **username_0**: 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.  

---

