Race conditions are the bugs you cannot prove. They need one specific interleaving to go wrong, so a hand-found candidate often cannot be confirmed, and a fix usually cannot be accompanied by a regression test that reliably fails before it and passes after.

Jann Horn’s post describes MAccConc, tooling that makes the interleaving itself something you can specify and replay in the Linux kernel.

The old workarounds are all trial and error:

  • Recompile the kernel with conditional mdelay() calls placed by hand, subject to the running thread’s name
  • DTrace chill() probes on platforms that support it — but only at function boundaries and explicit trace points
  • Read the ASCII interleaving diagrams that often ship with kernel race-condition fixes, and reason about them

The approach rests on two ideas:

  • Communication points — pairs of accesses on two threads to overlapping memory where at least one is a write. Those are the orderings worth exploring.
  • Count-augmented stack traces as stable names — “the second call to __x64_sys_recvfrom, then the first __sys_recvfrom, then the first sock_recvmsg… and the first access at address X.” Data addresses are useless because objects are freshly allocated each run; bare instruction addresses are useless inside memcpy() or spin_lock().

Coverage comes from ASAN outline-mode instrumentation routed through KCOV, with delay injection exposed as an ioctl that sets and waits on shared flags at named accesses. Two usage styles fall out of that: constraint style (A happens before B), which the terminal UI and GUI use, and fully specified context-switch ordering, which drives an automatic tester that walks every A-B-A interleaving of a two-thread test case.

In the demo, racing dup() against close() on a file descriptor, the automatic tester finds an ordering where dup(5) returns 5 — correct per POSIX, and not what you would guess. In the GUI you right-click two memory accesses to add a constraint and re-run; the trace then shows brown delay-injection lines where the constraints applied.

The honest limits are worth as much as the result. ASAN does not instrument direct stack accesses, so races on wait queues may be invisible; TSAN would report access atomicity but cannot coexist with the ASAN hooks. Impossible orderings are currently discovered by waiting out a spin timeout. KCOV remote coverage is not wired up in upstream for RCU callbacks or loopback packet receive.

The LLVM support needed to report function entry and exit landed in LLVM 23.1.0; the kernel patches are on the list, not yet upstream, so testing means running Horn’s branch. The transferable lesson outlasts the tool: naming an event so the name survives re-execution — not by address, not by instruction, but by position in the call path — is the part other debugging tools should steal.