[mark14wu]

Summary

The second layer of the race detector port: the race detector's pure-Z3 solver library, taken from the frozen PR #361 (62c6d7c). Nothing calls it yet. The eager race detector client that uses it comes in the next PR, and the compiled race detector later.

No user-visible change: no client, config field or environment variable is added, and the eager sanitizer, tracer, profiler and compiled sanitizer are untouched.

Stacked on #501 (top of #494 → #479 → #495 → #480 → #482 → #501). Triton 3.8 only.

Change

Modules under tilelens/clients/race_detector/, ported from #361 with triton_viz renamed to tilelens:

• two_copy_symbolic_hb_solver.py: TwoCopySymbolicHBSolver. It lowers the access records under two program instances, alpha-renaming pids, arange lanes and per-record copy-local vars (CAS and RMW returns, loop iterators). It then asks Z3 for pairs of events that conflict, alias and are not ordered by happens-before: across two instances, and between lanes or operations of one instance. find_races() returns RaceReports with a RAW/WAR/WAW type, a witness address and the two witness pids. check_feasibility() checks that the launch's premises admit some execution, so a race-free result over no executions is not reported as a proof. The model covers:

  • CAS, and integer RMW returns (add/max/min/xchg, and or/xor with 0) as values: closed-world read-from with an rf_unknown escape when an unmodeled writer can overlap, per-location atomic coherence, value causality (no out-of-thin-air values), release sequences through RMW chains, and the counting axiom (last block done, work-queue slots, single winner) with its guards;
  • await records (await_dependencies, await_observations, causal_constraints) and pre-exit representatives;
  • the enumeration fallback: an undecided query is re-asked as a case split over concrete pids at enum_fallback_grid;
  • the restrictions the compiled race detector needs: only_pairs, launch_ceiling, extra_assumptions.

  Z3 unknown is never read as UNSAT. An undecided race or feasibility query raises UnsupportedSymbolicRaceQuery, and an undecided overlap check opens the rf_unknown escape. The constructor raises the same exception (or its subclass CountingScopeUnsupported, which the compiled race detector retries at a pinned grid) when a record cannot be lowered. The caller must report such a launch as unsupported, never as race-free. All terms live in Z3's main context, which is not thread-safe, so the caller serializes solves (the module docstring says so).

• hb_common.py: shared primitives (substitution, lane helpers, the conflict predicate for atomic pairs, the read-from predicate) and the sparse transitive HB closure.

• conflict_simplification.py, snapshot_lemmas.py: the conflict precheck. It relaxes nonlinear and array terms in a necessary conflict condition and may only discard a pair when that weaker condition is UNSAT. Snapshot lemmas add the range and injectivity facts that complete integer tables already asserted in the query entail.

• guarded_division.py: folds a variable divisor to a constant only when an original top-level mask in the query proves its value.

• report_diagnostics.py: explains an intra-instance witness between two operations that no captured fence orders.

• data.py: [FEAT] [RACE DETECTOR] Z3-based race detector #361's version replaces the skeleton's. It adds RaceType, RaceReport and the solver's record fields to AccessEventRecord. The skeleton's fields are unchanged, so race_detector.py and its tests are unchanged. RaceReport.race_type drops [FEAT] [RACE DETECTOR] Z3-based race detector #361's access-mode fallback, which only HBSolver's reports used; the two-copy solver always sets the type.

• The 7-line hb_solver.py placeholder is deleted. Nothing imported it.

What changed from #361:

• Fence rule is a hook. Fence order is always on: program order between two operations of one instance is a happens-before edge only when a fence separates them, and unfenced pairs of distinct operations enter the intra-instance query. Which fence orders which pair is now the caller's rule. The solver takes fence_between(first, second) -> bool, asked for two records of one instance with first.program_seq < second.program_seq, and caches each answer per record pair. None means no fence orders any pair. This replaces the fence_seqs float tuple and _fence_between, so the eager race detector can keep [FEAT] [RACE DETECTOR] Z3-based race detector #361's sequence-position rule while the compiled one uses its own. The solver owns no fence policy. The missing-fence diagnostic asks the same hook (its boolean argument is now fenced, and its text says "no captured fence that orders them", which is right for either rule).
• Per-solve Z3 timeout. Every Solver the two-copy solver creates (race queries, feasibility, guard and overlap checks, enumeration cases) gets its own timeout. It comes from the constructor's timeout_ms, defaulting to TwoCopySymbolicHBSolver.TIMEOUT_MS = 180_000 (180 s, the eager budget); timeout_ms <= 0 raises ValueError, because Z3 reads 0 as "no limit". No global Z3 parameter is set, so a solve cannot change Z3's defaults for another client such as the compiled sanitizer. In [FEAT] [RACE DETECTOR] Z3-based race detector #361 the compiled client set the global timeout around each solve, and the eager client set none. The enumeration fallback's 5 s per case and 10 s capped retry are now min(timeout_ms, limit), so they only ever shorten the caller's budget. For any timeout_ms of 10 s or more (180 s eager, 10 s / 120 s compiled) this is [FEAT] [RACE DETECTOR] Z3-based race detector #361's behaviour. The precheck's 500 ms and the division certificate's 200 ms stay fixed, per-solver budgets: an undecided precheck keeps the pair for the full query, and an undecided certificate keeps the original formula. An unknown answer still raises UnsupportedSymbolicRaceQuery; Z3's reason (for example timeout) is only in the message for now, and the eager client in the next PR decides whether it needs it as an attribute.

Removed while porting. #361's default path is fence-ordered and non-ablated, and these removals leave that path's behaviour unchanged:

• the fence_order=False reading (every earlier operation orders every later one), and with it the fence_order argument of the diagnostic. A caller can still get that reading with a hook that returns True;
• cuTile token order (token_order and its guards). cuTile support comes much later;
• the ablations switch ("hb", "coherence"), which only the evaluation harness used;
• hb_common.minimal_atomic_read_from, which only the HBSolver demo used, and the getattr fallbacks for demo events without a width, scope or pid. The unused iter_lane is also dropped;
• comments that referred to removed features, to [FEAT] [RACE DETECTOR] Z3-based race detector #361's clients, or to internal design notes; the intra-instance comments now describe the fence-ordered reading only.

Kept: the compiled-only paths (enum_fallback_grid, only_pairs, launch_ceiling, extra_assumptions, await records), which the compiled race detector needs. Splitting the solver across PRs would cost more review churn. Also kept: the private _ENABLE_* switches in conflict_simplification.py and guarded_division.py, which tests use to compare a precheck path with the full query.

Not ported: bounds.py. Only #361's concrete-enumeration channel and compiled replay use it, and neither is in this PR, so it would be dead code here. It can come with the first PR that needs it.

Tests

New tests in tests/unit/race_detector/ are pure Z3 on hand-built records, with no interpreter. They are a rewritten subset of #361's solver unit tests, one case per distinct behaviour. Most proofs have a twin, one changed premise away, that must flip to a report.

• test_two_copy_solver.py:
  • cross-instance pid and lane renaming;
  • each RaceType;
  • masks and byte overlap;
  • fences through the hook: unfenced operations of one instance race with the missing-fence explanation; a fence between them orders them; the hook is called with the records in program order; with three operations each pair gets its own answer; dependency order;
  • atomics: same-location/same-width exemption, torn widths, cta scope across CTAs, the CAS try-lock single winner, float and oversized flags falling back to rf_unknown;
  • release/acquire CAS ordering only through the exact location, and only across a fence;
  • duplicate lanes in one instance;
  • feasibility with unsatisfiable premises;
  • only_pairs and extra_assumptions;
  • the enumeration fallback and its refusals, including an undecided case, which re-raises the original unknown;
  • timeouts: every Solver instance created during construction, find_races() and check_feasibility() carries timeout_ms; with launch_ceiling the 10 s retry cap applies only when timeout_ms is larger, and enumeration cases never exceed timeout_ms; timeout_ms=0 is rejected; z3.get_param("timeout") is unchanged after a solve; a 50 ms timeout makes an x³ + y³ = z³ query raise UnsupportedSymbolicRaceQuery instead of hanging (run in a thread with a 60 s join, so a regression fails instead of hanging CI);
  • an undecided overlap check opens rf_unknown.
• test_rmw_solver.py:
  • the written-value table, and the max/min write parts reaching a relaxed reader (a wrong write part would hide the data race);
  • last block done, the single winner and work-queue slots (counting axiom) and their twins;
  • an uncounted observation in an address is unsupported; a counter that may wrap on a symbolic grid raises CountingScopeUnsupported, and one that wraps on a concrete grid raises the plain exception;
  • the rf_chain source;
  • the counting guards, including wraparound, where the wrap-gated store must race (a wrap-capable add counts as an unmodeled writer);
  • release sequences through an RMW chain, which race without fences;
  • torn-width writers;
  • an await's exit as a control dependency, where zero flags make the premises infeasible and the twin without the edge is feasible;
  • a pre-exit representative opens no rf_unknown escape for its own poll.
• test_hb_closure.py: the sparse closure against the layered recurrence (conditional edges, cycles, arrays, a custom context); program-order edges for every fence and dependency case; reads-through scope checks.
• test_conflict_precheck.py: mixed-radix relaxation and the premises it needs; the private switches; an unknown precheck falls back to the full query; snapshot lemmas (range, injectivity, holes, duplicates, conditional cells), and the solver's SnapshotLemmaCache refusing a table with a hole; launch scope versus any grid; the UNSAT query cache; the base-constraint cache following mutated families.
• test_guarded_division.py: mask-certified folding; absent or conditional masks keep zero and negative divisors; every certificate failure keeps the original formula; the applicability cache.
• solver_records.py: record builders and two fence hooks, fences_at(*positions) ([FEAT] [RACE DETECTOR] Z3-based race detector #361's sequence rule) and every_fence.

Not ported: tests that need the eager client, the TTIR/cuTile readers, the compiled client, replay or concrete enumeration (for example test_cutile_loop_conflicts.py, test_route2_snapshot_select.py, test_t0_symbolic_loop_bounds.py, test_await_abstraction.py, the end-to-end test_fence_order.py).

Equivalence check (not committed): before trimming, I ran #361's 22 pure-solver test files unchanged against the ported solver through a shim that maps fence_order=False to a hook returning True and fence_order=True, fence_seqs=… to the sequence rule. 466 passed. The 19 token-order and ablation cases were skipped. The rename-only copy had passed all 485.

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

uv run --extra test pytest tests/unit/race_detector -q -p no:cacheprovider [-n 4]
uv run --extra test pytest tests/unit/test_race_detector.py tests/end_to_end/test_race_detector.py -q -p no:cacheprovider

The new solver tests: 129 passed, serial and -n 4, in about 4 s. With the race detector skeleton tests: 139 passed.

Mutation checks (not committed): each of these single-line mutations makes at least one new test fail: an undecided enumeration case read as UNSAT; the snapshot cache accepting a table with a hole; max/min write parts replaced by the old value; a wrap-capable add not counted as an unmodeled writer; a bare Solver() in the guard-check or base solver; one cached fence answer reused for every pair; the enumeration's case and retry limits not capped by timeout_ms.

Regression gate: the same 20 files as #501. The base is a pristine worktree of #501's head (bc229ce).

run	base bc229ce	this PR
serial	544 passed, 2 skipped	544 passed, 2 skipped
-n 4	544 passed, 2 skipped	544 passed, 2 skipped

Line counts, from git diff --numstat against bc229ce:

module	added
two_copy_symbolic_hb_solver.py	2626
conflict_simplification.py	434
snapshot_lemmas.py	425
hb_common.py	262
guarded_division.py	260
data.py	131 (151 total)
report_diagnostics.py	71
hb_solver.py	7 deleted
product	4209 added, 7 deleted
tests (6 files)	1771 added

Added test lines stay below added product lines (1771 ≤ 4209). The two-copy solver is 62% of the product lines. The precheck modules (conflict_simplification.py, snapshot_lemmas.py, guarded_division.py, 1119 lines) only speed queries up: the precheck discards a pair only when it is UNSAT, and the folding keeps the query equivalent. They could move to a follow-up PR if that is easier to review; the solver would then ship first without the precheck and the folding.

[github-actions]

Performance Benchmark

Benchmark	main (min)	PR (min)	Change	Samples
gemm	0.104s	0.106s	+1.8%	20 / 20
gemm_oob	0.116s	0.119s	+2.5%	20 / 20
indirect_load	0.022s	0.022s	+1.8%	20 / 20
nested_loop	0.233s	0.235s	+0.8%	20 / 20
block_pointer_loop_advance	0.124s	0.126s	+1.9%	20 / 20
liger_jsd	0.138s	0.140s	+1.2%	20 / 20
flaggems_layernorm	0.390s	0.395s	+1.3%	20 / 20
swiglu	0.169s	0.172s	+1.5%	20 / 20
cross_entropy	0.966s	0.979s	+1.3%	20 / 20
fused_linear_jsd	0.210s	0.212s	+1.2%	20 / 20
Total	2.473s	2.507s	+1.4%	N/A

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