Correctness: The following theorem expresses the fact
that the Goldilocks algorithm is both sound, i.e.,
detects all actual races in a given execution, and
precise, i.e., never reports false alarms. The full proof of the
original Goldilocks algorithm for Java can be found in
Elmas et al. 5
Theorem 1 (Correctness). Let E Tid, Act, W, →po .,→so .
be a well-formed execution, x a data variable, and p a linear
order on Act as described earlier. Let i < j, and let p(i) and p(j)
be two accesses to x performed by threads ti and tj, with no other
action p(k) in between (i < k < j) accessing x. Then tj ∈ GLSj(x),
i.e., the access p(j) is declared to be race free by the Goldilocks
algorithm iff p(i) →hb p(j).
3. 1. example: precise data-race detection
In this section, we illustrate on an example the Goldilocks
algorithm and how Goldilocksets capture the synchronization mechanism protecting access to a variable at each point
in an execution. In this example, earlier lockset algorithms
would have erroneously declared a race condition.
Consider the execution shown in Figure 3 in which all
actions of T1 happen first, followed by all actions of T2 and
then of T3. This example mimics a scenario in which an
object is created and initialized and then made visible globally by T1. This Int object (referred to as o from now on) is
a container object for its data field (referred to as x from
now on). The object o is referred to by different global variables (a and b) and local variables (tmp1,tmp2,and tmp3)
figure 3. Precise data-race detection example.
Class Int { int data; }
Int a, b; // Global variables
Execution
Thread 1 (T1):
tmp1 = new Int;
tmp1.data = 0;
acquire(La);
a = tmp1;
release (La);
Goldilockset update rule applied GLS(x)
Initialize lockset
First access
La ∈ GLS(x) → add T1 to GLS(x)
No access to x
T1 ∈ GLS(x) → add La to GLS(x)
0/
{T1}
{T1}
{T1}
{T1,La}
Thread 2 (T2):
acquire(La);
tmp2 = a;
release(La);
acquire(Lb);
b = tmp2;
release(Lb);
La ∈ GLS(x) → add T2 to GLS(x)
No access to x
T2 ∈ GLS(x) → add La to GLS(x)
Lb ∈ GLS(x) → add T2 to GLS(x)
No acces s to x
T2 ∈ GLS(x) → add Lb to GLS(x)
{T1,La,T2}
{T1,La,T2}
{T1,La,T2}
{T1,La,T2}
{T1,La,T2}
{T1,La,T2,Lb}
Thread 3 (T3):
acquire(Lb); Lb ∈ GLS(x) → add T3 to GLS(x)
{T1,La,T2,Lb,T3}
b.data = 2; T3 ∈ GLS(x) → Race-free access
tmp3 = b; No access to x
release(Lb); T3 ∈ GLS(x) → add Lb to GLS(x)
tmp3.data = 3; T3 ∈ GLS(x) → Race-free access
{T3}
{T3}
{T3,Lb}
{T3}
at different points in this execution. The contained variable
x is protected by synchronization on the container object o,
and during the execution, the lock (La or Lb) protecting o
and x changes depending on which variable (a or b) points
to o. Notice that, T2 changes the protecting lock of the container object o from La to Lb, without accessing x. Figure 3
shows the Goldilocks update rules applied on GLS(x) for
each action and the resulting value of GLS(x).
Observe that the update rules allow a variable’s
Goldilockset to grow during the execution. This enables
them to represent threads transfering ownership using
different synchronization variables during the execution.
In this example, this ownership transfer takes place without the variable itself being accessed. For example, after
T2 finishes in Figure 2, GLS(x) has the value {T1, La, T2,
Lb}, meaning that a thread can access x without data race
by locking either La or Lb. Then T3 makes Lb the only protecter lock by acquiring Lb and accesses x.
3. 2. Distinguishing read and write accesses
The basic Goldilocks algorithm in Figure 2 tracks the
happens-before relationship between any two accesses to a
variable x. In order to perform race detection, we must check
the happens-before relationship only between conflicting
actions, i.e., at least one action in the pair must be a write
access. We extend the basic Goldilocks algorithm by keeping track of (i) GLSW (x), the “write Goldilockset of x”, and (ii)
GLSR(t, x), the “read Goldilockset of t and x” for each thread t.
The update rules in ApplyLocksetRules are adapted to maintain these Goldilocksets, but have essentially the same form
as the rules in Figure 2. In the extended algorithm, it is sufficient to check happens-before between the current access
to x and the most recent accesses (in the linear order p) to
x. How this extension is performed for Java can be found in
Elmas et al. 6
3. 3. specializing Goldilocks to the Jmm
The JMM requires that all synchronization operations be
ordered by a total order →so , whereas in our execution model,
a separate total order →so o per synchronization variable is
sufficient.
Data Variables and operations: In Java, every data variable is
in the form of (o, d) where o is an object and d is a nonvolatile field. The byte-code instructions x load and xstore access
memory to read from and write to fields of objects, respectively (x changes depending on the type of the field).
The JMM specifies three synchronization mechanisms:
monitors, volatile fields, and fork/join operations.
Monitors: In Java, a monitor per object (denoted by mo) provides a reentrant lock for each object o. Acquiring the lock
of an object o (acquire(o) ) corresponds to a sync-sink
operation on mo, while releasing the lock of o (release(o)) corresponds to a sync-source operation on mo. Nested acquires
and releases of the same lock are treated as no-ops. In the
JMM, each release(o) synchronizes with the next acquire(o)
operation in →so mo.
Volatile Variables: Each volatile variable is denoted (o, v)
where o is an object, and v is a volatile field. Each read
volread(o, v) from a volatile variable (o, v), and each write
