Summaries of the papers I read for my PhD candidacy exam, grouped by topic. For each paper I keep only the part of my full post that runs the method end to end on a worked example. The full posts add the background, results and limitations.

Data races: And how to find them?

A data race is two accesses to the same memory location from different threads, at least one of them a write, with nothing ordering them. I will discuss four data-race detection techniques that build on each other:

← More precisefewer false alarms More recall →fewer missed races

Lamport + Vector Clocks Lamport 1978 · Fidge & Mattern 1988 Pure happens-before, computed exactly with vector clocks. No false alarms on the schedule it sees, but an unrelated lock hand-off can hide a real race.

RaceFuzzer Sen 2008 Reports only races it actually makes happen, but can only confirm races its detector suspected.

Hybrid O'Callahan & Choi 2003 Lockset plus a limited happens-before.

Eraser (lockset) Savage et al. 1997 Flags every access without a common lock, so it misses the least but has false positives due to non-lock synchronization.

1. Lamport’s algorithm: logical and vector clocks

Paper: Leslie Lamport, Time, Clocks, and the Ordering of Events in a Distributed System, CACM 1978. Read the full post. Its central idea fits in one sentence: in a distributed system, “time” really means causality.

Vector clocks: Colin Fidge, Timestamps in Message-Passing Systems That Preserve the Partial Ordering, Australian Computer Science Conference 1988; Friedemann Mattern, Virtual Time and Global States of Distributed Systems, Workshop on Parallel and Distributed Algorithms 1988.

Thinking about Causality, and not the absolute time

Lamport models a distributed system as a set of processes. Each process does one thing after another, so its events are in a fixed order. Additionally, each process and can send messages to and receive messages from other processes—thus sending a message is an event, and receiving one is an event.

He then defines happened before, written a → b, as the smallest relation satisfying three rules:

1. Same process: if a comes before b in the same process, then a → b.
2. Messages: if a sends a message and b receives it, then a → b.
3. Chains: if a → b and b → c, then a → c (think transitive closure).

In plain terms, a → b means information could have flowed from a to b. If neither a → b nor b → a, the two events are concurrent. Neither could have influenced the other, so neither came “first” in any sense the system can observe.

Here is the running example used throughout this post: three processes, P, Q and R, exchanging three messages.

Figure 1: The running example: 3 processes, 3 messages, with the Lamport timestamps computed in the next section. Orange is the path p1 → r2, green is r1 → p4, and the dashed loop marks r1 and q4 as concurrent.

To check whether a → b, look for a path from a to b that moves forward along process lines and message arrows. p1 → r2: is ordered (orange line); r1 → p4: is ordered (green line); but r1 vs q4: is concurrent (even if r1 is to the left).

Logical clocks: a counter is enough

A logical clock is just an integer counter kept by each process. It has nothing to do with seconds. Its only job is to satisfy the Clock Condition:

If a → b, then C(a) < C(b).

If a could have influenced b, then a gets the smaller number. Two implementation rules, which Lamport calls IR1 and IR2, are enough to guarantee it:

• IR1: tick your counter between any two of your own events.
• IR2: stamp every message with your counter. When you receive a message with stamp T, move your counter past T.

Figure 2: The update rules at work. Every event ticks the clock by 1 (IR1); each message carries its sender’s clock; each receive (orange) sets the clock to max(C, T) + 1 (IR2). At every send and receive, the grey arrows show what goes in (the clock, and on a receive the message’s stamp T) and the teal arrow the clock coming out. Only r2 actually jumps.

What is concurrent?

The definition

Concurrency is defined in terms of happened-before, not clocks:

If two events have no happened-before relationship in either direction (neither a → b nor b → a), they are concurrent, written a ∥ b.

• Example: r1 and q4 are concurrent. No path of messages connects them.
• What it does not mean: concurrent is not “simultaneous”. It only means that neither event could have influenced the other.

The problem: deriving it from clock numbers

• The goal: the definition talks about paths, but an algorithm cannot “see” paths. All it has are the logical clock numbers we just assigned. So we would like to decide a ∥ b from C(a) and C(b) alone.

• The catch: the Clock Condition only works in one direction. If a → b, then C(a) < C(b); but this does not mean that

  If C(a) < C(b), then a → b.

• A counterexample: C(r1) = 1 < C(q4) = 4, yet r1 ∥ q4. A smaller number shows up for ordered pairs, but also for plenty of concurrent ones.
• So: C(a) < C(b) only rules out b → a. It cannot tell “ordered” from “concurrent”.

The rule used in practice: equal timestamps mean concurrent

Claim. If two events have the same timestamp, C(a) = C(b), then a ∥ b.

Why.

1. If a → b, the Clock Condition would force C(a) < C(b). It doesn’t, so not a → b.
2. If b → a, it would force C(b) < C(a). It doesn’t, so not b → a.
3. Neither direction holds, which is exactly the definition: a ∥ b.

On the running example, the rule groups events into one loop per timestamp. Every pair inside a loop is concurrent:

Figure 3: The equal-timestamp rule on the running example. The four loops hold 6 concurrent pairs: p1 ∥ q1, p1 ∥ r1, q1 ∥ r1, p2 ∥ q2, p3 ∥ q3 and p4 ∥ q4. The dotted pair, r1 and q4, is concurrent too, but their timestamps differ, so the rule misses it.

Strengths and limits.

• No false alarms: every pair it reports really is concurrent.
• Misses many pairs: it also works in one direction only. Concurrent events with different timestamps, like r1 (1) and q4 (4), slip through. It finds only 6 of the running example’s 21 concurrent pairs. Catching the rest needs vector clocks, below.

Telling concurrent from ordered: vector clocks

As shown above, the only thing a single Lamport number can say about concurrency is that equal timestamps mean concurrent. In the running example that finds 6 of the 21 concurrent pairs, and it never proves that two events are ordered. Vector clocks decide every pair exactly. They are not in Lamport’s paper; Colin Fidge (Timestamps in Message-Passing Systems That Preserve the Partial Ordering) and Friedemann Mattern (Virtual Time and Global States of Distributed Systems) introduced them independently in 1988.

What a single number can tell you

What you see, for a and b on different processes	What you can conclude	Why
C(a) = C(b)	a ∥ b	a → b would force C(a) < C(b), and b → a would force C(b) < C(a)
C(a) < C(b)	Only that b does not happen before a; a and b may be ordered or concurrent	The Clock Condition only works one way

Table 1: What a single Lamport number lets you conclude about two events.

So with one number, concurrency shows up only as a tie, and an order can never be proven.

The idea

• Instead of one counter, every process keeps one counter per process. Q’s entry for P records how much of P’s history Q has heard about, directly or through a chain of messages. If a vector that reaches a process is ≤ its own in every entry, the process has already heard everything that vector carries. So the event behind that vector happened before the process’s current event.

The rules

These are a small change to Lamport’s two rules:

1. Every process starts with all entries at 0.
2. Before each event, a process adds 1 to its own entry.
3. A message carries the sender’s whole vector.
4. On a receive, the process first takes the larger value of each entry (its own vector vs. the message’s), then applies rule 2.

The test

For two events A and B:

• A → B exactly when every entry of V(A) is ≤ the matching entry of V(B), and the vectors differ.
• A ∥ B exactly when each vector is larger in some entry.
• Shortcut: A → B exactly when B’s entry for A’s process is at least A’s own entry. In words: B has heard of A.

Why the shortcut gives the same answer as the full comparison?

• A’s own entry, say k, simply means “A is the k-th event of its process”.
• If B’s entry for that process is at least k, then a chain of messages carried news of A to B, so A → B; and anything A had heard of, B has heard of too, so the whole vector of A is ≤ B’s.

Vector clocks on the running example

Figure 4: Vector clocks on the running example. p1 → r2 (orange) shows up as “≤ in every entry”. The two loops are concurrent pairs, r1 and q4 and p3 and r2: in each, every vector is larger somewhere, even though Lamport’s numbers (1 < 4, 3 < 5) look like an order.

Side by side: single number vs. vector clocks

• The running example has 32 pairs of events on different processes. Table 2 counts how each method judges them.

	Single Lamport number	Vector clocks
Concurrent pairs found	6 (only the ties)	21 (all of them; including the six)
Ordered pairs proven	0	11 (all of them)
Pairs left undecided	26	0

Table 2: How each method classifies the 32 pairs of events on different processes.

The price

• A vector has one entry per process. With N processes, every timestamp is N numbers, every message carries N extra numbers, and every comparison checks up to N entries, where a Lamport clock needs just one. Charron-Bost showed in 1991 that no smaller exact encoding exists in the worst case. Dynamic data race detectors, where the processes are threads, pay that cost on memory accesses to decide whether two of them are ordered.

Strengths and weaknesses for race detection

A happens-before race detector treats threads as the processes and synchronization as the messages: an unlock followed by a lock of the same lock, a fork, a join. It keeps vector clocks and reports two conflicting accesses (same location, at least one write) when neither happened before the other.

Strengths

• No false alarms on the run (i.e specific schedule) it sees. If two accesses are unordered in this run, nothing kept them apart, so they really could be concurrent. Every report is a real race.
• Works with any synchronization. Locks, fork/join and messages all become edges.
• Exact. Vector clocks decide every pair as ordered or concurrent, with no guessing.

Weaknesses

• It only knows the observed run (i.e. specific schedule). It judges the one interleaving that actually happened, and cannot predict what another interleaving would do.
• Unrelated synchronization hides races. The example below shows this.
• Cost. N-entry vectors on memory accesses, as described above.

Example: one race, two runs

Two threads write x without holding any lock. Each also takes lock m for some unrelated work:

T1:  x = 1                 T2:  lock(m)
     lock(m)                    ...
     ...                        unlock(m)
     unlock(m)                  x = 2

The writes to x race in every run, because no lock protects them. Whether happens-before notices depends on which thread takes m first (see Figure. 5) :

Figure 5: The same race in two runs. In run A, T1 releases m before T2 takes it, so happens-before records a partial order (i.e. no race). In run B, T2 is done with m before T1 takes it, nothing orders the two writes, and the race is reported.

So happens-before is very conservative. It reports only what the observed run proves, and stays silent about races that a different schedule would expose. Lockset analysis (Eraser, next) addresses this.

2. Lockset analysis: Eraser

Paper: Savage, Burrows, Nelson, Sobalvarro and Anderson, Eraser: A Dynamic Data Race Detector for Multithreaded Programs, SOSP 1997 / ACM TOCS 1997. Read the full post.

Instead of asking whether two accesses happened in an order the program enforced, ask whether one lock was held for every access to the variable across threads.

A tiny server with two bugs

MiniServer is a toy web cache. A main thread sets a config value, two workers serve requests from a shared table, and a reporter thread prints statistics.

Variable	Intended protection	What happens	Verdict we want
config_max	none needed: written once before other threads exist, then only read	exactly that	stay quiet
hits	stats_mu	the reporter uses the wrong lock log_mu	Bug 1: wrong lock
table	table_rw, write mode must be used for writes	evict_stale writes under a read lock	Bug 2: wrong mode

A good detector flags hits and table and says nothing about config_max. Eraser’s design is, more or less, the story of getting all three right.

The core idea: intersect the locks

Eraser enforces a locking discipline: every shared variable is protected by some common lock, held on every access across threads. The program never says which lock protects which variable, so Eraser infers it from the run. For each variable v it keeps a candidate set C(v):

locks_held(t)@l = locks t holds when it executes line l

C(v) := all locks                        // initially
on each access to v by thread t at line l:
    C(v) := C(v) ∩ locks_held(t)@l
    if C(v) = { } then warn

This is all done dynamically: the instrumented program updates locks_held(t) on every lock and unlock, and intersects on every load and store.

Dry run on MiniServer

Assumed schedule: main runs first, then W1 (a cache miss, so it inserts), then W2 (a cache hit), then R, each running to completion. Line numbers refer to the MiniServer code above.

This naive version gets one of three right. It catches Bug 1, but it raises a false alarm on config_max (its first write held no lock) and misses Bug 2 (table_rw is held at evict_stale, just in the wrong mode [read mode instead of write mode]).

Quieting false alarms: a per-variable state machine

Two common patterns are harmless but violate the naive rule:

• Initializing data without a lock before anyone else can see it.
• Sharing data that is only read after initialization.

Eraser’s two fixes:

• For initialization: Eraser cannot tell when initialization ends, so it uses a proxy. A variable counts as initialized when a second thread first touches it.
• For read-only sharing: Eraser reports only once a variable is written after being shared.

State Machine for the above two fixes

One detail that trips people up: allocation is not an access. Allocating memory just marks it Virgin. The first real read or write (initialization is treated as a write), by any thread, makes that thread the owner, and the owner’s accesses never enter C(v).

Dry run with the state machine

Assumed schedule: the same as in the first dry run: main, then W1 (cache miss), then W2 (cache hit), then R.

With this, config_max goes Exclusive (owned by main), then Shared when a worker reads it. C(v) is empty, but Shared never reports, so the false alarm is gone. Bug 1 is still caught.

The price: a schedule-dependent blind spot

The modification

For this subsection only, change main so that it starts the threads before setting config_max:

What Eraser sees under two schedules

The price is a new blind spot that depends on the schedule. If main started the workers before setting config_max, a worker might read 0. Eraser catches that only if the worker’s read lands first:

The authors admit this makes Eraser more schedule-dependent than they would like, but doubt it mattered in practice.

Reader-writer locks: finding the last bug

A reader-writer lock held in read mode lets other readers in at the same time, so it protects a read but not a write. Eraser’s last refinement changes one line: reads intersect with locks held in any mode, writes intersect only with locks held in write mode. An ordinary mutex is always exclusive, so it counts in both sets, and Bug 1 behaves as before.

locks_held(t)@l       = locks t holds in ANY mode when it executes line l
write_locks_held(t)@l = locks t holds in WRITE mode when it executes line l

on each access op(v) by thread t at line l:
    if op(v) = read then
        C(v) := C(v) ∩ locks_held(t)@l
    else if op(v) = write then
        C(v) := C(v) ∩ write_locks_held(t)@l     // the one changed line
    if C(v) = { } then warn

e.g. line 26: locks_held(R)@26 = {table_rw}, but write_locks_held(R)@26 = { }

Here is the whole run under the final algorithm, with the held-lock sets shown at every access:

At evict_stale, the reporter holds table_rw only in read mode, so its write-mode set is empty and C(table) empties: Bug 2 is caught. The scorecard is now three for three: quiet on config_max, warnings on hits and table.

3. Hybrid detection: lockset plus limited happens-before

Paper: Robert O’Callahan and Jong-Deok Choi, Hybrid Dynamic Data Race Detection, PPoPP 2003. Read the full post.

Report a race only when no common lock was held and a deliberately limited happens-before relation cannot order the two accesses.

A small program with five fields

I’ll use one 18-line Java program, JobServer, for the whole post. A main thread M starts one worker W, and the two share five fields. Two fields hold real races, two are safe but fool lockset, and one is correctly locked. Each field copies a case from the paper’s own figures.

Figure 1: The JobServer program, stitched together from the paper’s Figures 1, 2 and 4.

• cfg is the paper’s globalFlag: written once before W starts, then only read.
• w is the paper’s childThread: W clears it, while M later reads it and calls interrupt().
• hits is the paper’s globalInt, and clock is the counter next to it, guarded by clockLock.
• Buf.data is the paper’s recycled BigObject, handed between threads through BufPool. The pool’s put and take are synchronized, with no wait/notify.

A detector sees one run. Here is the one we’ll replay, in the order of the circled numbers:

Figure 2: The observed run of JobServer, step by step, with the events each step emits. MEM = memory access, ACQ = lock acquire, REL = lock release, SND = message send, RCV = message receive (g_s is the start message).

The run does not crash. M11 reads null and skips the call. A good detector must still warn about it, because the truth is this:

Field	What protects it	Verdict	Why
cfg	start()	Safe	Written once before W exists, only read afterwards
w	Nothing on W’s side	Real bug	If W7 lands between M11’s null check and interrupt(), M throws a NullPointerException
hits	Nothing	Real race	In another schedule W3 runs before M4 and W reads 0
clock	clockLock	Safe	Every access holds clockLock
Buf.data	Ownership handed over through the pool	Safe	Only the thread that took the buffer touches it

Table 1: What a perfect detector would say about each JobServer field.

A perfect detector reports w and hits, and nothing else. Let’s see who manages it.

Lockset: cheap, but it cries wolf

The paper treats the program as a black box that emits events: memory accesses MEM(m, a, t), lock acquires and releases ACQ(l, t) / REL(l, t), and thread messages SND(g, t) / RCV(g, t). Every detector is then a predicate over pairs of events. Lockset’s predicate is:

\[\begin{aligned} \text{IsPotentialLocksetRace}(i,j) =\;& e_i = \mathrm{MEM}(m_i,a_i,t_i) \wedge e_j = \mathrm{MEM}(m_j,a_j,t_j) \\ &\wedge t_i \ne t_j \wedge m_i = m_j \wedge (a_i = \mathrm{WRITE} \vee a_j = \mathrm{WRITE}) \\ &\wedge L_i(t_i) \cap L_j(t_j) = \emptyset \end{aligned}\]

Two different threads, the same location, at least one write, and no lock held at both accesses. L_i(t) is the set of locks thread t holds just before event i.

Two details differ from Eraser:

• Pairs, not a running intersection. Eraser intersects one candidate set with every access, which can go empty even when every conflicting pair shares a lock. Three threads writing under {a, b}, {b, c} and {a, c} are mutually exclusive, yet Eraser warns. The pairwise check stays silent.
• One report per location. The tool reports the first race on a location and stops watching it. So it only needs to store a set of (a, t, L) tuples per location, and drops any access whose tuple is already there.

On JobServer:

Field	First racing pair reported	Correct?
cfg	M1 ↔ W1	False alarm: start() orders them
w	M2 ↔ W7	Right field, wrong pair (the dangerous one is W7 ↔ M11)
hits	M4 ↔ W3	Real race
clock	none	Correct: both accesses hold clockLock
Buf.data	M6 ↔ W5	False alarm: the pool hands the buffer over

Table 2: The pairwise lockset check on the JobServer run.

Two real races found, two false alarms, and one report that points at the harmless pair. Every false alarm comes from synchronization that is not a lock: start() and the pool.

Pure happens-before: precise, but blind in a different way

Pure happens-before turns every interaction between threads into a message: start, join, notify, every lock release to the next acquire, and every memory write to later accesses of that location. Two accesses race only if no chain of messages orders them.

Figure 3: The JobServer run as a space-time diagram. Pure HB also adds memory write-to-read edges, not drawn here.

Following the arrows in Figure 3:

Field	Pair	Path in Figure 3	Pure HB says	Right?
cfg	M1 ↔ W1	M1 → start() → W1	Ordered	✓
w	W7 ↔ M11	No path from W7 to M11	Reported	✓ right pair
hits	M4 ↔ W3	M4 → M5 releases clockLock → W2 acquires it → W3	Ordered	✗ real race missed
clock	M5 ↔ W2	Through clockLock	Ordered	✓
Buf.data	M6 ↔ W5, W5 ↔ M9	Through the pool’s lock	Ordered	✓

Table 3: Pure happens-before on each JobServer field, following the arrows in Figure 3.

No false alarms, but hits slips through. clockLock protects clock, not hits; the ordering is an accident of this schedule. Had W2 taken clockLock first, M4 and W3 would be unordered and pure HB would report them. This is the paper’s Figure 4, and it is the key observation: not every happens-before edge reflects real synchronization.

Every pure HB race is a lockset race

The paper’s Theorem 1 says pure HB never reports a pair that lockset would miss. Its proof is omitted, but it is three lines. If both accesses held a common lock l, the first thread must release l before the second acquires it. That release-to-acquire chain orders the two accesses, so pure HB would not report them.

The converse fails, as cfg and Buf.data show. This is the “folk theorem”: happens-before has fewer false positives than lockset, but more false negatives.

And it is expensive

The best earlier pure HB detector for Java, TRaDe, slowed programs 4 to 15 times relative to an interpreter, and JIT-compiled code is about ten times faster still. The cost comes from vector clocks. Every lock release and every memory write becomes a pending message, and each carries a vector with one entry per thread.

The hybrid: keep only the edges that mean something

The paper’s move is to split the work. Locks are judged by the lockset check, which understands them. Happens-before is kept only for the few events that really order threads, and lock hand-offs and memory accesses stop being messages.

Message source	Send	Receive	Pure HB	Hybrid
t2.start()	caller	t2 as it begins	✓	✓
t2.join()	t2 as it ends	caller when join returns	✓	✓
o.notify() / notifyAll()	the notifier	every thread waiting on o	✓	✓
User-marked methods (e.g. put / take)	the marked send	the marked receive		✓ (optional)
Lock hand-off	after REL(l)	the next ACQ(l)	✓
Memory	after each write to m	later accesses to m	✓

Table 4: Thread messages, and which detector uses them.

Call the resulting relation ⇢ (the paper draws an arrow with a dot over it). The hybrid check is the lockset check plus one line:

\[\text{IsPotentialHybridRace}(i,j) \;=\; \text{IsPotentialLocksetRace}(i,j) \;\wedge\; \neg(i \dashrightarrow j) \;\wedge\; \neg(j \dashrightarrow i)\]

That gives two consequences at once:

• Few messages, so cheap clocks. Threads start, join and notify rarely compared with how often they touch memory or locks.
• Lock edges can no longer hide races. clockLock stops ordering hits. Mutual exclusion is handled by the lockset half of the check.

The reports nest neatly:

Figure 4: Lockset, hybrid and pure happens-before reports as nested sets, with the paper’s own examples placed.

• Hybrid ⊆ lockset, because the hybrid adds a condition to the lockset check.
• Pure HB ⊆ hybrid, because of Theorem 1, and because ⇢ has fewer edges than →: a pair that → cannot order, ⇢ cannot order either.

The middle ring is where the trade lives. It holds a real race pure HB misses (globalInt, our hits) and a false alarm pure HB avoids (the pooled object, our Buf.data). The paper accepts the second to get the first, plus a large speedup.

Vector clocks, the paper’s way

The hybrid decides ⇢ with vector clocks: every live thread keeps one counter per thread, each message carries its sender’s vector, and the receiver takes the entrywise max. (The Lamport clocks post walks through the standard version.) The paper’s version differs in two ways:

• A stamp is one integer. Each access is stored with only its own thread’s entry, v, not the whole vector.
• Only sends bump the clock. A thread’s own entry rises only right after it sends a message (start, join, notify or an annotated channel). Reads, writes and lock operations leave it alone, so long runs of accesses share one stamp.

The check is then one comparison:

An earlier access by thread A, stamped v, is ordered before thread B’s new access iff B’s entry for A ≥ v: B has already heard of that point in A’s history.

Figure 5: Vector clocks on the JobServer run, written as (M-entry, W-entry). The start message tells W about M up to 1, so W1 can see M1 but W3 cannot see M4.

The check runs online: each time a thread touches m, the new access is compared at that moment against the accesses stored for m. That is why the trade is deliberate: few clock updates (each O(|T|), only on sends and receives) and many clock checks (each O(1), on every access).

The hybrid on JobServer

Only one message is sent in the whole run: M3’s start(). M’s own entry goes from 1 to 2 right after it, so M1 and M2 carry stamp 1 and every later M access carries 2. W begins at (1, 1) and never changes. Here is every access that meets a stored access from the other thread:

New access	Locks held	Compared with	Ordered? (B’s entry for A ≥ v)	Locks shared?	Result
W1 READ cfg	{}	M1, v = 1	yes: 1 ≥ 1	no	no race
W2 WRITE clock	{clockLock}	M5, v = 2	no: 1 < 2	yes	no race
W3 READ hits	{}	M4, v = 2	no: 1 < 2	no	race M4 ↔ W3
W5 WRITE Buf.data	{}	M6, v = 2	no: 1 < 2	no	race M6 ↔ W5 (false alarm)
W7 WRITE w	{}	M2, v = 1	yes: 1 ≥ 1	no	no race; W7 is stored
M11 READ w	{srv}	W7, v = 1	no: 0 < 1	no	race W7 ↔ M11

Table 5: The hybrid check on every cross-thread comparison in the JobServer run.

The w rows are the ones I like best. Lockset alone reported M2 ↔ W7, the harmless pair, and then stopped watching w. The hybrid knows start() orders M2 before W7, so it keeps looking and reports W7 ↔ M11, the pair that can crash. The paper saw the same effect on real programs: lockset’s first report on a field was sometimes false, while the hybrid skipped it and found a true race on the same field.

Score so far: both real races found, cfg correctly silent, and one false alarm left on Buf.data.

Removing the pool false alarm

The Buf.data alarm is the paper’s object-pool problem: ownership moves through the pool’s lock, and the hybrid deliberately ignores lock hand-offs. The tool offers two fixes:

• Automatic, for blocking channels. If a class calls wait or notify, every release of that class’s locks becomes a send and the next acquire a receive. A blocking queue is caught this way. BufPool never blocks, so it is not.
• Manual, for everything else. The user marks put as a send and take as a receive.

With BufPool marked, the new messages move the clocks. M7’s put bumps M to (3, 0), and W’s take at W4 lifts W to (2, 1). At W5 the check against M6 now passes: 2 ≥ 2, ordered. The return trip works the same way, so M9 is ordered after W5. The real races survive. W3 still knows M only up to 1, below M4’s stamp of 2. And W’s send at W6 lifts W7’s stamp to 2, while M11 knows W only up to 1.

The annotation is trusted, not checked. It tells the detector that everything a thread did before put happens before everything the taker does after take, for all data, not just the buffer. A race on some other field that happens to straddle a put/take in the observed run is then hidden, exactly as clockLock hid hits from pure HB. (A thread that keeps writing a buffer after returning it is still caught: its clock moves past the send.)

Here is every detector on the same run:

Field	Truth	Lockset	Lockset + thread locality	Pure HB	Hybrid	Hybrid + pool marked
cfg	safe	false alarm	—	—	—	—
w	bug	found (wrong pair)	found	found	found	found
hits	race	found	found	missed	found	found
clock	safe	—	—	—	—	—
Buf.data	safe	false alarm	false alarm	—	false alarm	—
Real found / false		2 / 2	2 / 1	1 / 0	2 / 1	2 / 0

Table 6: Every detector on the JobServer run.

“Lockset + thread locality” is the paper’s Detailed-NoHB baseline, its stand-in for earlier lockset tools. It is lockset with a filter that ignores an object’s accesses until a second thread touches it. That avoids the cfg alarm by luck of timing: M1 happens while only M has touched srv.

4. RaceFuzzer: race-directed random testing

Paper: Koushik Sen, Race Directed Random Testing of Concurrent Programs, PLDI 2008. Read the full post.

Take each race a predictive detector suspects, and steer the thread scheduler until the two racing accesses are one step apart in two different threads. If that moment happens, the race is real.

A tiny program with four suspects

LogService has two threads. M sets up a config, signals readiness under a lock L, serves requests for a while, then shuts the logger down. W is a worker: it reads the config if the service is ready, then writes to the logger if the logger still exists. A launcher starts both threads together, so nothing like start or join orders them.

The paper’s model assumes each statement touches at most one shared variable. That’s why the null check (w7) and the call (w8) are separate statements. In practice this holds automatically, because the tool works on Java bytecode, where every field access is its own instruction.

Only ready is accessed under L. The other three shared variables are touched with no lock held:

So any lock-based detector will suspect four pairs of statements. Here is what is actually true of each:

Pair	Variable	Truth
P1 (m1, w6)	cfg	False alarm. W reads cfg only after seeing ready == true, which M sets after m1. The flag, guarded by L, orders them.
P2 (m5, w1)	lastActive	Real, benign. A debugging field nobody reads.
P3 (m6, w7)	log	Real, harmless. If the shutdown wins, the null check sees null and W skips the append.
P4 (m6, w8)	log	Real, harmful. If the shutdown lands between the check and the use, W throws a NullPointerException.

A good tool should stay quiet on P1, confirm P2 through P4, and show that P4 can crash.

Phase 1: where the suspects come from

RaceFuzzer doesn’t invent its suspects. It takes them from an existing predictive detector. The paper uses the hybrid detector of O’Callahan and Choi (PPoPP 2003), but says any static or dynamic detector would do. This phase is not the paper’s contribution.

The hybrid detector watches one run and flags two memory accesses when all of these hold:

• different threads, same memory location, at least one write;
• no common lock held (the lockset part, from Eraser);
• not ordered by start, join or wait/notify (a happens-before check that deliberately ignores lock release → acquire edges).

Formally, a memory event is MEM(σ, m, a, t, L): thread t, executing statement σ, performs access a (READ or WRITE) on location m while holding lock set L. Two events are reported when:

\[\begin{aligned} & e_i = \mathrm{MEM}(\sigma_i, m_i, a_i, t_i, L_i) \;\wedge\; e_j = \mathrm{MEM}(\sigma_j, m_j, a_j, t_j, L_j) \\ & \wedge\; t_i \neq t_j \;\wedge\; m_i = m_j \;\wedge\; (a_i = \mathrm{WRITE} \vee a_j = \mathrm{WRITE}) \\ & \wedge\; L_i \cap L_j = \emptyset \;\wedge\; \neg(e_i \prec e_j) \;\wedge\; \neg(e_j \prec e_i) \end{aligned}\]

Here ≺ is happens-before built only from start, join and wait/notify. When the condition holds, the statements (σi, σj) become a racing pair.

Here is one run of LogService in which M runs up to m5, W runs to the end, and then M shuts down:

All four suspects are flagged, including the false alarm P1: the real ordering goes through ready and L, and the hybrid test ignores lock edges. Notice also that nothing crashed in this run. Phase 1 predicts P4 from a run where it did not crash. That’s the payoff of lockset-style reasoning.

Two terms are worth keeping apart here:

• An event race is two specific executions in one run, such as events #8 and #9 above.
• A racing pair is the two statements behind them, here (m6, w8). Many event races, from many schedules, converge on the same pair, and the pair is what Phase 1 hands to Phase 2.

Phase 1 is not schedule-free either. It can only flag statements that actually executed: if W happens to read ready == false, it never runs w6, and P1 is never flagged. But that’s only a coverage requirement. A happens-before detector needs coverage and a lucky ordering: the two accesses must also be unordered in the interleaving it saw.

Phase 2: postpone, then flip a coin

Phase 2 is the contribution. It takes one racing pair at a time, RaceSet = {σ1, σ2}, and runs the program under its own scheduler. Only one thread runs at a time, and every choice comes from a seeded random number generator:

The idea, step by step:

1. Pick a random thread that is enabled and not postponed.
2. If its next statement isn’t σ1 or σ2, just run it. Everything outside the pair is uninteresting.
3. If it is, look for a partner. Racing returns R: the postponed threads that all wait at the same statement (σ1 or σ2) and are all about to access the same address as this thread, with at least one write.
4. No partner yet: postpone the thread. It waits, frozen one step before its racing access.
5. Partner found: that’s a real race. Two threads are each one step from conflicting accesses to the same address, with nothing in between. RaceFuzzer reports it, then flips a coin. Heads: run this thread first. Tails: postpone it, and run every thread in R first.
6. If every enabled thread is postponed, release one at random. That thread runs its next statement unconditionally, which avoids an infinite loop. This is how a false pair ends: the partner never shows up, so the waiting thread is eventually let go.

Three details make this work.

• The invariant. At line 5, no two postponed threads ever race with each other. Every race is detected the moment it becomes complete, when a thread that isn’t postponed arrives to finish the pair, and it’s settled right away. That’s why tails runs all of R, not just one thread: leaving one behind would put two racing threads in postponed, where nothing ever compares them.
• The coin flip doesn’t fix anything. It only decides which of the two conflicting accesses goes first. Both orders are possible in real executions, and usually only one is harmful, so trying both at random is how RaceFuzzer finds out whether the race can crash the program.
• Replay is free. Because the seed fixes every choice, rerunning with the same seed reproduces the crash exactly. Nothing needs to be recorded.

Watching it work on LogService

To check the traces and numbers below, I wrote a small simulator of the algorithm and ran it on LogService.

P4: the crash

With RaceSet = {m6, w8}, one run goes like this:

1. W runs w1–w7. It sees a live logger at w7, so it heads for w8.
2. W arrives at w8. No partner is postponed yet, so W is postponed.
3. M runs through its setup and serve(). W just waits, however long that takes.
4. M arrives at m6. Racing finds W, so a real race is reported.
5. The coin says “run M first”: log = null. M finishes.
6. Now everyone enabled is postponed, so W is released and runs log.append(...): NullPointerException.

If the coin had gone the other way, W would have appended first and nothing would break. If M had reached m6 first, M would have waited for W instead, and the race would be found from W’s side. Over 2,000 seeds, the race was created in 100% of runs and the crash happened in about 50%.

P1: the partner never comes

With RaceSet = {m1, w6}, M gets postponed at m1 before even setting cfg. W then reads ready == false, skips w6, and finishes. Everyone enabled is now postponed, so M is released and runs to the end. W can only reach w6 after m3, which comes after m1, so the two threads can never meet. 0 of 2,000 runs reported a race. RaceFuzzer stays silent without anyone reading the code.

The scorecard

Pair	Phase 1	Race created	Crash	RaceFuzzer’s verdict
P1 (m1, w6)	suspected	0%	—	not confirmed
P2 (m5, w1)	suspected	100%	0%	real
P3 (m6, w7)	suspected	100%	0%	real
P4 (m6, w8)	suspected	100%	≈ 50%	real and harmful

Phase 1 gave four identical-looking warnings. Phase 2 sorted them into three tiers.