Conversation
Performance Benchmark
Threshold: >5% regression flagged with |
mark14wu
changed the title
mark14wu
changed the title
mark14wu
changed the title
… 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.
…ation Real warmup compilation walks the kernel AST to hash and inline referenced device functions. When a kernel calls a @triton.jit helper that is also wrapped in trace() (the CLI / wrap-every-jit pattern), the reference resolves to a TritonTrace, which Triton's dependency walker rejects with "Unsupported function referenced". Only compiled-mode clients trigger this warmup; eager traces never compile and were immune. During warmup, temporarily swap every TritonTrace reachable from the kernel's globals for its underlying JITFunction, then restore. Same-module helpers share the kernel's module dict; helpers imported from another module are reached as `mod.helper`, so the unwrap also descends one level into module objects in those globals (torch._inductor-style kernels). Unblocked 22/184 TritonBench_G_v1 files under Sanitizer(compile=True).
Mirror of triton-sanitizer, wrapping every @triton.jit / @triton.autotune kernel with Sanitizer(compile=True): instead of interpreting the kernel, it warms up the real compilation to capture TTIR and checks out-of-bounds statically, aborting with a report on a SAT witness. Unsupported constructs (data-dependent addressing, block pointers, nested loops) are reported as unsupported rather than aborting. triton.heuristics is deliberately left unpatched, like the existing CLI wrappers: a @triton.heuristics @triton.jit kernel then keeps its real Heuristics around the traced inner jit, whose warmup path is the one the trace runner drives correctly.
…t TypeError The factory's __new__ popped `compile` from a local kwargs copy and then manually invoked the target's __init__ — but when the returned object is a Sanitizer SUBCLASS (SymbolicSanitizer / NullSanitizer), Python re-invokes its __init__ automatically with the ORIGINAL call kwargs, compile= included. SymbolicSanitizer.__init__ accepted only abort_on_error, so the legitimate spelling Sanitizer(compile=False) raised TypeError; the manual call also double-initialized the instance. Drop the manual __init__ for subclass paths (the automatic one suffices) and let SymbolicSanitizer.__init__ swallow the stray factory-only kwarg. Regression test pins compile=False -> SymbolicSanitizer with the abort flag honored.
…reader A tt.load/tt.store syntax variant the regexes do not match, or an unmodeled side-effecting memory op (tt.atomic_*), previously fell through to the generic handling: a store has no SSA result so it was silently dropped, and an atomic's access went unchecked while its result became a harmless-looking DataDep. Either way check_graph could then prove "ok" without having checked a real access — an unsound proof. Guard after the load/store matches: any remaining tt.load / tt.store / tt.atomic_* line raises UnsupportedTTIR, so the launch is reported unsupported instead. Tests pin both shapes (an attribute-dict store variant and tt.atomic_rmw). Also scrub leftover "dynamic-mode fallback" wording from UnsupportedTTIR and check_graph docstrings: v1 reports unsupported and never auto-falls back to interpreted checking.
Member
|
Closing as stale during PR cleanup. |
Two invariants make the branch sound without finalize-on-error routing: - last_status is pessimistically "aborted" from construction and re-armed in arg_callback/grid_callback; only finalize() upgrades it. A launch that dies anywhere (mid-kernel, in the user's grid lambda, during arg conversion) can no longer be read as a clean "ok", with or without a harness-level finalize-on-error guard. - SymbolicClient.grid_callback unconditionally reclaims the class-level scalar-concretize observer slots at launch start: any observer still installed there belongs to a launch that died before finalize() could uninstall it, so the next symbolic client launch self-heals instead of dispatching truthiness to a dead detector's hook. Regression tests cover the mid-kernel crash, the pre-grid-callback crash after a healthy launch, and the stale-observer leak into a following Sanitizer launch.
…istic status The pessimistic-verdict change (last_status stays "aborted" from grid_callback until finalize() produces a verdict) missed this unit test, which calls _handle_access_check directly and asserted "ok" — a state that direct-call path can no longer reach, since the capture is never sealed and finalize() never runs. Assert the launch-start "aborted" instead: a healthy check must neither degrade it to "unsupported" (the block-ptr lowering regression this test guards) nor prematurely upgrade it to "ok". The tile-footprint record assertions — the substance of the test — are unchanged.
…tion over TTGIR (#476)
… truncated division Extend the compiled-mode OOB checker's TTIR coverage and fix a signed-division soundness bug: - Model arith.remsi/minsi/maxsi as %/min/max in the reader and lower them to Z3 (remainder carries the dividend's sign; min/max via If). - Fix arith.divsi lowering: it truncates toward zero, but Z3's Int `/` is Euclidean (floor for a positive divisor); divide magnitudes and re-apply the sign so negative dividends match hardware. Apply the same to remsi. - Track scf.if regions with a region stack (replacing the single in_loop flag), handling `} else` and nested braces. Accesses inside an scf.if are marked guarded: checked as unconditional (UNSAT stays a sound proof), but a SAT hit becomes `unsupported` rather than a witness, since the branch condition is not modeled and the model may sit in an untaken branch. An unguarded SAT witness still takes precedence. - Fail closed on other control flow (scf.while, cf.*) instead of flat-scanning it as if unconditional. - Accept multi-result SSA operands (`%acc#N`) so stores of a for-loop result value parse instead of failing closed.
# Conflicts: # tests/golden/ttgir/generate_golden.py # triton_viz/core/frontend/base.py # triton_viz/core/frontend/triton.py # triton_viz/core/trace.py # triton_viz/wrapper.py
Rename race_detector_compiled_mode_plan.md to race_detector_static_hybrid_plan.md and reorganize into three parts: - Part I (new): the conceptual skeleton — one solver, one claim ladder (T0 all-symbolic / T1 params-concrete), five terminal states, front-end reachable regions, the per-term tier selector, and the three hybrid information channels (concrete injection, witness replay, differential cross-check). - Part II: the shipped TTGIR shared-memory track, carried over near-verbatim with milestone status (M0-M3 landed, M4/M5 outstanding). - Part III (new): the planned TTIR global-memory track — design decisions (TTIR, solver reuse, T1 as primary target), verified in-tree asset inventory, steps S1-S5 with exit criteria, timeline and risks. Update the two code docstrings that referenced the old filename.
Combine immutable precheck cache admission, strict runtime dependency transport, and fail-closed enumeration cloning. Preserve existing grid and input-content claim scopes while preventing stale or changed execution state from yielding a clean result.
Discover constant arithmetic terms only from original conjuncts and independently certify every equality before substitution. Retain the equalities for exact SAT models, preserve all grid and content premises, and leave query budgets and fallback policy unchanged. Bound optional certification work, retain the original formula on failed certificates, and cache only equivalent rewrites of complete immutable queries. Add scope, zero-divisor, conditional-mask, context, and failure-path regressions.
Substitute both concrete program-instance tuples into every assertion before each existing exhaustive fallback check. Retain the original PID equalities in SAT models so reported witnesses still satisfy the complete original query. Preserve all cases, constraints, feasibility handling, timeout budgets, fallback ordering and proof extent. No new decision cache is introduced. Validation: 220 focused solver, enumeration, query-cache, compiled-global and div/rem tests pass. A matched classic-MM intra-instance query diagnostic keeps all 32 cases and reduces 39.50 seconds to 0.071 seconds; the 992 cross-instance cases remain about 2.8 seconds. These are extracted-query measurements, not full-kernel timings.
Replace a free integer array's sole distinct read with one shared scalar only when the complete query has no other use of that array. Bind each array to the corresponding constant array so native models still satisfy the original assertions, including nested reads through other arrays. Use simplify, solve-eqs, and general SMT with model conversion for matching queries. Preserve caller timeout settings and return to the original path when eligibility or preparation fails. No query scope, captured contents, grid, or memory-model premise is changed. Add 34 focused checks for native witnesses, projected satisfiability, masking, repeated and nested reads, scalar fallback pins, resource-limit unknown, contexts, rejected array uses, and preparation exceptions.
Derive optional facts only from original top-level constant array equations after exhaustively checking a contiguous integer interval and distinct values. Preserve all original assumptions, guard every fact by the known interval, and bound optional pair generation without restricting any query. Validate fifteen unit cases covering absent or conditional cells, duplicate values, out-of-domain reads, independent arrays and contexts, quantified reads, partial byte overlap, and bounded lemma growth. Existing copy-by-destination query diagnostics retain the any-grid SAT result and accelerate the original launch-scoped UNSAT query.
Use exact single-read array elimination only after all original query premises have been normalized. Preserve original solver budgets, immutable cache keys, and native model reconstruction through PID enumeration. Strengthen only the existing UNSAT precheck with guarded facts entailed by snapshot cells already asserted in that query. Add integration regressions for original launch bounds, broader-grid collisions, repeated targets, and solver reset behavior.
Simplify again after constant-array equation elimination and select the general SMT backend's arithmetic solver 2 for this isolated-array path. The full KDA diagnostic exposed unstable arithmetic-solver-6 behavior even though the original complete query and array eligibility were unchanged. Keep native model conversion, original query limits, and general SMT support. Do not assume QF_LIA or add any grid, input, or domain premise. Add nonlinear SAT/UNSAT and uninterpreted-function witness checks. Validation: 37 focused tests pass, including resource-limit unknown and preparation fallback. Three bounded replays of the actual captured query returned SAT with valid original models using arithmetic solver 2; full kernel adoption remains subject to the integrated measurement.
…alidation Retain certified divisor folding, complete PID substitution, and guarded snapshot lemmas in production. Complete KDA profiles at both array strategy revisions did not improve the static-stage runtime, despite fast isolated queries. Remove the production array factory hooks and retain its exact transformation and model regressions under evaluation/solver_prototypes for reproducible investigation. Preserve original proof domains, query budgets, and all fallback cases.
Add an optional solver-local cache for immutable AST applicability facts. Repeated queries without variable integer divisors reuse negative subtree results while every positive case retains query-local certification, original premises, and the existing certificate budget. Retain AST and context references to prevent identifier reuse, and conservatively defer unsupported syntax to the original normalization path. Add regression coverage for shared DAG traversal, changing guards, independent contexts, deep expressions, unsupported syntax, and certificate budgets. Validation: 18 guarded-division unit tests passed; git diff --check passed.
Reuse immutable AST summaries, original table certificates, and guarded range and injectivity expressions across changing conflict pairs. Revalidate certificates when asserted cells change, and preserve quantifier, context, launch, and substitution boundaries. Keep uncached standalone extraction and the existing pure-Select rewrite cache. Add production-precheck scope regressions and counters proving common cells are parsed and certified once. Validation: 92 focused unit tests passed.
Pass immutable guarded-divisor and snapshot summaries through the production query paths and reset their lifetime on each race-finding invocation. Keep current full premises, model ordering and fallback budgets unchanged. Add integration regressions for changed guards, mutated table cells, revoked launch pins and cache isolation. The shared-core and compiled/dynamic end-to-end selection passes 337 tests with 7 skips.
Summarize literal cell equations over plain array symbols as leaves while preserving all traversal through complex array expressions. Reuse cached read summaries to defer certificates when no eligible read is present, without changing guards, premises, or lemma results. Reduce repeated z3py wrapper calls during cell recognition. Cover deferred certification, changing read sets, conditional equations, and nested reads in complex array terms; 90 focused helper and production precheck tests pass.
Try the existing relaxation of original necessary conditions before deriving optional snapshot facts on the simplify-first path. Only UNSAT discharges an access pair; inconclusive or failed attempts retain the original guarded query and its independent 500 ms budget. Reuse a normally completed check when no lemmas were generated. Keep mixed-radix processing, caller fallback budgets and proof scope unchanged. Add regression coverage for unknown results, optional exceptions and unchanged guarded checks. Validation: 100 focused unit tests and all applicable pre-commit hooks pass.
Let evaluation borrow a unique parsed graph only when its exact source, ladder level, multipath mode, identity and mutable graph state still match the original parse. Keep binding retention opt-in and independent of production verdict computation. Preserve the original parse fallback and True/False/None gate results after failures, ambiguous captures or graph changes. Keep diagnostic gate work outside static.time_s. Add parser-count, lifecycle, mutation, timing-boundary and real static-analysis equivalence coverage; 126 related unit tests pass.
Reuse the pure-Select path's existing normalized conditions across the weak and guarded attempts while keeping original conditions as snapshot certificate inputs. Return directly on literal false relaxations without constructing QF_LIA solvers. Retain the weak-first policy already present at 12fe429, including exception fallback, empty-lemma reuse and independent 500 ms budgets; this change adds no SMT attempts. Preserve snapshot gates, unsupported-input exception boundaries, general radix processing and independent feasibility. Add source-premise, normalization-count, solver-count, custom-context and fallback regressions. The relevant selection including existing lazy-precheck tests passes 149 tests, and all repository checks pass. No kernel performance claim is made.
Gate full read discovery on shallow top-level cell candidates and defer fact assembly when no current symbolic read applies. Certify each relevant array using its complete current original facts, preserving standalone lemma order, context isolation, and mutation behavior. Reuse each immutable AST child tuple across recognition, read discovery, and fact assembly. Preserve the literal-cell shortcut from f5a8466 and leave the existing solver checks and budgets unchanged. Add structural operation-count and boundary regressions; 149 focused unit tests and all applicable pre-commit hooks pass.
Reuse successful TTIR parsing for gate metadata, avoid irrelevant snapshot certification and repeated AST child enumeration, and reuse normalization with literal-false precheck exits. Preserve the independently landed weak-first policy at 12fe429. Each change retains the original query semantics and carries targeted correctness and operation-count tests.
Accept the exact triton root module alongside its descendants so next_power_of_2 and cdiv retain their checked ConstexprFunction identities. Preserve callable source, code, defaults, closures, parent-child equality and fail-closed handling. Add six regression instances for serialization and rejected replacements. All 73 related tests pass; both affected FLA launches pass real READY admission and complete L2 with proved@enum. Record the source-bound checks while leaving the active frozen rerun unchanged.
Balance the 70 labeled TritonRaceBench cases at 35 racy and 35 race-free without modifying historical cases. Add independent output and registration checks and record the correctness arguments and analysis limitations. Existing pinned paper measurements remain unchanged.
Distinguish atomic-address refusals caused by the symbolic grid's counter wrap bound, then rebuild the complete static query at the supplied launch extent without relaxing counting guards. Bind existing grid expressions, check every relevant pair and feasibility, and retain launch-only proof provenance and the original analysis conditions. Add 16 regressions covering vector batch tickets, real overflow and other counter guards, cross-instance and duplicate-lane races, NumPrograms binding, vacuity, unknown feasibility, and content qualification. Validation: 146 focused solver/frontend tests passed; the 16 new tests passed again after formatting; all applicable pre-commit hooks passed. The unchanged trb013_batch_ticket_no case now returns proved@T1-launch through the native complete-system harness at grid 4.
Admit the exact ordinary-CAS fragment through the existing conditional write, reads-from and synchronization machinery. Preserve operand observations in copy-local renaming and explicitly lower boolean values to zero or one. Refuse loaded operands, arithmetic, unmodeled observations and width changes rather than inventing CAS success or publication values. Keep generic reader behavior and the existing awaited-CAS admission unchanged; cast checks only gate ordinary CAS and add no scan for non-CAS kernels. Cover role-specific release/acquire CAS, CAS unlock, failed-CAS nonwriting, failure-acquire, semantic/scope mutations, operand dependence, overflow and cast-chain refusal. Preserve all benchmark kernels and labels.
Separate operational control conditions from execution-domain assumptions when deriving atomic value dependencies. Retain legacy interpreter masks and loop premises, and preserve addresses, RMW operands and CAS conditions. Record preceding await candidates and all observations used by their exit conditions. Add same-copy control edges only under the await, target and source activities, so exclusive branches do not create false cycles while real relaxed wait/publication cycles remain forbidden. Keep all termination premises and the independent feasibility obligation. Add 21 regression cases covering independent/sequential waits, branch joins, expected-value dependencies, domain predicates and genuine RF/value cycles. Validation: 255 focused tests pass; all applicable pre-commit checks pass.
The definitive pinned manifest rejected every non-rehearsal roster whose size differed from the 1242 rows frozen before cf099aa added the seven race-free TritonRaceBench repair variants. The committed corpus now enumerates 1249 rows over the same 17 corpora, so the frozen count moves to 1249; rehearsal manifests, row identities, sidecar checks and every other admission rule are unchanged. PINNED_RESUME.md states the new count. Validation: the pinned run, resume and state unit tests pass.
Reuse whole-storage and identical-view digests only for ordinary physical tensor views within a single identity calculation. Hash continuous byte buffers directly, preserving layout, aliases, reinterpretation, mutation detection and exceptional-view behavior. Add compatibility and work-count tests; the 67 focused dynamic transport and runtime-dependency tests pass.
Add an explicit preload launcher with fresh row workers and fresh analysis children. Bind each completed row to real child wait receipts, verify the service domain before acceptance, and retain fully charged session setup, shutdown, interruption and recovery records. Freeze launcher/environment/source identities and validate original receipt hashes again at publication. Add prepare-only creation so a run can be frozen without dispatching a service. Keep the ordinary launcher as the default and leave private mmap disabled. Validation: 80 mocked launcher/controller/resume unit tests and the normal pre-commit checks pass. Real integrated lifecycle checks and full L2 execution await the user's explicit start order.
The TritonRaceBench cuTile track covered 62 of the Triton roster's rows; the seven race-free repair rows added at cf099aa had no twin. Port them with the corpus conventions: same row name, ground-truth label, pattern, grid and argument contents, atomics one to one with sem/scope written as MemoryOrder/MemoryScope, captured on the same cuda.tile 1.5.0, torch and sm_89 as the original rows. The 62 pre-existing captures are unchanged byte for byte, and no pre-existing verdict moves. Six of the seven Triton kernels order the payload against the synchronizing atomic with tl.debug_barrier; batch_ticket_queue needs no such order. cuda.tile has no fence, and its token pass does not order everything unconditionally: same-array accesses chain directly, and a RELEASE or ACQ_REL atomic receives join_tokens of the preceding memory operations while a RELAXED or ACQUIRE-only atomic receives none. Every twin rests on the second edge or needs no order at all, and trb026_fenced_tile_handoff_no is the corpus's first row whose label rests on a cross-allocation token edge. The module docstring records the rule; the previous wording ("supplies the order unconditionally") was wrong and is corrected. trb026_reread_unfenced_yes and trb026_guarded_no_producer_fence_yes stay Triton-only: they are racy BECAUSE a fence is absent, and their cuTile port is textually identical to an already-registered row carrying the opposite label. The track therefore covers 69 of 71 rows and the frozen definitive roster moves from 1,249 to 1,256 configurations; runs pinned before this commit keep their own manifests. check_tritonracebench_cutile_twins.py validates, independently of any detector verdict, the catalog and twin pairing, the token chains each label rests on (with a negative control on two racy rows that must have no releasing atomic), and ten launches per new row against the outputs the Triton twin is specified to produce. At L2 three rows prove and four abstain on reader-fragment boundaries that already bound pre-existing rows: indirect-address for the ticket queue, cas-value for the three with an ordinary non-spin CAS. No new row reports a race. Validation: 391 focused pinned/cuTile unit tests pass; the twin checker passes with --gpu; all applicable pre-commit hooks pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VWiTd5LAf1x9kgU5Uf66N7
cuda.tile writes a bitonic partner index as an integer xor and a radix key
as a shift, straight into an address. The reader refused those rows with
indirect-address while their Triton twins, which reach the same addresses
through floordiv/mod, were decided; the corpus even carries the control,
ctb_top_k_selection___bitonic_step_kernel, a bitonic step written
arithmetically that proved all along.
_fold_bitwise rewrites an integer bitwise operation into the existing
affine fragment when the second operand is a known integer of a shape
whose identity is exact: a shift by a known count, a mask of 2^k - 1, and
a xor with a single bit. Bin("//") and Bin("%") truncate toward zero, so
floor division and floor modulo are written out rather than assumed, which
makes every identity exact for negative operands too. Anything else keeps
its DataDep and the refusal; nothing widens a footprint.
A shift count or mask is usually a scalar argument known only from the
captured launch, so parse_cutile_ir now takes those values and marks a
graph that consumed one param_pinned. t0_linearity_gate refuses such a
graph, so the ANY-params claim is never made from a rewrite that holds for
one launch's parameters; a lowering from a literal pins nothing.
Also fixes a soundness hole found by the new tests: raw_binary_bitwise
bound and_/or_ to a boolean conjunction regardless of result type, so an
integer and_ in an address became a modeled boolean term instead of an
abstention. The branch is now guarded on a boolean result.
Measured: every row of both cuTile corpora rerun at L2 (130 rows). Exactly
two verdicts change, both abstain to race-free (proved@T1): the two
bitonic_sort steps. No other verdict, no proof rung, and no Triton-track
row moves. tilebench_cutile goes from 47 proofs and 14 abstentions to 49
and 12. Record: evaluation/CUTILE_BITWISE_ADDRESSING.md.
Validation: 2041 unit tests pass; all applicable pre-commit hooks pass; the
lowering identities were checked against Python's operators over 192,240
values including negative and large ones.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VWiTd5LAf1x9kgU5Uf66N7
cuda.tile has no `for` construct in its final IR for a python `while`. A kernel written as `while m_tile < n_tiles: ...; m_tile += 1` lowers to the while-form `loop` construct, with the counter as a loop-carried value, the test as the first body operation, and the exit as a `break` in that test's else arm. The reader refused every while-form loop carrying a non-token value, because a carried value in general means a data-dependent trip count. The counter shape is not that: it has an ordinary range trip count, and the Triton twins of the same operators, which spell it `for m_tile in range(...)`, were decided all along. _counted_while_shape matches that shape on the IR text, before any state is touched, and hands _lift_counted_loop the bounds range(init, bound, K). That function is the former body of _handle_for, now shared, so a counted while and its `for` twin build the same AccessGraph: one LoopInfo slot, the counter bound to LoopVar, other carried values bound to DataDep, the same zero-trip rule, and the same _serial_loop_boundary obligation on the body. Every clause of the match is a soundness obligation. The test must be the first body operation (no do-while); exactly one integer scalar slot is the counter; the bound names no carried parameter, and is read on the first body line so SSA dominance puts its definition outside the loop; `then` is a bare yield and `else` a break whose operands repeat the carried parameters in order; no other break targets this loop and the body's only terminator is its trailing continue; the counter advances by a positive integer constant at the top level of the body. Single exit matters most, because the zero-trip rule deletes in-loop accesses rather than widening them, so a loop that can also leave early would lose real accesses. A break inside a nested `if` region still exits the enclosing loop, so _nesting_scan treats only a nested loop, for, or combiner do block as shielding one. Anything that fails a clause falls through unchanged, first to the AWAIT shape and then to the byte-identical control-flow refusal. Stream-K's first_wave_kernel is the live example: its outer iterator advances by min, which is the data-dependent walk the refusal exists for. Both cuTile corpora were rerun at L2 (130 rows). Exactly four verdicts changed, all abstain to race-free (proved@T1): the three linear_self_attention kernels and streamk_matmul full_tiles. All 69 tritonracebench_cutile rows are unchanged in verdict and reason, so the await shape and the planted races are untouched. tilebench_cutile goes from 49 proofs and 12 abstentions to 53 and 8. A parse-level sweep of both corpora in both modes (260 outcomes) shows nine differences: those four rows plus block_sparse_attention, whose refusal advances from control-flow to the loaded tile index that Route 2 owns. Two unit tests carry the negative control: a counted while writing tile bid*N + i, token-chained, proves race free, and the same kernel with the block id dropped still reports the race. Six more pin the refusals and the inherited cross-iteration obligation. Record in evaluation/CUTILE_COUNTED_WHILE_LOOP.md. The pinned evaluation numbers are unchanged; a cuTile population including these proofs needs a new pinned run. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VWiTd5LAf1x9kgU5Uf66N7
Route 2 gave the Triton track a source of values for addresses that depend on a loaded value (evaluation/ROUTE2_SNAPSHOT_SELECT.md): an integer load with a modeled mask binds a Loaded term, the encoder turns it into a Select over the tensor's pre-launch contents, and the proof is content-qualified. The cuTile track had neither half. Its reader bound DataDep for every loaded value, and its captures predate the value-capture rule, so all 166 tensor descriptors were value-free. Six real-operator rows and five benchmark rows abstained for that reason while their Triton twins decided. _loaded_binding mirrors the TTIR reader's loaded_binding clause for clause: bound only under multipath (L2), so L0 and L1 keep DataDep and every refusal message is byte-identical; a float pointee or a DROPPED mask keeps DataDep, because only a modeled mask can keep a masked-off lane apart from the snapshot value. cuTile has no `other` operand, so it comes from the source: a partition view's padding_mode=ZERO supplies Const(0), UNDETERMINED and NEG_INF leave the lane unspecified, and load_pointer takes its padding_value when that is modelable. Both cuTile captures now record the address snapshot under the Triton track's own bound (ADDRESS_SNAPSHOT_MAX_ELEMENTS), and _cutile_bindings passes it into GlobalTensor gated on L2 exactly as CompiledRaceDetector gates the capture. Both corpora were re-captured on the pinned TileBench checkout with cuda.tile 1.5.0, all 45 operators and all 69 benchmark rows, zero failures. The merge adds ONLY the new value fields and refuses on anything else: 61 rows and 183 fields for tilebench_cutile, 69 rows and 170 for tritonracebench_cutile, zero problems, with the IR text and every pre-existing descriptor byte-identical and no row added or removed. A claim-strength fix came out of it. param_pinned, introduced with the exact bitwise lowering, was a WHOLE-GRAPH flag set by any rewrite that consumed a scalar param's captured value, and the T0 gate refuses such a graph. That was safe while those rewrites only happened in address chains, because a loaded operand was DataDep and the fold refused. With Loaded bound, radix sort's (key >> bit) & 1 folds, and the two count_ones_in_block rows fell from proved@T0 to proved@T1 although the value is only counted, never used to address. _fold_bitwise now records the rewritten TERM and _pinned_claim marks the graph only when one reaches a position the claim rests on: an address, mask, path, exit predicate, atomic operand or loop bound. The bitonic rows still pin and the gate still refuses them. At L2 tilebench_cutile goes from 53 proofs and 8 abstentions to 57 and 4, the four being block_sparse_attention and cross_entropy at proved@T1+content and both destindex rows at proved@T1-launch+content. tritonracebench_cutile goes from 24 race-free / 24 race / 21 abstain to 26 / 27 / 16, and every one of those five rows now matches its oracle label, including trb010_gather_no at proved@T0, the read-only-group rule Route 2 predicts. Level invariance was measured rather than assumed: the re-capture also filled in init_values, which is not gated on L2, so both corpora were rerun at L0 against the old and new specs with zero differences in verdict, terminal or reason. The scatter litmus in cuTile IR carries the negative control: a permutation proves content-qualified, one duplicated index reports exactly one race, no snapshot refuses by name, and single-path reproduces the pre-Route-2 message verbatim. Record in evaluation/CUTILE_ROUTE2_SNAPSHOT.md. The pinned evaluation numbers are unchanged; adopting any of this needs a new pinned run. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VWiTd5LAf1x9kgU5Uf66N7
The real-operator cuTile experiment measured 61 configurations, one per TileBench operator at case 0 of its own benchmark case grid, because the capture ran run_benchmark_suite(op, case_indices=[0]). Every operator's grid holds twenty or more cases, so a second configuration is an already-authored input shape rather than a new kernel or a fabricated one. tilebench_cutile_capture gains a --case-index flag: a non-zero index stores the record under the case name <op>_case<N> and records case_index and case_params, so the configuration reads off the corpus without the TileBench checkout. The corpus module builds those as ctb_<op>_case1__<kernel>. The seven are chosen by rule, not by convenience: every SINGLE-KERNEL operator whose case 1 changes a shape or a structural parameter rather than only the element dtype. Single-kernel keeps one operator contributing exactly one configuration; a shape change makes the configuration genuinely new. Eight operators qualify and quantize_global is left out, being the same change on the same shape as fused_activation. The seven are flash_attention (seq_len 1024 to 2048), flash_decode (seq_len 2048 to 4096), block_sparse_attention (M 512 to 1024), dequantize_rowwise (cols 512 to 1024), kl_divergence (cols 1024 to 2048), matmul_int8 (K 1024 to 2048) and fused_activation (n doubled). Four compile to different CuTile IR; the other three compile to the same text but launch differently, changing the grid or the array extents the flattened shape parameters carry, so all seven encode differently. All seven were captured on the pinned TileBench checkout with cuda.tile 1.5.0 on the RTX 4090, zero errors, one kernel record each. The merge refuses on anything but an addition: every pre-existing case entry byte-identical, no new record duplicating an existing one under the capture's own fingerprint, and the total landing on 68. It reported 7 rows added, 68 total, zero problems. Rerun at L2 the corpus is 68 rows, 64 proofs and 4 abstentions. All seven new configurations prove, and none of the 61 pre-existing rows changed verdict or proof rung. The four abstentions are the ones the abstention-closure work left open: histogram_partial against the address-snapshot bound, both radix_sort rows through tile_scan, and stream-K's data-dependent first_wave walk. The frozen pinned roster goes from 1256 to 1263. These rows have no same-operator Triton twin, since the tilebench corpus is at case 0, so they sit outside the cross-DSL differential; the corpus module says so. Record in evaluation/CUTILE_SECOND_CONFIGURATIONS.md. The pinned evaluation numbers are unchanged: the paper's real-operator group may be restated as 68 with 64 proofs and 4 abstentions only after a pinned run adopts it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VWiTd5LAf1x9kgU5Uf66N7
This branch has not been deployed
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.