[mark14wu]

Summary

This PR adds the compiled race detector: RaceDetector(compile=True) or tile-race --compile script.py. Each launch is analyzed for global-memory races on the TTIR Triton compiles for it, on the host, without running the kernel. Like the compiled sanitizer (#480), it needs no GPU, the kernel's outputs are not written, every autotune config is analyzed, and a config that does not compile for the target is unsupported while the program goes on.

The analysis is #361's compiled (TTIR) race detector, taken from the frozen 62c6d7c and rebuilt on the shared IR layer of this stack: the TTIR reader's facts (#509, #515), the shared lowering (TermLeaves, Lowerer, fold, GuardDag; #482, #528), the compile-failure classification (#528) and the two-copy solver (#503, #505). It always reads the reader's multipath and while-region facts, and always reads loaded integer values from launch-value snapshots; there is no level switch.

Stacked on #528 (stack #508). Triton 3.8 only. One commit.

User-visible changes:

• RaceDetector(compile=True) returns a CompiledRaceDetector (until now it raised NotImplementedError). With ENABLE_RACE_DETECTOR=0 it is the NullRaceDetector, as for the eager mode. SymbolicRaceDetector(compile=True) raises a TypeError naming RaceDetector(compile=True), like SymbolicSanitizer(compile=True).
• tile-race --compile script.py runs it; tile-race script.py is unchanged.
• Each launch records a CompiledRaceRecord per race, then a RaceVerdict with one RaceConfigVerdict per config, in Launch.records. tilelens.save()/load() keep them. CompiledRaceDetector, CompiledRaceRecord, RaceVerdict and RaceConfigVerdict are exported from tilelens.clients.
• Every race is printed when the launch finalizes, in the eager race detector's layout with a "(compiled race detector)" line and the config. Every part of a launch that was not analyzed is printed once per site ([CompiledRaceDetector] not analyzed ...), with the launch's notes, so a quiet launch never reads as race-free; this matches the compiled sanitizer's default and the eager race detector's warning. A proved launch prints one line only under TILELENS_VERBOSE=1 or the tile-race CLI. Nothing calls sys.exit.
• The README gets a "Compiled race detector" section.

The eager race detector, the compiled sanitizer, the tracer and the profiler behave as before. The compiled sanitizer sends the same Z3 queries and returns the same results on the 977 corpus texts (see Tests).

Change

1. The client (tilelens/clients/race_detector/compiled/client.py)

CompiledRaceDetector is an IRClient with its own NAME (compiled_race_detector), IR_STAGES = {"ttir"} and LAUNCH = "skip". It does not subclass the eager detector or the sanitizer; it is registered as a virtual subclass of RaceDetector, so the factory's disable flag reads it alike. The constructor is CompiledRaceDetector(abort_on_error=False, *, target=None): abort_on_error is the eager factory's parameter, kept and unused (a separate PR, #502, retires it everywhere); target names the IR target as in Sanitizer(compile=True, target=...).

• Snapshots. before_launch calls IRClient.before_launch (which records the event) and reads the binding it recorded from the new neutral ArtifactLog.last_binding; then, for each tensor argument, it takes its pre-launch contents when they can be read: an integer or bool, contiguous tensor of 1 to 16384 elements (SNAPSHOT_MAX_ELEMENTS), with no lazy conj/neg, while the launch's snapshots stay under 256 MiB (SNAPSHOT_CAP_BYTES). Otherwise the tensor's LaunchTensor carries the reason ("float dtype ...", "too large (... elements, bound 16384)", "non-contiguous", ...), which a refusal names. No kernel has run at that point, in an IR-only trace and in a mixed one (the host compile comes before the interpreted run).

• Configs. Every config the launch compiled is analyzed against its own bindings, grouped by config kwargs as the compiled sanitizer groups them. Configs whose TTIR (minus its source locations), scalar arguments, tensor facts and snapshots, grid and binding errors are the same share one solve; autotune configs that differ only in num_warps or num_stages compile to different kernels with the same TTIR. There is no launch-level time budget: each solver has its own timeout (T0 10 s, T1 120 s, the T0_TIMEOUT_MS / T1_TIMEOUT_MS class attributes), set on the solver object, never through z3.set_param.

• Compile failures go through tilelens/ir/failures.py exactly as in the compiled sanitizer: an error no target compiles past is a note; any other is a compile-failed config whose refusal names RaceDetector(compile=True, target=...), or TILELENS_IR_TARGET; a host compile that could not run is host-compile-unavailable; a launch with no JITFunction is no-compiled-kernel, naming the eager RaceDetector().

• Verdicts. A config is:

  • ok, with its rung and qualifiers;
  • races, with its CompiledRaceRecords; possible races under over-approximation found beside them are withheld, and a launch note counts them;
  • unsupported, with a Refusal: the reader's kind (prefixed with the site), the race detector's own kind, timeout / unknown for an undecided Z3 query (the launch-grid requery included: its any-grid races are then kept as grid_fragile evidence, never as races of the launch), or potential-race when every race found is between over-approximated records (a dropped mask, a loaded value with no snapshot);
  • vacuous: no execution satisfies the premises, so no proof is claimed.

  The launch's status is races if a config races, else unsupported, else vacuous, else ok. For ok, RaceVerdict.scope says what the weakest config's proof holds for: any-params-any-grid (T0), this-params-any-grid (T1) or this-params-this-grid (T1-launch). The qualifiers are assumes no i32 overflow (the widths named are all those whose obligations can fail in the proof's domain: one query per width until none is left, since one model need not show them all), assumes termination (the kernel awaits a flag) and reads tensor contents (the verdict read a snapshot, so it holds for those contents).

• Records (tilelens/clients/race_detector/data.py), plain data with no Z3 terms and no tensors:

  • CompiledRaceRecord(RaceRecord): the eager record's fields (race type, both accesses with op, write, tensor name, source location and element; the witness program ids; the reason) plus the config. An element is counted from the launch tensor's data pointer;
  • RaceConfigVerdict(ConfigVerdict): rung, qualifiers, and grid_fragile, the any-grid races behind a T1-launch proof, or behind an unsupported config whose launch-grid requery Z3 did not decide. These are evidence only, never races of this launch;
  • RaceVerdict(IRVerdict): qualifiers, the configs' union.

  The shared tilelens/ir/verdict.py is unchanged. trace_io already registers data.py, so nothing is added there.

• Threads. Everything the analysis builds lives in Z3's main context, which is not thread-safe. CompiledRaceDetector._solve holds hb_common.MAIN_CONTEXT_LOCK (one process-wide RLock) around analyze_graph and the conversion of its outcome to plain data, and drops the outcome before releasing it; a refusal kept in an outcome has its traceback cleared, and so does a contained internal error, so no frame full of Z3 terms outlives the lock and is collected on another thread. The eager detector's solve takes the same lock (its record building, during the interpreted run, does not). Traced launches on several host threads therefore take turns.

• Ctrl+C. When Z3's own SIGINT handler cancels a query (unknown, "interrupted from keyboard"), the analysis raises KeyboardInterrupt, as the compiled sanitizer does, instead of reading the query as undecided and asking the next rung.

• Qualifiers are attached to ok and races configs only; an undecided config carries none.

• configs_of and saveable_config move from the compiled sanitizer's client to tilelens/ir/capture.py, unchanged, so both clients use one copy. ArtifactLog gains last_binding, the binding the latest record returned.

2. Program-id names (tilelens/clients/pids.py)

A neutral move: one place for the program-id and grid variable names: PID_AXES, pid_name, pid_var(axis, ctx), grid_name, grid_var(axis, ctx), and PID0–PID2 in Z3's main context. It touches three other clients, with no change in behaviour: the eager engine's SymbolicExpr.PID0–PID2 and node labels, the solver's per-copy pid rename (its helper is now _main_context_pids) and the compiled sanitizer's environment pids and witness keys now use it, with the same Z3 names as before. PID0–PID2 are created on first use: created at import, they made main-context Z3 terms when the compiled sanitizer imported the module, and its own per-check contexts then picked other models (25 of the 977 corpus rows got other witnesses from the same queries).

3. A reader fact: the tile shape (tilelens/ir/ttir_reader.py)

AccessEvent.shape is the access's tile shape, read from the pointer operand's tensor type (tensor<16x16x!tt.ptr<i32>> is (16, 16), a scalar pointer ()). Nothing else in the reader changes, and the compiled sanitizer does not read it (its queries and results are the same, see Tests).

4. Leaves (compiled/leaves.py)

RaceLeaves is the race detector's TermLeaves, in Z3's main context (ctx None), so the solver's per-copy z3.substitute rename applies to what it lowers:

• a program id is pids.pid_var(axis), the grid size pids.grid_var(axis);
• an arange is start + lane, one lane per (dim, extent) (the reader's contract), registered in the solver's arange dict so each copy has its own lane in [0, extent);
• an atomic observation is one variable per access;
• a scalar argument is a shared free Int at T0 and the launch's value, read signed at the argument's width, at T1;
• a loaded value is If(mask, snapshot[offset], other), the snapshot an array whose elements are asserted equal to the launch's contents, read at the load's own width with the signed reading (i1/bool included). Constant and affine offsets fold through snapshot_lookup. A width that differs from the tensor's element width, a non-contiguous tensor, a view smaller than its allocation, a tensor the kernel writes, an unsigned tensor holding a value the signed reading makes negative (a uint8 of 128 or more: an extui of it would fail its width obligation although the program computes it exactly), or one with no snapshot leaves the value free, and the record that reads it is over-approximated. Each read adds mask -> 0 <= offset < numel as a domain premise;
• an unmodeled value (DataDep) refuses with unmodeled-value;
• // and % go through BoundedDivRem, the race detector's divrem for the shared Lowerer (a new hook; its default is the truncating encoding the lowering had, which the compiled sanitizer keeps, so its queries are unchanged). It takes inclusive bounds over the domains every query assumes and nothing else: constants, the launch's parameters (none at T0), program ids >= 0, the grid >= 1, lanes in [0, extent), and + - * // % min max, selects and casts over them; never a mask, a path, a launch pin or a loop's range (a loop's iteration range is a premise of its own accesses' records only). With a dividend >= 0, Z3's Euclidean a / b and a % b equal the IR's truncating ones for either sign of b (% is guarded at b == 0, where the truncating remainder is a, unless b's sign is known); with a dividend <= 0 and a divisor of known sign, the same on -a with the sign re-applied; otherwise the truncating encoding with its sign branches. A grouped program-id swizzle (pid // width, pid % group_size) no longer branches on signs (see Validation).

Refusals are RaceRefusals with the race detector's RaceKind (spin-shape, cas-value, control-flow, indirect-address, snapshot-bound, unmodeled-value, missing-binding, loop-bound, integer-overflow, timeout, unknown, potential-race, vacuous, other, and the client's kinds), not the reader's closed TTIRKind. Walkers over terms (terms_below, loaded_leaves, observed_leaves, the T0 linearity gate, the CAS gate) are built on lowering.children / fold and step into a Loaded's offset, mask and other. #361's own walker missed products under an IntCast.

5. Records (compiled/global_records.py)

The Encoder builds the solver's AccessEventRecords from the access graph, ported from #361's encode_graph / encode_graph_t0 / _record_for:

• byte addresses with the in-bounds premise at T1, per-tensor byte offsets at T0;
• one iteration index per loop: concrete trip counts, or a symbolic existence premise, which must be linear in pids, lanes and iterations at T1; a zero-trip loop has no footprint, a single-trip loop binds k = 0; a non-constant or non-positive step refuses (loop-bound);
• value-modeled RMW and CAS observations, the initial values atomics read from (at most 1024 elements, not unsigned), and refusals for an unmodeled observation or a free loaded value in an address (indirect-address, snapshot-bound for a table over the bound);
• the await premises in every record, the await dependencies and observations, and the pre-exit representative of each awaited poll. An await's exit predicate is exact only where its own width obligations hold: the premise is reach(poll) ∧ held -> exit, and where the poll is reached the obligations' failure joins the encoder's violations, so the qualifier and the launch discharge cover them ((pid * big) // big as the expected flag value wraps for one program, which then reads the payload unsynchronized: a race);
• deps from the reader feed the solver's dependency order, closed transitively through an intermediate access only when it runs wherever the dependent does (no dropped mask, no unmodeled branch, its mask and path conjuncts among the dependent's, a constant-true mask counting as none): causal order composes lane for lane, but where an atomic is masked off, the value the store writes is not the load's. Without the closure a load → unmasked exchange → store chain at one lane was a false WAR ([FEAT] [RACE DETECTOR] Z3-based race detector #361's test_atomic_rmw_mutual_atomicity); with it ungated, a masked atomic in the chain hid a real WAR;
• copy-local variables: a record's own loops' iteration indices (and those of an awaited poll's loops, whose premise every record carries), its observations, the await observations and the free loads. Only its own loops: the solver reads them as the record's iterators, and one of a loop the access is not in let one execution count as two (a false WAR between an in-place load and its store beside another loop, found in Validation);
• lanes. A tile record (AccessEvent.shape with an extent above 1) carries its shape for the solver (symbolic_expr, a stub with .shape) and, when every dimension of extent above 1 is named by the lane variable of that (dim, extent) occurring in its lowered address or activity, a lane_position (one lane variable per dimension, 0 along an extent-1 one). A tile with a dimension no lane variable names (a broadcast pointer, p + tl.zeros([B]), tl.broadcast_to(row_ptr, (B, B))) has none, so the solver reads its lanes as not named (distinct lanes at any assignment) and its B lanes on one element are compared; such a tile is no dependency anchor either. Before, compiled records carried neither, so the solver read a tile whose address used no lane variable as one scalar and proved stores of B different values to one element race-free.

Width obligations. Each access's width_obligations become one premise, guarded with lowering.GuardDag so an obligation holds only where a tl.where arm reads its term (an unguarded premise could exclude real executions). A signed quotient that does not fit is undefined in either arm, so it is never guarded. For each obligation the encoder also records where it fails while it matters: a loop's obligations where the loop is reached, guarded by the access's path and the outer loops' iteration premises (the increment also under the loop's own); path obligations at every iteration; mask obligations where the path holds; offset obligations where path and mask hold. A loop under a branch is guarded by that branch this way, which is what #515 left to this PR (LoopInfo has no path).

CAS gate. A CAS operand may be a constant, an observation, a comparison of those, not / and / or of comparisons, the extui of an i1 condition to the operand's width ((pid == 0).to(tl.int32)), or a select of these. Any other IntCast is refused (cas-value, "changes an integer's width"), and so are arithmetic, loaded operands, unmodeled observations and float CASes; a CAS in a loop is control-flow. #361 refused a CAS when any value-changing integer cast appeared anywhere in the graph.

6. Fences (compiled/fences.py)

The race detector's fence rule, passed to the solver through #503's fence_between hook and #505's fence_epoch hook:

• a ttg.barrier counts only when its address space has both the global-read (2) and global-write (4) bits (Triton 3.8's tl.debug_barrier prints all);
• it orders a < f < b only when its block path is a prefix of both accesses' block paths, so a barrier under a branch orders nothing outside it;
• a barrier inside an scf.for orders the two accesses of one iteration around it; it orders every pair of executions only when another barrier of that loop body lies outside [a, b] (one on the back edge: for iterations i < j, a_i < f_i < b_j; for i > j, b_j < g < a_i). That back-edge case goes past "a loop barrier orders same-iteration pairs only"; it is sound, and called out here for review;
• epoch(record) counts the barriers run before an execution, as an int or an affine term in the loop iteration indices. It is exact for unconditional barriers with constant trip counts; anything else (a conditional barrier, one inside a while, a symbolic trip count) gets a fresh unconstrained epoch.

#361 placed each barrier at a float position between sequence numbers, which ordered a conditional barrier's accesses as if it always ran, and a loop barrier's accesses across iterations.

7. Awaits (compiled/awaits.py)

A pass over the reader's WhileRegion facts decides which scf.while loops are spins on a flag, with #361's rules (its two structural ones, an scf.condition outside a condition region and a spin without one, are now the reader's refusal and rule 8): no carried values; not nested in another scf.while (inside an scf.for it may be); the body is only scf.yield; no store in the condition region; exactly one access, not float; an RMW poll is an add, or or xor of 0; the condition is a comparison; the poll is compared against a value that does not depend on it. Anything else refuses with spin-shape, the race detector's kind. It returns {access: exit predicate} as the race detector's own table (the reader marks nothing as awaited). The verdict then assumes the spin terminates.

8. Rungs (compiled/analysis.py)

analyze_graph(graph, params, tensors, grid) picks the least concretization that decides a kernel, ported from #361's _solve_one_graph, _try_t0, _t1_content_free and _launch_scoped_requery:

• T0, any scalar parameters and any grid along the axes the kernel reads: tried when the launch's tensors are pairwise disjoint (the per-tensor encoding stands for non-aliased arguments) and every term is linear with the parameters symbolic. Each tensor's group must be UNSAT over a feasible base; anything else falls through.
• T1, this launch's parameters and any grid: first content-free (every loaded value free; its UNSAT is a proof for any contents) when a term reads a loaded value, then with the snapshots. A counting query the solver cannot scope to any grid retries at the launch's grid.
• T1-launch: when the any-grid query finds races, only those pairs are asked again with the grid pinned. UNSAT proves the kernel as launched, and the any-grid races are kept as grid-fragility evidence. When Z3 does not decide that requery, the config is unsupported (timeout / unknown) and the any-grid races are evidence only: they may lie outside the launch's grid.
• Width obligations. An any-grid proof's qualifier names the widths whose obligations can fail in its domain (one query). Whatever the rung, they are then discharged at the launch (its parameters and grid; a T0 proof through a launch encoding of the kernel): when one can fail there, or Z3 cannot tell, the config is unsupported (integer-overflow, or timeout), since the unbounded reading it proved is not what this launch computes. So tl.store(out + ((pid * 2**30) // 2**30) % 3, 1) is proved with the qualifier at grid 2 and refused at grid 3, where program 2 wraps to element 0. A content-free T1 attempt refused this way leaves the snapshot attempt to decide.

Not in this PR

• Witness replay (confirming a race by running the two witness programs in the interpreter, [FEAT] [RACE DETECTOR] Z3-based race detector #361's C2), with its watchdog and footprint recorder: the next PR. A race here is the solver's witness.
• [FEAT] [RACE DETECTOR] Z3-based race detector #361's differential footprint cross-check: not ported.
• The shared-memory (TTGIR) track and the PTX barrier gate: later.
• cuTile and token order; LAUNCH = "run"; several IR targets in one trace.
• Any change to the compiled sanitizer's behaviour.
• [FEAT] [RACE DETECTOR] Z3-based race detector #361's evaluation-only switches (level ladder, ablations, the fence-order switch, telemetry bindings) and its _snapshot_constant, which specializes a loop bound that is constant over a correlated table (rowptr[pid + 1] - rowptr[pid]); constant offsets still fold through snapshot_lookup.

Known limitations

• Kernels are not run, so a later launch whose arguments or index tables the script computes from an earlier kernel's output is analyzed with the unwritten values (as in the compiled sanitizer).
• A proof with assumes no i32 overflow holds where the obligations hold; they hold at this launch, but may fail at another grid (or, at T0, other parameters) in the scope it names.
• "Any grid" in a scope is any extent along the grid axes the kernel reads; along an unread axis the analysis keeps the launch's extent (blocks that differ only there behave alike, except with atomics, whose axes stay symbolic where there is no launch extent and at T0). A store that reads no program id, proved at grid 1, races at grid 2.
• Width obligations cover what the reader lists (path, mask, offset, loop bounds) and an await's exit predicate. An RMW's written value (atomic_xchg(flag, pid * BIG)) can wrap without a premise; a wrap-capable RMW chain falls to the solver's unknown read-from. The CAS gate refuses arithmetic, so CAS operands cannot.
• A barrier after an early return (store; if p >= n: return; barrier; load) orders nothing: the block-path prefix rule does not reach across cf blocks, so the pair races ([FEAT] [RACE DETECTOR] Z3-based race detector #361 proved it). A grid-stride loop (step = tl.num_programs(0)) is refused as loop-bound even with a concrete launch grid.
• Division keeps its sign branches where a bound needs more than the unconditional domains: a quotient by a divisor of unknown sign (the min(grid_m - group_id * GROUP_M, GROUP_M) group size of a grouped swizzle) has no bound, so a remainder of it downstream is the truncating encoding.
• An unsigned index table with a value of 2**(bits-1) or more has no usable snapshot (an address on it is indirect-address).
• Snapshots are taken for every readable integer tensor argument, including ones the kernel writes and views of a larger allocation, which are never read; they still count against the 256 MiB cap and the dedup key.
• An autotune Config.pre_hook does not run under LAUNCH = "skip", so a verdict that reads tensor contents read them as the launch began, not as a config's pre_hook would leave them.
• The spin loops of an awaiting kernel are assumed to terminate (assumes termination).
• A Z3 timeout can depend on the machine's load; a timed-out config is unsupported (timeout).
• Every launch is solved again; there is no cross-launch memo (up to 120 s per T1 query).
• Solves are serialized process-wide, so traced launches on several host threads wait for each other.

Tests

TTIR is compiled at test time; crafted texts are inlined; no .ttir files are checked in.

• tests/unit/race_detector/compiled_kernels.py: 47 small kernels and their signatures, ttir() / graph() through tests/unit/ir/ttir_corpus.py (cuda:89). Every kernel is built with real_jit, which pins knobs.runtime.interpret off around triton.jit (as ttir_corpus._load does), so the kernels are JITFunctions even when tests/unit/test_multithreading.py (which sets TRITON_INTERPRET=1 on import) is collected first.
• tests/unit/race_detector/test_compiled_analysis.py (33 rows, analyze_graph directly): one race per class between two programs (WAW, RAW, WAR, atomic vs load) with their source lines; a proof per rung (T0 with and without the qualifier, T1, T1-launch with grid-fragile evidence and its racing grid-3 twin); aliased views of one buffer race (no T0); a loaded mask proved by the content-free attempt without the content qualifier, and the same mask with no snapshot as a possible race only; a snapshot proof with the content qualifier, a duplicate index that races, the refusal without a snapshot, a view of a larger allocation refused, a table the kernel writes refused, and a masked load's other racing; fences (unfenced race, global barrier proved, conditional barrier races, loop barrier orders one iteration only, a back-edge barrier orders all); dependency order (in place proved, shifted races, a load → exchange → store chain proved, the same chain through a masked-off atomic racing); tiles whose lanes no variable names (B lanes on one element, a broadcast row pointer) racing beside their named or masked twins; awaits (an acquire spin proved, assuming termination; a relaxed poll, a poll for the initial value and a skipped poll race; a wrapping exit value racing at grid 5 and proved at the launch at grid 2); a counting while refused with spin-shape; a CAS lock; four fenced CAS handoffs; the CAS gate (extui of a comparison accepted, a narrowing cast and arithmetic refused, a CAS in a loop control-flow); an early return, two sequential loops and their overlapping twin, nested loops, an in-place update after a read-only loop and inside a second loop (both proved at T0); width obligations (a loop under a branch whose bounds wrap only where it is not reached, the Select-guarded premise of tl.where(pid >= 2, 0, pid * 2**30 // 2**30) racing at grid 3, a qualified T0 proof at grid 2 and its refusal at grid 3, a qualifier naming both i32 and i64 where no one execution wraps both, a launch that wraps refused); a timeout; an undecided launch-grid requery unsupported (timeout) with the any-grid races as evidence only; a cancelled query raising KeyboardInterrupt.
• tests/unit/race_detector/test_compiled_rules.py (35 rows): the pid-rename contract; // and % without sign branches exactly where they equal the truncating encoding (9 cases: non-negative, non-positive and unknown dividends, positive, negative, zero and unknown divisors, a lane and a select dividend), proved equal to it under the domains; lanes keyed by (dim, extent), the reader's tile shape and the lane position; signed parameters and symbolic T0 parameters; the unmodeled-value refusal; snapshot width rules, the signed reading and the unsigned refusal; 4 accepted spins and 10 spin-shape refusals; the failed polls of an await: a cta-scope reset of the flag (WAW) and a plain read of it (WAR) race the pre-exit representative, the no-reset and gpu-scope reset twins are proved; the barrier address-space rule end to end; fence epoch forms.
• tests/end_to_end/test_compiled_race_detector.py (49 rows, through tilelens.trace(RaceDetector(compile=True)) on CPU tensors with the driver unreachable):
  • one race per class: the records, Launch.records, the per-config counts and the printout;
  • a verdict table of 25 rows: status, rung, scope, qualifiers and refusal kind for each rung, the content qualifier, fences, dependency order, awaits, spin-shape, the CAS gate, an early return, several loops, a loop under a branch, the width qualifier, the guarded premise, the any-grid proof refused at a launch that wraps, potential-race;
  • a possible race beside a race is withheld, with the launch's note; the snapshot element bound (snapshot-bound) and the launch's byte cap;
  • the barrier recorded, and rewritten to shared memory only through inject_ttir, races;
  • a timeout is unsupported (timeout); an undecided launch-grid requery records the verdict alone, no CompiledRaceRecord, with the evidence in grid_fragile;
  • autotune: a num_ctas=2 config compile-failed beside a proved one; a racing config beside a compile-failed one makes the launch races; configs proved at T0 and T1-launch give the launch scope this-params-this-grid; three configs, two sharing a TTIR, solved twice; bindings of one specialization that differ only in grid or only in snapshot contents solved apart;
  • two host threads' traced launches analyzed in turn (without the lock this crashes the process);
  • the not-analyzed part printed once without verbose, and the race-free line only under verbose;
  • verdicts, races and grid-fragile evidence survive tilelens.save() / load();
  • fenced CAS publications and the comm/comp pattern ([FEAT] [RACE DETECTOR] Z3-based race detector #361's compiled tests that fail on Triton 3.8, rewritten): five fenced CAS publications proved, the comm/comp pattern proved assuming termination;
  • tile-race --compile on a script (subprocess).
• tests/unit/ir/inject.py: inject_ttir(traced, text_or_fn).
• tests/unit/ir/test_lowering.py: a client's divrem encodes every quotient and remainder.
• tests/unit/test_race_detector.py: RaceDetector(compile=True) is a CompiledRaceDetector; SymbolicRaceDetector(compile=True) raises; the flag off gives the NullRaceDetector.

Commands, Triton 3.8.0, CPU only (CUDA_VISIBLE_DEVICES="", UV_NO_SYNC=1):

uv run --extra test pytest tests/unit/ir tests/unit/sanitizer_compiled tests/end_to_end/test_compiled_sanitizer.py tests/end_to_end/test_ir_lifecycle_compiled.py tests/end_to_end/test_ir_client.py tests/unit/test_ir_lifecycle.py -q -p no:cacheprovider [-n 4]
uv run --extra test pytest tests/unit/test_race_detector.py tests/end_to_end/test_race_detector.py tests/unit/race_detector tests/end_to_end/test_compiled_race_detector.py -q -p no:cacheprovider [-n 4]
uv run --extra test pytest tests -q -p no:cacheprovider

The base is a pristine worktree of #528's head (fca42ef) with the same setup.

run	base fca42ef	this PR
IR and compiled-sanitizer tests, serial and -n 4	718 passed, 4 skipped	719 passed, 4 skipped
race detector tests, serial and -n 4	189 passed	306 passed
regression gate (the 20 files of #501–#505), serial and -n 4	595 passed, 2 skipped	595 passed, 2 skipped
full tests/, serial	1356 passed, 11 skipped	1474 passed, 11 skipped

The 118 new rows are the 68 race detector unit rows, the 49 end-to-end rows and the lowering row above. The new tests also pass with tests/unit/test_multithreading.py collected first (127 passed).

A pre-existing order leak, not from this PR: tests/unit/test_patch_scope.py::test_scope_restores_tensor_descriptor_base_builtins followed by ::test_patch_lang_restores_core_reduce_scan_from_tl_kernel leaves triton.language patched, so every later host compile in that process fails (host-compile-unavailable, "'block_argument' object has no attribute 'dtype'"). Under -n 8 the scheduler sometimes puts the two on one worker without the rest of their file; then that worker's compiled tests fail. On the base, the same two tests before tests/end_to_end/test_compiled_sanitizer.py fail 57 of its 66 tests. It is left for a separate fix.

Compiled sanitizer unchanged. The 977 Triton 3.8.0 TTIRs of #509–#528, each parsed with the default reader and checked with check_graph under #509's synthetic binding, against a pristine worktree of #528's head: the 527 graphs are identical apart from the new AccessEvent.shape field (their reprs compared with it removed), the 450 refusals are identical, and so are all 6668 Z3 queries (Solver.sexpr() at every check) and the findings, refusals and abstentions in kind, access, base, line and loc. The full result reprs, witnesses included, are identical in some runs; in others one witness differs, that of the c_ptr store of tb_matmul_dequantize (element offset 4096 or 8064). It differs the same way between two runs of the pristine base: it is the Z3 model choice #528 reports for its base and its head.

#361's unit suites, as a baseline (not committed; measured on this PR's first revision, before the review fixes): test_t1_global_races, test_multipath_races, test_route2_snapshot_select, test_await_abstraction and test_compiled_cas from 62c6d7c, run against this code through a shim of #361's API (crafted texts given argument names, five invalid texts fixed, tl.debug_barrier added where a test relied on #361's program-order default): 90 passed, 47 failed, no verdict different. The 47: 20 call #361's client API and 11 its evaluation harness; 1 is a replay watchdog test (next PR); 2 use texts that are invalid MLIR; 4 read the AccessEvent.awaited field the reader no longer has; 3 test the single-path mode, which is gone; 3 count local constraints, which the width premise adds one to; 3 match #361's refusal wording; 1 expects a refusal the reader now raises while parsing.

Validation

Row by row against #361's compiled (static) track at its shipped level, on the 207-row Triton 3.8.0 sample used for the earlier PRs of this stack. The oracle is #361 (62c6d7c) run through its own harness (run_one at its shipped level, the host-compiled TTIR rewritten ttg.barrier all -> gpu.barrier, which #361 does not read on 3.8). Its witness replay (confirmation) is ignored; it comes with the next PR. This PR runs each row's launch under tilelens.trace(RaceDetector(compile=True, target="cuda:80")): host compile only, CPU tensors, no GPU. cuda:80 is the target #361's harness compiles for on a host with no GPU. The spec loader and argument binding are the oracle's; no TTIR is rewritten for this PR. Rows ran 16 at a time.

Compared per row: the status; for a proof, the rung and the content / termination qualifiers (proved@T1-launch+content, ...); for races, the set of witnesses (race type, first line, second line).

This PR's first revision had three port bugs, found by this validation and fixed in this revision (below). On this revision:

	rows
identical	199
compile failure on sm80, named differently	3
reader reads more	1
rung T1 -> T1-launch (open-world read-from)	4

Two runs of this revision give this table; between them only the witness program ids of two racing rows differ (Z3's model choice), with the same race pairs.

• Compile failures (3). Two fp8e4nv kernels and liger's tl.float32(...) fail to compile for cuda:80. [FEAT] [RACE DETECTOR] Z3-based race detector #361's harness records a compile error; this PR records unsupported (compile-failed). It is the same failure under this PR's name.
• The reader reads more (1). fla_ttt_fused_chunk loads through a pointer that an scf.if yields. [FEAT] [RACE DETECTOR] Z3-based race detector #361's reader refused it ("load of a non-pointer value"); this stack's reader reads it. The kernel is proved at T1 (assuming no i32 overflow). The load is of eta, which the kernel never writes.
• T1 -> T1-launch (4): trb021_guarded_acq_rel_no, trb021_role_specific_order_no, trb022_acquire_on_failure_no, trb026_fenced_tile_handoff_no. At grid 3 the any-grid query finds a RAW whose read-from source is a third program's CAS ([FIX] Close two false proofs in the race detector's two-copy model #505's open-world read-from). At the launch's grid (2) that query is UNSAT, so these rows are proved at T1-launch, with the grid-3 RAW kept as grid-fragile evidence. The grid-3 report over-approximates: the third program's CAS succeeds only after it reads the producer's release, so it extends the producer's release sequence. This difference was registered in advance.

The port bugs, and what changed with each fix:

• False races between an in-place load and its store (4 rows). fla_delta_rule_fused_recurrent (bwd), fla_gated_delta_rule_chunk and fla_gated_delta_rule_chunk_varlen (prepare_wy_repr_bwd), fla_simple_gla_parallel (bwd): [FEAT] [RACE DETECTOR] Z3-based race detector #361 proves each of them, and the first revision reported a WAR inside one program between an in-place tl.load(p) and the dependent tl.store(p, ...). In the witness both copies were at the same lane and the same iteration of the accesses' own loop, and differed only in the iteration index of another loop. Encoder._record put the iteration variable of every loop of the kernel in each record's copy_local_vars, which the solver reads as the record's loop iterators, so a dependency-ordered pair could "differ in iteration" in a loop neither access is in. Minimal repro: a loop that only reads, then v = tl.load(p); tl.store(p, v + acc) after it or inside a second loop (the one-loop twin was proved at T0). A record now lists only its own loops, plus the loops of an awaited poll, whose premise every record carries. The four rows match [FEAT] [RACE DETECTOR] Z3-based race detector #361; the repro is a regression test (read_loop_then_inplace, proved at T0 both ways).
• An undecided launch-grid requery reported as races (1 row). tritonbench_meta_gemm _splitk_kernel: [FEAT] [RACE DETECTOR] Z3-based race detector #361 proves it at T1-launch, in a 46 s row. Here the any-grid query finds a WAW, and in the first revision the requery at the launch grid took 104 to 142 s alone (170 s with 16 rows running), against the 120 s T1 timeout. When it did not finish, the config was reported as races with the any-grid witness, programs (1792, 0, 0) and (1792, 1, 0), neither a program of the launch's grid (2048, 1, 1). [FEAT] [RACE DETECTOR] Z3-based race detector #361 did the same. An undecided requery now makes the config unsupported (timeout / unknown), with those races kept as grid_fragile evidence only (unit and end-to-end regression tests).
• The division encoding (same row, and slow rows). The shared lowering encodes // and % as truncating division with sign branches, even for a constant positive divisor and a program-id dividend; on the kernel's grouped program-id swizzle this is what made the requery slow (with a measurement-only Euclidean // and % everywhere, the row was proved in 37 s). The divrem hook and BoundedDivRem (Change, section 4) bring back [FEAT] [RACE DETECTOR] Z3-based race detector #361's bounds-guided division. _splitk_kernel is now proved at T1-launch in 16 s in the 16-row run (20 to 39 s in four more runs beside other jobs; in the 39 s one the requery took 34 s), as [FEAT] [RACE DETECTOR] Z3-based race detector #361 proves it. tut03_matmul_leaky_relu takes 3.1 s, against 15.0 s on the first revision and 2.0 s for [FEAT] [RACE DETECTOR] Z3-based race detector #361. The rows' analysis times add up to 505 s (525 s in a second run), against 702 s for the first revision with only the false-race fix. Apart from this row, no status, rung or witness changes.

One more defect showed up in the same comparison: the width qualifier named the widths that fail in one model of the obligation query, so which widths it named depended on Z3's model choice (between two runs with different division encodings, one proof went from i32/i64 to i32 and another from i32 to i32/i64). It now asks again until no further width can fail; 15 proofs name one more width (i32/i64 where one was named), with no change in status, and a regression row (two_widths, whose i32 and i64 products wrap on disjoint paths) checks it. The width qualifier appears on 79 of the 123 proofs (assumes no i32 overflow on 55, assumes no i64 overflow on 6, both on 18).

Race-labelled rows: the sample has 52 rows labelled race; the port reports races on all 52. None is proved race-free.

Advance-registered differences that did not show up in this sample: the conditional-fence and loop-fence rules, launch-time width refusals (the rv_* rows are not in the sample), lane keying, and the CAS extui gate.

After the fixes the race detector suites, the IR suites, the regression gate and the compiled sanitizer equivalence were run again (the Tests numbers above are this revision's).

Driver: run_row_compiled.py (one row) and compare.py, in the validation scratch directory.

Line counts

From git diff --numstat against #528's head (fca42ef):

file	added	deleted
tilelens/clients/race_detector/compiled/global_records.py (new)	1109	0
tilelens/clients/race_detector/compiled/client.py (new)	674	0
tilelens/clients/race_detector/compiled/leaves.py (new)	635	0
tilelens/clients/race_detector/compiled/analysis.py (new)	443	0
tilelens/clients/race_detector/compiled/fences.py (new)	155	0
tilelens/clients/race_detector/compiled/awaits.py (new)	101	0
tilelens/clients/race_detector/compiled/__init__.py (new)	8	0
tilelens/clients/pids.py (new)	46	0
tilelens/clients/race_detector/data.py	72	0
tilelens/clients/race_detector/race_detector.py	27	6
tilelens/clients/race_detector/hb_common.py	7	0
tilelens/clients/race_detector/two_copy_symbolic_hb_solver.py	7	8
tilelens/clients/symbolic_engine.py	5	5
tilelens/clients/sanitizer/compiled/client.py	13	84
tilelens/clients/sanitizer/compiled/oob.py	3	2
tilelens/ir/capture.py	96	1
tilelens/ir/lowering.py	31	6
tilelens/ir/ttir_reader.py	7	0
tilelens/wrapper.py	17	4
tilelens/clients/__init__.py	13	0
product total	3469	116
tests/unit/race_detector/compiled_kernels.py (new)	583	0
tests/end_to_end/test_compiled_race_detector.py (new)	572	0
tests/unit/race_detector/test_compiled_analysis.py (new)	370	0
tests/unit/race_detector/test_compiled_rules.py (new)	355	0
tests/unit/ir/inject.py (new)	69	0
tests/unit/ir/test_lowering.py	12	0
tests/unit/test_race_detector.py	9	5
test total	1970	5
README.md	30	0

The tests add fewer lines than the product. About 80 of the product lines are moved, not new: the two config helpers leave the compiled sanitizer's client for tilelens/ir/capture.py.

[github-actions]

Performance Benchmark

Benchmark	main (min)	PR (min)	Change	Samples
gemm	0.102s	0.103s	+0.8%	20 / 20
gemm_oob	0.113s	0.115s	+1.6%	20 / 20
indirect_load	0.021s	0.022s	+2.2%	20 / 20
nested_loop	0.228s	0.228s	-0.0%	20 / 20
block_pointer_loop_advance	0.121s	0.123s	+1.1%	20 / 20
liger_jsd	0.134s	0.136s	+2.0%	20 / 20
flaggems_layernorm	0.382s	0.387s	+1.2%	20 / 20
swiglu	0.165s	0.166s	+0.7%	20 / 20
cross_entropy	0.940s	0.950s	+1.1%	20 / 20
fused_linear_jsd	0.205s	0.208s	+1.6%	20 / 20
Total	2.411s	2.436s	+1.1%	N/A

Iterations: 1 warmup + 20 measured
Samples are shown as main / PR; long pytest benchmarks may use fewer samples.