notes-computer-programming-typecheckedRaceFreeMultithreadingViaOwners

some notes on http://bartoszmilewski.wordpress.com/2009/05/26/race-free-multithreading/ and http://bartoszmilewski.wordpress.com/2009/06/02/race-free-multithreading-ownership/

i changed the description of the system somewhat, but i'm hoping the "spirit" is the same.

Goal

The goal is to prevent races, which the Milewski defines as "access to mutable shared variables without locking".

In other words, the goal is to for the compiler to be able to prove that it is never the case that following sort of thing can happen (except when the programmer "opts-out" of these safety checks):

Thread A and B both have a reference to object X. X has three fields: X.a, X.b, and X.sum. An invariant is supposed to be that X.sum = X.a + X.b. At time t=0, X.a = 2, X.b = 3, X.sum = 5. At time t=1 thread A reads X.a. At time t=2 thread B writes 3 to X.a. At time t=3 thread B writes 6 to X.sum. At time t=4 thread A reads X.b. At time t=5 thread A reads X.sum. Thread A has observed X.a = 2, X.b = 3, X.sum = 5 -- so from A's point of view, the invariant does not hold.

Note: actually, it isn't a problem if two different threads only READ from a mutable shared variable at the same time; so I propose the following definition of race: "when it is possible for one thread to read from an object at the same time that another thread is in the process of changing it".

Introduction to the method

There are three basic ways used in this technique to prevent races. First, the compiler can make sure that some objects are not shared between threads. Second, the compiler can use locking to ensure that objects are not read by any thread while another thread is working on them. Third, the compiler can ensure that there is never more than one "writable" reference to an instance of an object outstanding (that is, a reference to the object that allows the holder to access and change the underlying object) -- this can be ensured if data which is passed in sharing can never be mutated by the sender afterwards.

Different objects may have their "race-safety" assured in different ways. Therefore, we attach some additional type information to the type of each object. These "race-safety" annotations can be per-instance and are orthogonal to the rest of the object's type; for example, an object of type T can be either of type T and not shared between threads or it could be of type T and use locking; the program writer does not have to create two definitions of the type T to encompass these two cases (although the compiler may create two implementations of type T behind the scenes).

The race-safety annotations can be thought of as a kind of polymorphism; just as a given container can be declared to be a container of integers or a container of strings, it can also be declared as not sharable between threads, or sharable with locking.

Aside: is this method comprehensive?

Are there other ways to prevent races that this technique doesn't use? Sure. For example, if there are only two threads, and each thread never takes more than 9 milliseconds to access an object, then thread 1 could only access the data at times t=10-19, 30-39, 50-59, etc, and thread 2 could could have the other times.

Is that a flaw? No. In general, i think the question of whether a program is race-safe is undecidable; proof: write a program A that interprets a program B, and spawns two threads with a race if and only if B halts.

A more interesting demonstration of the intractability of checking race-safety is this: a group of threads is each equipped with a thread ID and a function f(state, id), where state represents the state of shared memory. Assume that f can be computed atomically (you can also assume that is a polynomial time-bounded total function). Now, each of the threads is allowed to each access some shared memory range only when f(state, id) is 1 (f is a generalization of a lock). This situation is race-safe if and only if, for each possible state, f(id, state) is nonzero for at most one id in the group. This can be expressed as a condition on f'(state), the curried version of f which maps inputs of type 'state' to an output which is a function from id to {0,1}. The task of checking, at compile time, if f' satisfies this property is NP-complete, because you are asking if there is any state such that f' has a certain sort of output on that state, and f' is unconstrained.

So, it is too much to ask that ANY method includes ALL the ways that programs may be guaranteed to be thread-safe; the most we can hope for is that a method like this one include SOME of those ways.

Every object either is lock-requiring, or is lock exempt

every object is either "lock exempt" (we'll just call this EXEMPT here), or is "lock-requiring". By default, an object is exempt with the THREAD exemption. This can be changed by adding race-safety annotations to the object's type (possibly on a per-instance basis).

whether or not each variable X is EXEMPT is fixed at compile-time.

Lock exemptions

There are five classes of exemptions:

The compile checks that exemptions are valid.

Here is what the exemptions mean:

THREADLOCAL means that the object cannot be shared between threads, and so no locking needs to be done. A reference to a THREADLOCAL object cannot be contained within a non-THREADLOCAL object.

UNIQUE means the object is guaranteed to have only one alias (that is, it can't have any references pointing to it; it can be "moved" by passing by reference, but this reference can't be copied; the variable that held the ref before the move is set to null after the move); it can be passed from thread to thread and doesn't need to be locked (because it can only be transferred, never "shared"). A reference to a UNIQUE object cannot be contained within a non-UNIQUE, non-THREADLOCAL object.

IMMUTABLE is an object that can't be changed once created -- they can be shared between threads (after creation) and don't need to be locked. A reference to an IMMUTABLE object can be contained within any object (provided the type of the underlying object is still marked as IMMUTABLE).

DEEPCOPY is an object which is always deep copied. It can be passed from thread to thread because, since such "passing" is actually deep copying, it is never the case that two threads have a reference to the same object. Referentially transparent value types are DEEPCOPY. A DEEPCOPY object can be contained within any other object, but references to it cannot be shallow copied.

LENDABLE is like DEEPCOPY except that shallow references to it are permitted, but they cannot be shared between threads.

LOCKFREE means that the programmer wants to opt-out of the system for this variable, and manage things hirself (there is still some sort of restriction on the interaction between lockfree things and non-lockfree things, but i don't understand what it is -- at least part of it is that it implies Java 'volatile', i.e. accesses are sequentially consistent. update: mb this is the restriction: "lockfree method (public or private) is not synchronized but its access to this is severely restricted. It can only operate on lockfree data members (if any), unless it takes the object’s lock or calls a synchronized method (all public methods of a shared object are, by default, synchronized)." -- http://bartoszmilewski.wordpress.com/2009/07/07/whats-wrong-with-the-thread-object/).

by default, the children of a LOCKFREE object are monitors (objects which are their own lockers, see below). There is also a type of thing called a "lockfree struct" is provided; unlike a lockfree object, children of a lockfree struct are by default lockfree.

Locking

Recall that every object which is not lock-exempt is lock-requiring. Every lock-requiring object has a "locker". A "locker" is an object L with an associated lock, such that L's lock must be held while accessing X. Every object which is the locker for any other object must also be its own locker.

For objects with lockers, the compiler transparently adds code to do the locking to object accesses, i.e. when a method is entered within an object with a locker, the caller acquires the lock; when a field is accessed on an object with a locker, the accessor acquires the lock.

an object which is its own locker is called a "monitor".

for each lock-requiring object, who the locker is is fixed at compile time.

by default, the locker of an embedded object (i.e. an object in a field in another object) is the same as the locker of the parent object. Thus, by default the containment relation between objects forms a tree, the root of which is a monitor which is the locker for all of the other nodes in the tree.

a global reference to a lock-requiring object is bound to one instance at compile time, like Java's 'final'. this is because, although the underlying object is protected by a lock, the reference itself is not, so there may be a problem if the reference is being changed by one thread while another one is reading it.

Sequential consistency

In many languages, out-of-order execution is possible if memory fences (sequential consistency commands) are not used. To protect against this, all data members in non-threadlocal objects are made sequentially consistent (as if they were declared with Java's 'volatile'), and all data members accessed by any non-threadlocal object (these might only be made sequentially consistent for the accesses by that object).