[FEAT] Add the race detector's TTIR reader facts by mark14wu · Pull Request #509 · Deep-Learning-Profiling-Tools/tilelens

mark14wu · 2026-10-14T20:45:15Z

Summary

This PR adds the TTIR reader facts that the compiled race detector (a later PR) needs. The facts are neutral: the reader reports what the IR says and puts no race-detector policy in. The compiled sanitizer, the reader's only client today, gets the same graphs and the same results as before (see Fact validation).

Stacked on #505 (top of #507 → #494 → #479 → #495 → #480 → #482 → #501 → #503 → #504 → #505). Triton 3.8 only. One commit.

Each fact is read from Triton's MLIR bindings: the walk's attribute table gets new rows, and nothing new is read from the text.

Change

1. Atomic attributes (`_mlir_walk._ATTRS`)

Six attribute rows under three new op keys, each read with get_int_attr and checked against a closed vocabulary, the same way the walk already reads arith.cmpi's predicate:

tt.atomic_rmw: atomic_rmw_op 1..10 = and, or, xor, add, fadd, max, min, umax, umin, exch; sem 1..4 = relaxed, acquire, release, acq_rel; scope 1..3 = gpu, cta, sys;
tt.atomic_cas: sem, scope;
ttg.barrier: addrSpace, which is a bit enum and is kept as its bits (local 1, global_read 2, global_write 4, tensor_read 8, tensor_write 16; all, which tl.debug_barrier() prints, is 31).

All of these are inherent attributes that the op verifiers type as signless i32, so get_int_attr cannot hit its assertion. An integer outside the vocabulary makes the module misaligned, as for the existing rows. The reader reports the printer's keywords (exch, not xchg).

2. Per-access facts (`AccessEvent`)

atomic: AtomicInfo(rmw_op, sem, scope), set exactly on atomics (rmw_op is None for CAS).
atomic_val and atomic_cmp: the operands in ODS order, tt.atomic_rmw (ptr, val, mask?) and tt.atomic_cas (ptr, cmp, val), each as a Term, or None when the operand is loaded data, a float or a pointer.
elem_float: whether the accessed pointer's pointee is neither an integer nor a pointer, read at the access, so a float type the walk does not list still reads as float. FuncArg gets no such field. This differs from [FEAT] [RACE DETECTOR] Z3-based race detector #361 by design: [FEAT] [RACE DETECTOR] Z3-based race detector #361 read the base parameter's pointee. The two disagree on width-preserving pointer bitcasts: the fmax atomics of golden_atomic_fmax go through i32 views of an f32 pointer and report False here (an integer observation, which is also how the reader binds their results). [FEAT] [RACE DETECTOR] Z3-based race detector #361 refuses that text, so the corpus shows no atomic disagreement.
deps: now a declared field. It lists the earlier loads and atomics whose result reaches the access's value operands lane for lane: a store's value and mask, an atomic_rmw's val and mask, an atomic_cas's cmp and val. Loads have (). The walk runs backwards over the bindings' def-use edges and is memoized per value:
- a load's or atomic's result is that access's own;
- element-wise ops keep every operand's: arith.*, math.*, tt.precise_*, tt.addptr, tt.bitcast, tt.fp_to_fp, tt.int_to_ptr, tt.ptr_to_int, tt.clampf, tt.mulhiui, tt.extern_elementwise and tt.elementwise_inline_asm;
- tt.dot keeps only its accumulator's;
- arith.select keeps its condition's, plus those that both arms have;
- every other op (splat, broadcast, reductions, ...), region results and block arguments keep none;
- an access's operands unite: a source counts if it reaches any of them lane for lane, since the access reads every operand at that lane.
deps adds happens-before edges, so it must be exact or narrower, never wider. The per-op rules match [FEAT] [RACE DETECTOR] Z3-based race detector #361's. Two results differ from [FEAT] [RACE DETECTOR] Z3-based race detector #361, both on shapes the 977-TTIR corpus does not contain:
- Operands unite. [FEAT] [RACE DETECTOR] Z3-based race detector #361 took the AND of a source's per-operand flag across the access's operands. For tl.store(out + offs, x, mask=tl.sum(x, 0) > 0) this reader gives (0,) (the value reads x lane for lane) and [FEAT] [RACE DETECTOR] Z3-based race detector #361 gives (). This is a wider edge than [FEAT] [RACE DETECTOR] Z3-based race detector #361's but an exact one: the store reads both operands at the lane, they are not alternatives. A test row pins it. Because it widens a happens-before edge relative to the frozen reference, it is called out here for review.
- Element-wise ops with several results. For %2:2 = tt.elementwise_inline_asm ... packed_element = 1 stored through %2#0, this reader gives the asm's operand as a dep and [FEAT] [RACE DETECTOR] Z3-based race detector #361 gives none (its text reader keyed provenance by %2 while the uses read %2#0). The dep is correct for one element per pack.
A packed inline asm (packed_element > 1) counts as element-wise in both readers, although the asm sees its whole pack and could permute inside it. The lanes of one pack sit in one thread, so a same-position pair stays in that thread. All 5 inline asms in the corpus have packed_element = 1.
block_path: the access op's Op.path, the block indices from the module body down to the access's own block.

3. Per-graph facts (`AccessGraph`)

pid_axes: every axis that a tt.get_program_id or tt.get_num_programs reads anywhere in the module, including one whose value reaches no modeled term and one inside a tt.reduce/tt.scan combine region (which the builder does not walk). It is read from the walk's ops, not from the ops the builder visits, because a consumer that pins an unread axis to 1 must not miss one.
fences: a Fence for every ttg.barrier. Until now the reader listed it as inert and dropped it. Each fence records:
- position, which is len(accesses) - 0.5 at the barrier;
- the op name and its addr_space bits;
- path, guarded and in_loop, read the same way as an access's;
- block_path, line_no and loc.
The block path is what the race detector's fence rule needs: a fence orders a < f < b only when its block path is a prefix of both accesses' block paths. That rule, and which addrSpace bits order global memory, belong to the race detector. The sanitizer does not read fences. A barrier inside a tt.reduce/tt.scan combine region stays inert and gives no Fence, as before (a test pins it), and an scf.while there gives no WhileRegion. That is the safe direction for a happens-before consumer: one fewer fence orders fewer pairs, and combine regions hold no accesses.
observed_indices(term, graph): the access indices of the Observed leaves that term reaches. It follows loop-carried pointers (an IterArgOffset's offset0 and delta), the same walk as mentions_observed. [FEAT] [RACE DETECTOR] Z3-based race detector #361's version stopped at IterArgOffset.

4. `scf.while`, opt-in (`parse_ttir(text, while_regions=True)`)

With the option off (the default, and what the sanitizer uses), scf.while is still refused as control flow, with the same message. With it on, each scf.while becomes a WhileRegion in graph.whiles with:

its line_no and loc;
the access indices of its before region;
the scf.condition Term (None when it is loaded data);
the op names of its after region, scf.yield included, and that region's access indices;
whether it has iter args or results (carries);
the enclosing WhileRegion (parent), its block_path, and its before and after block indices (blocks), so an op or fence is inside the loop when its block path extends block_path with one of them.

The accesses themselves are ordinary entries of graph.accesses. in_loop still means "inside the scf.for". Inside the before region, an integer tt.load result (a volatile poll included) binds as Observed(index), the way atomic results already do; the Observed docs now say an observation can index a load. Region arguments and results are loop-carried DataDeps. An scf.for inside a while region refuses as a nested loop. Which while loops count as an await (the spin-shape rules) is for the race detector to decide. A text without scf.while gives an equal graph with the option on or off.

5. `ArtifactLog.record` returns the binding it records

Returning the binding lets the race detector tie the values it captures in before_launch to the LaunchBinding that the log stores.

Not in this PR

Loaded terms, multipath/cf blocks, several loops and DataDep.keep. These belong to a later PR.
Any race-detector policy: spin-shape rules, the fence ordering rule, addrSpace policy, the exch → xchg mapping.
LoopInfo.induction_var. Only [FEAT] [RACE DETECTOR] Z3-based race detector #361's TTGIR reader used it, and LoopVar already names the induction variable.
New IR stages, and any change to the compiled sanitizer.

Tests

The unit tests read TTIR that is compiled at test time. Seven kernels are added to tests/unit/ir/reader_kernels.py; no .ttir files are checked in.

test_ttir_reader.py:
- test_atomics_carry_their_attributes_and_operands: every rmw op, every sem and scope, and a CAS; atomic_val / atomic_cmp as Terms, and None for loaded or float operands; elem_float at the access (the fmax atomics of golden_atomic_fmax go through i32 views of an f32 pointer).
- test_observed_indices_reach_through_loop_carried_pointers: an observation in an iter-arg's offset0 and in its delta.
- test_pid_axes_are_every_axis_read: axes that reach only a stored value, and a program id and a barrier inside a tt.reduce combine function (pid_axes == {0, 1}, no Fence).
- test_barriers_are_fences_among_the_accesses: positions, addr_space (including local and global_read|global_write), path, guarded, in_loop, line/loc, and block-path prefixes: a fence is a prefix of exactly the accesses in its block.
- test_deps_are_the_loads_a_value_reads_lane_for_lane: each rule. Element-wise ops keep their deps (arith.*, math.exp, tt.bitcast); select by condition, by both arms, and by one arm each; a tt.reduce, a splat of a scalar sum, an scf.if result and an scf.for loop-carried value drop their deps; a load masked by a loaded value has (); the operands of one access unite; tt.dot keeps only the accumulator's; a store's value and mask; rmw val and mask; cas cmp and val; an atomic's result; a splat. It also checks elem_float on f32 stores.
- test_while_regions_are_read_only_on_request. Off: a control-flow refusal. On:
  - a volatile poll, a poll under a modeled branch, and a nested poll (parent), each condition over Observed;
  - from the existing walk corpus, a CAS spin and a loop that carries a value;
  - no change for texts without scf.while, and the option passed through ParseCache.
test_mlir_walk.py: the generic-form tt.atomic_rmw reads its three attributes.
test_oob.py, test_the_race_detector_facts_change_no_check: check_graph returns the same result with fences, deps, block paths and pid_axes stripped, once on a clean launch and once on a launch with findings.
test_ir_capture.py: record returns the binding that specializations lists.

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

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]

run	base `a3847f7`	this PR
IR and compiled-sanitizer tests, `-n 4`	606 passed, 4 skipped	626 passed, 4 skipped
the same, serial		626 passed, 4 skipped
regression gate (the 20 files of #501–#505), `-n 4`	594 passed, 2 skipped	595 passed, 2 skipped
the same gate, serial		595 passed, 2 skipped

The 20 new IR rows are the six reader tests, thirteen parametrized rows for the new kernels and the test_oob row. The gate gains the test_oob row.

Fact validation

Method. The corpus is the 977 Triton 3.8.0 TTIRs that were host-compiled for the race detector's validation roster (16 corpora). Each text is read three ways:

by this PR's reader, both with while_regions=True and with the default;
by [FEAT] [RACE DETECTOR] Z3-based race detector #361's frozen text reader (62c6d7c, used as is) on the same text, with ttg.barrier all rewritten to gpu.barrier because [FEAT] [RACE DETECTOR] Z3-based race detector #361 only knew gpu.barrier.

Graphs are compared access by access, in order. Terms are compared in canonical form, which strips widths, sites, IntCast wrappers (#361 has none) and arange dims (the 3-D make_range fix). #361 has no block paths, so those are not compared.

Parse status. Both readers parse 556 texts (39 of them with scf.while) and both refuse 410. Eleven texts differ, and they differ the same way before this PR:

this reader parses 10 texts that [FEAT] [RACE DETECTOR] Z3-based race detector #361 refuses (9 "non-pointer value" refusals, 1 indirect address);
it refuses 1 that [FEAT] [RACE DETECTOR] Z3-based race detector #361 parses (an impure inline asm).

Agreement on the 556 graphs (2708 accesses; the access kinds and bases line up in all 556):

fact	agree	disagree
atomic op / sem / scope (114 atomics)	2708	0
`atomic_val` presence; equal Term where present (112)	2708	0
`atomic_cmp` presence; equal Term where present (22)	2708	0
`deps` (378 non-empty)	2708	0
`elem_float`	1942	766
`observed_indices` of offset, mask, path, val and cmp (41 non-empty)	13540	0
`pid_axes`	556 graphs	0
fences: count and positions (113 fences)	556 graphs	0
while regions vs #361's awaits (40 loops in 39 texts)	39 texts	0

elem_float: all 766 differences are stores to a float pointee. [FEAT] [RACE DETECTOR] Z3-based race detector #361 never set elem_float on a store (its store path does not pass the pointee), while this reader reports the pointee for every access. Every load and atomic agrees, and those are the only accesses the race detector reads the field on.
Fences: all 113 have addr_space 31, 56 have a path, and none is guarded or in a loop. [FEAT] [RACE DETECTOR] Z3-based race detector #361 records positions only.
While regions: each of the 40 regions has one before-region access, an scf.yield-only body and no carried values. Its access is exactly [FEAT] [RACE DETECTOR] Z3-based race detector #361's awaited access, and [FEAT] [RACE DETECTOR] Z3-based race detector #361's exit_pred equals Not(cond). The other 3 texts with scf.while are refused by both readers. The option changes nothing on the 935 texts without scf.while.
observed_indices: no observation in this corpus is carried by a loop pointer, so the graph-aware walk finds no more than [FEAT] [RACE DETECTOR] Z3-based race detector #361 here. test_observed_indices_reach_through_loop_carried_pointers covers that case.

The sanitizer is unchanged. The default parse_ttir was run on all 977 texts at this PR and on a pristine a3847f7 (with the new fields stripped):

the 527 parsed graphs are identical;
the 450 refusals are identical in kind, message, line and loc;
check_graph under one synthetic binding (4096-element tensors, scalars 64, grid (4, 2, 1)) returns identical results on all 527 graphs, 268 of them with findings.

A second binding (37-element tensors, scalars 300, grid (3, 1, 2)) gives the same finding kinds, access indices, refusals and abstentions on all 977 rows. Two tritonbench matmul kernels return different witness lanes and violation offsets there, but two runs of the pristine base differ in the same way: it is Z3's run-to-run choice of witness, not this PR.

Line counts

From git diff --numstat against a3847f7:

file	added	deleted
`tilelens/ir/ttir_reader.py`	298	24
`tilelens/ir/_mlir_walk.py`	23	4
`tilelens/ir/capture.py`	4	1
`tilelens/ir/lowering.py`	1	1
product total	326	30
`tests/unit/ir/test_ttir_reader.py`	178	1
`tests/unit/ir/reader_kernels.py`	147	0
`tests/unit/sanitizer_compiled/test_oob.py`	14	0
`tests/unit/ir/test_ir_capture.py`	2	1
`tests/unit/ir/test_mlir_walk.py`	2	0
test total	343	2

The tests are 17 lines over the product. The overrun is the deps test (18 of the lines added in review): deps is the one fact where an error points in the unsound direction, because a wrong dep adds a happens-before edge and can hide a race. So each rule has a row that fails when the rule is widened or narrowed: math.* and tt.bitcast as element-wise ops, a real tt.reduce, a load whose mask is a loaded value, a loop-carried value, and the operand union.

Read the facts a compiled race detector needs from the TTIR, without any race-detector policy in the reader and without changing what the compiled sanitizer sees: - the walk reads tt.atomic_rmw's atomic_rmw_op / sem / scope, tt.atomic_cas's sem / scope and ttg.barrier's addrSpace bits through get_int_attr, each against a closed vocabulary; - AccessEvent.atomic (AtomicInfo), atomic_val / atomic_cmp as Terms, elem_float from the accessed pointer's pointee, block_path, and a declared deps: the earlier loads and atomics whose result reaches a store's value and mask, an atomic_rmw's val and mask or an atomic_cas's cmp and val lane for lane, the operands united (element-wise ops keep it, tt.dot only through its accumulator, arith.select through its condition or both arms, anything else and region results drop it); - AccessGraph.pid_axes (every program-id read in the module, combine regions included), and a Fence for every ttg.barrier with its position among the accesses, addrSpace bits, path, guarded, in_loop, block path and loc; - observed_indices(term, graph), which reaches through loop-carried pointers like mentions_observed; - parse_ttir(while_regions=True) reads each scf.while as a WhileRegion (before / after accesses and blocks, the scf.condition term, the body's ops, carried values, nesting) and binds an integer load of its condition region as Observed; by default scf.while is still refused; - ArtifactLog.record returns the binding it records.

github-actions · 2026-10-14T20:49:19Z

Performance Benchmark

Benchmark	main (min)	PR (min)	Change	Samples
gemm	0.106s	0.106s	-0.1%	20 / 20
gemm_oob	0.118s	0.119s	+1.0%	20 / 20
indirect_load	0.022s	0.022s	+0.4%	20 / 20
nested_loop	0.236s	0.237s	+0.5%	20 / 20
block_pointer_loop_advance	0.126s	0.128s	+1.3%	20 / 20
liger_jsd	0.140s	0.140s	+0.2%	20 / 20
flaggems_layernorm	0.394s	0.399s	+1.4%	20 / 20
swiglu	0.171s	0.173s	+1.2%	20 / 20
cross_entropy	0.976s	0.992s	+1.7%	20 / 20
fused_linear_jsd	0.212s	0.215s	+1.5%	20 / 20
Total	2.499s	2.530s	+1.2%	N/A

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

mark14wu added this pull request to stack #508 October 14, 2026 20:45

Navigation Menu

Repository navigation

[FEAT] Add the race detector's TTIR reader facts - #509

[FEAT] Add the race detector's TTIR reader facts#509
mark14wu wants to merge 1 commit into
rd-solver-soundnessfrom
rd-4-reader-facts

mark14wu commented Oct 14, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Oct 14, 2026

Uh oh!

This branch has not been deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

mark14wu commented Oct 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Change

1. Atomic attributes (_mlir_walk._ATTRS)

2. Per-access facts (AccessEvent)

3. Per-graph facts (AccessGraph)

4. scf.while, opt-in (parse_ttir(text, while_regions=True))

5. ArtifactLog.record returns the binding it records

Not in this PR

Tests

Fact validation

Line counts

Uh oh!

github-actions Bot commented Oct 14, 2026

Performance Benchmark

Uh oh!

This branch has not been deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

mark14wu commented Oct 14, 2026 •

edited

Loading

1. Atomic attributes (`_mlir_walk._ATTRS`)

2. Per-access facts (`AccessEvent`)

3. Per-graph facts (`AccessGraph`)

4. `scf.while`, opt-in (`parse_ttir(text, while_regions=True)`)

5. `ArtifactLog.record` returns the binding it records