Bartosz Milewski's Programming Cafe

I’ve blogged before about the C++ unique_ptr not being unique and how true uniqueness can be implemented in an ownership-based type system. But I’ve been just scratching the surface.

The new push toward uniqueness is largely motivated by the demands of multithreaded programming. Unique objects are alias free and, in particular, cannot be accessed from more than one thread at a time. Because of that, they never require locking. They can also be safely passed between threads without the need for deep copying. In other words, they are a perfect vehicle for safe and efficient message passing. But there’s a rub…

The problem is this: How do you create and modify unique objects that have internal pointers. A classic example is a doubly linked list. Consider this Java code:

public class Node {
    public Node _next;
    public Node _prev;
}
public class LinkedList {
    private Node _head;
    public void insert(Node n) {
        n._next = _head;
        if (_head != null)
            _head._prev = n;
        _head = n;
    }
}

Suppose that you have a unique instance of an empty LinkedList and you want to insert a new link into it without compromising its uniqueness.

The first danger is that there might be external aliases to the node you are inserting–the node is not unique, it is shared. In that case, after the node is absorbed:

_head = n;

_head would be pointing to an alias-contaminated object. The list would “catch” aliases and that would break the uniqueness property.

The remedy is to require that the inserted node be unique too, and the ownership of it be transferred from the caller to the insert method. (Notice however that, in the process of being inserted, the node loses its uniqueness, since there are potentially two aliases pointing to it from inside the list–one is _head and the other is _head._prev. Objects inside the list don’t have to be unique–they may be cross-linked.)

The second danger is that the method insert might “leak” aliases. The tricky part is when we let the external node, n, store the reference to our internal _head:

n._next = _head

We know that this is safe here because the node started unique and it will be absorbed into the list, so this alias will become an internal alias, which is okay. But how do we convince the compiler to certify this code as safe and reject code that isn’t? Type system to the rescue!

Types for Uniqueness

There have been several approaches to uniqueness using the type system. To my knowledge, the most compact and comprehensive one was presented by Haller and Odersky in the paper, Capabilities for External Uniqueness, which I will discuss in this post. The authors not only presented the theory but also implemented the prototype of the system as an extension of Scala. Since not many people are fluent in Scala, I’ll translate their examples into pseudo-Java, hopefully not missing much.

Both in Scala and Java one can use annotations to extend the type system. Uniqueness introduces three such annotations, @unique, @transient, and @exposed; and two additional keywords, expose and localize.

-Objects that are @unique

In the first approximation you may think of a @unique object as a leak-proof version of C++ unique_ptr. Such object is guaranteed to be “tracked” by at most one reference–no aliases are allowed. Also no external references are allowed to point to the object’s internals and, conversely, object internals may not reference any external objects. However, and this is a very important point, the insides of the @unique object may freely alias each other. Such a closed cross-linked mess is called a cluster.

Consider, for instance, a (non-empty) @unique linked list. It’s cluster consists of cross-linked set of nodes. It’s relatively easy for the compiler to guarantee that no external aliases are created to a @unique list–the tricky part is to allow the manipulation of list internals without breaking its uniqueness (Fig 1 shows our starting point).

Fig 1. The linked list and the node form separate clusters

Look at the definition of insert. Without additional annotations we would be able to call it with a node that is shared between several external aliases. After the node is included in the list, those aliases would be pointing to the internals of the list thus breaking its uniqueness. Because of that, the uniqueness-savvy compiler will flag a call to such un-annotated insert on a @unique list as an error. So how can we annotate insert so that it guarantees the preservation of uniqueness?

-Exposing and Localizing

Here’s the modified definition of insert:

public void insert(@unique Node n) @transient {
    expose (this) { list =>
        var node = localize (n, list);
        node._next = list._head;
        if (list._head != null)
            list._head._prev = node;
        list._head = node;
    }
}

Don’t worry, most of the added code can be inferred by the compiler, but I make it explicit here for the sake of presentation. Let’s go over some of the details.

The node, n passed to insert is declared as @unique. This guarantees that it forms its own cluster and that n is the only reference to it. Also, @unique parameters to a method are consumed by that method. The caller thus loses her reference to it (the compiler invalidates it), as demonstrated in this example:

@unique LinkedList lst = new @unique LinkedList();
@unique Node nd = new @unique Node();
lst.insert(nd);
nd._next; // error: nd has been consumed!

The method itself is annotated as @transient. It means that the this object is @unique, but not consumed by the method. In general, the @transient annotation may be applied to any parameter, not only this. You might be familiar with a different name for transient–borrowed.

Inside insert, the this parameter is explicitly exposed (actually, since the method is @transient, the compiler would expose this implicitly).

expose (this) { list => ... }

The new name for the exposed this is list.

Once a cluster is exposed, some re-linking of its constituents is allowed. The trick is not to allow any re-linking that would lead to the leakage of aliases. And here’s the trick: To guarantee no leakage, the compiler assigns the exposed object a special type–its original type tagged by a unique identifier. This identifier is created for the scope of each expose statement. All members of the exposed cluster are also tagged by the same tag. Since the compiler type-checks every assignment it automatically makes sure that both sides have the same tag.

Now we need one more ingredient–bringing the @unique node into the cluster. This is done by localizing the parameter n to the same cluster as list.

var node = localize (n, list);

The localize statement does two things. It consumes n and it returns a reference to it that is tagged by the same tag as its second parameter. From that point on, node has the same tagged type as all the exposed nodes inside the list, and all assignments type-check.

Fig 2. The list has been exposed: all references are tagged. The node has been localized (given the same tag as the list). Re-linking is now possible without violating the type system.

Note that, in my pseudo-Java, I didn’t specify the type of node returned by localize. That’s because tagged types are never explicitly mentioned in the program. They are the realm of the compiler.

Functional Decomposition

The last example was somewhat trivial in that the code that worked on exposed objects fit neatly into one method. But a viable type system cannot impose restrictions on structuring the code. The basic requirement for any programming language is to allow functional decomposition–delegating work to separate subroutines, which can be re-used in other contexts. That’s why we have to be able to define functions that operate on exposed and/or localized objects.

Here’s an example from Haller/Odersky that uses recursion within the expose statement. append is a method of a singly-linked list:

void append(@unique SinglyLinkedList other) @transient
{
    expose(this) { list =>
        if (list._next == null)
            list._next = other; // localize and consume
        else
            list._next.append(other);
    }
}

In the first branch of the if statement, a @unique parameter, other, is (implicitly) localized and consumed. In the second branch, it is recursively passed to append. Notice an important detail, the subject of append, list._next, is not @unique–it is exposed. Its type has been tagged by a unique tag. But the append method is declared as @transient. It turns out that both unique and exposed arguments may be safely accepted as transient parameters (including the implicit this parameter).

Because of this rule, it’s perfectly safe to forgo the explicit expose inside a transient method. The append method may be thus simplified to:

void append(@unique SinglyLinkedList other) @transient
{
    // 'this' is implicitly exposed
    if (_next == null)
        _next = other; // localize and consume
    else
        _next.append(other);
}

Things get a little more interesting when you try to reuse append inside another method. Consider the implementation of insert:

void insert(@unique SingleLinkedList other) @transient
{
    var locOther = localize(other, this);
    if (other != null) 
    {
        locOther.append(_next)
        _next = locOther;
   }
}

The insert method is transient–it works on unique or exposed lists. It accepts a unique list, other, which is consumed by the localize statement. The this reference is implicitly exposed with the same tag as locOther, so the last statement _next=locOther type-checks. The only thing that doesn’t type-check is the argument to append, which is supposed to be unique, but here it’s exposed instead.

This time there is no safe conversion to help us, so if we want to be able to reuse append, we have to modify its definition. First of all, we’ll mark its parameter as @exposed. An exposed parameter is tagged by the caller. In order for append to work, the this reference must also be tagged by the caller–with the same tag. Otherwise the assignment, _next=other, inside append, wouldn’t type-check. It follows that the append method must also be marked as @exposed (when there is more than one exposed parameter, they all have to be tagged with the same tag).

Here’s the new version of append:

void append(@exposed SinglyLinkedList other) @exposed
{
    if (_next == null)
        _next = other; // both exposed under the same tag
    else
        _next.append(other); // both exposed under the same tag
}

Something interesting happened to append. Since it now operates on exposed objects, it’s the caller’s responsibility to expose and localize unique object (this is exactly what we did in insert). Interestingly, append will now also operate on non-annotated types. You may, for instance, append one non-unique list to another non-unique list and it will type-check! That’s because non-annotated types are equivalent to exposed types with a null tag–they form a global cluster of their own.

This kind of polymorphism (non-annotated/annotated) means that in many cases you don’t have to define separate classes for use with unique objects. What Haller and Odersky found out is that almost all class methods in the Scala’s collection library required only the simplest @exposed annotations without changing their implementation. That’s why they proposed to use the @exposed annotation on whole classes.

Conclusion

Every time I read a paper about Scala I’m impressed. It’s a language that has very solid theoretical foundations and yet is very practical–on a par with Java, whose runtime it uses. I like Scala’s approach towards concurrency, with strong emphasis on safe and flexible message passing. Like functional languages, Scala supports immutable messages. With the addition of uniqueness, it will also support safe mutable messages. Neither kind requires synchronization (outside of that provided by the message queue), or deep copying.

There still is a gap in the Scala’s concurrency model–it’s possible to share objects between threads without any protection. It’s up to the programmer to declare shared methods as synchronized–just like in Java; but there is no overall guarantee of data-race freedom. So far, only ownership systems were able to deliver that guarantee, but I wouldn’t be surprised if Martin Odersky had something else up his sleeve for Scala.

I’d like to thank Philip Haller for reading the draft of this post and providing valuable comments. Philip told me that a new version of the prototype is in works, which will simplify the system further, both for the programmer and the implementer.