Gagallium

In the previous blog post, I introduced a new framework for reasoning about programs: permissions, a sort of hybrid between a type system and a program logic. The main selling point is that it allows one to reason in a finer-grained manner about programs. The current incarnation of the permission mechanism is Mezzo, a language in the tradition of ML.

The first question that comes fairly naturally is: why are we going such great lengths trying to design such a complex reasoning framework? Here are some answers:

• since mutable portions of the heap have a unique owner, programs written in Mezzo enjoy the property that they are data-race free, that is, we may never have two people trying to access a writable location at the same time;
• thus, we are allowed to perform strong updates, that is, updates that change the type of a variable.

The latter item may seem of dubious usefulness; indeed, the mswap example that I used seems artificial, and I have never needed it in practice. However, the example of concat at the end of the previous post is much more useful: it is emblematic of a more general concept of “destination-passing-style” algorithms that allow one to write functions in a safe, tail-recursive way, without resorting to unsafe hacks.

However, as I hinted in the conclusion of the previous blog post, with the elements I have presented so far, there are some serious limitations.

In this blog post, I will introduce a novel mechanism called adoption and abandon, which allows one to safely alias mutable data, while remaining inside the permission framework; in particular, this means we’ll continue to guarantee the unique-owner property for mutable blocks. Of course, there’s no free lunch: this adoption and abandon mechanism incurs a dynamic cost at runtime.

A story of adoption and abandon

Meet the fifo, our favorite example

The running example in this section will be a first-in first-out structure, that is, a fifo. Cells are appended at the end, and popped from the front of the fifo. The loop at the end of the fifo is just a trick to avoid making the next field an option type.

• The type cell is mutable: we need to rewire the pointers when we we call either retrieve or insert on the fifo.
• The type fifo is also mutable, since its head and tail fields change over time.

An aliasing problem

One can see already that there is a problem with this aliasing pattern. If there’s only one element in the fifo, and the user does:

let x = fifo.head in
let y = fifo.tail in
(* x @ cell ∗ y @ cell *)

…then the user has aliased the same cell, and has two exclusive permissions for it. This is a violation of our rules, and the permission system definitely won’t allow that! So we can’t declare the head and tail field to be cells…

Getting back an ownership tree

In essence, the problem is that the ownership graph is not a forest, and the permission system can only express forest-like ownership patterns. We need to move back to a forest-like ownership pattern. We achieve this through the adoption mechanism.

We say that the fifo can now adopt the cells. That is, the permission for the cells is “hidden” under the permission for the fifo; in other words, if you own the fifo, you own the cells. Once adopted, the type of a cell changes to reflect the fact that it may be owned by someone else.

Some data types

Let us first take a look at the definition of type fifo a and cell a, respectively fifo and cells holding elements of type a.

mutable data fifo a =
  | Empty { head: (); tail: () }
  | NonEmpty { head: dynamic; tail: dynamic }
adopts cell a

mutable data cell a =
  | Cell { contents: a; next: dynamic }

The important point here is the adopts clause that’s attached to the definition of fifo; this clause refers to the whole type. We will see in a minute the meaning of type dynamic.

Adoption

The first operation consists in giving up our ownership of a cell, and transferring it to the fifo object.

(* x @ cell a ∗ f @ fifo a *)
give x to f;
(* x @ dynamic ∗ f @ fifo a *)

After we’ve given up our knowledge of x, we no longer know that it is a cell. The only thing that remains for us to know about x is that it has type dynamic: it means that x may be currently adopted by someone.

What is the point, then, of giving up our knowledge of x? The key difference is that, unlike cell a, dynamic is a duplicable type, which means we can alias x.

Abandon

The converse operation, abandon, works as follows; it allows one to regain the whole knowledge about a variable; in our case, regain the permission x @ cell a.

(* x @ dynamic ∗ f @ fifo a *)
take x from f;
(* x @ cell a ∗ f @ fifo a *)

How do we know that the type that x should regain is x @ cell a? This is achieved by doing a lookup on the definition of f, and seeing that fifos adopt elements of type cell a.

An element, in order to be an adopter, must be mutable. Moreover, adopters can only adopt one type of elements.

The safety of the whole thing depends on the fact that the take operation must never succeed twice, otherwise we could have x @ cell a ∗ x @ cell a: this would be a definite breach of soundness.

The general idea is that when you give an element, you become free to alias it, but it is your responsibility to make sure you never take it twice, that is, to make sure you never call take x from f; take y from f with x and y being aliases. In the case of the fifo, it is easy to make mistakes: if the fifo only has one element, the following code will fail:

take fifo.head from fifo;
take fifo.tail from fifo;

Making sure the code fails

The last point that we need to address is how to make sure that the take operation cannot succeed twice for the same element. This is achieved using a hidden field and dynamic tests.

Each mutable object has a hidden field; the hidden field contains the address of the adopter if the object is currently adopted, null otherwise.

• When give’ing x to f, we set the hidden field of x to be the address of f.
• When taking x from f, we check that the hidden field of x and the address of f match; if this is the case, we can safely assume that x has the type to be found in the adopts clause in the definition of the type of f; then, we null out the field.

In the example of the one-element fifo, after taking head, the hidden field would be nulled out, and the second attempt to take tail would fail, since the value in the hidden field (null) and the address of the adopter would fail to match.

Illustrating all these concepts

In order to better understand how we use all these mechanisms to type-check a program, we have a step-by-step animation explaining how a given piece of code is type-checked. We chose the insert function that inserts an element into the fifo.

See the insert example (use the “step forward” and “step back” links).

Some notes about this example:

• the dynamic permission is always available on-demand for x, as long as we know that there is an exclusive permission for x;
• we use the tag of <- instruction; it allows one to change the tag of a value; the definition for the new tag must have the same number of fields;
• structural types feature an adopts clause – without it, the system would be unsound;
• when we enter the function, the permissions we gain are those brought to us through the arguments;
• when we exit the function, we must make sure f @ fifo a is still available; however, because x is consumed, we don’t have anything to ensure about x.

The power of adoption/abandon

Adoption and abandon provide an easy escape hatch to make sure you can write your program, even if the aliasing pattern is too complex to be expressed in the pure permission mechanism. The give and take operations are thread-safe; they incur no race conditions, that is, give cannot succeed in two separate threads simultaneously.

Of course, there is a penalty, both in terms of memory space (hidden field) and runtime tests (give and take operations). Time will tell whether this is something that we can live with, or if it is too expensive. A short-term goal is to allow one to declare a data type is being “slim” (no hidden field) or “fat” (with a hidden field). A long-term goal is to allow one to plug in a proof that the extra dynamic tests are not needed, so that the compiler can skip the tests altogether.

What is the state of Mezzo?

If you’ve reached that stage of the blog post, you have my entire gratitude, as this was quite a technical topic and I’m afraid it has been fairly long.

The prototype

We currently have a prototype type-checker that is available on our web page, along with several examples of programs that the type-checker currently accepts. There is a fairly long to-do list, and the type-checker is currently unsound in many corners, but this is something that we’re aware of and that we know how to fix.

Concurrency

Of course, if we are to go such great lengths, we might as well have concurrency built into the language. Thibaut Balabonski is currently tackling the problem. Here is an example of how we could leverage the permission mechanism:

abstract lock (p: perm)
fact duplicable (lock p)
val create @ [p :: PERM] () -> lock p
val acquire @ [p :: PERM] lock p -> (| p)
val release @ [p :: PERM] (lock p | consumes p) -> ()

A lock simply protects access to a permission (think of p as x @ ref int where x is a variable in scope). You can copy the lock around, pass it to other threads, and try to acquire it: when you succeed, you obtain the permission. When you want to release the lock, you must give up the permission from your context.

data outcome (p :: PERM) =
  | Success { | p }
  | Failure { }

val try_acquire @ [p :: PERM] lock p -> outcome p

If we were to implement try_acquire, we could write a data type that expresses the fact that in case the operation succeeds, you obtain p in the corresponding match branch.

The signature for a spawn function could be as follows:

val spawn (f: (|p) -> () | p) -> ()

…where f requires a set of permissions p to execute, and spawn takes p from its caller, and uses it to launch p.

Compilation

We had an intern, Henri Chataing, work on a very prototype-ish implementation of a compilation scheme emitting OCaml code with calls to Obj.magic sprinkled in the right places. We’re unsure as to whether that’s the right direction; we’re also considering emitting CIL code, or C# code directly to take advantage of the real multithreaded capabilities of the CLR…

I want to participate!

We have many opportunities for internships, do contact us if you feel like you want to work on designing an exciting new language!