Type System



I’ve been using auto_ptrs before they were available in C++ (I made my own). I wrote several articles about resource management, in which auto_ptr played a prominent role. auto_ptr had always had many flaws, but it was a workhorse of memory management in a language that shuns garbage collection. Many of the flaws have been understood over the years and, in the 0x version of C++, auto_ptr was supplanted by the new improved unique_ptr. Using the latest features of C++, like rvalue references, unique_ptr implements move semantics in a consistent manner. You can now store unique_ptrs in most containers and apply many algorithms to them.

So why am I not jumping for joy? Because I know how much more can be done.

But first let me summarize the idea behind the unique pointer. It is a (smart) pointer that is the only reference to the object it’s pointing to. In particular, you cannot make a copy of a unique pointer–if you could, you’d end up with two references to the same object. You can only move it (hence the move semantics), making the source of the move invalid. With the older auto_ptr the moving was done quietly during assignment or pass-by-value. The problem with that arrangement was that the source auto_ptr would suddenly turn to null, which was sometimes confusing and occasionally led to access violations–as in this example:

void f(auto_ptr<Foo> foo); // pass by value

auto_ptr<Foo> pFoo (new Foo());
f(pFoo); // pass by value nulls the internal pointer
pFoo->method(); // access violation

The improvement provided by unique_ptr is to require an explicit move, to sensitize the programmer to the fact that the source of move becomes invalid. Still, the following code will compile, although the bug is much more prominent:

void f(unique_ptr<Foo> foo);

unique_ptr<Foo> pFoo (new Foo())
f(move(pFoo)); // explicit move
pFoo->method(); // access violation

A bigger problem is that there is no guarantee that a unique_ptr indeed stores the unique reference to an object. To begin with, unique_ptr can be constructed from any pointer. That pointer might have already been aliased, as in:

void f(unique_ptr<Foo> foo) {
    // destructor of foo called at the end of scope
}

Foo * foo = new Foo();
unique_ptr<Foo> upFoo(foo); 
// foo now aliases the contents of upFoo
f(move(upFoo)); // explicit move
foo->method(); // undefined behavior

There is also an obvious backdoor in the form of the method unique_ptr::get, which can be used to spread new aliases. This can be particularly insidious when you have to pass the result of get to a foreign function:

void f(Foo * pf) {
    globalFoo = pf; // creates a global alias
}

unique_ptr<Foo> pFoo(new Foo());
f(pFoo.get()); // leaks an alias

Finally, it’s possible to create aliases to data members of the object stored in unique_ptr, as well as assign aliased references to its data members. Consider this example:

class Foo {
public:
    ~Foo() { delete _bar; }
    Bar * _bar;
};

Bar * pBar = new Bar();
unique_ptr<Foo> upFoo(new Foo());
pFoo->_bar = pBar;
// pBar is now an alias to a member of Foo
upFoo.reset(); // deletes _bar inside foo
pBar->method(); // undefined behavior

All this adds up to quite a number of ways to shoot yourself in the foot! Still, if the only problems were deterministic access violations, I could live with them (I’m a very disciplined programmer). They are reasonably easy to reproduce and can be debugged using standard methods (code coverage). But now there is a new elephant in the room–multithreading.

The beauty of unique objects is that they can be safely passed (moved) between threads and they never require locking. Indeed, since only one thread at a time can reference them, there is no danger of data races. Except when, as in the examples above, aliases are inadvertently leaked from unique_ptr. Accessing an object through such aliases from more than one thread without locking is a very nasty bug, usually very hard to reproduce.

Type system approach

Okay, so what’s the panacea? I’m glad you asked–the type system, of course! Make unique a type qualifier and all your troubles are gone. Notice that the compiler has no idea about the semantics of some library class called unique_ptr, but it can be made aware of the semantics of the unique type qualifier. What’s more, it can enforce this semantics from cradle to grave–from construction to destruction. (I know this proposal has no chance to be incorporated into C++, but it might be useful in, let’s say, the D programming language.)

You don’t construct a unique pointer from an arbitrary pointer. You just construct the object as unique (I’m still using C++-like syntax):

unique Foo * foo = new unique Foo();

Now that the compiler knows the meaning of unique, it can, for instance, detect if a unique pointer is accessed after having been moved. The compiler might prevent such an invalid pointer from being dereferenced or passed to other functions. Such bugs can be detected at compile time, rather than through access violations at runtime.

Do we need separate syntax for move? It might seem that using the assignment syntax (the equal sign) wouldn’t be so bad, as long as the compiler prevents us from dereferencing the null pointer left behind after a move. However, another problem arises when you start instantiating templates with unique pointers. Some containers and algorithms will work out of the box. Some will refuse to be instantiated because internally they try to access unique pointers after the move. But there is a third category of templates that, although move-correct, will generate unexpected results–like vectors with null unique pointers. Unfortunately, there are situations where the compiler has limited vision (i.e., it cannot do whole-program analysis) and can miss a null unique pointer dereference. For instance, it can’t prevent the use of a vector after a random element has been moved out of it.

Let’s assume that we have a special syntax for move, say := . Here’s a simple example of its use:

unique * Foo foo1 = new unique Foo();
unique * Foo foo2 := foo1; // move
foo1->method(); // compile-time error: foo1 invalid after move

In C++0x, a lot of containers and algorithms have been rewritten to use the explicit move instead of the assignment. It wouldn’t be a big deal to use := instead. Notice that the compiler would not allow the use of a regular assignment on unique pointers (unless they are rvalues), so the templates that are not ready for move semantics would refuse to get instantiated with unique template parameters.

Obviously, the move operator applied to a non-unique pointer must also work, otherwise we’d have to write separate templates for unique and non-unique template arguments.

We also have to use our special notation when passing unique arguments to functions, as in:

void f(unique * Foo);

unique * Foo foo = new unique Foo();
f(:= foo); // move
foo->method(); // compile-time error: foo invalid after move

When returning an lvalue unique pointer (for instance a member of a data structure), we use the notation return := foo;. The move operator may be elided when returning a local unique pointer, since the source ceases to exist upon the return (in general, move is implied when the source is a unique rvalue).

The biggest strength of the type-based approach is that the compiler can reliably prevent the aliasing of unique pointers. An assignment (as opposed to move) of an (lvalue) unique pointer to either unique or non-unique pointer is impossible. Taking the address of a unique pointer is forbidden too.

That leaves us with an interesting dilemma: How do you call a (library) function that takes a regular pointer if all you have at your disposal is a unique pointer? C++ unique_ptr let’s you do it through its method get. But we know how dangerous get is as far as aliasing goes.

If you don’t have the source code for the function you are calling, you probably shouldn’t be calling it with a unique pointer, because you have no idea what this function will do with it (store an alias in a global variable?). If you know the implementer of the function and he/she is willing to donate his/her kidney in case the function leaks aliases, you may risk casting away the uniqueness.

There is however a way for a function to guarantee that it’s alias-safe by declaring its parameters lent. The compiler will check the body of the function to make sure it doesn’t leak aliases to any part of the lent parameter, nor does it store non-unique (and possibly aliased) objects inside the lent object. Of course, the function can only pass the lent parameter (or any sub-part of it) to another function that makes the same guarantee.

It’s not obvious which should be the default: lent or it’s opposite, owned. If lent were the default, the compiler would be flagging a lot of valid single-threaded code (although it makes sense to assume that methods of a monitor object take lent parameters by default).

The relationship between unique and lent is very similar to that between immutable and const in D. If you declare data as unique or immutable you can safely pass it to a functions that declares its parameter as lent or const, respectively. lent guarantees that the parameter will not be aliased, const that it won’t be mutated.

Speaking of immutable–there’s always been a problem with constructing non-trivial immutable objects. The tricky part is that during construction we often need to explicitly modify the object, but we don’t want to leak non-const aliases to it or to its sub-parts. And now we have a new tool at hand to control aliasing–unique pointers. Instead of constructing an immutable object, you may construct a unique object, with all the guarantees about aliasing, and then move it to an immutable pointer. Just like this:

unique Foo * pFoo = new unique Foo();
immutable Foo * imFoo := pFoo;

(Of course, C++ doesn’t have immutable types either, but D does.)

By the way, you can always safely move a unique pointer to any of immutable, const, or regular pointers. Notice that it doesn’t mean that unique is a supertype of, for instance, immutable. You can’t pass unique where immutable is expected (you don’t want read-only aliases to escape to another thread!)–you can only move it.

A method that promises not to leak aliases to this is declared as lent. The compiler will detect any violations of this promise, as in:

class Foo {
    Bar * _bar;
public:
    Bar * get() lent {
        return _bar; // error: a lent method returning an alias
    }
};

In general, when you are dealing with a unique object, you may only call its lent methods.

Issues

Strict uniqueness imposes constraints on the internal structure of objects. Imagine creating a unique doubly-linked list. A link in such a list must be accessible from two places: from the previous link and from the next link. The scheme that absolutely prevents the creation of aliases to unique objects will not allow the creation of doubly-linked lists–and rightly so! Imagine moving a link out of the list: you’ll end up with a null pointer in the list, and a possible cross-thread aliasing if the (unique) link migrates to another thread.

There is a solution to this problem based on the ownership scheme (like the one used in Guava or GRFJ), which allows cross-aliasing of objects that share the same owner (e.g., all links are owned by the list). Such aliases cannot be leaked because the compiler won’t allow objects owned by a unique object to be moved. But that’s a topic for another blog post.

The use of iterators on unique containers is also highly restricted, but there are other ways of iterating that are inherently more thread-safe.

Conclusion

Any extension to the type system is usually met with some resistance from the user community. While some appreciate the added safety, others complain about added complexity. So it’s very important to be able to limit this complexity to specific areas.

When are unique and lent qualifiers really needed? In C++, at least in my experience, unique_ptr serves mostly as a poor man’s garbage collector. Since memory management permeates all C++ programs, the switch to using unique qualifiers would require a lot of changes even in single-threaded programs. In contrast, in garbage-collected languages, the main usefulness of unique is for multithreaded programming. A message queue that passes large unique objects between threads is more efficient than the one that deep-copies them. And unique objects never require locking.

When multithreading is involved, a safer type system doesn’t really add complexity. It translates the hard complexity of shared-memory concurrency into something that is more approachable by mere mortals.

As always, the introduction of new type modifiers may lead to code duplication (as in the case of const and non-const accessors). This problem can be dealt with using qualifier polymorphism–a topic for a whole new blog post.

I understand that this post might be hard to follow. That doesn’t mean that the uniqueness scheme is difficult to understand. My task was not only to explain the hows, but also the whys–and that requires giving a lot of background.

Bibliography

  1. Jonathan Aldrich, Valentin Kostadinov, Craig Chambers, Alias Annotations for Program Understanding. Describes unique and lent annotations in detail.
  2. See also my previous blog on Generic Race-Free Java.

Making the C language race-free is quite a challenge. I discussed one approach in my previous post. Here’s another one, based on lightweight annotations and whole-program analysis.

SharC is a sharing checker and program transformer for C. It is described in the paper SharC: Checking Data Sharing Strategies for Multithreaded C.

Sharing modes

The goal of SharC is to detect (and possibly eliminate) data races from legacy C programs. This is an incremental process in which the programmer annotates the program with type qualifiers, runs the checker, listens to its complaints, ads more annotations, etc., until SharC is totally satisfied and produces an instrumented version of the program with additional built-in runtime checks.

Some of the annotations that specify sharing modes are similar to those of Cyclone, but there are some new ones.

  • private: Thread-local
  • readonly: Does not change (immutable). Interestingly, it may be cast to another sharing mode that is writable.
  • locked(lock): Shared under specific lock. The lock must be readonly.
  • racy: Intentionally racy. No compile- or runtime checks.
  • dynamic: May change sharing mode at runtime, at which point it’s checked for readonly or single-thread access.

Note that SharC provides ways to move data between various sharing modes. The key to these operations is a very clever reference counting scheme built into the memory allocator. The paper provides the details of that scheme, but I’ll skip them here.

The overall policy of SharC is to consider almost all sharing (even under locks) illegal unless explicitly declared by the user.

Safe cast

Dynamic types can be cast between sharing modes. Here’s an example:

int readonly * y;
...
x = SCAST(int private *, y);

A pointer to a readonly int (which may be shared) is cast to a pointer to private (thread-only) int. Normally such cast would be unsafe. The int might be referenced by multiple readonly pointers (potentially shared between threads). The clients of those pointers don’t expect the value to ever change and may access it without locking. That’s why SCAST not only nulls the original pointer y, but also checks if the data reference count is zero (using the clever reference counting scheme I mentioned before). If it’s not, it reports an error.

Example

The paper offers a more elaborate example, which shows the use of dynamic data types and checked casting. The example is based on a pattern typical for multimedia processing and games.

A data buffer is processed in stages and passed from thread to thread.

We start with a linked list of stages. Each stage is run by a separate thread. The first stage is fed some data in a buffer (for instance a frame of a movie). The thread responsible for that stage starts its own processing. When it’s done, it hands the buffer over to the next stage, and so on. The buffer is like a car on an assembly line.

When the assembly line is created, each stage is assigned a different processing function through the function pointer fun (see code below).

You may also think of a stage as a one-element synchronous channel, with the buffer being the message.

What is important in this example is that we don’t want to copy a potentially very large buffer. We want to pass it between threads by reference without risking data races.

This is a stage structure with all the necessary SharC annotations.

typedef struct stage(q) {
    struct stage dynamic * q next;
    cond racy * q cv;
    mutex racy * readonly mut;
    char locked(mut) * locked(mut) sdata;
    void (*q fun)(char private * private fdata);
} stage_t;

Don’t be put off by the sheer number of annotations. Most of them are defaults or can be easily inferred by SharC.

This is what the programmer must annotate:

  • The buffer sdata is shared and protected by mut.
  • The function pointed to by fun takes a private (thread-local) buffer, fdata.

Notice that, without casting, fun cannot be called with sdata, because sdata is shared.

What SharC infers is that:

  • Structure stage is parametrized by some sharing policy, q (which stands for “qualifier”). This qualifier will be provided when the variable of type stage is defined. (This is called qualifier polymorphism.)
  • All pointers inside stage, except for mut and sdata inherit the qualifier q.
  • The field next, which is a pointer to the next stage, has two qualifiers. The pointer itself inherits the qualifier q from its parent. The data it points to is marked dynamic, which means that it will be checked during runtime to be either accessed by a single thread or immutable.
  • The pointers cv and fun also inherit the parent qualifier, q. Condition variable cv is declared racy to turn off compiler checks for sharing. cv is shared between threads but does not require locking.
  • The mutex object is also racy. The pointer to it though is readonly (immutable). This is an important detail, since it is unsafe to change the mutex during the lifetime of data it protects (which is sdata in this case).
  • sdata is a pointer to a char buffer. Both the pointer and the buffer it points to are protected by the mutex, mut.
  • Finally, the pointer fun inherits its qualifier from the parent. The function parameter, fdata, is a private pointer to a private buffer.

This is the beginning of the thread function, thrFunc:

void dynamic * private thrFunc(void dynamic * private d) {
    stage_t dynamic * private S = d;
    stage_t dynamic * private nextS = S->next;
    char private * private ldata;
    ...

The function takes and returns a private void pointer to dynamically shared data. In reality this pointer points to a stage structure–this is reflected in the definition of S. Notice that in C a void pointer can be converted to a typed pointer. In SharC, the compiler makes sure that the qualifiers match.

The next field of S inherits its qualifier private from S. The data it points to (the next stage) is dynamic, as per the definition of stage.

Finally there is a private pointer to a private buffer, which will be used to point to the shared buffer. Since in general private and shared don’t mix, a sharing cast will be performed in the body of thrFunc (see below).

Here’s the rest of thrFunc:

    ...
    while (notDone) {
        mutexLock(S->mut);
        while (S->sdata == NULL)
            condWait(S->cv,S->mut);
        ldata = SCAST(char private *, S->sdata);
        condSignal(S->cv);
        mutexUnlock(S->mut);
        S->fun(ldata);
        if (nextS) {
            mutexLock(nextS->mut);
            while (nextS->sdata)
                condWait(nextS->cv,nextS->mut);
            nextS->sdata =
                SCAST(char locked(nextS->mut) *, ldata);
            condSignal(nextS->cv);
            mutexUnlock(nextS->mut);
        }
    }
    return NULL;
}

The stage S that was passed to the thread function contains shared pointer sdata. To access this pointer we need to take the correct lock, S->mut. This is the lock that was specified in the declaration of sdata inside stage.

First we loop waiting for S->sdata to become non-null. Another thread is supposed to initialize that pointer. As long as the pointer is null, we block on the condition variable S->cv.

while (S->sdata == NULL)
    condWait(S->cv,S->mut);

Notice that condWait takes the mutex as its second argument. It has to unlock it while waiting for the signal, otherwise no other thread would have a chance to modify S->sdata (and we’d have a livelock). (In the channel analogy, we are performing a synchronous receive.)

Now we are ready to call the function S->fun to process the buffer. However, that function is declared to take a private buffer, not a shared buffer. It could, for instance, be a library function that has no provisions for sharing. It could be strlen or a Fast Fourier Transform.

The programmer knows that it is safe to call this function, because the buffer has been handed over between threads and shared access is no longer in the picture. What remains is to convince the compiler that that’s okay, and to add some code that does necessary checks at runtime. All this is done by SCAST.

The line

ldata = SCAST(char private *, S->sdata);

casts S->sdata to a pointer to a private (thread-local) buffer and stores it in the private variable ldata (local data). It also nulls the source and makes sure there are no more references to it (a very clever reference counting scheme, remember?). If this looks to you like move semantics, you get the right idea.

Still under lock, we signal the previous thread that the shared buffer has been nulled so it can re-fill it.

We are now ready to release the lock and do some local processing. We call the function S->fun with the (now private) buffer.

If there is a next stage (pointed to by S->next), we want to pass our processed buffer to it. Before we do that, we have to wait until the buffer in the next stage becomes null. (In the channel analogy, we are now doing a synchronous send.)

while (nextS->sdata)
    condWait(nextS->cv,nextS->mut);

We have to do it under the next stage lock.

We assign our current buffer to the next stage and signal the next thread. Here, again, we have to perform a cast: our buffer is private, and next->sdata is shared and locked under next->mut. The statement:

nextS->sdata = SCAST(char locked(nextS->mut) *, ldata);

casts ldata (local data) to a pointer to char locked(nextS->mut). This is exactly the opposite of what we did earlier (casting shared data to local data). As before, the runtime has to null the source and check if there are no other references to it. This way thread-local unique data may be moved to another thread. If you followed my previous posts, you notice the pattern: unique data, move semantics.

Conclusion

What is unique in SharC approach is the presence of dynamically checked casts that are used to change sharing modes at runtime. This is probably the best that can be done on top of C.

When designing a new language, we could use different mechanisms to achieve the same goals. For instance, the buffer could be declared unique. The move semantics would then guarantee the absence of dangerous aliasing thus eliminating the need for behind-the-scenes reference counting.

The problem of passing a unique object to an unsuspecting library function (without nulling the source) can be solved by declaring the function parameter as lent (which should be the default).

If you read this space on a semi-regular basis, you might have noticed that recently it turned into a series of “Cliff Notes for CS grad students.” That was because I tried to prepare myself for the task of designing a multithreading system and memory model for the D programming language. My future posts will (hopefully) track progress in that direction.


When I read Dan Grossman’s paper, Type-Safe Multithreading in Cyclone, I imagine Dan on a raft in the middle of a tropical cyclone, his threads soaked by the rain, frantically racing to build a shelter. Maybe a type system can’t protect you from the rain, but it sure can protect you from data races–even if the final product looks a little like a Rube Goldberg contraption.

Cyclone, as it turns out, is a safe dialect of C. Dan’s goal was to extended Cyclone’s type system to make it safe in a multithreaded environment. This is not an easy task in a language that uses pointers and manual memory management. The ideas are similar to those in the dialects of Java in my previous posts, but the type-theoretical concepts are pretty advanced.

-Locks

A Cyclone lock is a special type parameterized by name. Defining such entities requires a major type-system tour de force. Little known notions like “existential types,” “dependent types,” and “effect systems” come into play. The major point of all this magic is that you want to use lock names without knowing what they are.

You create a Cyclon lock using the following pseudo-syntax:

let lk<λ> = newlock();

I’ll use Greek letters for symbolic lock names (except for the special name, loc), since the author didn’t propose any concrete syntax and, admittedly, never finished the implementation.

What’s happening behind the scenes is that newlock returns an existential type, which is unpacked into variable lk of type lock_t<λ>. That variable may, for instance, be passed to a (generic) function taking lock_t<λ>.

The beauty of an existential type is that it won’t let the client “guess” the name of the lock. The name is totally opaque–there is not even a type for it. It can only be generated by the system in the call to newlock.

To synchronize a (possibly compound) statement, you precede it with sync(lk), where lk is a lock variable (or an expression that evaluates to such). Continuing the previous example, we may write:

sync(lk) ++*p;

which increments the value pointed to by p under the lock lk.

-Ownership

In an OO language, ownership is the key to a race-free type system. The owner of a given object has to be locked before the object may be accessed.

In a non-OO language, like Cyclone, instead of specifying the owner of data, you specify the lock that protects it. Since you might not have access to the lock variable when you are declaring data, the symbolic lock name is used instead.

Also, since all references in Cyclon are expressed through pointers, lock annotations are associated with pointers. (This is again parallel to annotating object references with their owner objects.)

We can now complete the example above with the annotated definition of p:

int *λ p = new 0;

The pointer p can only be access when the lock whose name is λ is held.

-Local and Shared data

In Cyclon, thread-local data appear as a special case of shared data. A special lock name loc and a (global) variable nonlock are used to turn off the locking of individual instances. (Compare this to the dummy owner thisThread in the OO approach.)

Lock names are also used to parameterize functions and structs. In that case it might be necessary to be able to encode the “sharability” of the type. If the lock type has the kind LS, it actually protects Shared data. The kind LU, on the other hand, may be Unsharable, i.e., it could be instantiated with the thread-local loc. LS is a sub-kind of LU.

The main purpose of “kinding” is to ensure that thread-local data can never be shared between threads.

-Example

All this sounds very dry without an actual (however contrived) example. Let’s start with a simple function inc:

void inc<λ:LU>(int *λ p; {λ}) 
{
    *p = *p + 1;
}

The function is parameterized by a lock name parameter λ of the LU kind. It means that it can be instantiated both in the sharing and thread-local context. Lock-name variable λ first appears in the declaration of the pointer parameter p. Data pointed to by p is protected by the lock named λ. That’s not telling a lot–every pointer in Cyclon is protected by some lock (or nonlock).

What makes the difference is that the same name λ appears in the effects part of the declaration. The runtime system keeps track of what locks are being held at any point in the program, and passes this information to every function. Here, {λ} is an effect that contains one lock name, λ. In other words, the lock that protects p must be taken before calling inc. (Of course, other locks might be held too.)

Here’s an example of how inc may be called from another function, inc2.

void inc2<λ:LU>(lock_t<λ> plk, int *λ p ;{}) 
{
    sync(plk) inc(p);
}

The effects part of the declaration of inc2 is empty. No locks need be held before calling it. But when inc is called, the current effects include the name of the lock specified in the declaration of plk (the sync section adds λ to the effects). Since the same lock name appears in the declaration of p, the precondition for calling inc is fulfilled.

A struct containing a pointer must also be an existential type. The actual value of λ is assigned to LkInt when the type is “packed” (created from its constituents).

struct LkInt 
{<λ:LS> 
    lock_t<λ> plk;
    int*λ p; 
};

Here, LkInt (locked integer) only makes sense in a sharing context, so λ is of the strictly sharing kind, LS. That allows LkInts to be passed between threads.

Here’s an example of using a pointer to LkInt:

void g<λ:LU>(struct LkInt *λ s ;{λ}) 
{
    let LkInt{<λ'> .plk=lk, .p=ptr} = *s;
    inc2(lk, ptr);
}

Function g is parameterized by some lock name of the LU kind (so it may be loc). This lock is used by the callee to lock the LkInt argument s (λ is present in the callee effects).

Now s itself contains a pointer and a lock (of the LS kind). We get at them by unpacking an existential type–splitting it into constituents and giving them new names, lk and ptr. The name of lk is λ’. A shallow copy of s is performed in the process. We can now call inc2, which doesn’t require any effects, and uses lk to lock and increment ptr.

Finally, all these things come together in the example below:

void f(;{}) {
    let lk<λ> = newlock();
    int *λ p1 = new 0;
    int *loc p2 = new 0;
    struct LkInt *loc s = new LkInt{.plk=lk, .p=p1};
    spawn(g, s, sizeof(struct LkInt));
    inc2(lk, p1);
    inc2(nonlock, p2);
}

Here’s the play-by-play:

  • Function f requires no effects.
  • The programmer creates a lock lk with the name λ (unpacks an existential type returned by newlock).
  • She creates a pointer p1 to an integer protected by the lock named λ.
  • Then she creates an unprotected thread-local pointer p2 (using dummy lock name, loc)
  • She combines the lock lk and the pointer p1 into a struct LkInt. This is an example of “packing” an existential type. Note that both components must share the same lock name. (The pointer to LkInt, s, is thread-local–lock name: loc.)
  • The programmer spawns a thread that executes the function g with the argument s. The argument is passed by a shallow copy, but deep contents (the lock and the pointer) are shared. In fact they must be shared with the kinding LS; otherwise spawn would not compile. This mechanism protects any thread-local data from being shared with a new thread.
  • While the call to g(s) executes in parallel, the programmer increments p1 under the lock lk. Notice that these are the same variables that the other thread operates on. The shared lock enforces mutual exclusion.
  • The increment of thread-local p2 requires no lock, that’s why dummy nonlock is used.

-Limitations

The biggest limitation of the Cyclon system is that it’s static. The association between data and locks is rigid. That makes several useful idioms impossible to implement. There is no way to “move” data between threads. You can either pass a pointer together with its lock (essentially creating a monitor), or pass data by value.

The other serious problem is the overall complexity of the system–especially the “effects” part. When effects have to be included and manipulated in generic code things get a little hairy.

Granted, a lot of annotations can be elided–the defaults “do the right thing” in most cases. Still, what remains is asking a lot from an average programmer.

-Conclusion

I would like to thank Dan Grossman for correcting some of my mistakes and explaining a few subtle points.

In my next installment I’ll describe a more recent race-free extension of C, SharC, which supports a mix of static and dynamic checking.


A type system that prevents data races must not eliminate useful concurrency patterns or force the programmer to maintain multiple copies of almost identical data structures.

In my previous post about Guava, a dialect of Java, I talked about a type system that enforces the separation of thread-local and shared objects at the class level. Unfortunately, such rigid system forces the programmer (especially a library writer) to provide dual implementations of many generic classes like vectors, queues, etc. Often the only difference between implementations is the use of synchronized (or, in case of Guava, the special base class called Monitor).

To solve this problem, Boyapati and Rinard proposed a system where the same generic class may be used in different sharing contexts. For instance, the same parameterized vector class, may be used to instantiate a thread-local instance that requires no locking, as well as a shared instance that has a built-in lock.

The paper precedes Generic Java, but employs similar notation. For instance, it lets you define a generic vector class like this:

  class vector<thisOwner> { ... }

and then instantiate it as thread-local (no locking requirements):

  vector<thisThread> localV= new vector<thisThread>;

or as a shared monitor:

  vector<self> sharedV= new vector<self>;

The first template parameter is always interpreted as “the owner” (more about it later). Objects owned by thisThread are thread-local, objects owned by self are monitors.

Even though the notation used in GRFJ (the acronym the authors use for their Java dialect) is different from that of Guava, there are many similarities in the two approaches, since both have to deal with similar issues: explicit sharing, ownership, passing objects between threads, etc.

-Explicit sharing

You might remember that, in Guava, only those classes that inherit from Monitor may be shared. In GRFJ, sharing is defined at the instance level (the instantiation of a template). Every instance declaration must specify the owner of the object. If the owner is not thisThread, the object may be shared between threads. The equivalent of the Guava Monitor is a self-owned object–its owner is declared as self.

-Ownership

Ownership plays an essential role in preventing data races. Every object has an owner. In GRFJ there are three basic types of owners:

  1. thisThread–the object owned by thisThread is never shared.
  2. self–the object is the root of an ownership tree.
  3. Another object–the sharing is defined by the root of the ownership tree

Types of ownership translate naturally into protection patterns. If the owner is thisThread there is no need for locking. If the owner is self, all methods must be synchronized by the object’s lock. In the third case, the object’s owner is responsible for locking. More precisely, the root of the ownership tree to which the object belongs has to be locked, if it’s not declared thread-local.

There are some interesting combinations of ownership. For instance, you can declare a thread-local vector that stores self-owned (shared) items. Or you can declare a shared Stack that contains (owns) a Vector object. All access to Vector will be protected by the Stack’s lock.

For this level of expressiveness, we need classes that are parameterized by owners. Notice that, if the owner of the object x is another object, that object must exist when the declaration of x is reached.

A template might be parameterized by multiple owners. The first one on the list is always the owner of this. In the example below, Stack is parameterized by two owners–the first owns the Stack, the second owns the Values. Note that, in this case, all Values will always share the same owner.

class Stack<thisOwner, valueOwner> {
    Node<thisOwner, valueOwner> head = null;

    void push(Value<valueOwner> value) requires (this) {
        Node<thisOwner, valueOwner> newNode = 
            new Node<thisOwner, valueOwner>;
        newNode.init(value, head);
        head = newNode;
    }
    Value<valueOwner> pop() requires (this) {
        if (head == null) return null;
        Value<valueOwner> value = head.value();
        head = head.next();
        return value;
    }
}

The requires clause specifies whose lock must be held when calling a particular method. In this case, the lock on this must be held. But if this is owned by another object, the locking responsibility automatically moves up a level, until it reaches the ownership root.

Here’s the definition of Node:

class Node<thisOwner, valueOwner> {
    Value<valueOwner> value;
    Node<thisOwner, valueOwner> next;

    void init(Value<valueOwner> v, Node<thisOwner, valueOwner> n)
        requires (this) {
        this.value = v;
        this.next = n;
    }
    Value<valueOwner> value() requires (this) {
        return value;
    }
    Node<thisOwner, valueOwner> next() requires (this) {
       return next;
    }
}

And the definition of Value:

class Value<thisOwner> { int x = 0; }

Using the declarations above we are now ready to declare different values and stacks:

Value<thisThread> v1 = new Value<thisThread>;
Value<self> v2 = new Value<self>;

We have created two values from the same template–v1 is thread-local, v2 is a monitor (access to x is protected by its lock).

Stack<thisThread, thisThread> s1 = new Stack<thisThread, thisThread>;
Stack<thisThread, self> s2 =  new Stack<thisThread, self>;
Stack<self, self> s3 = new Stack<self, self>;

Stack s1 is thread-local and can store only thread-local values. No locks or locking code will be created by the compiler. Stack s2 is also thread-local, but it stores shareable values. A thread-local stack will never be visible from other threads. But self-owned values it stores might be accessed from multiple threads. Finally, s3 is a shared stack containing shared values. Both, the stack s3 and the values it stores have their own independent locks.

s1.push(v1);
s2.push(v2);

We may push a thread-local value v1 on the stack s1, but if we tried to push v2 on s1, the compiler would consider it an error. Pushing v2 on s2, on the other hand, is okay.

Since GRFJ is based on Concurrent Java, the locking and threading look a little odd. To illustrate the sharing of s3, we fork a thread, passing it s3 and v2 (both are sharing-ready) and executing the code s3.push(v2) under the lock of s3.

fork (s3,v2) {synchronized (s3) in {s3.push(v2);}}

Notice that, according to the declaration of s3, it would be an error to push v1 onto it. Indeed, that could result in illegal sharing of a thread-local object. The type system protects us from a hard-to-detect error.

This is hardly a free lunch, though. Annotating every class and every variable might be just too much for a programmer. Fortunately, most owners can be inferred by the compiler by analyzing assignments. Because of that, single threaded programs in GRFJ require virtually no annotations.

-Foreign owners

In most cases, ownership tree follows the containment tree. The owner contains the ownee. Although desirable from the architectural point of view, this arrangement is not strictly necessary. An object might declare another separate object as its owner. This is safe under one condition–the owner object may not be overwritten. Hence the requirement that the owner be final. Here’s the relevant example:

final Foo<self> owner = new Foo<self>;
Bar<owner> ownee = new Bar<owner>;

This becomes important when building new locking protocols from pre-existing parts.

-Object migration

The passing of objects between threads requires either deep copying (like Guava’s Values), or move semantics. In GRFJ, move semantics is implemented by specifying another special type of owner–unique. Unique objects cannot be copied, they have to be moved. The “move” operator is the postfix decrement, just like in Guava. It moves the reference and nulls the source.

Value<unique> v3 = new Value<unique>
Value<unique> v4 = v3--;

Our Stack class is not prepared to store unique objects. This prohibition may be included in its definition (compare it with C++ “concepts”):

class Stack<thisOwner, valueOwner> where (valueOwner != unique)

Conversely, we might want to redefine Stack to store unique objects. A few code changes would be necessary though. For instance, in push, the value must be moved:

newNode.init(value--, head);

In pop, the return value has to be moved:

return value--;

The class Node requires similar changes.

The authors note that, despite appearances, the moving of objects is multiprocessor safe. Even though the assignment to a new reference is not guaranteed to be immediately visible to other threads, a unique object is always published to another thread via a monitor (for instance, a shared stack). The new thread can only get hold of the object by first acquiring the monitor’s lock, which forces previous stores to commit.

-Alias control

Move semantics requires control over aliasing–a moved object may not leave any aliases, nor may it carry along any references to thread-local objects. GRFJ provides additional annotations to mark non-escaping method parameters. The syntax is !e appended to the parameter type. Here’s an example:

void display(Value<unique>!e val);
Value<unique> v5 = new Value<unique>;
display(v5);

A unique object here is passed by reference only because display guarantees that its argument won’t escape.

-Immutable objects

Immutable objects may be passed between threads by reference. In GRFJ, immutable objects are marked by another special owner type, readonly. Interestingly, the problem of the construction of immutable objects is cleverly avoided. You first create a unique object and then move it to a readonly reference.

Value<unique> v6 = new Value<unique>;
v6.x = 1;
Value<readonly> v7 = v6--;

This is a perfectly safe operation, since there is a guarantee that no writable aliases to the unique object may stay behind. The move to readonly freezes the object forever.

Immutable objects can only be passed to methods that promise not to modify their arguments. This is done by appending !w to the type of the parameter. The two suffixes may be combined to form !ew (I am not kidding you!), a parameter that doesn’t escape and is not modified by the method.

-Limitations

– Some concurrent programs use multi-stage access patterns that are not expressible in GRFJ. For instance, a shared array is divided into disjoint sections and each thread operates exclusively on its section without any locking. After all threads synchronize on a barrier, they pick up different sections and continue. The ownership of sections changes with time. (In D this pattern might be implementable using array slices.)

– Dynamic downcasting, which used to be the workhorse of Java before generics, can’t verify the ownership part of the cast, because this information is not available at runtime.

– Static variables may be accessed only when the client holds the class lock. Each class with static variables must therefore have a static lock.

– The authors mention the idea of parameterizing methods that accept poly-owned arguments. This is not so easy as it sounds, since virtual functions cannot be parameterized by a potentially infinite set of types. My guess is that this is possible because detailed ownership information is only needed during type checking. Still, the compiler might have to produce additional implementations of a method depending on whether the parameter is thread-local or not (imagine the parameterized method creating a local variable of the same ownership type–sometimes this variable must contain a lock, sometimes not). Still, this is a finite set of possibilities, so vtable slots may be preallocated for all of them.

– The template syntax for ownership won’t work in languages where templates already accept value parameters, and the compiler isn’t always able to distinguish between types and values.


Can a good type system prevent concurrency errors? Or is this a quest for the Holy Grail?

There are two parts to this question, corresponding to two major types of concurrency errors:

  1. Preventing data races
  2. Preventing deadlocks

I’ll start with the first one.

Data races occur only when memory is shared between threads. Disallow sharing and data races are gone! In fact there is a name for threads that don’t share memory: processes. It’s perfectly feasible to have a concurrent language that disallows sharing–Erlang is one (see my post about Erlang). The trick is to always pass data between threads by value. This is especially easy in functional languages.

Non-functional languages like C++, Java, or D (I was told by Walter Bright, the creator of D, to always use the full name, “the D programming language,” so that search engines can index it properly) tend to share data almost by default (see, however, this post).

In Java, all non-primitive types have reference semantics. When you pass a Java object between threads, you’re only passing a handle; the object behind it becomes accessible from both threads.

C++ at least has means to express passing by value and move semantics for user-defined types. Still, it’s up to the programmer to use them.

Who ordered Guava?

For every type-system idea there is one or more dialects of Java that implement it. I’ll start with an older attempt at data-race free Java called Guava, as it illustrates some of the basic premises.

-Explicit sharing

The most important step–if we don’t want to completely ban the sharing of data–is to regulate it. Let the programmer explicitly mark the data destined for sharing as such. The corollary is that the data that is not marked for sharing cannot be shared. This can be accomplished, for instance, by making all objects thread-local by default, or by using type modifiers that prevent references to such objects from escaping.

In Guava, the data type designed for sharing is called a Monitor. As the name suggests, all access to a Monitor is automatically synchronized by the Monitor’s lock. This, incidentally, eliminates the need for the synchronized keyword, which is absent from Guava.

The non-shared data types are either Objects or Values.

Objects are just like regular Java Objects, except that they don’t have a built-in lock, since they can never be shared between threads.

Values are either primitive values, like integers, or user-defined types with value semantics.

Monitors, Objects, and Values are collectively called instances.

-Value semantics

When you pass a Value, the compiler will make a deep copy of it (well, sort of–the monitors embedded in a Value are not deep copied). Since deep copying might be expensive, Guava defines operator “move”, which nulls the source. The syntax is:

  v2 = v1--;

The value v1 becomes null after the move to v2. This is similar to C++ unique_ptr and std::move.

-Ownership

The biggest problem in lock based concurrency is to make sure that the correct lock(s) are taken when accessing shared data. In Guava, all Monitor’s data are protected by that Monitor’s lock. As long as they stay inside that Monitor, nothing bad can happen to them from the point of concurrency.

Values stored inside a Monitor are never accessible outside of the Monitor–only their copies may be passed out.

The same is not true about Objects. Since Objects have reference semantics, there is a real danger that Objects’ references might escape the Monitor that protects them. Imagine a situation where two Monitors have references to the same Object. It is possible then that two threads may operate on that Object at the same time–one entering through one Monitor, the other through the other Monitor. We have a data race!

Therefore it is important that every Object have an owner at all times. The Object’s owner is either a Value or a Monitor. (The exception is a fresh Object that’s been just allocated–it has no owner until it is assigned to a variable.) Since an Object may only be owned by at most one Monitor, it is that Monitor that protects it from simultaneous (racy) access.

-Regions

All Objects that are owned by a particular Monitor or Value form a region. Equivalently, assigning a monitored region to an object specifies what lock must be held when accessing it.

All instances may contain (references to) monitors, but monitors are not “owned” by anybody. References to the same monitor may appear in multiple regions and may be freely passed around. It is thus up to programmers to define an ordering scheme for their monitors in order to avoid deadlocks.

How can we protect Objects from moving between regions and acquiring multiple owners? We need a way to control aliasing.

Here are some Guava rules for passing Objects. A method may declare its Object parameter as either kept or lent. (By default, parameters to Object methods are kept and to Monitor methods are lent.) If the parameter is kept it must belong to the same region as this, and there are no limitations on its use. If, however, the parameter is lent, the method may not store a reference to it in this, nor may it store this inside a lent Object. No cross-aliasing is allowed.

A method may also be marked new if it returns a freshly created object, which has no owner yet. Constructors are considered new unless they accept kept parameters.

Notice that you may have multiple references to the same Object, but they will all be within the same region. The only instances that may be passed between threads are Monitors and Values.

-Constructors

Guava final fields may either be initialized inside a constructor or in a private method that is only called from inside a constructor. (BTW, in D a private method is not private within a module, so the compiler would have to analyze the whole module to establish the latter condition.) [Note to self: The same scheme might be useful in the construction of immutable objects in D.]

Partially constructed Objects must not be visible outside constructors. The compiler must verify that constructors don’t pass this to other methods, and don’t store this inside other instances (no alias cross-contamination).

-Optimizations

Copying Values around may be expensive. I already mentioned one optimization, the use of the “move” operator. The other optimization is related to immutability. If a Value is immutable, it may be safely passed by reference. Guava defines immutable classes as ones that have no update methods. Any method that may modify this must be marked update. The update notation is also extended to method parameters–by default parameters are immutable.

There is a bonus advantage to separating update methods from the rest. In a Monitor, a non-update method may safely use a readers’ lock, which allows multiple readers to access data simultaneously, to increase concurrency.

-Global and local methods

A method is considered local if its effects cannot be observed or influenced by other threads. All Object and Value methods are by default local. A local method is immune to races thus allowing single-thread optimizations.

Conversely, all Monitor methods are considered global, since operations on Monitors may be visible or influenced by other threads.

These defaults may be overridden. For instance, an Object may contain a reference to a Monitor. The methods that call this Monitor’s methods must be marked global. Moreover, Object or Value methods that access Monitors that are passed to them as arguments must also be marked global. So touching a Monitor (which is equivalent to using its lock) taints the whole callers’ tree with the global annotation.

This is similar to the way update taints the callers tree, except the update annotation of a method only pertains to this, not to its arguments. However, when global and update are combined, they have the same tainting power as global. In particular, a method that invokes a global update method on its argument becomes tainted with global update.

Methods that are global update cannot be invoked from non-update methods, even if they only global-update their arguments.

Note: This part of the paper is not very clear to me. The authors never explain the importance of global update methods (other than optimization opportunities).

-Limitations

Guava implements a relatively simple and somewhat limited system to eliminate races. It punts the problem of ownership-passing and lock-free programming. Even with those limitations the Guava type system is not simple.

The idea that safe multithreading may be achieved with a few simple modification to the type system seems to be untenable. However, as long as special type annotations are limited to the code that does actual multithreading, I think they’re worth the added complexity.


Strong typing–you either love it or hate it! Elaborate type systems catch a lot of programming errors at compile time. On the other hand they impose the burden of type annotation on the programmer, and they sometimes disallow valid programs or force type casting.

In Java there’s been a never-ending discussion about the lack of support for const types. People coming from the C++ background see it as a major flaw. Others would defend Java from constness with their own bodies.

I’m always on the lookout for solutions that let programmers have a cake and eat it too. Pluggable types are just the thing. You want const enforcement? Add a constness plug to your compiler. You want compile time null reference checks? Add another plug.

How is it possible?

Java annotations as type modifiers

Did you know that Java had a system of user-defined annotations (C# has a similar thing)? Annotations start with the @ sign and can be used, for instance, to annotate classes or variables. The Java compiler doesn’t do much with them other then embed them as metadata in class files. They can be retrieved at runtime as part of the reflection mechanism.

I never thought of annotations as more than an ad hoc curiosity until I read Matthew Papi’s Ph.D. thesis, Practical pluggable types for Java. The paper proposes the use annotations to extend the Java type system. This work contributed to the JSR 308 proposal, which allows annotations to appear anywhere types are used. For instance, you could annotate a declaration of an object with the @NonNull qualifier:

@NonNull Object nnObj;

or declare a read-only list of read-only elements:

class UnmodifiableList<T>
  implements @ReadOnly List<@ReadOnly T>
{ ... }

What distinguishes such annotations from bona fide comments is that they can be type checked by user-defined checkers. These checkers can be plugged into the compiler and run during compilation. They get access to abstract syntax trees (ASTs) produced by the language parser, so they can also do semantic checks (e.g., detect method calls through a potentially null pointer).

Examples of type system extensions

A simple NonNull checker detects assignments of potentially null objects to non-null objects, as in:

Object obj;
@NonNull Object nnObj = obj; // warning!

The checker must know that the default qualifier is @Nullable (potentially null) and @NonNull is a “subtype” of @Nullable (strinctly speaking, @NonNull T is a subtype of @Nullable T). In fact, simple type annotations of the @Nullable variety may be defined within the program and type-checked by the generic Basic Type Checker provided as part of the type checker framework. For instance, the subtyping relationship may expressed declaratively as:

@TypeQualifier
    @SubtypeOf( { Nullable.class } )
    public @interface NonNull { }

However, a specialized checker can do more than just check type correctness. The NonNull checker, for instance, issues a warning every time the program tries to dereference a @Nullable object (remember that @Nullable is the default implicit annotation).

An even more useful checker enforces immutability constraints (the generalization of const types). The IGJ checker (Immutability Generic Java) introduces, among others, the following annotations:

  • @Mutable: The default. Allows the object to be modified.
  • @ReadOnly: An object cannot be modified through this reference. This is analogous to C++ const reference.
  • @Immutable: An object may not be modified through any reference (not only the current one). Java Strings are immutable.

Incidentally, similar immutability constraints are built into the type system of the D programming language, except that D’s const and immutable (formerly known as invariant) are transitive.

Try it!

Suppose you are a fan of immutability constraints and you want to try them right now. First, download the JSR 308 compiler and checkers from the pluggable types web site. To compile your annotated program, use the command line:

javac -processor checkers.IGJ.IGJChecker <source-files>

If your program doesn’t obey immutability constraints specified in your source code, you’ll see a bunch of warnings and errors.

Now for the annotations. You might want to do them bottom up:

  • Annotate methods that don’t modify this:
    void foo() @ReadOnly;

    These methods may only call other @ReadOnly methods of the same object (the checker will tell you if you break this rule).

  • Annotate arguments that are not modified by a method, e.g.,
    void foo(@ReadOnly Bar bar);
  • Annotate objects that never change after creation:
    @Immutable Bar bar = new @Immutable Bar();

And so on…

You can pass @Immutable as well as @Mutable objects to methods that take @ReadOnly arguments, but not the other way around.

Of course, any attempt to modify a @ReadOnly or @Immutable object will be flagged as error by the checker.

Nullness checker

The nullness checker protects your program from dereferencing uninitialized objects. For instance, you can only call a method or access a property of an object that is typed as @NonNull.

Since the implicit default annotation is @Nullable, the following code will be flagged as an error:

Bar bar;
bar.toString();

There are some interesting issues related to nullness. For instance, during object construction, this cannot be considered @NonNull. Consequently you cannot call regular methods from an object’s constructor. To remedy this situation without compromising the type system, a special annotation @Raw was added. Inside the constructor, this (and all @NonNull subobjects under construction) are considered @Raw. So if you want to call an object’s method from inside its constructor, such method must be annotated @Raw.

Polymorphism

It’s possible to overload functions based on their nullness annotation. For instance, if you know that a function’s argument is @NonNull, you might want to skip a null test:

String stringize(Bar bar)
{
   if (bar != null)
      return bar.toString();
   else
      return "";
}

// Specialized version
String stringize(@NonNull Bar bar)
{
   return bar.toString();
}

Interestingly, since the compiler does flow analysis, it knows that inside the if statement bar is not null, even though it’s (implicitly) declared as @Nullable, so it won’t flag it as an error. (This is called flow-dependent typing–I implemented something like that in my Dr. Dobb’s article using local variable shadowing.)

Let’s try something more challenging–declaring the identity function, a function that simply returns its argument. The naive declaration

T identity(T x);

has a problem when nullability annotations are in force. Since the default annotation is @Nullable, the above is equivalent to

@Nullable T identity(@Nullable T x);

When called with a @NonNull argument, this function will return a @Nullable result. That’s not good! You can ameliorate this situation by declaring a separate overload:

@NonNull T identity(@NonNull T x);

The problem is that, when you keep adding new kinds of type annotations to your system, the number of overloads of identity starts growing exponentially.

Enter polymorphic annotation @PolyNull. The identity function can pass the nullness annotation through, if you declare it as follows:

@PolyNull T identity(@PolyNull T x);

Amazingly enough, @PolyNull will also work with multiple arguments. Consider the max function:

@PolyNull T max(@PolyNull T x, @PolyNull T y);

Through the magic of type unification, this declaration does the right thing. The nullability annotations of both arguments are unified to the lowest common denominator–the most derived annotation in the subtyping hierarchy to which both types can be implicitly converted. So, if both arguments are @NonNull, their unification is @NonNull, and the result is @NonNull. But if even one of the arguments is @Nullable, then the result is @Nullable. Notice that this declaration covers four possible overloads:

@NonNull T max(@NonNull T x, @NonNull T y);
@NullableT max(@NonNull T x, @NullableT y);
@NullableT max(@NullableT x, @NonNull T y);
@Nullable T max(@NullableT x, @NullableT y);

For non-static methods, the annotation of this may also take part in the unification:

@PolyNull T foo(@PolyNull T x) @PolyNull;

Shortcomings

One of the limitation of user-defined type annotations is that they can’t take part in program optimization. That’s because the type checker is not allowed to modify the AST. (See Walter Bright’s blog in Dr. Dobbs about optimization opportunities based on immutability in the D programming language.)

Acknowledgments

Michael Ernst, who was Matthew Papi’s doctoral adviser, clarified some of the issues for me. Since I’m attending his seminar, I’ll be blogging more about his work.

« Previous Page