[FEAT] [RACE DETECTOR] Z3-based race detector#361
Draft
mark14wu wants to merge 107 commits into
Draft
Conversation
Performance Benchmark
Threshold: >5% regression flagged with |
mark14wu
changed the title
mark14wu
changed the title
…st_sanitizer PR #356 moved _range_to_iterator_constraint from sanitizer.sanitizer to clients/symbolic_engine.py, but PR #364 inadvertently restored the old import path in tests/end_to_end/test_sanitizer.py. The symbol no longer exists on sanitizer.sanitizer, so pytest collection fails with ImportError before any test runs. Move the import back to clients.symbolic_engine to match the symbol's current home and restore CI on this branch.
…k false negative (#365)
…ad-dependent mask false negative The counterexample test added in #365 exposed two root causes: 1. SymbolicClient._op_load_overrider / _op_store_overrider concretised any tl.load inside `mask` via `replace_subtree("load")`. Under one-shot symbolic capture, the first block's `flag[0]==1` made `mask = False` the template for every symbolic PID, so the WAW between pid=1 and pid=2 was masked out. 2. IndirectSymbolicExprBase._to_z3_impl returned the pointer expression; LoadSymbolicExpr inherited it. Even with concretisation removed, `v == 0` would lower to `(flag_ptr + pid) == 0`, false because the base address is non-zero. Fix: model tl.load as a value via a per-launch Z3 Array snapshot of the source tensor's contents, accessed by Select(arr, addr). Address-of-event recording stays on expr.ptr._to_z3() so memory events still record pointers, not loaded values. - SymbolicExpr grows a narrow `_load_value_provider` ClassVar hook (plus an owner token to survive nested/exception flows). LoadSymbolicExpr delegates to it when installed; sanitizer is untouched. - SymbolicRaceDetector installs the provider in grid_callback. It builds arr = K(IntSort(), 0); Store(arr, IntVal(base+i*es), IntVal(v_i)) for the source tensor, cached per (base, elem_size, numel, dtype). - Masked loads model `If(mask, Select(arr, addr), other)` with `Implies(mask, domain)` so masked-out lanes don't have to point inside the tensor. Masked load without explicit `other` is unsupported. - _handle_access_check splits address and mask evaluation; mask flows into the event's `active` field instead of being And'd into local_constraints, so the two-copy solver's _lower_record can do proper per-lane lane-value lowering on vector masks. _make_event_signature keys on active_expr to keep loop dedupe correct. - Bidirectional self-write guard using byte-region overlap (not just data_ptr equality) tracks load-source and written regions. Loads from a written region, writes into a snapshotted region, and writes to unresolved targets all mark the launch unsupported. A defensive cross-product sweep runs in post_run_callback. - Race-detector overrides _op_load_overrider / _op_store_overrider to drop the ptr/mask `replace_subtree("load")` concretisation. The pointer-side _reject_data_dependent_address gate now correctly fires for scatter/histogram patterns rather than silently smuggling through first-block-concrete addresses. Unsupported boundaries in v1: non-contiguous, float/complex, numel > 1024, masked load without `other`, and load source overlapping a tensor this kernel writes to. Tests: - counterexample assertion tightened (witness PIDs == {1,2}, witness_addr == out.data_ptr()) - new: masked-load `other`, float dtype unsupported, non-contiguous unsupported (unit), oversize unsupported, write-then-load self-write, load-then-write self-write - test_raw_waw_histogram updated to assert unsupported (the prior detection was via the now-removed unsound concretisation path; the atomic-add variant test_no_race_atomic_histogram already exercises the sound atomic-RMW path) Full suite: 302 passed, 7 skipped.
…ndant histogram writes The fused MoE routing kernel `_combined_routing_fused` calls `_sum_bitmatrix_rows_fused` on every program instance without `tl.program_id`-based partitioning of the output buffer. Every pid writes the same global addresses (WAW even with matching values), and subsequent `tl.load(ExpertHist + pid)` reads race against those writes (RAW). The two phases are collapsed into a single minimal kernel; the detector reports both races with distinct witness pids and addresses inside the histogram tensor. Verified: WAW witness pid_a=0 vs pid_b=1 at hist_base+0; RAW witness pid_a=0 vs pid_b=1 at hist_base+4. last_status == "ok".
mark14wu
changed the title
# Conflicts: # triton_viz/clients/__init__.py
…nch crash finalize() always calls _clear_launch_runtime(), which nulled self.addr_sym. addr_sym is created once in SymbolicClient.__init__ and never recreated, but the next launch's grid_callback dereferences it via _addr_ok_premise(), so the second launch of any traced kernel crashed with an AssertionError. Stop clearing addr_sym: it is an instance-lifetime Z3 symbol, not launch-scoped state. Add e2e regression tests that relaunch a traced kernel (plain racy kernel asserting WAW is detected on both launches, and a loop kernel covering the _loop_hook_after assert).
…iteration races The two-copy solver only alpha-renames vars listed in a record's copy_local_vars, but _loop_hook_after pops the flushed LoopContext before _process_pending_check runs, so the flushed loop's own iterator was never included (empty for non-nested loops). Both program copies were therefore pinned to the same loop iteration: any race between iteration i of block A and iteration j != i of block B forced pid_a == pid_b, which different_blocks excludes — every cross-iteration cross-block race in a loop was silently missed while last_status stayed ok. Fix: include the flushed loop's ctx.idx_z3 in copy_local_vars; its range constraint already travels via iter_constraints -> premises, so the renamed var stays bounded per copy. Renaming is launch-wide per var, so post-loop records that reuse the leftover Python loop variable would get the renamed var with no range premise — an unbounded var producing false positives on race-free kernels. Model the actual semantics instead: after a loop exits, every program instance holds the same final iterator value, so the detector now tracks finished loops and substitutes IntVal(final) into records at capture time. Two lifecycle corners are handled explicitly: - a zero-trip re-activation leaves the leftover variable unchanged, so the previous substitution is stashed on re-entry and restored on a zero-iteration exit; - an inner loop whose final value varies across activations under a still-active outer loop (e.g. range(2 - outer)) has no single correct constant, and deferred records dedupe across those activations — its var is marked unstable and any record still referencing an unsubstituted finished iterator marks the launch unsupported instead of producing a silently wrong verdict. Add e2e regression tests: cross-iteration WAW detected (plain range, tl.range with load+store, nested loops), disjoint-blocks loop kernels stay race-free (iterator range preserved per copy), post-loop leftover iterator (false-positive guard plus a true race where every block stores to out[i_final]), sibling-loop leftover reuse, varying inner final value -> unsupported, and zero-trip re-entry restore.
…d instead of concretizing to block 0 One-shot symbolic capture executes the kernel body for block (0,0,0) only. Host-side control flow on per-instance values was silently resolved with that block's concrete values, producing wrong verdicts with last_status still ok in both directions: - if pid == 0: guarded stores were recorded unconditionally for every PID — a race-free single-writer kernel reported a phantom WAW; - branches the capture block does not take recorded nothing — a real WAW between blocks 1 and 2 behind if pid > 0 reported zero races; - pid-dependent loop bounds (tl.range(0, pid + 1)) were truncated to block 0's trip count via _materialize_loop_value. No path condition is modeled, so the only sound verdict is unsupported: - symbolic_engine.py gains a narrow scalar-concretize observer hook (owner-token pattern like _load_value_provider) dispatched from SymbolicExprDataWrapper._scalar_data, and _on_data_dependent_value now passes the expression being concretized; the engine carries no policy. - SymbolicRaceDetector installs the observer per launch and marks the launch unsupported when the concretized scalar varies per program instance (pid/arange/load/sort/cumsum/atomic ops). Its _on_data_dependent_value override does the same for loop bounds but exempts bounds built only from enclosing loop iterators, which concretize correctly per iteration and are modeled by the finished-iterator machinery. - Triton's own frontend does truthiness on scalar tensors as None-guard plumbing (semantic.py: if mask and mask.type.is_block()), which must stay benign — otherwise any scalar pid-derived mask/other flips the launch to unsupported and real races are missed. The observer walks the stack to the initiating frame, skipping triton_viz frames and triton's interpreter: a triton-package initiator is internal canonicalization (uniform across blocks); anything else is user control flow. - TraceRunner.run wraps the launch in try/finally so a mid-launch abort (abort_on_error) still runs finalize and releases the class-level hooks, which otherwise leaked into the next launch and crashed a subsequent sanitizer run. Add e2e regression tests for the false-positive guard, the false-negative guard, and the pid-dependent loop bound.
… overlap a CAS location
The closed-world CAS read-from model constrained a reader's old value to
{launch-time initial value} + {values written by modeled CAS writers}
via a hard Implies(r.reads, Or(choices)). Values published by writers the
model does not include — plain stores and atomic RMWs (tl.atomic_xchg,
tl.atomic_add, ...), whose written values are not modeled — were excluded
entirely. Any race guarded by such a value was silently missed: with a
flag initialized to 0 and published to 1 via atomic_xchg, the model made
old == 1 infeasible, deactivated every guarded store, and reported zero
races with last_status ok.
Add _has_unmodeled_overlapping_writer: a Z3 check (under grid/arange
bounds, filtered by _can_be_rf_candidate) for whether any plain-store/RMW
event's byte range can overlap the CAS location. When one exists, the
rf_unknown escape is added even if the initial source is identifiable —
the old value becomes unconstrained but deliberately does NOT enable
synchronizes-with, so the model only over-approximates (more reports),
never under-approximates. Overlap is decided on concrete tensor base
addresses, so writers to other tensors never weaken the closed world and
the guarded acq/rel CAS no-race results are preserved (verified: solver
unit suite fully green, alias-view publishing detected, no measurable
solver overhead).
Add e2e regression tests: an atomic_xchg-published guard must report the
WAW, and the closed world must hold when the xchg targets a different
tensor.
…lar tensor checks The interpreter resolves `if tensor:` via data-based truthiness (_get_bool: bool(data) when size == 1), but compiled Triton evaluates the same expression as plain object truthiness — always True for a present tensor. Triton's frontend relies on the compiled semantics in None-guards such as semantic.py's `if mask and mask.type.is_block():` in _store_legacy/_load_legacy. Under symbolic capture those guards forced SymbolicExpr.concretize() on scalar symbolic masks, which is undefined for value-less ops: every kernel passing a scalar CAS-derived mask (mask=(old == 1)) crashed with 'NotImplementedError: Concretize for op atomic_cas' — the root cause of the six failing guarded-CAS e2e tests. SymbolicExprDataWrapper.__bool__ now returns True when the truthiness initiator is triton/triton_viz-internal, matching compiled semantics and never concretizing; user host-side control flow keeps the interpreter's concrete-value semantics and the scalar-concretize observer policy. The initiator frame walk moves from the race detector into the engine as the shared scalar_truthiness_from_user_code() (triton package dir resolved lazily), and the race detector's private copy is removed. A full scan of the triton package found exactly one value-dependent internal truthiness site (semantic.py's `other.handle if other else None`): forcing True there also matches compiled behavior — previously a falsy symbolic `other` was silently dropped to None. Mask value semantics are unaffected: the mask expression still flows into record.active and the Z3 model (verified by exclusive-writer no-race probes), and the race-detector e2e suite goes fully green (49 passed; the six guarded-CAS tests now produce their intended verdicts).
… not per (start, end) ArangeSymbolicExpr interned its summary Z3 var in ARANGE_DICT keyed only by (start, end), so two semantically independent arange instances with the same range — the row and column index vectors of a square tile, combined via broadcasting — lowered to the SAME var. Within each solver copy row == col was pinned and the modeled footprint collapsed to the tile diagonal: every race whose witness needs row != col was silently missed while last_status stayed ok. Key the interned var by (start, end, filename, lineno) of the creation site. Site capture is a plain package-boundary frame walk (innermost_user_site: skip triton_viz and the triton package; the first remaining frame is the user line calling tl.arange) rather than traceback_utils' code-key matching, which fails for kernels defined inside functions — recompiled code objects lose the <locals> qualname, so every site would collapse to the launch line. Re-executions of the same line (loop iterations) keep reusing one var, preserving loop signature dedup. TwoCopySymbolicHBSolver derives per-copy renames from the original var's name so every dict entry renames uniquely, and accepts both key shapes. Documented residual diagonal-only under-approximations: two same-range arange instances created on a single source line, and one arange broadcast against itself (offs[:, None] + offs[None, :]). Add e2e tests for the 2D-tile cross-block race (previously unsat) and the disjoint-tile no-race control; the unit arange-name assertion now checks the stable prefix.
…, width, exact address) conflicting_access_modes declared every atomic-vs-atomic pair race-free, ignoring scope and access width. On hardware two operations are only mutually atomic when each is atomic with respect to the other: - PTX .cta scope guarantees atomicity within one CTA only, and the solvers exclusively query cross-block pairs — two cta-scoped atomics from different blocks at the same address are a real data race that was silently passed; - byte-overlapping atomics with different widths (a 4-byte and an 8-byte RMW over the same bytes) or at different addresses are torn accesses, not mutual atomicity. The predicate now treats both-atomic pairs as conflicting unless both scopes are at least device scope, the widths match, and the addresses are exactly equal. Events without width metadata (demo HBSolver) keep address-equality semantics. Same-width device-scope atomics at one address — competing CAS, atomic histograms — stay race-free. Update the cta guarded-CAS tests (e2e and the demo HBSolver twin) to expect the additional CAS-CAS report alongside the data race; add e2e tests for cta-scoped same-address atomics (race) and gpu-scoped ones (no race), plus solver unit tests for mixed-width, same-width, and partially-overlapping atomic pairs.
…ssumptions Under symbolic capture the interpreter's create_assert/create_assume do `assert condition` on a SymbolicExpr, which has no __bool__ — the check was object-truthy and every tl.device_assert / tl.assume was silently swallowed. Intercept them properly: new DeviceAssert/Assume op types are mapped to the builder's create_assert/create_assume, and the shared SymbolicClient overrider routes the condition to a _handle_assumption hook (default: drop — the prior behavior made explicit; the sanitizer is unchanged, and clients without overriders, like the tracer, keep the original concrete path). SymbolicRaceDetector collects the conditions as launch assumptions: every feasible real execution satisfies them, so the two-copy solver instantiates each template once per program copy (pid/arange/copy-local substitutions) and adds them to every race query — tl.assume hints now prune infeasible race witnesses instead of being ignored. In-loop assumes are per-iteration path conditions one-shot capture cannot attribute and mark the launch unsupported; finished-loop leftovers concretize through the existing iterator machinery. Add e2e tests: a restricting assume eliminates the WAW a loose assume keeps, and assume-inside-loop reports unsupported.
The ternary-op overrider only handled np.where; any kernel clamping a
symbolic value crashed with NotImplementedError('Unsupported ternary
operation: clip'). Lower np.clip as minimum(maximum(x, lo), hi) — one
open bound is tolerated, and the hi-wins behavior of the degenerate
min > max case matches np.clip semantics.
Add an e2e test covering a clean clamped store and a racy overlapping
variant.
… wrapping it symbolically tl.static_range is compile-time unrolled: every iteration executes with a concrete index, and host-side consumers depend on that — indexing a pointer tuple (peer_ptrs[i]) needs a real __index__, which raised 'ValueError: cannot coerce ArithRef to int' under the symbolic iterator (the long-standing test_tuple_pointer_item_selection failure). Wrapping it also mismodeled the unrolled semantics. _wrap_range now returns None for the tl_static_range spelling, so the loop runs as a plain Python loop (the loop hooks already skip non-RangeWrapper iterables) and each unrolled iteration records with its concrete index. Side benefits verified: per-iteration concrete OOB checks under the sanitizer, and atomic CAS/RMW inside tl.static_range is now supported (unrolled iterations are not 'inside a loop'). tl.range and plain range keep the symbolic iterator machinery. Add a race-detector e2e test for an unrolled static_range cross-block race.
…TTIR Adds Sanitizer(compile=True), the torch-style dual-mode counterpart to the eager interpreter-driven sanitizer. It analyzes the kernel's TTIR (acquired through the real compilation warmup) once per specialization and instantiates the out-of-bounds check per launch with concrete tensor metadata and scalar argument values — proving in-boundedness for ALL inputs consistent with those scalars and the grid, with no interpreted execution. Components (triton_viz/clients/sanitizer/compiled/): - ttir_reader: parses TTIR into an AccessGraph. Each tt.load/tt.store pointer is traced through tt.addptr back to a base pointer ARGUMENT; the access becomes an element-offset expression (a lazy term tree) over program ids, arange lanes, and the loop induction variable, with scalar args left as Param leaves for per-launch substitution. A make_range reused for a 2D tile's row and column (triton does this) is split into independent (ssa, dim) variables via expand_dims, so the footprint does not collapse to the diagonal. Indirect/gather addressing, block pointers, and nested loops raise UnsupportedTTIR so the eager mode can take over — never a silent wrong verdict. - oob: per access, a Z3 query over the free variables with scalar args as constants — OOB iff SAT(mask AND (offset < 0 OR offset >= numel)) for the base tensor's element count. UNSAT over all accesses is a proof; SAT yields a witness with the byte violation address. The valid element range is the closed interval [0, numel-1], matching eager's inclusive bounds. - client: CompiledSanitizer(Client). Warmup captures asm['ttir']; arg_callback collects per-tensor numel/elem_size/data_ptr (contiguous only) and scalar values, distinguishing constexpr from runtime int args; grid_callback takes the concretized 3-tuple. finalize runs the check and emits OutOfBoundsRecordZ3 with the TTIR source location, honoring abort_on_error / records like eager. Analysis is cached per TTIR hash; per-launch metadata is reset after finalize (arg_callback precedes grid_callback). Factory: Sanitizer.__new__ dispatches compile=True to CompiledSanitizer (a plain Client, not a Sanitizer subclass, so Python does not re-invoke __init__ on the returned object). Verified by an adversarial differential against the eager sanitizer over 15 affine kernels (masked/unmasked, ragged tails, wrong strides, 2D tiles, broken masks, negative offsets, boundary-exact accesses): every verdict matches, no false negatives or positives in the supported class; per-tensor numel, constexpr-vs-runtime scalars, i64 extsi offsets, and inclusive [0,numel-1] parity confirmed. The adversarial pass caught a nested-loop false-negative (the guard keyed on a flag set only at loop close) — fixed to reject nested loops; the same fix corrected the scf.for regex to recognize accumulator-free store loops, now analyzed rather than skipped. Add reader/oob unit tests and trace-level e2e tests; extend the golden generator with the tile2d and gather kernels. Dynamic-mode suites untouched.
…oop lower/step Two P2 review findings on the compiled sanitizer: 1. Respect ENABLE_SANITIZER=0 in compiled mode. CompiledSanitizer is a plain Client (not a Sanitizer subclass), so trace's _is_sanitizer_client did not match it and the flag-off escape hatch never fired — an explicit Sanitizer(compile=True) under ENABLE_SANITIZER=0 still warmed up, analyzed, and could abort on OOB. The factory now collapses compile=True to NullSanitizer when the flag is off, exactly like the eager path, so trace() leaves the kernel untraced. 2. Model the loop lower bound and step. The OOB query bounded the loop induction value as [0, upper), ignoring the parsed lower/step, so for range(1, n) or range(0, n, 2) it checked iterations that never run and could false-flag valid launches. The loop free variable is now the 0-based ITERATION INDEX: the induction value at iteration iter is lower + iter*step and a loop-carried pointer sits at offset0 + iter*delta, with iter constrained by lower + iter*step < upper. This is sound for any positive-step affine loop and unchanged for the common range(0, n) / range(0, n, BLOCK) cases (matmul: lower=0, step=1). Descending (non-positive step) loops are marked unsupported rather than mis-modeled. Add unit tests for the lower/step iteration model (non-zero lower with no false positive, step-2 skipping unrun iterations while still catching a real even-iteration OOB, descending loop unsupported) and an e2e test that ENABLE_SANITIZER=0 turns Sanitizer(compile=True) into NullSanitizer.
…-launch TTIR, honest unsupported docs Three correctness/clarity findings from review: 1. Missing tensor metadata is now unsupported, not a silent skip. When a base pointer has no registered TensorMeta, check_access used to return None, which check_graph treated as 'this access has no OOB' — so an unchecked load/store could slip through and the launch still report last_status='ok' with empty records, a false proof. A static proof is only valid once EVERY access is checked, so this now raises UnsupportedTTIR (the client surfaces it as last_status='unsupported'). 2. _pending_ttir no longer leaks across launches. It is the current launch's captured TTIR input; the persistent state is the parsed-graph cache (keyed by TTIR hash). It is now cleared at launch teardown (finalize's finally) and at warmup start, so a later launch whose warmup yields no TTIR falls to 'unsupported' instead of re-analyzing a previous kernel's graph against the current launch's metadata (wrong locs, or a wrong-graph false verdict). 3. Docs corrected: unsupported constructs (indirect/gather, block pointers, non-contiguous tensors, nested loops) are REPORTED as unsupported with empty records — not a silent wrong verdict, but also NOT an automatic eager fallback. v1 does not interpret unsupported kernels; the docstrings and package doc now say to run the eager Sanitizer() on them instead of claiming 'the eager mode takes over'. Add regression tests: missing-metadata -> unsupported (not ok); stale TTIR does not leak when a later warmup yields no TTIR; unsupported is report-only with no auto eager fallback.
The language snapshot only recorded attributes that already existed (`if hasattr`), but Triton's interpreter ADDS some attributes that have no native counterpart (tensor.__bool__ / __index__; tl.core.tensor defines neither). After restore those stayed installed process-wide, so a later REAL compilation (the compiled sanitizer's warmup) resolved tensor truth tests through the interpreter's _get_bool and crashed with "'triton._C.libtriton.ir.value' object has no attribute 'data'" on any re-launch of a kernel using tl.load/tl.store with a mask. Snapshot now schedules absent attributes for removal (mark_removed), and restore deletes them only if present, staying idempotent when the same class is reachable via several language targets (tl.tensor is tl.core.tensor). Root cause for 58/184 TritonBench_G_v1 files failing under Sanitizer(compile=True) on their second launch.
… operators) thunlp/TritonBench data/TritonBench_G_v1 at upstream commit 603e28a5, byte-identical (excluded from the repo formatters via the pre-commit global exclude), Apache-2.0 with the license and a README recording the commit, retrieval date and the acquisition rationale: vendored rather than a git submodule or download-on-demand for artifact self-containment — archived repo tarballs keep the corpus (submodule contents are dropped by GitHub/Zenodo snapshots), evaluation runs offline, and the exact sources are pinned. Each file is a standalone operator (kernels + host wrapper + an import-time CUDA test block after a '#####' separator); the corpus machinery lands in the next commit and never executes the test blocks.
…y-name launch binding evaluation/tritonbench_capture.py runs ONCE on a CUDA machine (the vendored files' test blocks execute at import on GPU): a JITFunction.run hook records per (file, kernel) the first real launch — the full name→value binding split into runtime args and constexprs, tensor descriptors (shape / dtype / init class incl. the OBSERVED int value range so index tensors rebuild in-bounds / contiguity / alias groups), exact scalars, and the grid resolved through the constexpr meta. Per-file subprocess with timeout; failures and skipped kernels all carry reasons. Yield: 202 launches from 179/184 files (2× removed triton.ops, 2× smem over the hardware limit, 1× autotune timeout; 24 kernels skipped: 14× non-contiguous args, 6× tl-dtype constexprs, 2× TensorWrapper, 2× misc). evaluation/kernels/tritonbench_g.py rebuilds the launches on ANY machine from tritonbench_g_specs.json: it execs only each file's pre-separator kernel section (never the CUDA test block), unwraps Autotuner/Heuristics stacks BY TYPE (the wrappers proxy arg_names, so attribute sniffing stops too early), reconstructs CPU tensors from the descriptors with seeded generators, rebuilds aliased pointer args from one tensor (LaunchSpec.aliased=True), and routes None-valued optional pointers through constexpr-None specialization. Every row is labeled race-free (production code) in the liger framing: the ladder distribution on real kernels is the data. Corpus.provenance (new Corpus field) carries the upstream commit into the results header via the runner. The sweep exposed a latent harness bug: launching kernel[grid](*args, **constexprs) misbinds any runtime parameter declared AFTER a constexpr (its value slides into the constexpr's slot — 13 rows' dynamic columns died with TypeErrors) and collides with constexpr-None pointers mid-signature. _launch_binding now binds the launch entirely BY NAME (zipping make_args against the kernel's non-constexpr arg_names, with a length check), applied to all three call sites; liger/tritonracebench/tutorials rows verified unchanged. Definitive sweep (202 rows): 70 proved@T1 + 30 proved@T0 (49.5% proofs on unfiltered real code), 76 honest abstentions (36 indirect addressing — the documented DataDep boundary — 7 data-dependent bounds, 4 nested loops, 2 unstructured cf), 23 races-unclassified, 3 kernels that no longer compile upstream. The 23 flagged rows were triaged by a 23-agent workflow with independent cross-checks (46/46 agree): ALL are the T1 any-grid verdict semantics meeting wrapper-coupled launches (safety depends on grid = cdiv(dim, TILE); the witness pids exceed the captured grid), not corpus artifacts and not detector bugs — the dynamic column is clean on every one. The launch-scoped verdict tier this suggests is recorded as an advisor decision point. concretization_map classifies crash/timeout as residual terminals.
…coped verdict tier decision point §3b records the vendored corpus, the capture/rebuild pipeline, the definitive sweep distribution and the 46/46 triage verdict on the 23 flagged rows (T1 any-grid semantics vs wrapper-coupled launches). §3c queues the launch-scoped verdict tier for advisor alignment: re-solving with read axes pinned to the captured grid would convert most of those into launch-scoped proofs with an any-grid caveat — a verdict-semantics change, so align first.
… three small fragment extensions Per the 2026-07-11 decision on the TritonBench evidence (36 of 202 rows abstain on indirect addressing, the largest class, and the interpreter refuses them too), address-position lifting is promoted from the backlog to a first-class item with its five validation work items spelled out — per-lane select lowering with domain constraints, the index-tensor read-only flow check, the select-address overlap query, witness-soundness revalidation whose acceptance tests are the backing, and a definition of done spanning the scatter litmus pair, the three doubly-undecided benchmark rows, and a sample of the TritonBench indirect rows through the composed dispatcher. The three approved small extensions queue behind it: snapshot-lifted loop bounds (7 rows), nested loops in the TTIR reader (4 rows, interpreter-rescuable today), and cf.cond_br path conditions (2 rows, reader-only since instance-dependent control flow breaks the interpreter's full-template assumption).
…line Per advisor positioning (2026-07-11): global memory is the headline and communication kernels are the new pattern category 8. - Section 2 (corpus growth): category 8a, the single-GPU half — comm/comp SM-partition semaphore kernels (DeepSeek-V3 style role split on pid, global-memory payload + semaphore, await on the comp side). Expressible today with the shipped B+C1 machinery; racy twins listed; reference shapes are upstream gsan's single-CTA sync/no-sync test kernels re-cut at gpu scope. - Backlog: category 8b, the cross-device half — symmetric-memory / UVM peer-GPU litmus from gsan's test_symmetric_memory.py (sys-scope atomic_add + atomic_poll spin + peer-payload load). Requires a model extension first: rank coordinate next to pid, symmetric-buffer identity across ranks; atomic_poll maps onto the await abstraction as-is. - Backlog: gsan as an external RQ5 baseline — upstream triton.experimental.gsan is execution-based global-memory detection (TritonInstrument pass, vector-clock + shadow-memory runtime), the direct dynamic counterpart of the global track; applicability pass first, GPU-gated like racecheck.
…§3d), adversarially verified The spec's central finding, independently verified 6/6 against the code: the lift is a GATE CHANGE, not new machinery. Everything address position needs already exists in the interpreter front-end for value position — snapshot arrays over live tensors with concrete address tables, Or-of-known-addrs domain pinning, the masked If(mask, Select, other) shape with hard-unsupported missing-other, bidirectional read-only region tracking with mark-then-raise fail-stop, and a constraint channel that provably carries nested subexpression conjunctions through every pointer-chain parent into the event's active. The placement follows §I.3 verbatim (loaded value in an address chain → the interpreter front-end); the static track's indirect-address abstention stays as the routing signal. Claim scope is explicit: verdicts on lifted-address kernels are per-launch AND per-contents (a new contents-snapshot premise, with a ladder-audit compatibility rule mirroring +assumes-termination). Soundness rests on three side conditions the spec walks in both directions: read-only index sources (any same-kernel write fail-stops — stale snapshots are wrong both ways), domain pinning (out-of-table indices can neither fabricate nor hide overlaps; the facts hold in every real execution so active-folding is sound), and byte-exact snapshot addressing. The verification pass contributed three findings the spec absorbs: removing 'load' from the gate CO-ADMITS plain-load-derived atomic addresses (semantically fine — snapshot-stability attaches to the value's source, not the consumer's atomicity — but now exercised by a dedicated acceptance family); the CAS record site discards its pointer constraints and survives only via the per-node eval cache (fix to match the RMW site, plus a pin); and two latent traps get test pins (the finalize-time force-eval constraint drop, the first-lowering-wins node cache). Definition of done: the trb010 scatter pair (racy all-zero table confirmed with a concrete byte witness + a new disjoint-index control), the trb013 plain-fetch flip with counting-axiom regression pins, the 37-row TritonBench indirect bucket-migration table, query_stats cost numbers for the QF_ALIA queries, and the RQ5 no-load-values refresh. TODO §3d/§3e counts corrected against the results file (37 not 36; 8 data-dependent-bound rows not 7).
…event addresses, interp verdict tier Implements address_position_lifting_spec.md (all eight §8 steps; the spec's status header records the implementation). As the verified spec predicted, the core is a GATE change: plain tl.load leaves _VALUE_DEPENDENT_ADDRESS_OPS, and an embedded load in an event pointer chain now lowers through the existing machinery — Select over the read-only launch snapshot, Or-of-known-addrs domain facts riding the pointer's constraint conjunction into active, the masked If(mask, Select, other) shape, and the bidirectional read-only region fail-stop. Atomic returns and sort/cumsum stay rejected (snapshot-unstable); the co-admitted plain-load-derived ATOMIC addresses are deliberate and tested. The CAS record site keeps its sub-eval constraint conjunctions explicitly (previously discarded and rescued only by the per-node eval cache). Verdicts on lifted launches carry the contents-snapshot premise, detected SYNTACTICALLY on the pointer expr (a provider-serve counter would miss cache-hit lowerings and under-mark the premise). The composed dispatcher finally surfaces interpreter decisions as terminals: static-abstained rows whose dynamic track ran to completion classify as race@interp / proved@interp (per-launch [+ contents-snapshot] scope), with dynamic witnesses serialized like static ones, witness scoring reading either side, an interp-disagreements audit bucket (launch/contents-scoped evidence is never scored against any-params claims), and both new terminals on the concretization map's interpreter point — which now hosts PROOFS. The six §4 acceptance families (15 tests): written-index fail-stop in both orders, OOB-index domains (facts pin the INNER address — two instances through one OOB slot still race), index/data aliasing, masked-gather defaults incl. the missing-other hard-unsupported, the atomic-consumer surface with the CAS constraint pin, and the two latent-trap pins (finalize force-eval path, first-lowering-wins node cache). Alpha-renaming and witness concreteness pin through the scatter litmus: distinct witness pids, as_long() lands on out's base. Corpus effects: tritonracebench 56 rows at precision=recall=1.0, witness 25/25, audit zero — trb010 scatter/gather and the trb013 plain-fetch flip from abstention to race@interp/proved@interp with the counting-axiom rows pinned unchanged (rmw_sync docstring updated). TritonBench 37-row indirect migration: 11 decided (7 proved@interp + 4 race@interp), abstention buckets 10x pid-divergent host control flow / 7x per-instance bounds / 5x the renamed snapshot-cap reason / 3x missing-other / 1x wrapper coercion; corpus unsupported 76->55. The 6 race@interp-on-race-free rows are randint index-table rebuild collisions (reconstruction fidelity, surfaced by the audit bucket; capture-side randperm fix queued). RQ5 gains the address-position FABRICATION demo: collapsing the index load to one observation aliases every lane onto one slot — the no-sound-fallback premise, empirically, mirroring the mask-position erasure direction. Three pre-lifting gate pins updated to the decided semantics (histogram, synthetic gate on cumsum, CAS-address).
…mily (trb025) The single-GPU half of the communication-kernel pattern (advisor positioning 2026-07-11): DeepSeek-V3-style SM partition — the pid range splits into a COMM role that publishes a global-memory payload and arrives on a semaphore with a release xchg, and a COMP role that acquire-polls the semaphore before reading the payload. The guarded producer/consumer family with a role split on pid instead of pid parity, decided by the static track's await abstraction. trb025 in TritonRaceBench (pattern comm-comp, tritonracebench now 56 rows): the control proves at T1+assumes-termination; the three racy twins each break exactly one ingredient — relaxed poll (value carries, ordering does not), polling the WRONG counter value (the initial 0 exits the spin without ever acquiring the arrival), and a role-split branch that skips the poll entirely — and all report on the payload store/load pair with needle-exact witnesses. Four static-track e2e pins in test_comm_comp_pattern.py (self-contained copies; the interpreter cannot execute pid-divergent spin loops). One machinery boundary probed and recorded in the corpus comment: the arrive is a release XCHG because a release ADD-arrive plus the add(0) acquire poll puts two value-interacting RMW records on the semaphore — the S6 ticket-lock boundary, under which the sw edge cannot be derived and the control reports. The true multi-arrival counting arrive lands with the S6 stretch. Category 8b (cross-device, rank coordinate) and the gsan baseline stay in the backlog as scoped.
…gory 8a landed §3d items (i)-(v) checked with the measured record: the acceptance families, the composed-dispatcher terminals, the tritonracebench definitive numbers (precision=recall=1.0, witness 25/25, audit zero), the TritonBench 37-row migration buckets (11 decided, corpus unsupported 76->55), and the two-directional RQ5 demo. The reconstruction-fidelity follow-up (capture index-tensor uniqueness, randperm rebuild, GPU re-capture) is queued inside the item. §2's 8a entry records trb025 + pins + the S6 release-ADD-arrive boundary probe.
…, TB re-capture Extract the JITFunction.run launch-capture hook + descriptor rebuild from tritonbench_capture into evaluation/capture_common.py so real-code corpora share one mechanism. Int/bool tensors up to 8192 elements now carry exact value snapshots (by-range randint rebuilds fabricate invalid inputs for value-coupled tensors: monotone cu_seqlens, permutation tables, disjointness-keeping masks — the TritonBench interp-disagreement class). Kwargs naming a DECLARED kernel parameter bind as kernel args even when they collide with a launch option (num_stages: tl.constexpr shadowing dropped two fla fused_recurrent kernels as 'unbound'). Per-case temp files are mkstemp-private with guarded read/parse (shared-/tmp collisions cross-contaminate runs). TritonBench re-captured on GPU with snapshots (same 202 kernels / 179 files; 100 args snapshotted): 2 of the 6 interp-disagreements retire (tb_token_softmax_bloom/llama -> proved@interp); the survivors triaged as 2 genuine races in the crawled corpus (tb_nested_loops_processing never reads program_id under grid=(2,); tb_quantize_kv_copy scatters through snapshot-faithful duplicate destinations), 1 interpreter and-truthiness divergence (tb_masked_select), 1 detector bug fixed separately (tb_cache_transform, reduce address gate).
…ed launches Third real-code corpus: fla-org/flash-linear-attention analyzed AS INSTALLED via fla-core==0.5.1 (pip, liger pattern; upstream tag v0.5.1 = 2e38c1fa recorded in every results header via _fla_provenance, now a shared _package_provenance helper). evaluation/fla_capture.py drives 64 GPU-validated cases — 23 op families x chunk/fused_recurrent/ parallel x fwd+bwd, dense + varlen cu_seqlens, small fp32 shapes — under the shared capture layer with autotune left ON (benchmark launches are real launches; the harness never consumes num_warps). Cross-case dedup fingerprints the FULL rebuild-relevant record (constexprs, grid, arg descriptors incl. scalar values and snapshots, aliases): families share fla/ops/common kernels with different scale scalars, and shape-only fingerprints wrongly merged gsa's scale=1 chunk_gla_bwd twins. evaluation/kernels/fla.py resolves kernels by importing the recorded module and unwrapping autotune/heuristics stacks by type (InterpretedFunction accepted for TRITON_INTERPRET=1), HARD-FAILS on fla-core version drift and on any unresolved kernel, and disambiguates bwd modules re-defining their fwd twin. runner --jobs N parallelizes sweeps (rows are subprocess-isolated; 378 rows in ~35 min at jobs=8 vs ~5 h sequential; definitive paper sweeps stay jobs=1). fla_specs.json is written compact and the check-added-large-files cap moves to 1500 KB — captured-launch spec JSONs with value snapshots legitimately exceed the 500 KB default (tritonbench_g_specs.json is already 965 KB). Sweep: 122 static proofs (107 proved@T1 + 15 proved@T0), 12 proved@interp, 1 race@interp triaged GENUINE (fused_chunk_based_fwd's z store omits the 'if i_v==0' guard its own bwd twin applies at 8 sites — benign same-value inter-program WAW, label-error not FP), 9 races-unclassified (launch-scoped class), 227 unsupported (indirect-address 147 / control-flow 31 / nested-loop 20 / data-dependent-bound 19), 5 timeouts, 2 compile-errors. Audit PASS. Notably tl.make_block_ptr never reaches the shared reader — make_ttir's rewrite_tensor_pointer lowers it first, so the fla coverage lever is compiled-track snapshot lifting, not block-ptr vocabulary.
The checked-in artifact was compacted by hand in the previous commit; make the writer match so a re-capture round-trips byte-stable.
ReduceSymbolicExpr folds over a SINGLE symbolic lane (an arange is one symbolic variable), so a reduce reaching an event ADDRESS degenerates to a solver-chosen element: tb_cache_transform's max(where(cumsum<=idx,...)) address modeled a 21 KB footprint over a 5 KB tensor and fabricated WARs NONDETERMINISTICALLY at a fixed seed (0/1/2 reports depending on where the CPU allocator placed the neighboring tensor). The reduce family — sum/max/min/xor_sum/ reduce_or/argmax/argmin — joins _VALUE_DEPENDENT_ADDRESS_OPS, turning the row into a deterministic honest abstention; value/mask-position reduces are untouched. Lift only with a true per-lane fold (queued in TODO 3f). Pin extended: max-over-arange in an address rejects, plain load stays lifted.
…-up closed 3d follow-up: value snapshots supersede the randperm design (they also preserve legitimate duplicates and monotone offset tables); the 6-row TritonBench interp-disagreement bucket fully resolved — 2 retired, 2 genuine races in the crawled corpus, 1 interpreter and-truthiness divergence, 1 detector bug fixed (reduce address gate). New 3f records the fla corpus numbers, the rewrite_tensor_pointer discovery (block ptrs never reach the reader; compiled-track snapshot lifting is the coverage lever, 147 indirect-address rows), and queues the and-truthiness divergence class (incl. the C3 replay SIGSEGV) and the reduce per-lane fold.
…ne races fla-org/flash-linear-attention#1018 (fused_chunk based fwd z store guarded to i_v==0; upstream test_based 5 passed, patched row re-checked 4->0 reports), thunlp/TritonBench#10 (nested3 grid clamped to min(n_cols//4, 1), byte-identical outputs), thunlp/TritonBench#11 (DestLoc randint->randperm, unique KV-cache slots). PR text describes mechanism + repro only. The vendored TB copy and the fla-core 0.5.1 pin stay unchanged — the racy versions are the evaluation evidence; upstream merges become confirmed-upstream citations.
…corpus builder Rule of two (fla + flagattn): the case-driven capture driver's main loop (per-case subprocess isolation, first-launch recording, full-record dedup fingerprint, compact specs writing) moves from fla_capture into capture_common.run_case_capture/capture_one_case/ fingerprint, and the corpus builder (version hard-check, fail-loud unresolved kernels, bwd-twin name disambiguation, InterpretedFunction unwrap) moves from kernels/fla.py into kernels/_captured.build_captured_corpus. Both former owners become thin: fla_capture keeps its CASES table + env policy, fla.py keeps its import guard + paths. fla regression-checked: 378/378 specs with field-identical provenance.
…unches
Fourth real-code corpus: FlagOpen/FlagAttention (13 Triton kernels —
flash/piecewise fwd+3-bwd, split-kv pair, paged + v2 reduce, total
attention; Apache-2.0; runs unmodified on triton 3.6). No PyPI
release, so it is git-pinned (flag_attn @ git+...@41fc31d) and
_flagattn_provenance reads the exact commit from pip's
direct_url.json — no release table. 10 fp16 cases (causal/non-causal,
GQA, dropout/philox, non-divisible seqlen, aux outputs, split-kv
decode, paged x2, piecewise) captured 28 specializations with 0
failures; no autotune anywhere (hand-written config tables, sm89
fallback 32x32) so captures are naturally deterministic.
Sweep (28 rows, audit PASS), every row attributed:
- 14 rows name a NEW abstention class, PID-AFFINE LOOP BOUNDS: the
flash causal inner loop runs to (pid_m+1)*BLOCK_M-style bounds,
which T1 refuses (wants launch-concrete bounds) and one-shot
symbolic capture concretizes. Representable in the existing affine
machinery — lift queued in TODO 3g.
- 10 races-unclassified: every witness has a pid OUTSIDE the launch
extent (grid=[4,2,2] vs pid_0=4/12, pid_1=3/5) — the 3c
wrapper-coupled any-grid class, joining TritonBench's 22 and
fla's 9. No real race under the captured launches.
- paged lands exactly on two queued 3e fragments (loaded
context_lens loop bound; cf.cond_br), giving them
attention-serving row support.
- 1 proved@interp: the split-kv combine kernel (interp rescues its
nested loops). Plus one small interp gap on the dropout bwd
dynamic track ('Patching math ops not yet supported', philox).
…ne loop-bound lift queued
Fifth real-code corpus and the race-relevant one: flagos-ai/FlagGems (production ATen operators in Triton; ~150 tl.atomic_* sites across scatter/index/histogram/embedding-bwd/loss, cumsum-addressed stores in unique/masked_select, and mm_streamk's inter-CTA spinlock). Git-pinned @1051e56c with --no-deps (PyPI lags master by 1000+ commits and the metadata pins numpy==1.26.4, which would downgrade the env; sqlalchemy is its one missing hard dep). 66 GPU-validated cases across 10 families -> 82 specializations, 0 failures. libentry/libtuner wrappers expose .fn chains, so the shared type-descent unwrap applies unchanged. capture_one_case gains module_prefix: runtime-CODEGEN kernels (pointwise_dynamic modules under ~/.flaggems/code_cache with process-dependent names) are filtered to skipped_kernels — they cannot be re-imported at rebuild time. Sweep (82 rows, audit PASS): 42 decided-clean (22 proved@T1 + 11 proved@T0 + 9 proved@interp, 51% coverage — best of the real corpora; the counting axiom's first at-scale field test: vdot's atomic scalar accumulate proves at T0, bincount/histc/scatter_reduce/index_reduce duplicate-index variants all clean). mm_streamk first_wave abstains 'spin-shape: scf.while carries values' — the carried-value spin is the first production S6 instance. Both race@interp rows triaged interpreter-artifact: weight_norm is the and-truthiness class (third instance); embedding_dup exposes a NEW two-copy solver bug (no same-axis coupling between arange vars — a kernel calling tl.arange twice on one axis yields a phantom intra-instance WAW; fix design in TODO 3h). 1 races-unclassified (bmm, any-grid witness pids), 1 timeout (classic_mm).
… detector bug queued
…, full triage ledger Consolidated evaluation snapshot at a364ebb: ground-truth scorecard (tritonracebench precision=recall=1.0, witness 25/25, audits zero), real-code corpora table (315/722 decided-clean; 276 static proofs), the three genuine races with upstream PR links, the triage ledger accounting for every surviving race report, detector defects surfaced by the round (reduce fold fixed, and-truthiness + lane-coupling queued), and the abstention-taxonomy-to-lift mapping.
…-written Triton kernels - evaluation/torchao_capture.py: 44 cases across 8 families (attention QKV fp8 quant incl. rope/hadamard, MoE fp8 rowwise/jagged scaling + mxfp8 swizzles, DeepSeek-style blockwise fp8 training, DeepGEMM-layout grouped quant, float8nocompile casts, torchao/kernel blockwise/intmm/ bsr, hqq int4 + int8 + split-k matmuls, mx_formats); git-pinned USE_CPP=0 install @ bfbc842; sm89-unreachable families documented in the docstring (fp8_sdpa torch-2.11 init, nvfp4/mxfp8/mx-dim0-dim1 sm100 gates, distributed comms, common-matmul fp8 upstream KeyError) - capture layer: non-contiguous args rebuild from recorded strides (stride-0 broadcast writes through a de-overlapped slice); tl.dtype/torch.dtype constexpr objects round-trip as tagged JSON; fp8e4nv/fp8e5 SIG_FOR_DTYPE entries; distinct-views-of-one-buffer alias guard - corpus rebuild: _resolve_kernel gains an unambiguous namespace-scan fallback (torchao/kernel lazy-init publishes kernels under different global names); the corpus module triggers _lazy_init_triton and surfaces CustomOpDef closure-held kernels - fp8 args surfaced two generic defects, both fixed: the shared TTIR reader's _DTYPE_BITS lacked MLIR fp8 spellings (f8E4M3FN family; 15 rows pseudo-abstained with elem_bits=0), and the harness host-compile hardcoded GPUTarget sm80 (false compile-errors below cc89) - sweep: 23 decided-clean (5 T0 / 9 T1 / 9 interp), 36 abstain, 8 races-unclassified with every witness pid out of launch extent (the 3c any-grid class, now 50 rows / 5 corpora), zero genuine races; SWEEP_REPORT totals 789 rows / 338 decided-clean; TODO 3i records the corpus and queued lifts (scalar-pointer atomic_rmw, strided in-bounds premise, runtime-scalar loop bounds)
…race confirmation at unrolled same-line stores meta-pytorch/tritonbench corpus (Meta's benchmark suite — distinct from thunlp/TritonBench = tritonbench_g): - evaluation/tritonbench_meta_capture.py: HARNESS-DRIVEN capture (drives the suite's own BenchmarkOperator via --only/--num-inputs/--input-id/ --test-only/--force) rather than a case table; module_prefix filters its liger/inductor/vendor backends. 43 cases -> 41 specializations. Registry-disabled impls each tried under --force, dropped only on a verified structural failure (xformers/cutlass-ck deps, stream-k TMA descriptor args, multi_cta cluster launch) — all documented. - evaluation/kernels/tritonbench_meta.py: dist version is constant 0.0.1, so the module hard-checks the installed direct_url.json commit against the captured one directly. - kernels/_captured.py _resolve_kernel: also scans module-level CLASS bodies (tritonbench's softmax Operator carries @triton.jit kernels as class attributes). - sweep: 20 decided-clean (5 T0 / 8 T1 / 7 interp), 20 abstain, 1 races-unclassified (out-of-extent flash-TMA artifact), zero races. Detector fix (aiter_originals was races-unclassified, should confirm): - compiled/client.py _confirm_reports: the C2 ambiguous-site gate (stops a dropped-mask WIDENED report riding an unrelated same-line access's overlap into a fabricated confirmation) also skipped EXACT reports whose store is unrolled by tl.static_range onto one source line (count>1 => ambiguous). The aiter#3091 kernel is that shape, so its genuine in-extent cross-block WAW landed on races-unclassified instead of race-confirmed. Gate WIDENED reports only — an exact report is a definite SAT witness whose access is live by construction, so the same-line bucket is its own real footprint and confirming it is sound. - pinned by test_c2_confirms_exact_waw_at_unrolled_ambiguous_site; tritonracebench ground-truth scorecard and every out-of-extent 3c artifact (torchao 8, tritonbench_meta 1) unchanged. SWEEP_REPORT totals 830 rows / 358 decided-clean; TODO 3j (corpus) + 3k (the confirmation fix) record it.
…ton twins First local-checkout corpus (TileBench has no packaging metadata): TILEBENCH_ROOT on sys.path, checkout HEAD commit as the pin — capture refuses tracked-dirty trees, and build_captured_corpus grew an installed_version= parameter so non-pip corpora ride the same drift guard. Harness-driven capture through the suite's core.engine with case_indices=[0] and report_benchmark stubbed out: the only recorded launch is the plain-stream verification run (autotune stays False, so every impl fires its raw @triton.jit kernel once). 45/45 operators, 56 specializations, zero failures. Every operator also ships a cuTile twin — this corpus is the Triton-side baseline for the planned cuTile frontend.
… defaults The tl-module patch intercepts BEFORE triton binds tl.cumsum's defaults, so a bare tl.cumsum(x) (tilebench radix_sort) reached _op_cumsum_overrider as one positional arg while the overrider required axis — aborting the dynamic track with a TypeError. Every other tl-level patched op already mirrored its defaults; cumsum now does too (axis=0, reverse=False, dtype=None). The radix_sort row's dynamic track lands on a clean unsupported (cumsum has no Z3 lowering) instead of a crash.
… grid-fragile attribute TODO 3c, decided: (c)-semantics on (b)-machinery with three guardrails. After an any-grid SAT, _launch_scoped_requery re-asks the SAME encoding with every grid axis pinned to the launch extent — tl.num_programs interns grid_i by name, so the pin is an extra_assumptions equality (no re-encode, zero solver changes). Extent-UNSAT => proved@T1-launch with the any-grid evidence on the independent grid-fragile attribute (hazard wording, never a race claim; sound from widened evidence too, since widening only enlarges footprints). Extent-SAT => the race path continues with the PINNED reports, whose witnesses are in-extent by construction. Z3-unknown => fall back to the any-grid reports, fail-closed on the claim. Full 14-corpus re-sweep at this state: ground-truth scorecard IDENTICAL (precision=recall=1.0, zero grid-fragile rows in GT), aiter stays race-confirmed, 51/52 wrapper-coupled rows become launch-scoped proofs, decided-clean 45% -> 51% reported per scope (any-grid 340, launch-scoped 114; grid-fragile 52 in its own column; findings stay 3). The one holdout (torchao split-k matmul) keeps races-unclassified, which now precisely means any-grid SAT + launch-scoped undecidable. Verdict attrs gain proved_scope=this-params-this-grid + grid_fragile; the concretization map gains the 'pid + trip (grid = launch)' row.
…he shared access-graph model First non-Triton DSL front-end. Parses the final CuTile IR text (compile_tile(return_final_ir=True), captured at launch) into the SAME AccessGraph/Term algebra the TTIR reader produces — encode_graph, the two-copy solver, the tier selector and the launch-scoped rung run unchanged. Semantic mapping: tile-space load/store lowers to index*tile_shape + arange affine terms with the implicit OOB-drop materialized as ordinary mask terms (cuTile has no explicit masks); pointer_offset + tile_atomic_rmw / load_pointer / store_pointer are exactly the TTIR raw-pointer shapes (the compiler emits the bounds-check mask itself); python floor-division lowers to c_mod plus a BOOLEAN-xor sign-fix the reader models exactly as (a AND NOT b) OR (NOT a AND b); structured for-range loops map to the single LoopInfo slot. Uncertainty discipline inherited verbatim: unmodeled ops bind DataDep, addresses fail closed (indirect-address), masks drop to the widened channel, integer xor and while-form loop/if blocks abstain honestly. Pinned by tests/unit/test_cutile_reader.py: proof AND detection directions end-to-end through the two-copy solver, atomic lowering, the bool-xor floor fix, int-xor abstention, load_pointer events, while-form refusal.
…h's cuTile twins Capture patches cuda.tile.launch (records, then runs — the engine's verification validates the recorded launch) and compiles the CuTile IR text INTO the record, so corpus rebuild needs neither cuda-tile nor a GPU. 45/45 operators, 385 raw specializations; the stored payload is trimmed to 2 per (case, kernel) with the drop count recorded (the bitonic-network operators bake one ct.Constant per host-loop step, and each record embeds its IR text — an uncapped payload exceeds the large-file limit). codespell now skips the machine-generated specs payloads (embedded IR SSA names). Harness: LaunchSpec.frontend='cutile' dispatch tag; the cutile static track drives the SAME _solve_one_graph tier selector (T0 gate, T1, launch-scoped rung) over the captured IR; no dynamic track (cuda.tile has no interpreter — documented, v1 static-only). Flattened-param binding (p_0 base / p_1..p_r shapes / strides) and fake disjoint allocations per captured alias group. Sweep: 17 T0 / 19 T1 / 2 T1-launch(+grid-fragile, the tier working unchanged through the new front-end) / 23 honest abstains, zero crashes, zero races-unclassified. Cross-DSL differential vs the Triton twins (SWEEP_REPORT 3b): 30/45 operators agree incl. identical data-dependent abstention kinds; cuTile AHEAD on the matmul family (structured tile indices prove @t1 where flat-pointer arithmetic timed out / went Z3-undecided); behind on multi-pass-loop shapes and the missing interpreter channel; top_k splits any-grid vs launch scope.
… widened reports Extends the launch-scoped proof-plus-attribute pattern (3c) to widened evidence: when a widened static report is demoted by faithful replay and the interpreter proved the launch clean, the composed dispatcher should return proved@interp carrying a content_fragile attribute instead of short-circuiting to race-unconfirmed at harness.py:494. Spec covers the dispatcher change, attribute plumbing with the widening-soundness note, 3c-style guardrails (structurally-unconfirmable demotions never upgrade; fail-closed on unknown), pinning tests, and the expected scorecard delta (benchmark TN 23->24, coverage 55/56). Found by the 2026-07-16 paper-vs-implementation comparison; option (b) decided by Hao.
…ened evidence with the interp proof
TODO 3n, decided (b): the launch-scoped proof-plus-attribute philosophy
applied to memory CONTENTS. The race-unconfirmed reason is the STRONG
demotion marker — the client sets it only when EVERY widened SAT was
faithfully replayed on this launch's data and none reproduced. The
composed dispatcher previously short-circuited there to an abstention
without consulting the interpreter, discarding its launch-scoped proof
(dd_mask_dead: dyn ok(0) yet terminal race-unconfirmed) — paper sec 2
promises the dead launch a proof.
_classify now pairs the marker with the dynamic track: interp clean =>
('race-free', 'proved@interp') and run_one stamps
verdict_attrs.content_fragile=True ('some memory contents enable an
overlap' — sound from widened evidence because widening only enlarges
footprints, the grid-fragile argument applied to contents); interp
reports => race@interp (they subsume the hazard); dyn absent or failed
=> race-unconfirmed unchanged, fail-closed. Capped / unavailable /
unclassifiable demotions carry the GENERIC reason and can never enter
the upgrade (guardrail i); the client only RETAINS the refuted hazard
as last_content_hazard evidence — it cannot see the dynamic track, so
its own attribute is always False and the dispatcher stamps.
Verified on the re-sweep: exactly two rows corpus-wide carried the
demotion and both flip with the attribute (trb006_dd_mask_dead_no,
smoke_dd_mask_dead_no); the live twin stays race-confirmed; scorecard
TN 23->24, coverage 55/56, precision=recall=1.0, witness-matched 25/25,
ladder audits zero; zero real-code rows affected. Pinned by
tests/unit/test_composed_dispatcher.py (6) and test_replay_channels
extensions (hazard evidence on the faithful demotion only).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This PR adds a solver-only Z3 happens-before demo for CAS-based synchronization in the race detector.
It intentionally keeps the scope narrow:
AccessEventRecordwith minimal solver metadatahb_solver.pyplaceholder with a small event-graph HB solverWhy
This isolates one question for review: whether the HB model can express CAS release/acquire synchronization correctly.
It does not mix that modeling work with real Triton atomic capture, concrete atomic execution, or race-detector integration.
What Changed
AccessEventRecordwith backward-compatible defaultsExplicit Non-Goals
This PR does not:
tl.atomic_cascapturetriton_viz/clients/race_detector/race_detector.pySymbolicRaceDetector.finalize()behaviorValidation
uv run pytest tests/unit/test_race_detector_hb_solver.py -quv run pytest tests/unit/test_race_detector.py -quv run pytest tests/end_to_end/test_race_detector.py -qNotes
The CAS read-from relation in
hb_solver.pyis intentionally a PR-A synthetic relation for the solver-only demo. It is not presented as a full memory-model implementation.