How do you make a race happen on purpose?

You cannot schedule a race message by message in a large system, and a hand-written directed test breaks as soon as the latency of any path changes. Instead, change the traffic so that race windows are wide and same-line conflicts are frequent, and let constrained random do the rest. Each knob targets a factor of the race probability: how often two requests meet the same line, how long the transient window lasts, and whether the conflicting message arrives inside it.

Knobs and the races they provoke

Worked case: forcing (MI^A, Fwd-GetS) on the course model

Target: order B of Eviction Versus Intervention, where C1's GetS reaches H while C0's PutM is still in flight. Recipe, keeping that lesson's roles (C0 evicts, C1 reads): give C0 a one-line cache; let C0 store to X (C0 M / 1, H exclusive(C0), memory = 0), then store to a second line Y in the same set, which evicts X into the WB entry and sends PutM W (C0 MI^A / 1 in WB); add a random delay of up to 16 cycles to PutM only; and give C1 a load-heavy stream over just X and Y. Each knob alone barely helps. Together they make the cell frequent, and the value checker confirms that C1 reads 1, not memory's 0.

The block below abstracts that recipe: C0 stores and evicts with an LRU cache, C1 reads, and a hit is a GetS for a line whose PutM is still in flight. It counts hits of (MI^A, Fwd-GetS) under each knob. Measured on seed 3 with 20,000 cycles, the counts are 4 (baseline: 1,024 lines, 64-line cache, no delay), 0 (hot spot only: 8 lines fit in the cache, so nothing is evicted), 5 (tiny cache only), 21 (slow writebacks only), 217 (hot spot and tiny cache) and 1,405 (all three).

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
27
28
29
30

import random
from collections import OrderedDict
def stress(lines, capacity, wb_delay, cycles=20000, seed=3):
    """Count (MI^A, Fwd-GetS) hits: C1's GetS finds C0's PutM for that line still in flight."""
    rng, cache, inflight, hits = random.Random(seed), OrderedDict(), {}, 0
    for _ in range(cycles):
        if rng.random() < 0.5:                       # C0 stores to a line (acquiring M abstracted)
            x = rng.randrange(lines)
            if x not in inflight:                    # a line in MI^A stalls C0's store
                cache[x] = True; cache.move_to_end(x)
                if len(cache) > capacity:            # eviction pressure: PutM enters the network
                    victim, _ = cache.popitem(last=False)
                    inflight[victim] = rng.randint(1, wb_delay)
        if rng.random() < 0.3:                       # C1 reads a line
            x = rng.randrange(lines)
            if x in inflight: hits += 1              # H still records C0: Fwd-GetS meets MI^A
            cache.pop(x, None)                       # otherwise C0 loses M to the read (simplified)
        inflight = {x: t - 1 for x, t in inflight.items() if t > 1}
    return hits
base = stress(lines=1024, capacity=64, wb_delay=1)
knobs = {"hot spot": stress(8, 64, 1), "tiny cache": stress(1024, 2, 1),
         "slow writeback class": stress(1024, 64, 16)}
tiny_hot = stress(8, 2, 1)
together = stress(8, 2, 16)
assert base <= 5 and knobs["hot spot"] == 0          # few lines alone: the 64-line cache never evicts
assert knobs["tiny cache"] >= base and knobs["slow writeback class"] > 4 * base
assert tiny_hot > 40 * base and together > 5 * tiny_hot      # knobs multiply when combined
# failing case: a configuration that cannot evict can never cover the cell, however long it runs
assert stress(lines=8, capacity=8, wb_delay=16, cycles=200000) == 0
print("PASS: eviction pressure plus few lines plus slow writebacks is what reaches MI^A, Fwd-GetS")

The hot-spot result is the lesson in miniature: a knob that is right for one race (upgrades) does nothing for another (evictions) unless the cache is also small enough to evict. Stress profiles are therefore named per target cross, and a regression mixes them.

Rules for stress knobs

Stay inside the protocol's assumptions. Random delays may reorder messages only where the protocol allows it: the course model assumes no FIFO, so any reordering is legal here, but a protocol that requires an ordered channel must keep it ordered under stress, or the test reports false failures. Back-pressure on the response class may delay responses for a bounded time, never withhold them indefinitely, because the deadlock-avoidance rule says responses always sink; withholding them for ever tests a system the design never promised. Finally, keep unbiased profiles in the mix: a regression that only runs hot spots stops covering the plain paths and the address-dependent logic.

Related topics

• Shared course model

• The race crosses being targeted

• Writeback buffers

• Credits and back-pressure

• Coverage-driven stimulus (First Principles of Verification Strategy)