of exposition, we initially do not distinguish between read and write accesses.

The Goldilocks algorithm processes the actions in Act
one at a time, as a sequence. Before a thread t performs an
action a in Act, t notifies the Goldilocks algorithm that
a is about to occur. The order in which these notifications
from different threads are interleaved and processed by
Goldilocks is represented mathematically by p, where p (i ) is
the i-th action in the sequence. This linear order, by construc-
tion, respects the program order for each thread, and the syn-
chronization total order for each synchronization variable.b
As Goldilocks processes each action p(i) from E,
it updates the Goldilocksets of variables. Initially, the
Goldilockset GLS(x) is empty for all data variables, including
static ones. When a new object is created, the Goldilockset
for all of its instance fields is initialized to the empty set.
After every action, the Goldilockset of every data variable x
is potentially updated. For every data variable x, three sim-
ple rules specify how GLS(x) is updated after p (i ) based on
whether p (i ) is ( 1) a synchronization source, ( 2) a synchroni-
zation sink, or ( 3) a read or write access to x, as shown in the
procedure ApplyLocksetRules in Figure 2.

If the action p (i ) is a synchronization operation on a variable o, we update the lockset GLS(x) for every data variable x in Data. If p (i) is a sync-source operation, rule 1 adds o to GLS(x) if it contains the id t of the current accessor thread. Intuitively, this represents that a later sync-sink operation by a thread u on synchronization variable o will be sufficient for u to gain race-free access to x. This is formalized by rule 2. If p (i) is a sync-sink(o) operation, rule 2 checks whether the synchronization variable o is in GLS(x). If this is the case, then t is added to the Goldilockset.

If the action p (i) is an access to a data variable x, rule 3 checks the Goldilockset of the variable GLS(x) to decide whether this access is race free. If GLS(x) is empty, it indicates that x is a fresh variable which has not been accessed so far and any access to x at this point is race free. If GLS(x) is not empty, only threads whose id’s are in GLS(x) can perform race-free accesses to x. If the accessing thread’s id t is not in GLS(x) then we throw a DataRaceException on x. Otherwise, the access to x is race free and GLS(x) becomes the singleton {t}, indicating that, without further synchronization operations, only t can access x in a race free manner.

Figure 1 shows two cases where the ownership of a data variable x is transferred from a thread ti to another thread tj, and indicates how the Goldilocksets evolve in each case. Program order (→po ) and synchronizes-with (→sw )

po

figure 1. transferring ownership of x, and GLS(x).

acquire(Lx) { ti, Lx, tj }

tj sw

p (j )

po
po
po

acquire(Lx)

{ Lx, ti } ti p (i)

access(x)
{ tj }
release(Lx)
{ tj, Lx }
access(x)

volwrite(o1)

volread(o1)

{ ti, o1, tk } { ti, o1, tk, o2 } volwrite(o2)

(b) Transitive ownership transfer using volatiles o1 and o2

{ ti, o1 }
tk
po
sw

p (i)

access(x)

{ ti, o1, tk, o2, tj } volwrite(o2)

{ tj } access(x)

edges between consecutive actions are indicated in the figure. Figure 1a illustrates direct ownership transfer from ti to tj. After accessing x, ti performs a sync-source operation (lock release) on synchronization variable Lx. Later, tj obtains ownership of x by executing a sync-sink operation (lock acquire) on synchronization variable Lx. Figure 1b illustrates transitive ownership transfer. Threads ti and tj do not synchronize on the same synchronization variable. Instead, the synchronization involves a chain of synchronizes-with edges between other threads and synchronization variables. ti synchronizes with tk via synchronization variable o1 and, later tk synchronizes with tj via synchronization variable o2.

Rules 1 and 2 in Figure 2 require updating the lockset of each data variable. A naive implementation of this algorithm would be too expensive for programs that manipulate large heaps. In Section 4, we present an efficient way of implement our algorithm by representing Goldilocksets implicitly and by applying update rules lazily.

figure 2. the core lockset update rules.

ApplyLocksetRules(p(i)):

1. if p(i) = sync-source(t, o)

foreach x ∈ Data: if t ∈ GLS(x)

GLS(x) := GLS(x)  {o}

2. if p(i) = sync-sink(t, o)

foreach x ∈ Data: if o ∈ GLS(x)

GLS(x) := GLS(x)  {t}
b A racy read may appear earlier in p than the write that it sees. If an execu-
tion contains a data race between a pair of accesses, Goldilocks declares a
race at one of these accesses regardless of which linearization p is picked.

3. if p(i) = write(t, x) or p(i) = read(t, x) if t ∈ GLS(x) or GLS(x) = 0/

GLS(x) := {t}

else throw a Dataraceexception on x