Where do coherence bugs actually live?

Stable-state transitions are exercised by almost any test. The bugs found late are in races: a message for one transaction arriving while the cache or H is in the middle of another. A race cross is a coverage item that names three things: the transient state, the conflicting message that arrives in it, and which request caused that message. Where the result depends on which of two messages H sees first, the cross also names the order, and both orders are bins.

The race crosses of the course controller

The two orders of the eviction race are separate bins: PutM reaches H first (order A) or the GetS does (order B). A regression that only ever produces order A has not tested the forward-from-WB path at all, even though both cells of the plain matrix (MI^A, Put-Ack) and (M, Fwd-GetS) look covered.

Why random traffic hits them rarely

A race needs a second request for the same line inside a short window: the cycles a cache spends in one transient state. Suppose (illustrative numbers) each core issues a request every 20 cycles on average (rate 0.05), addresses are uniform over A lines, and the window is 20 cycles. The chance that one of the other N - 1 cores requests this line during the window is 1 - (1 - 0.05 / A)^((N - 1) x 20).

The second row extends the course model to eight cores to show the effect; the protocol is unchanged. Few lines and many cores raise the rate by a factor of about 3,400. The same factor applies to every race cross, since each one starts with a same-line conflict, and a specific cross then also needs the right states and order. A plain random regression with realistic address spread can run for days without one PutM crossing a forward.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

import random
def p_conflict(cores, lines, rate, window):
    """P(at least one other core requests the same line during one transient window)."""
    per_cycle = rate / lines                 # one other core hits this line in one cycle
    return 1 - (1 - per_cycle) ** ((cores - 1) * window)
def simulate(cores, lines, rate, window, trials, seed=1):
    rng, hits = random.Random(seed), 0
    for _ in range(trials):
        line = 0                             # the line in its transient window
        hits += any(rng.random() < rate and rng.randrange(lines) == line
                    for _ in range((cores - 1) * window))
    return hits / trials
WINDOW, RATE = 20, 0.05                      # illustrative: 20-cycle window, 1 request per 20 cycles
spread = p_conflict(cores=2, lines=4096, rate=RATE, window=WINDOW)
hot = p_conflict(cores=8, lines=4, rate=RATE, window=WINDOW)
assert abs(spread - 2.44e-4) < 1e-5 and abs(hot - 0.828) < 0.001
assert hot / spread > 3000                   # hot spot: thousands of times more races per window
for cores, lines in [(2, 64), (8, 4), (8, 16)]:
    model, sim = p_conflict(cores, lines, RATE, WINDOW), simulate(cores, lines, RATE, WINDOW, 4000)
    assert abs(model - sim) < 0.03, (cores, lines, model, sim)
# failing case: an estimate that forgets the other cores (counts one competitor) is wrong at 8 cores
naive = p_conflict(cores=2, lines=4, rate=RATE, window=WINDOW)
assert abs(naive - simulate(8, 4, RATE, WINDOW, 4000)) > 0.3
# transient windows needed for 100 expected conflicts
assert round(100 / spread) == 409648 and round(100 / hot) == 121
print("PASS: few lines and many cores raise the per-window race probability from 0.02% to 83%")

The formula assumes independent uniform requests; real traffic is burstier, and locks and shared counters produce natural hot spots (see Hot Lines and Locks). The point survives: race coverage has to be engineered, which is the next lesson.

Related topics

• Shared course model

• The eviction-versus-forward race, both orders

• The full state x event matrix

• Crosses and explosion (First Principles of Verification Strategy)