From dac6207e99adbd1085de65d3eae253873ee69033 Mon Sep 17 00:00:00 2001 From: Hao Wu Date: Tue, 13 Oct 2026 12:39:29 -0400 Subject: [PATCH] [FEAT] Add the race detector's two-copy happens-before solver The race detector's pure-Z3 solver library from PR #361, for the eager and compiled race detectors to call; no client uses it yet. - two_copy_symbolic_hb_solver.py: TwoCopySymbolicHBSolver lowers the records under two alpha-renamed program instances and asks Z3 for unordered, conflicting, aliasing event pairs across instances and between lanes or operations of one instance. It models CAS and value-modeled RMW returns (closed-world read-from, per-location atomic coherence, value causality, reads-through release sequences, the counting axiom), await records and pre-exit representatives, the feasibility check, the enumeration fallback, and the compiled restrictions (only_pairs, launch_ceiling, extra_assumptions). - hb_common.py (shared primitives, transitive HB closure), conflict_simplification.py and snapshot_lemmas.py (the UNSAT-only conflict precheck), guarded_division.py (certified divisor folding), report_diagnostics.py (the missing-fence explanation). - data.py gains RaceType, RaceReport and the solver's record fields; the hb_solver.py placeholder is deleted. Changes from #361: - Fence order is always on, and which fence orders which pair is the caller's rule: the solver takes fence_between(first, second), asked for two records of one instance in program order (None: no fence orders any pair). It replaces fence_seqs, so the eager and the compiled detector can each keep their own fence rule. - Every Solver gets its own timeout (timeout_ms, default TIMEOUT_MS = 180 s, must be positive); no global Z3 parameter is set. The enumeration's 5 s per-case and 10 s retry limits are capped by timeout_ms. An unknown answer stays unsupported. - RaceReport.race_type drops the access-mode fallback only HBSolver reports used. - Removed: the fence_order=False reading, cuTile token order, the ablations switch, CAS-only minimal_atomic_read_from and the unused iter_lane. --- tests/unit/race_detector/__init__.py | 0 tests/unit/race_detector/solver_records.py | 145 + .../race_detector/test_conflict_precheck.py | 343 +++ .../race_detector/test_guarded_division.py | 119 + tests/unit/race_detector/test_hb_closure.py | 166 ++ tests/unit/race_detector/test_rmw_solver.py | 449 +++ .../race_detector/test_two_copy_solver.py | 549 ++++ .../race_detector/conflict_simplification.py | 434 +++ tilelens/clients/race_detector/data.py | 131 + .../clients/race_detector/guarded_division.py | 260 ++ tilelens/clients/race_detector/hb_common.py | 262 ++ tilelens/clients/race_detector/hb_solver.py | 7 - .../race_detector/report_diagnostics.py | 71 + .../clients/race_detector/snapshot_lemmas.py | 425 +++ .../two_copy_symbolic_hb_solver.py | 2626 +++++++++++++++++ 15 files changed, 5980 insertions(+), 7 deletions(-) create mode 100644 tests/unit/race_detector/__init__.py create mode 100644 tests/unit/race_detector/solver_records.py create mode 100644 tests/unit/race_detector/test_conflict_precheck.py create mode 100644 tests/unit/race_detector/test_guarded_division.py create mode 100644 tests/unit/race_detector/test_hb_closure.py create mode 100644 tests/unit/race_detector/test_rmw_solver.py create mode 100644 tests/unit/race_detector/test_two_copy_solver.py create mode 100644 tilelens/clients/race_detector/conflict_simplification.py create mode 100644 tilelens/clients/race_detector/guarded_division.py create mode 100644 tilelens/clients/race_detector/hb_common.py delete mode 100644 tilelens/clients/race_detector/hb_solver.py create mode 100644 tilelens/clients/race_detector/report_diagnostics.py create mode 100644 tilelens/clients/race_detector/snapshot_lemmas.py create mode 100644 tilelens/clients/race_detector/two_copy_symbolic_hb_solver.py diff --git a/tests/unit/race_detector/__init__.py b/tests/unit/race_detector/__init__.py new file mode 100644 index 000000000..e69de29bb diff --git a/tests/unit/race_detector/solver_records.py b/tests/unit/race_detector/solver_records.py new file mode 100644 index 000000000..bfac6e9e5 --- /dev/null +++ b/tests/unit/race_detector/solver_records.py @@ -0,0 +1,145 @@ +"""Hand-built AccessEventRecords for the two-copy solver's unit tests.""" + +from __future__ import annotations + +import torch + +from tilelens.clients.race_detector.data import AccessEventRecord +from tilelens.clients.race_detector.two_copy_symbolic_hb_solver import ( + TwoCopySymbolicHBSolver, +) +from tilelens.core.data import AtomicCas, AtomicRMW, Load, Store + + +def store(addr, *, event_id, program_seq=0, elem_size=4, mask=None, active=True): + return AccessEventRecord( + op_type=Store, + access_mode="write", + addr_expr=addr, + local_constraints=() if mask is None else (mask,), + active=active, + reads=False, + writes=True, + event_id=event_id, + program_seq=program_seq, + elem_size=elem_size, + ) + + +def load(addr, *, event_id, program_seq=0, elem_size=4, mask=None, active=True): + return AccessEventRecord( + op_type=Load, + access_mode="read", + addr_expr=addr, + local_constraints=() if mask is None else (mask,), + active=active, + reads=True, + writes=False, + event_id=event_id, + program_seq=program_seq, + elem_size=elem_size, + ) + + +def cas( + addr, + cmp_value, + new_value, + old_value, + *, + event_id, + program_seq=0, + sem="acq_rel", + scope="gpu", + elem_size=4, + tensor=None, + active=True, +): + return AccessEventRecord( + op_type=AtomicCas, + access_mode="read", + tensor=tensor, + addr_expr=addr, + active=active, + reads=True, + writes=None, + is_atomic=True, + atomic_kind="cas", + sem=sem, + scope=scope, + old_value=old_value, + cas_cmp_value=cmp_value, + cas_new_value=new_value, + event_id=event_id, + program_seq=program_seq, + elem_size=elem_size, + copy_local_vars=(old_value,), + ) + + +def rmw( + addr, + old=None, + *, + op=None, + operand=None, + event_id, + program_seq=0, + sem="acq_rel", + scope="gpu", + elem_size=4, + tensor=None, + active=True, +): + """An atomic RMW; value-modeled when ``old`` (its observation var) is + given, exactly like the CAS return.""" + return AccessEventRecord( + op_type=AtomicRMW, + access_mode="read", + tensor=tensor, + addr_expr=addr, + active=active, + reads=True, + writes=True, + is_atomic=True, + atomic_kind="rmw", + sem=sem, + scope=scope, + old_value=old, + rmw_op=op, + rmw_operand=operand, + event_id=event_id, + program_seq=program_seq, + elem_size=elem_size, + copy_local_vars=() if old is None else (old,), + ) + + +def counter(value=0): + return torch.full((1,), value, dtype=torch.int32) + + +def fences_at(*positions): + """The eager capture's fence rule: a fence recorded at program_seq + position ``f`` orders the two records exactly when ``f`` lies strictly + between their positions.""" + + def fence_between(first, second): + return any(first.program_seq < f < second.program_seq for f in positions) + + return fence_between + + +def every_fence(first, second): + """A fence between every two operations: source order is HB order.""" + return True + + +def solve(records, *, grid=(2, 1, 1), arange_dict=None, **kwargs): + return TwoCopySymbolicHBSolver( + records, grid=grid, arange_dict=arange_dict or {}, **kwargs + ) + + +def report_pairs(reports): + return {(r.first.event_id, r.second.event_id) for r in reports} diff --git a/tests/unit/race_detector/test_conflict_precheck.py b/tests/unit/race_detector/test_conflict_precheck.py new file mode 100644 index 000000000..81048a44d --- /dev/null +++ b/tests/unit/race_detector/test_conflict_precheck.py @@ -0,0 +1,343 @@ +"""The UNSAT-only conflict precheck, the snapshot lemmas it derives, and the +query caches: each may discard a pair only when the full query is UNSAT.""" + +from __future__ import annotations + +import pytest +import z3 + +from tilelens.clients.race_detector import conflict_simplification as cs +from tilelens.clients.race_detector import two_copy_symbolic_hb_solver as tc +from tilelens.clients.race_detector.snapshot_lemmas import ( + SnapshotLemmaCache, + snapshot_table_lemmas, +) +from tilelens.clients.symbolic_engine import SymbolicExpr + +from .solver_records import every_fence, rmw, solve, store + +PID0, PID2 = SymbolicExpr.PID0, SymbolicExpr.PID2 + + +def _check(*conditions): + solver = z3.Solver(ctx=conditions[0].ctx) + solver.set(timeout=2000) + solver.add(*conditions) + answer = solver.check() + assert answer != z3.unknown + return answer + + +# ──────────────────────── mixed-radix relaxation ──────────────────────── + + +def _radix_formula(*, missing=None, lane_extent=64, bytes_per_block=256): + """Two flattened block indices q*r + d with 0 <= d < r, r >= 1.""" + qa, qb, da, db, la, lb, r = z3.Ints("qa qb da db la lb radix") + aa = bytes_per_block * (qa * r + da) + 4 * la + ab = bytes_per_block * (qb * r + db) + 4 * lb + bounds = {"positive": r >= 1, "lower": da >= 0, "upper": da < r} + conditions = [value for name, value in bounds.items() if name != missing] + conditions += [ + db >= 0, + db < r, + la >= 0, + la < lane_extent, + lb >= 0, + lb < lane_extent, + z3.Or(qa != qb, da != db), + aa < ab + 4, + ab < aa + 4, + ] + correspondence = ((qb, qa), (db, da), (lb, la)) + variables = dict(qa=qa, qb=qb, da=da, db=db, la=la, lb=lb, r=r) + return conditions, correspondence, variables + + +def test_mixed_radix_precheck_proves_disjoint_blocks_without_pinning_radix(): + conditions, correspondence, _ = _radix_formula() + assert cs.conflict_impossible(conditions, correspondence) + + +@pytest.mark.parametrize( + "kwargs,witness", + [ + ({"missing": "positive"}, None), # implied, but not explicit + ({"missing": "lower"}, dict(r=2, qa=1, da=-1, qb=0, db=1, la=0, lb=0)), + ({"missing": "upper"}, dict(r=2, qa=0, da=2, qb=1, db=0, la=0, lb=0)), + # a lane carries into the next block + ({"lane_extent": 65}, dict(r=2, qa=0, qb=0, da=0, db=1, la=64, lb=0)), + # partial byte overlap of unequal starts + ( + {"lane_extent": 1, "bytes_per_block": 2}, + dict(r=2, qa=0, qb=0, da=0, db=1, la=0, lb=0), + ), + ], +) +def test_radix_relaxation_needs_every_original_premise(kwargs, witness): + conditions, correspondence, variables = _radix_formula(**kwargs) + assert not cs.conflict_impossible(conditions, correspondence) + if witness is not None: + pins = [variables[name] == value for name, value in witness.items()] + assert _check(*conditions, *pins) == z3.sat + + +@pytest.mark.parametrize("factor", ["radix", "snapshot"]) +def test_private_switch_disables_only_its_optional_path(monkeypatch, factor): + if factor == "radix": + conditions, correspondence, _ = _radix_formula() + switch = "_ENABLE_RADIX_PRECHECK" + else: + value = z3.Select( + z3.Array("switch_table", z3.IntSort(), z3.IntSort()), z3.Int("i") + ) + conditions, correspondence = [value < 0, value >= 0], () + switch = "_ENABLE_SNAPSHOT_PRECHECK" + assert cs.conflict_impossible(conditions, correspondence) + monkeypatch.setattr(cs, switch, False) + assert not cs.conflict_impossible(conditions, correspondence) + + +def test_unknown_precheck_leaves_the_pair_to_the_full_query(monkeypatch): + settings = [] + + class UnknownPrecheck: + def set(self, **options): + settings.append(options) + + def add(self, *conditions): + pass + + def check(self): + return z3.unknown + + monkeypatch.setattr(cs.z3, "SolverFor", lambda logic: UnknownPrecheck()) + g2 = z3.Int("grid_2") + rec = store(2 * (PID0 * g2 + PID2), event_id=0) + solver = solve([rec], grid=(1, 1, g2), extra_assumptions=(g2 == 2,)) + assert solver.find_races() + assert settings and all(options == {"timeout": 500} for options in settings) + + +def test_precheck_decides_disjoint_blocks_without_the_full_query(monkeypatch): + g0, g1, g2 = z3.Ints("grid_0 grid_1 grid_2") + row, col = z3.Ints("row col") + addr = 4 * (4096 * (PID0 * g2 + PID2) + 4096 * SymbolicExpr.PID1 + 64 * row + col) + mask = z3.And(SymbolicExpr.PID1 * 64 + row < 64, SymbolicExpr.PID1 * 64 + row >= 0) + solver = solve( + [store(1_000_000 + addr, event_id=0, mask=mask)], + grid=(g0, g1, g2), + arange_dict={(0, 64, "row"): (row, None), (0, 64, "col"): (col, None)}, + ) + + def full_query_must_not_run(*args): + raise AssertionError("the necessary conflict condition is already UNSAT") + + monkeypatch.setattr(solver, "_race_query_is_sat", full_query_must_not_run) + assert solver.find_races() == [] + assert [(kind, sat) for kind, _, sat in solver.query_stats] == [ + ("cross", False), + ("intra", False), + ] + # Feasibility stays an independent obligation of the full base system. + monkeypatch.setattr(solver, "_conflict_precheck", full_query_must_not_run) + assert solver.check_feasibility() + + +@pytest.mark.parametrize("atomic", [False, True]) +def test_partial_byte_overlap_survives_the_precheck(atomic): + g2 = z3.Int("grid_2") + addr = 2 * (PID0 * g2 + PID2) + rec = rmw(addr, event_id=0) if atomic else store(addr, event_id=0) + reports = solve([rec], grid=(1, 1, g2), extra_assumptions=(g2 == 2,)).find_races() + assert reports and reports[0].witness_grid_a != reports[0].witness_grid_b + + +# ──────────────────────── snapshot lemmas ──────────────────────── + + +def _snapshot(values=(9, 4, 7), *, start=0): + array = z3.Array("snapshot", z3.IntSort(), z3.IntSort()) + a, b, va, vb = z3.Ints("a b va vb") + cells = [array[start + i] == value for i, value in enumerate(values)] + return z3.And(*cells, array[a] == va, array[b] == vb), array, a, b + + +@pytest.mark.parametrize("start", [-8, 0, 13]) +def test_complete_table_entails_range_and_injectivity(start): + expression, array, a, b = _snapshot(start=start) + lemmas = snapshot_table_lemmas(expression) + assert len(lemmas) == 3 + assert _check(expression, z3.Not(z3.And(*lemmas))) == z3.unsat + inside = [a >= start, a <= start + 2, b >= start, b <= start + 2] + collide = [a != b, array[a] == array[b]] + assert _check(expression, *lemmas, *inside, *collide) == z3.unsat + # Outside the certified interval every value stays possible. + assert ( + _check(expression, *lemmas, a == start, b == 10**6, array[a] == array[b]) + == z3.sat + ) + + +def test_duplicate_values_or_a_missing_cell_keep_the_collision(): + expression, array, a, b = _snapshot((9, 9, 7)) + lemmas = snapshot_table_lemmas(expression) + assert len(lemmas) == 2 # range facts only + assert _check(expression, *lemmas, a == 0, b == 1, array[a] == array[b]) == z3.sat + expression, array, a, b = _snapshot() + holes = z3.And(*[c for c in expression.children() if not z3.eq(c, array[1] == 4)]) + assert snapshot_table_lemmas(holes) == () + # The solver's path: the cache must refuse the hole too. + assert SnapshotLemmaCache().lemmas([*holes.children()]) == () + + +@pytest.mark.parametrize("connective", ["or", "implies", "ite"]) +def test_conditional_cells_never_become_facts(connective): + expression, array, a, b = _snapshot() + cells, reads = expression.children()[:3], expression.children()[3:] + flag = z3.Bool("flag") + conditional = { + "or": z3.Or(flag, z3.And(*cells)), + "implies": z3.Implies(flag, z3.And(*cells)), + "ite": z3.If(flag, z3.And(*cells), z3.BoolVal(True)), + }[connective] + assert snapshot_table_lemmas(z3.And(conditional, *reads)) == () + assert SnapshotLemmaCache().lemmas([conditional, *reads]) == () + + +def test_cached_lemmas_match_the_standalone_helper_and_follow_changes(): + expression, array, a, b = _snapshot((2, 0, 1)) + cells, reads = list(expression.children()[:3]), expression.children()[3:] + cache = SnapshotLemmaCache() + lemmas = cache.lemmas([z3.And(*cells), *reads]) + expected = snapshot_table_lemmas(expression) + assert [x.sexpr() for x in lemmas] == [x.sexpr() for x in expected] + cells[1] = array[1] == 2 # a duplicate value drops the injectivity fact + assert len(cache.lemmas([*cells, *reads])) == 2 + + +def _destination_conflict(values=(2, 0, 1), *, launch=True): + table = z3.Array("destination", z3.IntSort(), z3.IntSort()) + pa, pb, la, lb, grid = z3.Ints("pa pb la lb grid") + address_a, address_b = 16 * table[pa] + 4 * la, 16 * table[pb] + 4 * lb + conditions = [ + *(table[index] == value for index, value in enumerate(values)), + grid >= 1, + pa >= 0, + pb >= 0, + pa < grid, + pb < grid, + pa != pb, + la >= 0, + lb >= 0, + la < 4, + lb < 4, + address_a < address_b + 4, + address_b < address_a + 4, + ] + if launch: + conditions.append(grid == len(values)) + return conditions + + +@pytest.mark.parametrize( + "values,launch,impossible", + [((2, 0, 1), True, True), ((2, 0, 1), False, False), ((2, 2, 1), True, False)], +) +def test_snapshot_precheck_keeps_scope_and_duplicate_destinations( + values, launch, impossible +): + """A permutation table rules out the collision at the launch extent only; + an any-grid query or a duplicate destination keeps it.""" + conditions = _destination_conflict(values, launch=launch) + assert (_check(*conditions) == z3.unsat) is impossible + answer = cs.conflict_impossible( + conditions, + simplify_first=True, + expression_cache=cs._PureSelectExpressionCache(), + snapshot_cache=SnapshotLemmaCache(), + ) + assert answer is impossible + + +def test_common_snapshot_premises_enable_the_linear_precheck(monkeypatch): + lane = z3.Int("common_lane") + table = z3.Array("common_table", z3.IntSort(), z3.IntSort()) + rec = store( + 4096 + 256 * PID0 + 4 * lane, event_id=0, mask=z3.And(lane >= 0, lane < 64) + ) + solver = solve( + [rec], + grid=(z3.Int("common_grid"), 1, 1), + arange_dict={(0, 64, "lane"): (lane, None)}, + extra_assumptions=(z3.Select(table, 0) == 7, z3.Select(table, 1) == 11), + ) + + def full_query_must_not_run(*args): + raise AssertionError("the linear necessary condition proves disjointness") + + monkeypatch.setattr(solver, "_race_query_is_sat", full_query_must_not_run) + assert solver.find_races() == [] + + +# ──────────────────────── query caches ──────────────────────── + + +def _repeated_stores(monkeypatch, *, grid=(2, 1, 1), **kwargs): + records = [store(4096 + 8 * PID0, event_id=i, program_seq=i) for i in range(2)] + core = solve(records, grid=grid, fence_between=every_fence, **kwargs) + # Exercise full-query reuse independently of the optional precheck. + monkeypatch.setattr(core, "_conflict_precheck", lambda *a, **kw: False) + return core + + +def test_identical_unsat_queries_are_decided_once_per_invocation(monkeypatch): + core = _repeated_stores(monkeypatch) + created = [] + original = tc.Solver + + def counted(*args, **kwargs): + created.append(True) + return original(*args, **kwargs) + + monkeypatch.setattr(tc, "Solver", counted) + assert core.find_races() == [] + assert len(created) == 1 + assert [(kind, sat) for kind, _, sat in core.query_stats] == [("cross", False)] * 4 + assert core.find_races() == [] and len(created) == 2 + + +def test_launch_extent_unsat_cannot_hide_an_any_grid_race(monkeypatch): + """The address ignores pid1: the fallback launch is disjoint, but a + second pid1 row aliases in the symbolic grid.""" + grid1 = z3.Int("any_grid_1") + core = _repeated_stores( + monkeypatch, grid=(2, grid1, 1), enum_fallback_grid=(2, 1, 1) + ) + original = core._race_query_is_sat + calls = [] + + def first_unknown(query, first, second): + calls.append(True) + if len(calls) == 1: + raise tc.UnsupportedSymbolicRaceQuery("force launch-only fallback") + return original(query, first, second) + + monkeypatch.setattr(core, "_race_query_is_sat", first_unknown) + reports = core.find_races() + assert core.enum_used and len(calls) == 4 + assert any(r.witness_grid_a[1] != r.witness_grid_b[1] for r in reports) + + +@pytest.mark.parametrize("family", ["rf_constraints", "extra_assumptions"]) +def test_base_constraint_cache_follows_mutated_families(family): + solver = solve([store(z3.IntVal(4096), event_id=0)], grid=(1, 1, 1)) + conditions = [] + setattr(solver, family, conditions) + assert solver._base_solver().check() == z3.sat + conditions.append(z3.BoolVal(False)) + assert solver._base_solver().check() == z3.unsat + conditions[0] = z3.BoolVal(True) + assert solver._base_solver().check() == z3.sat + solver.hb[0][0] = z3.BoolVal(True) # a forced HB cycle admits no execution + assert solver._base_solver().check() == z3.unsat diff --git a/tests/unit/race_detector/test_guarded_division.py b/tests/unit/race_detector/test_guarded_division.py new file mode 100644 index 000000000..f1d98455f --- /dev/null +++ b/tests/unit/race_detector/test_guarded_division.py @@ -0,0 +1,119 @@ +"""Guarded division folding: only an original mask certifies a variable +divisor's value, and every failure keeps the original query.""" + +from __future__ import annotations + +import pytest +import z3 + +from tilelens.clients.race_detector import guarded_division as gd + + +def _grouped(*, masked=True): + pid, lane, grid = z3.Ints("pid lane grid") + quotient = pid / 4 + size = z3.If(quotient >= 0, 2 - 2 * quotient, 2) + remainder = z3.If(size == 0, pid % 4, (pid % 4) % size) + row = 64 * quotient + 32 * remainder + lane + conditions = [pid >= 0, pid < grid, grid >= 1, lane >= 0, lane < 32] + if masked: + conditions.append(row < 64) + return z3.And(*conditions), (pid, lane, grid), quotient, size, row + + +def _check(formula, *extra): + solver = z3.Solver() + solver.set(timeout=3000) + solver.add(formula, *extra) + result = solver.check() + assert result != z3.unknown + return result, solver + + +def test_access_mask_certifies_constants_without_a_grid_pin(): + original, (pid, lane, grid), quotient, size, _ = _grouped() + rewritten = gd.guarded_division_normal_form(original) + assert not z3.eq(original, rewritten) + assert _check(z3.Xor(original, rewritten))[0] == z3.unsat + for extent in (4, 1000000): + answer, solver = _check(rewritten, grid == extent, pid == 1, lane == 0) + assert answer == z3.sat + model = solver.model() + assert z3.is_true(model.eval(original, model_completion=True)) + assert model.eval(quotient).as_long() == 0 + assert model.eval(size).as_long() == 2 + + +@pytest.mark.parametrize("guard", [None, "or", "implies"]) +def test_absent_or_conditional_mask_keeps_zero_and_negative_divisors(guard): + base, (pid, lane, grid), _, size, row = _grouped(masked=False) + flag = z3.Bool("flag") + original = { + None: base, + "or": z3.And(base, z3.Or(flag, row < 64)), + "implies": z3.And(base, z3.Implies(flag, row < 64)), + }[guard] + rewritten = gd.guarded_division_normal_form(original) + extra = () if guard is None else (flag if guard == "or" else z3.Not(flag),) + for instance, divisor in ((4, 0), (8, -2)): + result, solver = _check( + rewritten, grid == 16, pid == instance, lane == 0, *extra + ) + assert result == z3.sat + assert solver.model().eval(size).as_long() == divisor + assert z3.is_true(solver.model().eval(original, model_completion=True)) + + +@pytest.mark.parametrize( + "failure", ["unknown", "sat", "exception", "budget", "disabled"] +) +def test_failed_certificate_keeps_the_original_formula(monkeypatch, failure): + original, *_ = _grouped() + check = z3.Solver.check + + def refuse_uniqueness(self, *args, **kwargs): + # Allow discovery of a candidate value, then refuse its uniqueness. + if any(z3.is_not(a) and z3.is_eq(a.arg(0)) for a in self.assertions()): + if failure == "exception": + raise z3.Z3Exception("injected certificate failure") + return z3.unknown if failure == "unknown" else z3.sat + return check(self, *args, **kwargs) + + if failure == "budget": + monkeypatch.setattr(gd, "_CERTIFY_TIMEOUT_MS", 0) + elif failure == "disabled": + monkeypatch.setattr(gd, "_ENABLE_GUARDED_DIVISION", False) + else: + monkeypatch.setattr(z3.Solver, "check", refuse_uniqueness) + assert z3.eq(gd.guarded_division_normal_form(original), original) + + +def test_quantified_input_is_unchanged(): + original, (pid, _, _), *_ = _grouped() + quantified = z3.Exists(pid, original) + assert z3.eq(gd.guarded_division_normal_form(quantified), quantified) + + +def test_applicability_cache_skips_known_negative_dags(monkeypatch): + cache = gd.GuardedDivisionApplicabilityCache() + x = z3.Int("cache_x") + original = x / 4 >= 0 # constant divisor: nothing to certify + + def unexpected_scan(*args, **kwargs): + raise AssertionError("negative applicability must skip normalization") + + monkeypatch.setattr(gd, "_guarded_division_normal_form", unexpected_scan) + for _ in range(2): + assert z3.eq( + gd.guarded_division_normal_form(original, applicability_cache=cache), + original, + ) + # A positive answer still runs the query-local certificate every time. + monkeypatch.undo() + masked, *_ = _grouped() + base, *_ = _grouped(masked=False) + assert not z3.eq( + gd.guarded_division_normal_form(masked, applicability_cache=cache), masked + ) + rewritten = gd.guarded_division_normal_form(base, applicability_cache=cache) + assert _check(z3.Xor(base, rewritten))[0] == z3.unsat diff --git a/tests/unit/race_detector/test_hb_closure.py b/tests/unit/race_detector/test_hb_closure.py new file mode 100644 index 000000000..13ec7b3be --- /dev/null +++ b/tests/unit/race_detector/test_hb_closure.py @@ -0,0 +1,166 @@ +"""Happens-before edges and their transitive closure keep every conditional +edge, cycle obligation and scope check.""" + +from __future__ import annotations + +import random +from dataclasses import replace + +import pytest +import z3 + +from tilelens.clients.race_detector import hb_common +from tilelens.clients.race_detector.hb_common import UnsupportedSymbolicRaceQuery + +from .solver_records import every_fence, fences_at, load, solve, store + + +def _dense_closure(edges): + """The plain layered Floyd-Warshall recurrence, as the oracle.""" + reach = [list(row) for row in edges] + for k in range(len(reach)): + reach = [ + [ + z3.Or(reach[i][j], z3.And(reach[i][k], reach[k][j])) + for j in range(len(reach)) + ] + for i in range(len(reach)) + ] + return reach + + +def _closure(edges): + return hb_common.build_transitive_hb( + list(range(len(edges))), lambda i, j: edges[i][j] + ) + + +def _assert_equivalent(actual, expected): + differences = [ + a != b + for actual_row, expected_row in zip(actual, expected) + for a, b in zip(actual_row, expected_row) + ] + assert len(actual) == len(expected) + if differences: + solver = z3.Solver(ctx=differences[0].ctx) + solver.add(z3.Or(*differences)) + assert solver.check() == z3.unsat + + +def test_empty_graph_and_constant_self_edges(): + def unreachable(*args): + raise AssertionError("an empty graph has no edges") + + assert hb_common.build_transitive_hb([], unreachable) == [] + for self_edge in (False, True): + assert z3.is_true(_closure([[z3.BoolVal(self_edge)]])[0][0]) == self_edge + + +def test_acyclicity_rejects_a_forced_cycle_and_keeps_a_conditional_cut(): + p, q = z3.Bools("acyclic_p acyclic_q") + f = z3.BoolVal(False) + result = _closure([[f, p], [q, f]]) + acyclic = z3.And(*(z3.Not(result[i][i]) for i in range(2))) + _assert_equivalent([[acyclic]], [[z3.Not(z3.And(p, q))]]) + + +def test_arithmetic_array_and_custom_context_edges_keep_full_conditions(): + ctx = z3.Context() + index, limit = z3.Ints("index limit", ctx=ctx) + snapshot = z3.Array("snapshot", z3.IntSort(ctx), z3.IntSort(ctx)) + f = z3.BoolVal(False, ctx=ctx) + edges = [ + [f, z3.And(index >= 0, index < limit), f], + [f, f, z3.Select(snapshot, index) == 7], + [index == limit, f, z3.BoolVal(True, ctx=ctx)], + ] + result = _closure(edges) + assert all(entry.ctx == ctx for row in result for entry in row) + _assert_equivalent(result, _dense_closure(edges)) + + +@pytest.mark.parametrize("seed,size", [(0, 2), (1, 3), (2, 4), (3, 5), (4, 6)]) +def test_small_symbolic_graphs_match_the_layered_recurrence(seed, size): + choose = random.Random(seed).choice + p, q, r = z3.Bools(f"random_p_{seed} random_q_{seed} random_r_{seed}") + choices = [ + z3.BoolVal(False), + z3.BoolVal(True), + p, + q, + r, + z3.Not(p), + z3.And(p, q), + z3.Or(q, r), + ] + edges = [[choose(choices) for _ in range(size)] for _ in range(size)] + _assert_equivalent(_closure(edges), _dense_closure(edges)) + + +def _edge_solver(*, fence_between=None, dependency=False): + active_load, active_store = z3.Bools("edge_active_load edge_active_store") + first = load(z3.IntVal(100), event_id=0, program_seq=0, mask=active_load) + second = store(z3.IntVal(100), event_id=1, program_seq=2, mask=active_store) + if dependency: + second.dep_loads = (first.event_id,) + return solve([first, second], fence_between=fence_between) + + +@pytest.mark.parametrize( + "fence_between,dependency,ordered", + [ + (every_fence, False, True), + (None, False, False), + (fences_at(1), False, True), + (None, True, True), + (fences_at(0, 2), False, False), + ], +) +def test_program_order_is_an_edge_only_across_a_fence_or_a_dependency( + fence_between, dependency, ordered +): + core = _edge_solver(fence_between=fence_between, dependency=dependency) + assert not core.reads_through + differences = [] + for first in core.events: + for second in core.events: + expected = ( + z3.And(first.active, second.active) + if ordered + and first.copy == second.copy + and first.program_seq < second.program_seq + else z3.BoolVal(False) + ) + differences.append(core._edge(first, second) != expected) + _assert_equivalent([differences], [[z3.BoolVal(False)] * len(differences)]) + + +def test_reads_through_keeps_the_cross_copy_cta_scope_condition(): + core = _edge_solver() + first = replace(core.events[0], sem="release", scope="cta") + second = replace(core.events[-1], sem="acquire", scope="gpu") + rt = z3.Bool("edge_reads_through") + core.reads_through[(first.idx, second.idx)] = rt + expected = z3.And(rt, *(a == b for a, b in zip(first.pid, second.pid))) + _assert_equivalent([[core._edge(first, second)]], [[expected]]) + + +@pytest.mark.parametrize("invalid_endpoint", ["writer", "reader"]) +def test_reads_through_rejects_an_unknown_scope(invalid_endpoint): + core = _edge_solver() + bad = "unsupported-scope" + first = replace( + core.events[0], + sem="release", + scope=bad if invalid_endpoint == "writer" else "gpu", + ) + second = replace( + core.events[-1], + sem="acquire", + scope=bad if invalid_endpoint == "reader" else "gpu", + ) + # Presence matters even when the stored reads-through formula is False. + core.reads_through[(first.idx, second.idx)] = z3.BoolVal(False) + with pytest.raises(UnsupportedSymbolicRaceQuery, match="unsupported memory scope"): + core._edge(first, second) diff --git a/tests/unit/race_detector/test_rmw_solver.py b/tests/unit/race_detector/test_rmw_solver.py new file mode 100644 index 000000000..8533381d8 --- /dev/null +++ b/tests/unit/race_detector/test_rmw_solver.py @@ -0,0 +1,449 @@ +"""Value-modeled RMW returns: reads-through release sequences, the counting +axiom and its guards, and the observation-in-address gate. Most proofs have +a mutation twin that must flip to a report.""" + +from __future__ import annotations + +import pytest +import torch +import z3 +from z3 import Int, IntVal + +from tilelens.clients.race_detector.hb_common import ( + CountingScopeUnsupported, + UnsupportedSymbolicRaceQuery, +) +from tilelens.clients.race_detector.two_copy_symbolic_hb_solver import ( + _rmw_written_value, +) +from tilelens.clients.symbolic_engine import SymbolicExpr +from tilelens.core.data import Load, Store + +from .solver_records import ( + cas, + counter, + every_fence, + load, + report_pairs, + rmw, + solve, + store, +) + +PID0 = SymbolicExpr.PID0 +PARTIAL = 1 << 20 +DATA = 1 << 21 +BUF = 1 << 22 + + +def test_rmw_written_value_table(): + old, v = Int("o"), Int("v") + for op in ("add", "max", "min", "xchg"): + assert _rmw_written_value(op, old, v) is not None + for op in ("and", "or", "xor", "umax", "umin", "fadd", None): + assert _rmw_written_value(op, old, v) is None + assert _rmw_written_value("or", old, IntVal(0)) is old + assert _rmw_written_value("add", None, v) is None + + +@pytest.mark.parametrize("op,operand", [("max", 7), ("min", -3)]) +def test_written_value_reaches_a_relaxed_reader(op, operand): + """pid 0 stores data, then a relaxed max/min writes ``operand`` to a + zero flag; another pid polls the flag and reads data on seeing it. The + relaxed write publishes nothing, so the data race is reported only if + the write part carries the right value.""" + flag = counter(0) + obs = Int(f"written_obs_{op}") + producer, consumer = PID0 == 0, PID0 != 0 + records = [ + store(IntVal(DATA), event_id=0, active=producer), + rmw( + IntVal(flag.data_ptr()), + Int(f"written_old_{op}"), + op=op, + operand=IntVal(operand), + event_id=1, + program_seq=1, + sem="relaxed", + tensor=flag, + active=producer, + ), + _add( + flag, + obs, + event_id=2, + program_seq=2, + operand=IntVal(0), + sem="acquire", + active=consumer, + ), + load( + IntVal(DATA), + event_id=3, + program_seq=3, + active=consumer, + mask=obs == operand, + ), + ] + pairs = report_pairs(solve(records, fence_between=every_fence).find_races()) + assert (0, 3) in pairs + + +def _add(tensor, old, **kwargs): + kwargs.setdefault("sem", "relaxed") + return rmw( + IntVal(tensor.data_ptr()), + old, + op="add", + operand=kwargs.pop("operand", IntVal(1)), + tensor=tensor, + **kwargs, + ) + + +# ──────────────────── last block done ──────────────────── + + +def _last_block(sem, *, tensor=True): + """partial[pid] = ...; old = atomic_add(counter, 1, sem); if old == 3: + read partial[0:4], on a grid of 4.""" + c = counter(0) + old, lane = Int("lbd_old"), Int("lbd_lane") + records = [ + store(IntVal(PARTIAL) + PID0 * 4, event_id=0), + _add(c, old, event_id=1, program_seq=1, sem=sem), + load(IntVal(PARTIAL) + lane * 4, event_id=2, program_seq=2, mask=old == 3), + ] + if not tensor: + records[1].tensor = None + return solve( + records, + grid=(4, 1, 1), + arange_dict={(0, 4): (lane, None)}, + fence_between=every_fence, + ) + + +def test_last_block_done_acq_rel_is_proved(): + solver = _last_block("acq_rel") + assert solver._counting + assert solver.find_races() == [] + + +def test_last_block_done_relaxed_flips_to_race(): + reports = _last_block("relaxed").find_races() + kinds = {(r.first_record.op_type, r.second_record.op_type) for r in reports} + assert (Store, Load) in kinds or (Load, Store) in kinds + + +def test_unknown_initial_value_omits_counting_and_over_reports(): + solver = _last_block("acq_rel", tensor=False) + assert not solver._counting + assert solver.find_races() + + +# ──────────────────── counting distinctness ──────────────────── + + +def test_single_winner_store_is_proved(): + c, old = counter(0), Int("winner_old") + records = [ + _add(c, old, event_id=0), + store(IntVal(DATA), event_id=1, program_seq=1, mask=old == 0), + ] + solver = solve(records, grid=(4, 1, 1)) + assert solver._counting and solver.find_races() == [] + records[0].tensor = None + solver = solve(records, grid=(4, 1, 1)) + assert not solver._counting and solver.find_races() + + +@pytest.mark.parametrize("stride,races", [(4, False), (2, True)]) +def test_work_queue_slots_are_disjoint_by_rank(stride, races): + """idx = atomic_add(head, 1); store buf[idx]: the observation feeds the + address, allowed exactly because the counting axiom fired.""" + head, old = counter(0), Int(f"wq_old_{stride}") + records = [ + _add(head, old, event_id=0), + store(IntVal(BUF) + old * stride, event_id=1, program_seq=1), + ] + solver = solve(records, grid=(4, 1, 1)) + assert solver._counting + assert bool(solver.find_races()) is races + + +def test_uncounted_observation_in_an_address_is_unsupported(): + head, old = counter(0), Int("xchg_old") + records = [ + rmw( + IntVal(head.data_ptr()), + old, + op="xchg", + operand=IntVal(7), + event_id=0, + sem="relaxed", + tensor=head, + ), + store(IntVal(BUF) + old * 4, event_id=1, program_seq=1), + ] + with pytest.raises(UnsupportedSymbolicRaceQuery, match="counting axiom"): + solve(records, grid=(4, 1, 1)) + + +def test_counter_that_may_wrap_on_a_symbolic_grid_asks_for_a_smaller_scope(): + """A work-queue counter whose capped maximum overflows int32 on a + symbolic grid raises the retryable CountingScopeUnsupported; at a + concrete grid that overflows, no smaller scope helps.""" + head, old = counter(2**31 - 8), Int("scope_old") + records = [ + _add(head, old, event_id=0), + store(IntVal(BUF) + old * 4, event_id=1, program_seq=1), + ] + with pytest.raises(CountingScopeUnsupported): + solve(records, grid=(Int("scope_g"), 1, 1)) + assert solve(records, grid=(4, 1, 1))._counting + with pytest.raises(UnsupportedSymbolicRaceQuery) as info: + solve(records, grid=(16, 1, 1)) + assert not isinstance(info.value, CountingScopeUnsupported) + + +def test_rf_chain_keeps_a_non_adjacent_rank_race(): + """rank 0 stores X, rank 2 reads X, relaxed: a real race the closed world + (init + the peer copy's write) alone could not justify.""" + c, old = counter(0), Int("chain_old") + records = [ + _add(c, old, event_id=0), + store(IntVal(DATA), event_id=1, program_seq=1, mask=old == 0), + load(IntVal(DATA), event_id=2, program_seq=2, mask=old == 2), + ] + solver = solve(records, grid=(4, 1, 1)) + assert solver._counting and solver.find_races() + + +def test_rank0_winner_duplicate_lanes_still_race(): + """The two copies of the one dynamic RMW in one instance are one + operation: the winner's own colliding lanes must stay reportable.""" + c, old = counter(0), Int("rank0_old") + records = [ + _add(c, old, event_id=0), + store([IntVal(DATA), IntVal(DATA)], event_id=1, program_seq=1, mask=old == 0), + ] + solver = solve(records, grid=(4, 1, 1)) + assert solver._counting and solver.find_races() + + +# ──────────────────── counting guards ──────────────────── + + +def test_counting_guards_omit_the_axiom(): + c = counter(0) + masked = _add(c, Int("masked_old"), event_id=0, active=PID0 == 0) + nonconstant = _add(c, Int("nc_old"), event_id=0, operand=PID0 + 1) + overlapped = [ + _add(c, Int("ovl_old"), event_id=0), + store(IntVal(c.data_ptr()), event_id=1, program_seq=1), + ] + for records in ([masked], [nonconstant], overlapped): + assert not solve(records, grid=(4, 1, 1))._counting + + +def test_possible_wraparound_omits_counting(): + """An INT32_MAX counter wraps on hardware; the unbounded-Int model does + not, so the axiom is omitted and the wrap-gated store races.""" + c, old = counter(2**31 - 1), Int("wrap_old") + records = [ + _add(c, old, event_id=0), + store(IntVal(DATA), event_id=1, program_seq=1), + store(IntVal(DATA), event_id=2, program_seq=2, mask=old == -(2**31)), + ] + solver = solve(records, grid=(4, 1, 1)) + assert not solver._counting + assert {(1, 2), (2, 2)} <= report_pairs(solver.find_races()) + sane = solve([_add(counter(0), Int("sane_old"), event_id=0)], grid=(Int("g"), 1, 1)) + assert sane._counting + + +# ──────────────────── release sequences ──────────────────── + + +def _release_chain(producer_sem, *, modeled_middle=True): + """pid 0: store data; xchg(flag, 10, producer_sem). Other pids: + cas(flag, 10, 15, relaxed) as the middle link; fetch = add(flag, 0, + acquire); if fetch == 15: read data. The sw edge reaches the reader only + through the relaxed middle link.""" + flag = counter(0) + base = IntVal(flag.data_ptr()) + producer, consumer = PID0 == 0, PID0 != 0 + fetch = Int("rc_fetch") + if modeled_middle: + middle = cas( + base, + IntVal(10), + IntVal(15), + Int("rc_mid"), + event_id=2, + program_seq=2, + sem="relaxed", + tensor=flag, + active=consumer, + ) + else: + middle = rmw( + base, + Int("rc_mid"), + op="or", + operand=IntVal(5), + event_id=2, + program_seq=2, + sem="relaxed", + tensor=flag, + active=consumer, + ) + return [ + store(IntVal(DATA), event_id=0, active=producer), + rmw( + base, + Int("rc_x"), + op="xchg", + operand=IntVal(10), + event_id=1, + program_seq=1, + sem=producer_sem, + tensor=flag, + active=producer, + ), + middle, + rmw( + base, + fetch, + op="add", + operand=IntVal(0), + event_id=3, + program_seq=3, + sem="acquire", + tensor=flag, + active=consumer, + ), + load( + IntVal(DATA), event_id=4, program_seq=4, active=consumer, mask=fetch == 15 + ), + ] + + +def test_release_sequence_through_an_rmw_chain_is_proved(): + records = _release_chain("release") + assert solve(records, fence_between=every_fence).find_races() == [] + # Without fences the producer's store is not ordered before its release. + assert solve(records).find_races() + + +@pytest.mark.parametrize("sem,modeled_middle", [("relaxed", True), ("release", False)]) +def test_broken_release_sequence_flips_to_race(sem, modeled_middle): + """A relaxed publisher heads no release sequence; an unmodeled middle + link opens rf_unknown instead of extending the chain.""" + records = _release_chain(sem, modeled_middle=modeled_middle) + assert solve(records, fence_between=every_fence).find_races() + + +def test_torn_width_modeled_writer_opens_the_escape(): + """An 8-byte modeled xchg over a 4-byte modeled reader is rf-incompatible: + it counts as an unmodeled overlapping writer.""" + flag = counter(0) + base = IntVal(flag.data_ptr()) + seen = Int("torn_seen") + records = [ + rmw( + base, + Int("torn_w"), + op="xchg", + operand=IntVal(10), + event_id=0, + sem="relaxed", + elem_size=8, + ), + rmw( + base, + seen, + op="add", + operand=IntVal(0), + event_id=1, + program_seq=1, + sem="acquire", + tensor=flag, + ), + store(IntVal(DATA), event_id=2, program_seq=2, mask=seen == 10), + store(IntVal(DATA), event_id=3, program_seq=3), + ] + solver = solve(records, grid=(4, 1, 1)) + assert any( + e.idx in solver.rf_unknown_source + for e in solver.events + if e.record is records[1] + ) + assert solver.find_races() + + +# ──────────────────── awaits ──────────────────── + + +@pytest.mark.parametrize("initial", [0, 1]) +def test_await_exit_controls_the_later_publication(initial): + """Each instance waits for its own flag to be 1, then sets the peer's + flag. With zero flags only a causal cycle (each publication justifying + the other's exit) could terminate: the launch premises are infeasible.""" + flags = torch.full((2,), initial, dtype=torch.int32) + base = IntVal(flags.data_ptr()) + poll = Int(f"await_poll_{initial}") + records = [ + rmw( + base + 4 * PID0, + poll, + op="add", + operand=IntVal(0), + event_id=0, + sem="relaxed", + tensor=flags, + ), + rmw( + base + 4 * (1 - PID0), + Int(f"await_pub_{initial}"), + op="xchg", + operand=IntVal(1), + event_id=1, + program_seq=1, + sem="relaxed", + tensor=flags, + ), + ] + records[1].premises = (poll == 1,) # the await's exit + records[1].causal_constraints = () # an exit premise is no value dependency + records[1].await_dependencies = (0,) + solver = solve(records) + assert solver._base_solver().check() == z3.sat + assert solver.check_feasibility() is bool(initial) + # Without the control edge the cycle would certify termination. + records[1].await_dependencies = () + assert solve(records).check_feasibility() + + +@pytest.mark.parametrize("pre_exit", [True, False]) +def test_pre_exit_representative_keeps_its_poll_closed_world(pre_exit): + """The value-model-free twin of an identity-RMW poll writes at the polled + location; as a pre-exit representative it opens no rf_unknown escape for + its own poll and is not a same-instance race partner of it.""" + flag = counter(0) + base = IntVal(flag.data_ptr()) + poll = rmw( + base, + Int(f"rep_poll_{pre_exit}"), + op="add", + operand=IntVal(0), + event_id=0, + sem="acquire", + tensor=flag, + ) + rep = rmw(base, event_id=1, sem="acquire", tensor=flag) + rep.pre_exit = pre_exit + solver = solve([poll, rep], grid=(1, 1, 1)) + assert bool(solver.rf_unknown_source) is not pre_exit + assert solver.find_races() == [] diff --git a/tests/unit/race_detector/test_two_copy_solver.py b/tests/unit/race_detector/test_two_copy_solver.py new file mode 100644 index 000000000..259bd3fae --- /dev/null +++ b/tests/unit/race_detector/test_two_copy_solver.py @@ -0,0 +1,549 @@ +"""TwoCopySymbolicHBSolver on hand-built records: race found or proved, race +types, atomics, fences through the caller's hook, intra-instance lanes, the +enumeration fallback, the compiled-only restrictions and the Z3 budget.""" + +from __future__ import annotations + +import threading + +import pytest +import torch +import z3 +from z3 import And, BoolVal, Int, IntVal + +import tilelens.clients.race_detector.two_copy_symbolic_hb_solver as tc +from tilelens.clients.race_detector.data import AccessEventRecord, RaceType +from tilelens.clients.race_detector.hb_common import UnsupportedSymbolicRaceQuery +from tilelens.clients.race_detector.two_copy_symbolic_hb_solver import ( + TwoCopySymbolicHBSolver, +) +from tilelens.clients.symbolic_engine import SymbolicExpr +from tilelens.core.data import Store + +from .solver_records import ( + cas, + every_fence, + fences_at, + load, + report_pairs, + rmw, + solve, + store, +) + +PID0 = SymbolicExpr.PID0 +DATA = 1 << 21 + + +# ──────────────────────── two copies ──────────────────────── + + +def test_pid_alpha_renaming_reports_cross_instance_waw(): + """elem_size 4 at stride 1: adjacent pids overlap by 3 bytes.""" + reports = solve([store(IntVal(DATA) + PID0, event_id=0)]).find_races() + assert len(reports) == 1 + assert reports[0].race_type is RaceType.WAW + assert reports[0].witness_grid_a != reports[0].witness_grid_b + assert reports[0].witness_addr in {DATA + 1, DATA + 2, DATA + 3} + + +def test_arange_lanes_are_renamed_per_copy(): + lane = Int("lane") + arange = {(0, 8): (lane, And(lane >= 0, lane < 8))} + aliasing = store(IntVal(DATA) + 28 * PID0 + 4 * lane, event_id=0) + disjoint = store(IntVal(DATA) + 32 * PID0 + 4 * lane, event_id=0) + assert solve([aliasing], grid=(4, 1, 1), arange_dict=arange).find_races() + assert solve([disjoint], grid=(4, 1, 1), arange_dict=arange).find_races() == [] + + +def test_masked_off_access_never_races(): + rec = store(IntVal(DATA), event_id=0, mask=BoolVal(False)) + assert solve([rec]).find_races() == [] + + +# ──────────────────────── fences via the caller's hook ──────────────────────── + + +def _two_operations(kind): + makers = {"RAW": (store, load), "WAR": (load, store), "WAW": (store, store)} + records = [ + make(IntVal(100), event_id=i, program_seq=i) + for i, make in enumerate(makers[kind]) + ] + for i, record in enumerate(records): + record.source_location = ("kernel.py", 10 + i, "kernel") + return records + + +@pytest.mark.parametrize("kind", ["RAW", "WAR", "WAW"]) +@pytest.mark.parametrize("fences", [None, (0.5,), (1.5,)]) +def test_unfenced_operations_of_one_instance_race(kind, fences): + hook = None if fences is None else fences_at(*fences) + solver = solve(_two_operations(kind), grid=(1, 1, 1), fence_between=hook) + reports = solver.find_races() + if fences == (0.5,): + assert reports == [] + return + assert len(reports) == 1 + report = reports[0] + assert report.race_type.name == kind + assert report.witness_addr == 100 + assert report.witness_grid_a == report.witness_grid_b + assert report.reason.startswith(solver._INTRA_INSTANCE_REASON) + assert "Missing source fence:" in report.reason + assert "kernel.py:10" in report.reason and "kernel.py:11" in report.reason + + +def test_fence_hook_is_asked_in_program_order_with_the_records(): + records = _two_operations("WAR") + records[0].event_id, records[1].event_id = 1, 0 + calls = [] + + def hook(first, second): + calls.append((first, second)) + return False + + report = solve(records, grid=(1, 1, 1), fence_between=hook).find_races()[0] + assert calls + assert all(first is records[0] and second is records[1] for first, second in calls) + # The report keeps its event-id order; the explanation uses source order. + assert (report.first.event_id, report.second.event_id) == (0, 1) + assert report.race_type is RaceType.RAW + assert "read at kernel.py:10 and the write at kernel.py:11" in report.reason + + +def test_fence_between_every_operation_orders_one_instance(): + records = _two_operations("RAW") + assert solve(records, grid=(1, 1, 1), fence_between=every_fence).find_races() == [] + + +def test_fence_hook_answers_each_pair_on_its_own(): + """A fence at 1.5 orders (0, 2) and (1, 2) but not (0, 1).""" + records = [store(IntVal(100), event_id=i, program_seq=i) for i in range(3)] + solver = solve(records, grid=(1, 1, 1), fence_between=fences_at(1.5)) + assert report_pairs(solver.find_races()) == {(0, 1)} + + +@pytest.mark.parametrize("case", ["unknown_seq", "equal_seq", "duplicate", "cross"]) +def test_missing_fence_diagnostic_needs_two_ordered_operations(case): + records, grid = _two_operations("RAW"), (1, 1, 1) + if case == "unknown_seq": + records[0].program_seq = -1 + elif case == "equal_seq": + records[1].program_seq = 0 + elif case == "duplicate": + records = records[:1] + records[0].addr_expr = [IntVal(100), IntVal(100)] + else: + grid = (2, 1, 1) + records[0].active = PID0 == 0 + records[1].active = PID0 == 1 + reports = solve(records, grid=grid).find_races() + assert reports + assert all("Missing source fence:" not in r.reason for r in reports) + + +def test_dependency_orders_only_the_same_position(): + """A store consuming a load's value is ordered after the load at the same + lane, but another lane of the store can still race the load.""" + lane = Int("dep_lane") + records = _two_operations("WAR") + records[0].addr_expr = IntVal(100) + 4 * lane + records[1].addr_expr = IntVal(104) + 4 * lane + records[1].dep_loads = (records[0].event_id,) + arange = {(0, 2): (lane, And(lane >= 0, lane < 2))} + report = solve(records, grid=(1, 1, 1), arange_dict=arange).find_races()[0] + assert report.witness_addr == 104 + assert "Missing source fence:" in report.reason + records[1].addr_expr = IntVal(100) + 4 * lane + assert solve(records, grid=(1, 1, 1), arange_dict=arange).find_races() == [] + + +# ──────────────────────── atomics ──────────────────────── + + +def test_competing_same_location_atomics_do_not_race(): + pair = [ + cas(IntVal(500), IntVal(0), IntVal(1), Int(f"c{i}"), event_id=i) + for i in range(2) + ] + assert solve(pair).find_races() == [] + assert solve([rmw(IntVal(900), event_id=0)]).find_races() == [] + + +@pytest.mark.parametrize( + "first,second,races", + [((0, 4), (0, 8), True), ((0, 4), (0, 4), False), ((0, 4), (2, 4), True)], +) +def test_only_same_address_same_width_atomics_are_mutually_atomic(first, second, races): + pair = [ + rmw(IntVal(DATA + offset), event_id=i, program_seq=i, elem_size=width) + for i, (offset, width) in enumerate((first, second)) + ] + assert bool(solve(pair).find_races()) is races + + +@pytest.mark.parametrize( + "scopes,races", [(("gpu", "gpu"), False), (("cta", "gpu"), True)] +) +def test_cta_scoped_atomics_race_across_ctas(scopes, races): + pair = [ + rmw(IntVal(DATA), event_id=i, program_seq=i, scope=scope) + for i, scope in enumerate(scopes) + ] + assert bool(solve(pair).find_races()) is races + + +def test_cas_trylock_single_winner_suppresses_guarded_waw(): + """Two CAS(0 -> 1) on one flag cannot both read 0: atomic coherence + leaves one winner, so the guarded stores never overlap.""" + flag = torch.zeros(1, dtype=torch.int32) + old = Int("trylock_old") + records = [ + cas( + IntVal(flag.data_ptr()), IntVal(0), IntVal(1), old, event_id=0, tensor=flag + ), + store(IntVal(DATA), event_id=1, program_seq=1, mask=old == 0), + ] + solver = solve(records) + assert next(e.idx for e in solver.events if e.copy == "a") in solver.rf_init_source + assert solver.find_races() == [] + + +@pytest.mark.parametrize("flag_kind", ["float", "large"]) +def test_unidentifiable_initial_flag_falls_back_to_rf_unknown(flag_kind): + """A float flag (int(0.7) == 0 would fabricate a lock winner) or one + larger than the initial-source cap has no closed-world initial value: + rf_unknown opens, and the guarded WAW is reported.""" + if flag_kind == "float": + flag = torch.full((1,), 0.7, dtype=torch.float32) + else: + size = TwoCopySymbolicHBSolver._MAX_INITIAL_ATOMIC_ELEMENTS + 1 + flag = torch.zeros(size, dtype=torch.int32) + old = Int(f"{flag_kind}_flag_old") + records = [ + cas( + IntVal(flag.data_ptr()), IntVal(0), IntVal(1), old, event_id=0, tensor=flag + ), + store(IntVal(DATA), event_id=1, program_seq=1, mask=old != 1), + ] + solver = solve(records) + reader = next(e for e in solver.events if e.copy == "a" and e.atomic_kind == "cas") + assert reader.idx in solver.rf_unknown_source + assert reader.idx not in solver.rf_init_source + assert solver.find_races() + + +@pytest.mark.parametrize("offset,races", [(0, False), (1, True)]) +def test_release_acquire_cas_orders_only_through_the_exact_location(offset, races): + """pid 0 stores data, then CAS-releases flag 0 -> 1; the other pid + CAS-acquires the flag and reads data once it observes 1. An acquire at a + byte-overlapping but different address is not the same location: no + synchronizes-with edge, so the data race stays.""" + flag = torch.zeros(1, dtype=torch.int32) + base = int(flag.data_ptr()) + seen = Int(f"acquire_old_{offset}") + producer, consumer = PID0 == 0, PID0 != 0 + records = [ + store(IntVal(DATA), event_id=0, active=producer), + cas( + IntVal(base), + IntVal(0), + IntVal(1), + Int(f"release_old_{offset}"), + event_id=1, + program_seq=1, + sem="release", + tensor=flag, + active=producer, + ), + cas( + IntVal(base + offset), + IntVal(1), + IntVal(1), + seen, + event_id=2, + program_seq=2, + sem="acquire", + tensor=flag, + active=consumer, + ), + load(IntVal(DATA), event_id=3, program_seq=3, active=consumer, mask=seen == 1), + ] + pairs = report_pairs(solve(records, fence_between=every_fence).find_races()) + # The misaligned CAS pair (1, 2) is itself torn. + assert pairs == ({(0, 3), (1, 2)} if races else set()) + # Without a fence, program order carries no happens-before edge. + assert (0, 3) in report_pairs(solve(records).find_races()) + + +def test_same_copy_later_writer_is_no_read_from_source(): + earlier = cas(IntVal(5100), IntVal(0), IntVal(1), Int("earlier"), event_id=0) + later = cas( + IntVal(5100), IntVal(0), IntVal(1), Int("later"), event_id=1, program_seq=1 + ) + solver = solve([earlier, later]) + a = {e.record.event_id: e.idx for e in solver.events if e.copy == "a"} + assert (a[1], a[0]) not in solver.rf_source + assert (a[0], a[1]) in solver.rf_source + + +# ──────────────────────── one instance ──────────────────────── + + +def _lane_store(addr_of, *, mask=None): + lane = Int("intra_lane") + arange = {(0, 4): (lane, And(lane >= 0, lane < 4))} + m = None if mask is None else mask(lane) + return store(addr_of(lane), event_id=0, mask=m), arange + + +@pytest.mark.parametrize( + "addr_of,mask,races", + [ + (lambda lane: IntVal(DATA) + 4 * (lane % 2), None, True), + (lambda lane: IntVal(DATA) + 4 * lane, None, False), + (lambda lane: IntVal(DATA) + 0 * lane, lambda lane: lane == 3, False), + (lambda lane: IntVal(DATA) + 0 * lane, lambda lane: lane < 2, True), + ], +) +def test_duplicate_lanes_of_one_store_race_in_one_instance(addr_of, mask, races): + rec, arange = _lane_store(addr_of, mask=mask) + reports = solve([rec], grid=(1, 1, 1), arange_dict=arange).find_races() + assert bool(reports) is races + if races: + assert reports[0].race_type is RaceType.WAW + assert reports[0].witness_grid_a == reports[0].witness_grid_b + + +def test_lanes_of_one_atomic_and_a_scalar_store_do_not_self_race(): + lanes = rmw([IntVal(DATA), IntVal(DATA)], event_id=0) + assert solve([lanes], grid=(1, 1, 1)).find_races() == [] + scalar = store(IntVal(DATA) + 4 * PID0, event_id=0) + assert solve([scalar], grid=(1, 1, 1)).find_races() == [] + + +# ──────────────────────── feasibility and restrictions ──────────────────────── + + +def test_unsatisfiable_premises_fail_feasibility(): + rec = store(IntVal(DATA), event_id=0) + assert solve([rec]).check_feasibility() + rec.premises = (PID0 < 0,) + solver = solve([rec]) + assert solver.find_races() == [] + assert not solver.check_feasibility() + + +def test_only_pairs_queries_just_the_listed_record_pairs(): + records = [store(IntVal(DATA + 100 * i), event_id=i) for i in range(2)] + assert report_pairs(solve(records).find_races()) == {(0, 0), (1, 1)} + only = frozenset({(1, 1)}) + assert report_pairs(solve(records, only_pairs=only).find_races()) == {(1, 1)} + + +def test_extra_assumptions_constrain_a_symbolic_grid(): + g0 = Int("grid_0") + rec = store(IntVal(DATA), event_id=0) + assert solve([rec], grid=(g0, 1, 1)).find_races() + assert ( + solve([rec], grid=(g0, 1, 1), extra_assumptions=(g0 == 1,)).find_races() == [] + ) + + +# ──────────────────────── enumeration fallback ──────────────────────── + + +def _force_unknown(monkeypatch): + def undecided(solver, a, b): + raise UnsupportedSymbolicRaceQuery(f"forced unknown for {a.name} vs {b.name}") + + monkeypatch.setattr( + TwoCopySymbolicHBSolver, "_race_query_is_sat", staticmethod(undecided) + ) + + +def test_enumeration_decides_an_undecided_query_at_the_extent(monkeypatch): + _force_unknown(monkeypatch) + disjoint = [store(IntVal(DATA) + 4 * PID0, event_id=0)] + solver = solve(disjoint, grid=(4, 1, 1), enum_fallback_grid=(4, 1, 1)) + assert solver.find_races() == [] + assert solver.enum_used + colliding = [store(IntVal(DATA), event_id=0)] + solver = solve(colliding, grid=(4, 1, 1), enum_fallback_grid=(4, 1, 1)) + reports = solver.find_races() + assert solver.enum_used and reports + for pid in (reports[0].witness_grid_a, reports[0].witness_grid_b): + assert 0 <= pid[0] < 4 and pid[1:] == (0, 0) + + +@pytest.mark.parametrize("fallback", [None, (100, 1, 1)]) +def test_enumeration_refusal_reraises_the_unknown(monkeypatch, fallback): + """No fallback grid, or more cases than ENUM_MAX_CASES.""" + _force_unknown(monkeypatch) + solver = solve( + [store(IntVal(DATA) + 4 * PID0, event_id=0)], + grid=(100, 1, 1), + enum_fallback_grid=fallback, + ) + with pytest.raises(UnsupportedSymbolicRaceQuery, match="forced unknown"): + solver.find_races() + + +def test_undecided_enumeration_case_reraises_the_unknown(monkeypatch): + """An undecided case must not count as UNSAT: that would be a false + launch-scope proof. A budget below the per-case limit caps each case.""" + _force_unknown(monkeypatch) + monkeypatch.setattr(_RecordingSolver, "made", []) + monkeypatch.setattr(tc, "Solver", _RecordingSolver) + solver = solve( + [store(IntVal(DATA) + 4 * PID0, event_id=0)], + grid=(4, 1, 1), + enum_fallback_grid=(4, 1, 1), + timeout_ms=1234, + ) + monkeypatch.setattr(z3.Solver, "check", lambda self, *a: z3.unknown) + with pytest.raises(UnsupportedSymbolicRaceQuery, match="forced unknown"): + solver.find_races() + assert solver.enum_used + assert {s.timeout for s in _RecordingSolver.made} == {1234} + + +def test_decided_query_never_enumerates(): + rec = store(IntVal(DATA) + 4 * PID0, event_id=0) + solver = solve([rec], grid=(4, 1, 1), enum_fallback_grid=(4, 1, 1)) + assert solver.find_races() == [] and not solver.enum_used + + +# ──────────────────────── Z3 budget and unknown ──────────────────────── + + +class _RecordingSolver(z3.Solver): + made: list = [] + + def __init__(self, *args, **kwargs): + super().__init__(*args, **kwargs) + self.timeout = None + type(self).made.append(self) + + def set(self, *args, **kwargs): + self.timeout = kwargs.get("timeout", self.timeout) + super().set(*args, **kwargs) + + +@pytest.mark.parametrize( + "timeout_ms,launch_ceiling,expected", + [(1234, False, {1234}), (1234, True, {1234}), (60_000, True, {60_000, 10_000})], +) +def test_every_solver_gets_its_own_timeout( + monkeypatch, timeout_ms, launch_ceiling, expected +): + """Each Solver carries the budget; the retry cap only shortens it.""" + monkeypatch.setattr(_RecordingSolver, "made", []) + monkeypatch.setattr(tc, "Solver", _RecordingSolver) + flag = torch.zeros(1, dtype=torch.int32) + records = [ + cas( + IntVal(flag.data_ptr()), + IntVal(0), + IntVal(1), + Int("t"), + event_id=0, + tensor=flag, + ), + store(IntVal(DATA), event_id=1, program_seq=1), + ] + before = z3.get_param("timeout") + solver = solve( + records, + timeout_ms=timeout_ms, + launch_ceiling=launch_ceiling, + enum_fallback_grid=(2, 1, 1), + ) + assert solver.find_races() and solver.check_feasibility() + assert z3.get_param("timeout") == before + assert _RecordingSolver.made + assert {s.timeout for s in _RecordingSolver.made} == expected + assert TwoCopySymbolicHBSolver.TIMEOUT_MS == 180_000 + assert solve(records).timeout_ms == 180_000 + with pytest.raises(ValueError, match="positive"): + solve(records, timeout_ms=0) + + +def test_tiny_timeout_makes_a_hard_query_unsupported(): + """x^3 + y^3 == z^3 over positive pids (no solution, which Z3 cannot + prove in time) gates a colliding store: unknown, never a proof.""" + p = (SymbolicExpr.PID0, SymbolicExpr.PID1, SymbolicExpr.PID2) + fermat = And( + *(v > 0 for v in p), sum(v * v * v for v in p[:2]) == p[2] * p[2] * p[2] + ) + grid = tuple(Int(f"fermat_grid_{i}") for i in range(3)) + before = z3.get_param("timeout") + solver = solve( + [store(IntVal(DATA), event_id=0, mask=fermat)], grid=grid, timeout_ms=50 + ) + outcome = [] + + def run(): + try: + solver.find_races() + except UnsupportedSymbolicRaceQuery as exc: + outcome.append(exc) + + # Fail instead of hanging the suite if the budget stops being applied. + worker = threading.Thread(target=run, daemon=True) + worker.start() + worker.join(timeout=60) + assert not worker.is_alive(), "the 50 ms budget was not applied" + assert outcome and "could not decide" in str(outcome[0]) + assert z3.get_param("timeout") == before + + +class _UnknownSolver: + """Stands in for z3.Solver: every query is undecided.""" + + def __init__(self, *args, **kwargs): + pass + + def add(self, *args, **kwargs): + pass + + def set(self, *args, **kwargs): + pass + + def push(self): + pass + + def pop(self): + pass + + def check(self): + return z3.unknown + + def reason_unknown(self): + return "stubbed unknown" + + +def test_unknown_overlap_check_opens_rf_unknown_escape(monkeypatch): + """Keeping the closed world on an undecided overlap would pin the + reader's old value and hide every conflict gated on it.""" + flag = torch.zeros(1, dtype=torch.int32) + old = Int("escape_old") + records = [ + cas( + IntVal(flag.data_ptr()), IntVal(0), IntVal(1), old, event_id=0, tensor=flag + ), + store(IntVal(DATA), event_id=1, program_seq=1), + ] + monkeypatch.setattr(tc, "Solver", _UnknownSolver) + solver = solve(records) + reader = next(e for e in solver.events if e.copy == "a" and e.atomic_kind == "cas") + assert reader.idx in solver.rf_unknown_source + with pytest.raises(UnsupportedSymbolicRaceQuery, match="stubbed unknown"): + solver.check_feasibility() + + +def test_records_need_byte_addresses(): + rec = AccessEventRecord(op_type=Store, access_mode="write") + with pytest.raises(UnsupportedSymbolicRaceQuery, match="addr_expr"): + solve([rec]) diff --git a/tilelens/clients/race_detector/conflict_simplification.py b/tilelens/clients/race_detector/conflict_simplification.py new file mode 100644 index 000000000..155264cab --- /dev/null +++ b/tilelens/clients/race_detector/conflict_simplification.py @@ -0,0 +1,434 @@ +"""A conservative linear precheck for conflict addresses. + +A full race implies its address/activity/template conditions. Replacing +nonlinear integer subterms and array Selects by unconstrained, consistently +shared variables only enlarges that necessary condition. Snapshot guards +and original domains remain, so an inactive array fallback need not pull +an otherwise linear address query into array solving. For ``q*r+d`` we may +also retain injectivity when the ORIGINAL condition explicitly contains +``r > 0`` and ``0 <= d < r``. Then equality of two flattened indices with +the same shared radix entails equality of their quotients and digits. +Only UNSAT of this weaker formula can discard a pair; SAT and unknown are +inconclusive and leave the complete HB/rf/feasibility query unchanged. +""" + +from __future__ import annotations + +from collections import defaultdict +from typing import Any + +import z3 + +from .snapshot_lemmas import snapshot_table_lemmas + +# Private switches that turn one optional precheck path off, so tests can +# compare it with the full query; analysis always uses both. +_ENABLE_SNAPSHOT_PRECHECK = True +_ENABLE_RADIX_PRECHECK = True +_PRECHECK_TIMEOUT_MS = 500 + + +def conflict_precheck_features(expr) -> tuple[bool, bool]: + """Return (symbolic product, Select), cached per lowered event.""" + if not isinstance(expr, z3.ExprRef): + return False, False + product, snapshot = False, False + pending, seen = [expr], set() + while pending: + node = pending.pop() + if node in seen: + continue + seen.add(node) + snapshot |= _ENABLE_SNAPSHOT_PRECHECK and z3.is_select(node) + product |= ( + _ENABLE_RADIX_PRECHECK + and z3.is_mul(node) + and sum(not z3.is_int_value(c) for c in node.children()) > 1 + ) + if product and snapshot: + break + pending.extend(node.children()) + return product, snapshot + + +def needs_conflict_precheck(expr) -> bool: + return any(conflict_precheck_features(expr)) + + +def _conjuncts(expr): + if z3.is_and(expr): + for child in expr.children(): + yield from _conjuncts(child) + else: + yield expr + + +def _numeral(expr): + return expr.as_long() if z3.is_int_value(expr) else None + + +def _explicit_digit_bounds(conditions): + """Read only conjunctions of asserted bounds, never disjunction arms.""" + nonnegative, positive, upper = set(), set(), set() + for condition in conditions: + for atom in _conjuncts(condition): + if not z3.is_app(atom) or atom.num_args() != 2: + continue + kind = atom.decl().kind() + left, right = atom.children() + if kind in (z3.Z3_OP_LE, z3.Z3_OP_LT): + left, right = right, left + kind = z3.Z3_OP_GE if kind == z3.Z3_OP_LE else z3.Z3_OP_GT + if kind not in (z3.Z3_OP_GE, z3.Z3_OP_GT): + continue + constant = _numeral(right) + if constant is not None: + floor = constant + (kind == z3.Z3_OP_GT) + if floor >= 0: + nonnegative.add(left) + if floor >= 1: + positive.add(left) + # After normalization, left > right means digit < radix. + if kind == z3.Z3_OP_GT: + upper.add((right, left)) + return { + (digit, radix) + for digit, radix in upper + if digit in nonnegative and (radix in positive or (_numeral(radix) or 0) > 0) + } + + +def _mixed_radix(expr, bounds): + if not z3.is_add(expr) or expr.num_args() != 2: + return None + for product, digit in (expr.children(), tuple(reversed(expr.children()))): + if not z3.is_mul(product) or product.num_args() != 2: + continue + for quotient, radix in ( + product.children(), + tuple(reversed(product.children())), + ): + if (digit, radix) in bounds: + return quotient, radix, digit + return None + + +_LINEAR_OPS = { + z3.Z3_OP_TRUE, + z3.Z3_OP_FALSE, + z3.Z3_OP_AND, + z3.Z3_OP_OR, + z3.Z3_OP_NOT, + z3.Z3_OP_IMPLIES, + z3.Z3_OP_XOR, + z3.Z3_OP_EQ, + z3.Z3_OP_DISTINCT, + z3.Z3_OP_ITE, + z3.Z3_OP_LE, + z3.Z3_OP_LT, + z3.Z3_OP_GE, + z3.Z3_OP_GT, + z3.Z3_OP_ADD, + z3.Z3_OP_SUB, + z3.Z3_OP_UMINUS, +} + + +class _PureSelectExpressionCache: + """One two-copy solver's assumption-independent expression rewrites. + + Only the simplify-first path uses this cache: it never has radix lemmas + or uses a pair's bounds/correspondence to rewrite another expression. + Keys are actual immutable Z3 ASTs, after any cross/intra substitutions. + Values are expressions, never Solver state or query decisions. + Every abstracted node records whether its traversal saw a Select, so a + cache hit retains the same applicability information as a fresh walk. + """ + + def __init__(self): + self._normalized = {} + self._abstracted = {} + + def normalize(self, expression): + cached = self._normalized.get(expression) + if cached is None: + cached = z3.simplify(expression) + self._normalized[expression] = cached + return cached + + def abstract(self, expression): + cached = self._abstracted.get(expression) + if cached is not None: + return cached + if z3.is_const(expression) and expression.sort().kind() in ( + z3.Z3_INT_SORT, + z3.Z3_BOOL_SORT, + ): + result, saw_select = expression, False + else: + kind = expression.decl().kind() if z3.is_app(expression) else None + allowed = kind in _LINEAR_OPS or kind in ( + z3.Z3_OP_MUL, + z3.Z3_OP_IDIV, + z3.Z3_OP_MOD, + ) + saw_select = z3.is_select(expression) + children = None + if allowed and all( + child.sort().kind() in (z3.Z3_INT_SORT, z3.Z3_BOOL_SORT) + for child in expression.children() + ): + rewritten = [self.abstract(child) for child in expression.children()] + children = [child for child, _ in rewritten] + saw_select |= any(seen for _, seen in rewritten) + if z3.is_mul(expression): + allowed = sum(not z3.is_int_value(child) for child in children) <= 1 + if kind in (z3.Z3_OP_IDIV, z3.Z3_OP_MOD): + allowed = len(children) == 2 and (_numeral(children[1]) or 0) != 0 + else: + allowed = False + if allowed: + result = expression.decl()(*children) + elif expression.sort().kind() == z3.Z3_INT_SORT: + result = z3.FreshInt("conflict_integer", ctx=expression.ctx) + elif expression.sort().kind() == z3.Z3_BOOL_SORT: + result = z3.FreshBool("conflict_boolean", ctx=expression.ctx) + else: + raise TypeError("non-integer conflict expression") + cached = result, saw_select + self._abstracted[expression] = cached + return cached + + def relaxation(self, conditions, *, normalized_conditions=None): + # A diagnostic can disable this factor after a cache was populated. + # An old memo entry must not silently re-enable the optional path. + if not _ENABLE_SNAPSHOT_PRECHECK: + return None + try: + normalized = normalized_conditions + if normalized is None: + normalized = [self.normalize(condition) for condition in conditions] + for condition in normalized: + if z3.is_false(condition): + return condition + rewritten = [self.abstract(condition) for condition in normalized] + if not any(seen for _, seen in rewritten): + return None + return z3.simplify(z3.And(*(expression for expression, _ in rewritten))) + except (TypeError, z3.Z3Exception): + return None + + +def _linear_relaxation( + conditions, + correspondence=(), + *, + same_instance=False, + simplify_first=False, + expression_cache=None, + normalized_conditions=None, +): + """Return a sound QF_LIA relaxation, or None outside the cheap pattern. + + ``correspondence`` maps b-copy variables onto matching a-copy variables + for SHAPE comparison only. It never identifies actual copies in a + cross-instance condition, and radix matching uses its original AST. + ``normalized_conditions`` reuses the pure-Select path's preparation; + it is ignored by the general path, which preserves original radix syntax. + """ + if simplify_first and expression_cache is not None: + return expression_cache.relaxation( + conditions, normalized_conditions=normalized_conditions + ) + if simplify_first: + # A pure Select path has no mixed-radix syntax to preserve. Fold + # constants and trivial conflict predicates in Z3's native rewriter + # before walking the DAG in Python, once per condition. + conditions = ( + normalized_conditions + if normalized_conditions is not None + else [z3.simplify(condition) for condition in conditions] + ) + if any(z3.is_false(condition) for condition in conditions): + return z3.BoolVal(False) + bounds = set() if simplify_first else _explicit_digit_bounds(conditions) + memo, flattened, array_reads = {}, [], [] + supported = _LINEAR_OPS + + def abstract(expr): + if expr in memo: + return memo[expr] + match = _mixed_radix(expr, bounds) if _ENABLE_RADIX_PRECHECK else None + if match is not None and _numeral(match[1]) is None: + quotient, radix, digit = match + result = z3.FreshInt("conflict_flat") + memo[expr] = result + flattened.append((expr, result, quotient, radix, digit)) + return result + if z3.is_const(expr) and expr.sort().kind() in ( + z3.Z3_INT_SORT, + z3.Z3_BOOL_SORT, + ): + return expr + if z3.is_select(expr) and not _ENABLE_SNAPSHOT_PRECHECK: + raise TypeError("snapshot precheck disabled") + kind = expr.decl().kind() if z3.is_app(expr) else None + arithmetic = kind in (z3.Z3_OP_MUL, z3.Z3_OP_IDIV, z3.Z3_OP_MOD) + allowed = kind in supported or arithmetic + children = None + if allowed and all( + c.sort().kind() in (z3.Z3_INT_SORT, z3.Z3_BOOL_SORT) + for c in expr.children() + ): + # Protect the original mixed-radix nodes above, then fold the + # remaining arithmetic bottom-up. In particular, truncating + # division emits If(2 >= 0, 2, -2) as its denominator: deciding + # linearity before this fold would lose the index/domain link. + children = [abstract(child) for child in expr.children()] + if z3.is_mul(expr): + allowed = sum(not z3.is_int_value(c) for c in children) <= 1 + if kind in (z3.Z3_OP_IDIV, z3.Z3_OP_MOD): + allowed = len(children) == 2 and (_numeral(children[1]) or 0) != 0 + else: + allowed = False + if allowed: + result = expr.decl()(*children) + if not simplify_first: + result = z3.simplify(result) + elif expr.sort().kind() == z3.Z3_INT_SORT: + result = z3.FreshInt("conflict_integer") + if z3.is_select(expr): + array_reads.append(expr) + elif expr.sort().kind() == z3.Z3_BOOL_SORT: + result = z3.FreshBool("conflict_boolean") + if z3.is_select(expr): + array_reads.append(expr) + else: + raise TypeError("non-integer conflict expression") + memo[expr] = result + return result + + try: + relaxed = [abstract(condition) for condition in conditions] + groups = defaultdict(list) + # Nested quotients can expose more flattened nodes during abstraction. + index = 0 + while index < len(flattened): + expr, value, quotient, radix, digit = flattened[index] + index += 1 + shape = z3.substitute(expr, *correspondence) if correspondence else expr + groups[(radix, shape)].append((value, abstract(quotient), abstract(digit))) + matched_radix = bool(flattened) and ( + same_instance or any(len(group) > 1 for group in groups.values()) + ) + if not array_reads and not matched_radix: + return None + for group in groups.values(): + for i, (va, qa, da) in enumerate(group): + for vb, qb, db in group[i + 1 :]: + relaxed.append(z3.Implies(va == vb, z3.And(qa == qb, da == db))) + return z3.simplify(z3.And(*relaxed)) + except (TypeError, z3.Z3Exception): + return None + + +def conflict_impossible( + conditions: list[Any], + correspondence=(), + *, + same_instance=False, + simplify_first=False, + expression_cache=None, + snapshot_cache=None, +) -> bool: + """Cheap UNSAT-only precheck; callers retain their original query budget.""" + normalized = None + weak_attempted = False + if simplify_first and _ENABLE_SNAPSHOT_PRECHECK: + # Pure Select abstraction can already rule out an address pair without + # inspecting the snapshot cells. Only UNSAT discharges the pair; an + # inconclusive attempt retains the original guarded-lemma check below. + normalize = ( + expression_cache.normalize if expression_cache is not None else z3.simplify + ) + try: + # Reuse this path's existing normalization in the guarded attempt. + # Snapshot certificates still receive the ORIGINAL conditions. + if expression_cache is None: + normalized = [normalize(condition) for condition in conditions] + else: + try: + normalized = [normalize(condition) for condition in conditions] + except (TypeError, z3.Z3Exception): + # The cached relaxation has always treated normalization + # failure as unsupported rather than throwing to its caller. + normalized = None + relaxed = ( + _linear_relaxation( + conditions, + correspondence, + same_instance=same_instance, + simplify_first=True, + expression_cache=expression_cache, + normalized_conditions=normalized, + ) + if normalized is not None + else None + ) + if relaxed is not None and _relaxation_impossible(relaxed): + return True + except (TypeError, z3.Z3Exception): + # The extra attempt must not prevent an original guarded query + # from succeeding, including when lemma extraction yields no facts. + pass + else: + weak_attempted = True + lemmas = () + if _ENABLE_SNAPSHOT_PRECHECK: + # These facts follow from snapshot cells ALREADY in this query. + # Keep all source conditions and the guards on each derived lemma. + try: + lemmas = ( + snapshot_cache.lemmas(conditions) + if snapshot_cache is not None + else snapshot_table_lemmas(z3.And(*conditions)) + ) + except (TypeError, z3.Z3Exception): + lemmas = () + if lemmas: + conditions = [*conditions, *lemmas] + if normalized is not None: + try: + normalized.extend(normalize(lemma) for lemma in lemmas) + except (TypeError, z3.Z3Exception): + if expression_cache is None: + raise + return False + if weak_attempted and not lemmas: + # With no added facts, the original precheck is exactly the attempted + # relaxation, including whether it is supported. When applicable, it + # has already received the original full 500 ms precheck budget. + return False + relaxed = _linear_relaxation( + conditions, + correspondence, + same_instance=same_instance, + simplify_first=simplify_first, + expression_cache=expression_cache, + normalized_conditions=normalized, + ) + if relaxed is None: + return False + return _relaxation_impossible(relaxed) + + +def _relaxation_impossible(relaxed) -> bool: + if z3.is_false(relaxed): + return True + solver = z3.SolverFor("QF_LIA") + # This is only a speculative shortcut. Expiring it has no effect on + # the full query's budget, answer, or proof scope. A weak-first attempt + # never consumes the original guarded-lemma check's independent budget. + solver.set(timeout=_PRECHECK_TIMEOUT_MS) + solver.add(relaxed) + return solver.check() == z3.unsat diff --git a/tilelens/clients/race_detector/data.py b/tilelens/clients/race_detector/data.py index 8f6abff8b..ebc7ca4f4 100644 --- a/tilelens/clients/race_detector/data.py +++ b/tilelens/clients/race_detector/data.py @@ -1,4 +1,7 @@ +from __future__ import annotations + from dataclasses import dataclass, field +from enum import Enum, auto from typing import Any, Literal import torch @@ -6,6 +9,16 @@ from ...core.data import Op +MemorySem = Literal["plain", "relaxed", "acquire", "release", "acq_rel"] +AtomicKind = Literal["none", "cas", "rmw"] + + +class RaceType(Enum): + RAW = auto() # Read-After-Write + WAR = auto() # Write-After-Read + WAW = auto() # Write-After-Write + + @dataclass class AccessEventRecord: op_type: type[Op] @@ -18,3 +31,121 @@ class AccessEventRecord: local_constraints: tuple[Any, ...] = field(default_factory=tuple) source_location: tuple[str, int, str] | None = None grid_idx: tuple[int, ...] | None = None + program_seq: int = -1 + debug_name: str | None = None + active: Any = True + reads: Any = None + writes: Any = None + is_atomic: bool = False + atomic_kind: AtomicKind = "none" + sem: MemorySem = "plain" + scope: str | None = None + old_value: Any = None + written_value: Any = None + + # Two-copy solver fields. + event_id: int = -1 # stable dedup key (per launch) + elem_size: int = 1 # for byte-overlap when > 1 + + # Pre-exit representative (the await abstraction): True for + # the value-model-free twin of an awaited poll that stands for ALL + # FAILED iterations of the spin. It mirrors the poll's footprint, + # activity and program_seq (equal seq = mutually po-unordered with the + # poll) under a fresh event_id, and carries NO value model — so no + # rf/sw edge can enter or leave it, preserving the failed iterations' + # unorderedness. The solver excludes it from the unmodeled- + # overlapping-writer escape and skips the (rep, own poll) + # intra-instance pair. + pre_exit: bool = False + + # CAS-specific raw symbolic pieces. None for non-CAS records. + cas_cmp_value: Any = None + cas_new_value: Any = None + + # RMW value modeling. ``rmw_op`` is the canonical lowercase + # op name ("add", "max", "min", "xchg", ...; "exch" is normalized to + # "xchg" at capture). ``rmw_operand`` is the symbolic operand v so the + # write part can be modeled as f_op(old, v). Both stay None for a + # non-RMW record or an RMW whose value semantics are not modeled (float + # ops, bitwise and/or/xor, unsigned umax/umin) — the solver then keeps + # the record's write in the UNMODELED-writer set (rf_unknown escape), + # which is the over-report direction. When the return value is modeled, + # ``old_value`` holds the fresh observation var o_r (alpha-renamed per + # copy via ``copy_local_vars``, exactly like the CAS return). + rmw_op: str | None = None + rmw_operand: Any = None + + # Z3 vars representing per-program-instance nondeterminism for THIS record + # (the fresh CAS return var, this record's loop iterator vars). The two-copy + # solver collects these across all records and alpha-renames each ORIGINAL + # var exactly once per copy (launch-level), so downstream records that + # reference the same var get the same _a/_b rename. Tensor base pointers, + # kernel scalar args, and global constants are explicitly NOT included. + copy_local_vars: tuple[Any, ...] = field(default_factory=tuple) + + # Dependency order: event_ids of the load / atomic records whose + # RESULT this record's value, mask, or compare operand consumes through + # an element-wise chain (no reduce, scan, broadcast, reshape, transpose, + # join/split, splat in between). At the same position such a pair is + # ordered by causality (the value must exist before it is written), so + # the intra-instance query ranges over DISTINCT positions only for + # these pairs. + dep_loads: tuple[int, ...] = () + + # Operational control conditions used for value-causality dependencies, + # before execution-domain premises are conjoined into event activity. + # None uses local_constraints/premises instead, which can contain + # real masks and loop control. Frontends with separate domain facts must + # supply only actual control conditions (for example loop existence). + # active, addresses and atomic operands are tracked separately. + causal_constraints: tuple[Any, ...] | None = None + + # Earlier await records that must exit before this operation when both + # execute in one program copy. These are conditional control edges: + # the solver must conjoin both endpoints' activity/path predicates, + # rather than treating source order alone as an unconditional dependency. + await_dependencies: tuple[int, ...] = () + # Observation-producing records consumed by this await's exit predicate, + # including the poll and any separately read expected/threshold value. + await_observations: tuple[int, ...] = () + + +@dataclass(frozen=True) +class RaceReport: + """Race detected between two memory events. + + ``first`` and ``second`` are the two events of the witness; each carries + its ``AccessEventRecord`` as ``.record``. + """ + + first: Any + second: Any + model: dict[str, str] = field(default_factory=dict) + reason: str = "" + race_type_value: RaceType | None = None + witness_addr: int | None = None + witness_grid_a: tuple[int, int, int] | None = None + witness_grid_b: tuple[int, int, int] | None = None + + @property + def first_record(self) -> AccessEventRecord: + return self.first.record + + @property + def second_record(self) -> AccessEventRecord: + return self.second.record + + @property + def race_type(self) -> RaceType: + # TwoCopySymbolicHBSolver, the only producer, always sets it. + assert self.race_type_value is not None + return self.race_type_value + + +__all__ = [ + "AccessEventRecord", + "AtomicKind", + "MemorySem", + "RaceReport", + "RaceType", +] diff --git a/tilelens/clients/race_detector/guarded_division.py b/tilelens/clients/race_detector/guarded_division.py new file mode 100644 index 000000000..3c66b2962 --- /dev/null +++ b/tilelens/clients/race_detector/guarded_division.py @@ -0,0 +1,260 @@ +"""Query-local, certified constant folding for variable integer divisors. + +Grouped tile addresses often have a variable divisor that is constant under +the access mask. Only original top-level conjuncts may certify this fact. +If Q entails E = (term == value), then Q is equivalent to substitute(Q) AND E. +Keep E so that SAT models still satisfy the original query. No launch bounds, +snapshot values, or other premises are introduced here. +""" + +from __future__ import annotations + +import time + +import z3 + + +_ENABLE_GUARDED_DIVISION = True +_CERTIFY_TIMEOUT_MS = 200 + + +class GuardedDivisionApplicabilityCache: + """Memoize only whether an immutable AST may need divisor certification. + + One solver can share this cache across conflict queries with common DAGs. + A negative answer avoids another complete walk of those DAGs. Positive + answers still run the original query-local certification, with its original + budget and premises. In particular, neither guards nor proven equalities + are cached here. + """ + + def __init__(self): + # Retain contexts and AST wrappers: Z3 may recycle AST identifiers once + # nodes are released, and identifiers alone do not distinguish contexts. + self._contexts = {} + + def may_have_variable_divisor(self, expression): + context_key = id(expression.ctx) + context_entry = self._contexts.get(context_key) + if context_entry is None: + context_entry = (expression.ctx, {}) + self._contexts[context_key] = context_entry + nodes = context_entry[1] + + # Explicit postorder traversal also handles deeply nested expressions. + # A cached subtree costs one lookup regardless of its size. + pending = [(expression, None)] + while pending: + node, children = pending.pop() + node_id = node.get_id() + if node_id in nodes: + continue + if children is None: + if z3.is_quantifier(node) or not z3.is_app(node): + # Do not infer applicability from unsupported syntax. The + # original normalization pass will leave the query alone. + nodes[node_id] = (node, True) + continue + if node.decl().kind() in ( + z3.Z3_OP_IDIV, + z3.Z3_OP_MOD, + ) and not z3.is_int_value(node.arg(1)): + nodes[node_id] = (node, True) + continue + children = node.children() + if not children: + nodes[node_id] = (node, False) + continue + pending.append((node, children)) + pending.extend((child, None) for child in children) + else: + nodes[node_id] = ( + node, + any(nodes[child.get_id()][1] for child in children), + ) + return nodes[expression.get_id()][1] + + +def _conjuncts(expression): + pending = [expression] + while pending: + node = pending.pop() + if z3.is_and(node): + pending.extend(reversed(node.children())) + else: + yield node + + +def guarded_division_normal_form(expression, *, applicability_cache=None): + """Keep the original query if the optional certificate machinery fails.""" + try: + if not _ENABLE_GUARDED_DIVISION: + return expression + if ( + applicability_cache is not None + and not applicability_cache.may_have_variable_divisor(expression) + ): + return expression + return _guarded_division_normal_form(expression) + except z3.Z3Exception: + return expression + + +def _guarded_division_normal_form(expression): + """Return an equivalent formula, or the original when no fact is proved. + + Candidate discovery is syntactic, but adoption always requires an independent + UNSAT proof from a subset of Q. Restrict that subset to one local scalar guard + and its existing variable bounds, avoiding the full two-copy conflict query. + SAT/unknown in certification simply leaves that term unchanged.""" + if not _ENABLE_GUARDED_DIVISION: + return expression + nodes, pending = [], [(expression, False)] + seen, complete = set(), set() + while pending: + node, ready = pending.pop() + if node in complete: + continue + if z3.is_quantifier(node) or not z3.is_app(node): + return expression + if not ready: + if node in seen: + continue + seen.add(node) + pending.append((node, True)) + pending.extend((child, False) for child in node.children()) + continue + complete.add(node) + nodes.append(node) + + divisors = [ + node.arg(1) + for node in nodes + if node.decl().kind() in (z3.Z3_OP_IDIV, z3.Z3_OP_MOD) + and not z3.is_int_value(node.arg(1)) + ] + if not divisors: + return expression + + variables = {} + for node in nodes: + if z3.is_const(node) and node.decl().kind() == z3.Z3_OP_UNINTERPRETED: + variables[node] = frozenset((node,)) + else: + variables[node] = frozenset().union( + *(variables[child] for child in node.children()) + ) + + candidates, visited = [], set() + pending = list(divisors) + while pending: + node = pending.pop() + if node in visited: + continue + visited.add(node) + if node in divisors or ( + node.decl().kind() == z3.Z3_OP_IDIV + and z3.is_int_value(node.arg(1)) + and node.arg(1).as_long() > 0 + ): + candidates.append(node) + pending.extend(node.children()) + + atoms = list(_conjuncts(expression)) + # Only scalar integer formulas with no arrays, quantifiers or uninterpreted + # functions are useful local arithmetic certificates. + arithmetic = { + z3.Z3_OP_TRUE, + z3.Z3_OP_FALSE, + z3.Z3_OP_ANUM, + z3.Z3_OP_UNINTERPRETED, + z3.Z3_OP_AND, + z3.Z3_OP_OR, + z3.Z3_OP_NOT, + z3.Z3_OP_ITE, + z3.Z3_OP_EQ, + z3.Z3_OP_DISTINCT, + z3.Z3_OP_LE, + z3.Z3_OP_LT, + z3.Z3_OP_GE, + z3.Z3_OP_GT, + z3.Z3_OP_ADD, + z3.Z3_OP_SUB, + z3.Z3_OP_UMINUS, + z3.Z3_OP_MUL, + z3.Z3_OP_IDIV, + z3.Z3_OP_MOD, + } + scalar = {} + for node in nodes: + scalar[node] = ( + node.sort().kind() in (z3.Z3_INT_SORT, z3.Z3_BOOL_SORT) + and node.decl().kind() in arithmetic + and (node.decl().kind() != z3.Z3_OP_UNINTERPRETED or z3.is_const(node)) + and all(scalar[child] for child in node.children()) + ) + simple_bounds = [] + for atom in atoms: + comparison = atom.arg(0) if z3.is_not(atom) else atom + if ( + comparison.decl().kind() + in (z3.Z3_OP_LE, z3.Z3_OP_LT, z3.Z3_OP_GE, z3.Z3_OP_GT, z3.Z3_OP_EQ) + and comparison.num_args() == 2 + and any(z3.is_int_value(child) for child in comparison.children()) + and all( + z3.is_int_value(child) + or (z3.is_const(child) and child.sort().kind() == z3.Z3_INT_SORT) + for child in comparison.children() + ) + ): + simple_bounds.append(atom) + + substitutions, equalities = [], [] + deadline = time.monotonic() + _CERTIFY_TIMEOUT_MS / 1000 + + def certified_check(solver): + remaining = deadline - time.monotonic() + if remaining <= 0: + return z3.unknown + solver.set(timeout=max(1, int(remaining * 1000))) + return solver.check() + + for term in candidates: + term_variables = variables[term] + if not term_variables or not scalar[term]: + continue + # Try each single local mask rather than joining unrelated guards. + for atom in atoms: + if time.monotonic() >= deadline: + break + atom_variables = variables[atom] + if ( + not scalar[atom] + or not term_variables <= atom_variables + or len(atom_variables - term_variables) > 1 + or atom in simple_bounds + ): + continue + # A shared variable alone does not make this a guard for the term. + if z3.eq(z3.substitute(atom, (term, z3.IntVal(0, ctx=term.ctx))), atom): + continue + premises = [atom] + [ + bound for bound in simple_bounds if variables[bound] <= atom_variables + ] + solver = z3.Solver(ctx=expression.ctx) + solver.add(*premises) + if certified_check(solver) != z3.sat: + continue + value = solver.model().eval(term, model_completion=True) + if not z3.is_int_value(value): + continue + equality = term == value + solver.add(z3.Not(equality)) + if certified_check(solver) == z3.unsat: + substitutions.append((term, value)) + equalities.append(equality) + break + + if not substitutions: + return expression + return z3.And(z3.simplify(z3.substitute(expression, *substitutions)), *equalities) diff --git a/tilelens/clients/race_detector/hb_common.py b/tilelens/clients/race_detector/hb_common.py new file mode 100644 index 000000000..6727fd2a1 --- /dev/null +++ b/tilelens/clients/race_detector/hb_common.py @@ -0,0 +1,262 @@ +"""Shared HB primitives for the race detector's two-copy solver.""" + +from __future__ import annotations + +from typing import Any, Callable, Iterable, Iterator + +from z3 import And, BoolSort, BoolVal, Not, Or, is_false, is_true, simplify, substitute +from z3.z3 import BoolRef, IntNumRef + + +class UnsupportedSymbolicRaceQuery(Exception): + """Raised when a record cannot be lowered to Z3 or a query is undecided. + + Either capture-side normalisation or solver-side lowering may raise this, + and so may any solver query that Z3 cannot decide. The caller must report + the launch as unsupported, never as race-free. + """ + + +class CountingScopeUnsupported(UnsupportedSymbolicRaceQuery): + """An atomic address needs a counter whose symbolic-grid bound may wrap. + + A caller may retry a smaller declared launch domain with every guard + intact. This does not certify that the counter is valid in that domain. + """ + + +def as_bool(value: Any) -> BoolRef: + """Coerce ``value`` to a Z3 ``BoolRef``. + + Accepts Python bool/int/float, Z3 ``IntNumRef``, and non-Bool-sort Z3 + expressions (returning ``value != 0``). ``None`` is intentionally NOT + handled — passing ``None`` indicates a caller-side bug and should + surface as a Z3 type error rather than silently inactivating the + event. + """ + if isinstance(value, bool): + return BoolVal(value) + if isinstance(value, IntNumRef): + return BoolVal(value.as_long() != 0) + if isinstance(value, (int, float)): + return BoolVal(value != 0) + if hasattr(value, "sort") and value.sort() != BoolSort(): + return value != 0 + return value + + +def iter_constraints(value: Any) -> Iterator[Any]: + """Flatten ``None`` / scalar / list / tuple into individual constraints.""" + if value is None: + return + if isinstance(value, (list, tuple)): + for item in value: + yield from iter_constraints(item) + return + yield value + + +def to_lanes(value: Any) -> tuple[Any, ...]: + """Return ``value`` as a tuple of per-lane components.""" + if isinstance(value, (list, tuple)): + return tuple(value) + return (value,) + + +def lane_value(value: Any, lane: int, n_lanes: int) -> Any: + """Return the component of ``value`` at ``lane``. + + - ``None`` → ``None``. + - Python scalar / Z3 expression → broadcast to every lane. + - list/tuple of length ``n_lanes`` → indexed lookup. + - list/tuple of length 1 → broadcast. + - any other shape → :class:`UnsupportedSymbolicRaceQuery`. + """ + if value is None: + return None + if isinstance(value, (list, tuple)): + if len(value) == n_lanes: + return value[lane] + if len(value) == 1: + return value[0] + raise UnsupportedSymbolicRaceQuery( + f"lane_value: vector of length {len(value)} cannot be aligned with " + f"n_lanes={n_lanes}" + ) + return value + + +def apply_sub(value: Any, substitutions: tuple[tuple[Any, Any], ...]) -> Any: + """Recursively apply Z3 substitutions through ``None`` / list / tuple / scalar.""" + if value is None: + return None + if isinstance(value, list): + return [apply_sub(v, substitutions) for v in value] + if isinstance(value, tuple): + return tuple(apply_sub(v, substitutions) for v in value) + if isinstance(value, (bool, int)): + return value + if not substitutions: + return value + return substitute(value, *substitutions) + + +def is_release_sem(sem: Any) -> bool: + return sem in ("release", "acq_rel") + + +def is_acquire_sem(sem: Any) -> bool: + return sem in ("acquire", "acq_rel") + + +def build_transitive_hb( + events: list[Any], + edge_fn: Callable[[Any, Any], BoolRef], +) -> list[list[BoolRef]]: + """Floyd-Warshall closure, omitting only identically false paths. + + Simplification uses no query assumptions: every conditional edge, including + cycles and self-edges, retains its original meaning. Each layer combines + only the non-false incoming and outgoing entries for its intermediate node, + instead of constructing expressions for all pairs. The initial matrix and + row/column scans cost O(n**2); path construction costs the sum of the layers' + incoming-count times outgoing-count, with O(n**3) worst-case work. + """ + n = len(events) + reach = [ + [simplify(edge_fn(events[i], events[j])) for j in range(n)] for i in range(n) + ] + for k in range(n): + # Snapshot both vectors before updating the matrix. Even for a cyclic + # graph, every right-hand side then refers to the previous FW layer. + incoming = [(i, reach[i][k]) for i in range(n) if not is_false(reach[i][k])] + outgoing = [(j, edge) for j, edge in enumerate(reach[k]) if not is_false(edge)] + for i, left in incoming: + for j, right in outgoing: + previous = reach[i][j] + if is_true(previous): + continue + if is_true(left): + through = right + elif is_true(right) or left.eq(right): + through = left + else: + through = And(left, right) + if is_false(previous) or is_true(through): + reach[i][j] = through + elif not previous.eq(through): + reach[i][j] = Or(previous, through) + return reach + + +def conflicting_access_modes(first: Any, second: Any) -> BoolRef: + """``(write,read|write)`` conflict, minus morally strong pairs. + + An atomic-vs-atomic pair is race-free only when the two operations are + actually atomic with respect to EACH OTHER: mutually inclusive scopes, + same access width, and the exact same address. Scope inclusion is + symbolic: a pair involving a ``"cta"`` scope is mutually inclusive + exactly when the two events share a block (PTX ``.cta`` scope + guarantees atomicity within one CTA only), which cross-copy queries + falsify via their different-blocks assertion while same-instance + queries satisfy. Byte-overlapping atomics at different addresses or + widths are torn accesses, which race like plain writes. + + Built with explicit ``And``/``Or`` to avoid Python operator-precedence + pitfalls between Z3 expressions and Python booleans. + """ + access_conflict = Or( + And(first.writes, Or(second.reads, second.writes)), + And(second.writes, Or(first.reads, first.writes)), + ) + if not (first.is_atomic and second.is_atomic): + return access_conflict + + if first.elem_size != second.elem_size: + return access_conflict + + if first.scope != "cta" and second.scope != "cta": + return And(access_conflict, Not(first.addr == second.addr)) + scope_ok = And( + first.pid[0] == second.pid[0], + first.pid[1] == second.pid[1], + first.pid[2] == second.pid[2], + ) + return And(access_conflict, Not(And(scope_ok, first.addr == second.addr))) + + +def modeled_atomic_read_from( + writer: Any, + reader: Any, + *, + same_atomic_addr_fn: Callable[[Any, Any], BoolRef], +) -> BoolRef: + """Read-from predicate between two VALUE-MODELED atomic events. + + Membership is field-presence-based: the writer must have a modeled + written value and the reader a modeled observation (CAS always has + both; an RMW has them exactly when its return value is modeled). An + atomic without value modeling never gets an rf edge — its write stays + in the unmodeled-writer set that opens the ``rf_unknown`` escape. + """ + if not writer.is_atomic or not reader.is_atomic: + return BoolVal(False) + if writer.written_value is None or reader.old_value is None: + return BoolVal(False) + return And( + writer.writes, + reader.reads, + same_atomic_addr_fn(writer, reader), + writer.written_value == reader.old_value, + ) + + +def normalize_copy_local_vars(values: Iterable[Any]) -> tuple[Any, ...]: + """Flatten and dedup copy-local Z3 vars. + + Dedup key is ``(v.hash(), str(v.sort()), v.decl().name())`` rather than + ``v.hash()`` alone, so distinct vars that happen to share a hash are not + collapsed. ``None`` and Python scalars are skipped — only Z3 vars are + retained. + """ + out: list[Any] = [] + seen: set[tuple[int, str, str]] = set() + + def visit(v: Any) -> None: + if v is None: + return + if isinstance(v, (list, tuple)): + for item in v: + visit(item) + return + if isinstance(v, (bool, int)): + return + try: + key = (v.hash(), str(v.sort()), v.decl().name()) + except Exception: + return + if key in seen: + return + seen.add(key) + out.append(v) + + for value in values: + visit(value) + return tuple(out) + + +__all__ = [ + "CountingScopeUnsupported", + "UnsupportedSymbolicRaceQuery", + "apply_sub", + "as_bool", + "build_transitive_hb", + "conflicting_access_modes", + "is_acquire_sem", + "is_release_sem", + "iter_constraints", + "lane_value", + "modeled_atomic_read_from", + "normalize_copy_local_vars", + "to_lanes", +] diff --git a/tilelens/clients/race_detector/hb_solver.py b/tilelens/clients/race_detector/hb_solver.py deleted file mode 100644 index 52a5cb758..000000000 --- a/tilelens/clients/race_detector/hb_solver.py +++ /dev/null @@ -1,7 +0,0 @@ -"""Happens-before reasoning for race_detector. - -HB logic intentionally deferred until after Step 1. Step 0 keeps this file -as a visible placeholder so the directory layout is stable, but nothing in -Step 0/Step 1 should import from here. The real ``HBSolver`` lands with -the Step-2 PR. -""" diff --git a/tilelens/clients/race_detector/report_diagnostics.py b/tilelens/clients/race_detector/report_diagnostics.py new file mode 100644 index 000000000..111ea5b76 --- /dev/null +++ b/tilelens/clients/race_detector/report_diagnostics.py @@ -0,0 +1,71 @@ +"""Explanations attached to already-established race witnesses. + +This module consumes only report facts. It must not construct constraints, +change witnesses, or decide whether an access pair conflicts. +""" + +from __future__ import annotations + + +def _located_source(site: tuple[str, int, str] | None) -> bool: + return ( + isinstance(site, (tuple, list)) + and len(site) >= 2 + and isinstance(site[0], str) + and bool(site[0]) + and isinstance(site[1], int) + and site[1] > 0 + ) + + +def append_missing_fence_diagnostic( + reason: str, + *, + same_instance: bool, + distinct_operations: bool, + first_seq: int, + second_seq: int, + fenced: bool, + first_site: tuple[str, int, str] | None, + second_site: tuple[str, int, str] | None, + first_mode: str, + second_mode: str, + pre_exit: bool = False, +) -> str: + """Explain a located cross-operation witness under source fence order. + + Unknown/equal sequence numbers and pre-exit representatives do not + identify two ordered source operations. Duplicate lanes and cross-instance + witnesses need different explanations. Preserve their original reasons. + """ + if ( + not same_instance + or not distinct_operations + or pre_exit + or first_seq < 0 + or second_seq < 0 + or first_seq == second_seq + or fenced + or not _located_source(first_site) + or not _located_source(second_site) + ): + return reason + assert first_site is not None + assert second_site is not None + # Report canonicalization uses event IDs, which need not follow source + # order. Explain the missing fence in source order without reordering + # the public report endpoints or its RAW/WAR classification. + if first_seq > second_seq: + first_site, second_site = second_site, first_site + first_mode, second_mode = second_mode, first_mode + return ( + f"{reason}. Missing source fence: the {first_mode} at " + f"{first_site[0]}:{first_site[1]} and the {second_mode} at " + f"{second_site[0]}:{second_site[1]} have no captured fence that orders " + "them. Their reported overlap is unordered under the tile-level " + "memory model. Review the required ordering; Triton's " + "tl.debug_barrier() is an option only with appropriate scope and " + "uniform participation. Compiler-inserted barriers may add ordering; " + "this diagnosis alone proves neither a real-execution race nor a " + "complete repair." + ) diff --git a/tilelens/clients/race_detector/snapshot_lemmas.py b/tilelens/clients/race_detector/snapshot_lemmas.py new file mode 100644 index 000000000..af9014f4a --- /dev/null +++ b/tilelens/clients/race_detector/snapshot_lemmas.py @@ -0,0 +1,425 @@ +"""Entailed range and injectivity facts from existing finite array equations. + +This helper never loads a snapshot or adds launch assumptions. It recognizes +only equations already asserted as top-level conjuncts. A finite, contiguous +integer interval and its values certify the resulting guarded lemmas. Values +outside that interval remain unconstrained, including in any-grid queries. +The original formula must remain present when these lemmas are used. +""" + +from __future__ import annotations + +from dataclasses import dataclass +from itertools import combinations + +import z3 + + +# Avoid generating quadratically many optional facts for an unrelated large +# base query. Declining injectivity leaves both the original formula and the +# linear number of valid range facts intact. +_MAX_INJECTIVITY_READS = 16 + + +@dataclass(eq=False, frozen=True, slots=True) +class _CellFacts: + """A persistent DAG of original asserted cell equations.""" + + children: tuple = () + cell: tuple | None = None + + +@dataclass(frozen=True, slots=True) +class _Summary: + reads: tuple = () + + +class SnapshotLemmaCache: + """One solver's reusable facts about immutable, original expressions. + + Node summaries do not depend on any assumptions. Only conjunctions lift + cell equations into the asserted-fact summary; bound reads never leave a + quantifier. Certificates are keyed by the exact current fact summaries + for each relevant array. Pair-specific reads reuse a common table without + reparsing its cells. Removing or changing an asserted equation requires + another certificate for that array. Other arrays are independent. + Neither mutable condition lists nor solver decisions are memoized. + """ + + def __init__(self): + self._context = None + self._children = {} + self._cells = {} + self._candidates = {} + self._summaries = {} + self._fact_summaries = {} + self._fact_joins = {} + self._certificates = {} + self._guarded_reads = {} + self._injectivity = {} + + def _node_children(self, node): + if node not in self._children: + self._children[node] = tuple(node.children()) + return self._children[node] + + def _cell_equation(self, node): + if not z3.is_eq(node): + return None + left, right = self._node_children(node) + for read, value in ((left, right), (right, left)): + if not ( + z3.is_int_value(value) and z3.is_select(read) and read.num_args() == 2 + ): + continue + array, index = self._node_children(read) + if not z3.is_int_value(index): + continue + array_sort = array.sort() + if ( + array_sort.domain().kind() == z3.Z3_INT_SORT + and array_sort.range().kind() == z3.Z3_INT_SORT + ): + # Decode values only when this array actually needs a + # certificate. Candidate and read scans need only its identity. + return array, index, value + return None + + def _cell(self, node): + if node not in self._cells: + self._cells[node] = self._cell_equation(node) + return self._cells[node] + + def _has_facts(self, expression, arrays=None): + """Look only through asserted conjunctions, without scanning reads.""" + key = expression, arrays + if key in self._candidates: + return self._candidates[key] + pending, seen = [expression], set() + while pending: + node = pending.pop() + if node in seen: + continue + seen.add(node) + node_key = node, arrays + if node_key in self._candidates: + if self._candidates[node_key]: + self._candidates[key] = True + return True + continue + if z3.is_and(node): + pending.extend(reversed(self._node_children(node))) + continue + cell = self._cell(node) + candidate = cell is not None and (arrays is None or cell[0] in arrays) + self._candidates[node_key] = candidate + if candidate: + self._candidates[key] = True + return True + self._candidates[key] = False + return False + + def _summary(self, expression): + # Iterative postorder handles deep expressions without Python recursion. + pending = [(expression, None)] + while pending: + node, children = pending.pop() + if node in self._summaries: + continue + if z3.is_quantifier(node): + self._summaries[node] = _Summary() + continue + if children is None: + cell = self._cell(node) + if ( + cell is not None + and z3.is_const(cell[0]) + and cell[0].decl().kind() == z3.Z3_OP_UNINTERPRETED + ): + # A literal cell of a plain array symbol has no eligible + # reads beneath it. Keep its original cell separately, but + # avoid summaries for the Select and its literals. + # Store/If/function array terms may contain symbolic reads + # and must follow the ordinary descendant traversal. + self._summaries[node] = _Summary() + continue + children = self._node_children(node) + if children: + pending.append((node, children)) + pending.extend((child, None) for child in children) + continue + summaries = [self._summaries[child] for child in children] + # Match the standalone helper's reverse-child DFS read ordering. + own_read = ( + (node,) + if z3.is_select(node) + and len(children) == 2 + and not z3.is_int_value(children[1]) + else () + ) + reads = tuple( + dict.fromkeys( + (*own_read, *(r for s in reversed(summaries) for r in s.reads)) + ) + ) + self._summaries[node] = _Summary(reads) + return self._summaries[expression] + + def _fact_summary(self, expression): + """Group complete original facts by array in first-occurrence order.""" + pending = [(expression, None)] + while pending: + node, children = pending.pop() + if node in self._fact_summaries: + continue + if not z3.is_and(node): + cell = self._cell(node) + self._fact_summaries[node] = ( + ((cell[0], _CellFacts(cell=cell)),) if cell is not None else () + ) + continue + if children is None: + children = self._node_children(node) + pending.append((node, children)) + pending.extend((child, None) for child in children) + continue + by_array = {} + for child in children: + for array, facts in self._fact_summaries[child]: + by_array.setdefault(array, []).append(facts) + facts = [] + for array, array_roots in by_array.items(): + roots = tuple(dict.fromkeys(array_roots)) + if len(roots) == 1: + root = roots[0] + else: + if roots not in self._fact_joins: + self._fact_joins[roots] = _CellFacts(roots) + root = self._fact_joins[roots] + facts.append((array, root)) + self._fact_summaries[node] = tuple(facts) + return self._fact_summaries[expression] + + @staticmethod + def _certify(roots): + tables, inconsistent = {}, set() + pending, seen = list(reversed(roots)), set() + while pending: + facts = pending.pop() + if facts in seen: + continue + seen.add(facts) + if facts.cell is None: + pending.extend(reversed(facts.children)) + continue + array, index, number = facts.cell + index, number = index.as_long(), number.as_long() + table = tables.setdefault(array, {}) + if index in table and table[index] != number: + inconsistent.add(array) + table[index] = number + certificates = {} + for array, table in tables.items(): + lower, upper = min(table), max(table) + if array in inconsistent or len(table) != upper - lower + 1: + continue + values = tuple(table.values()) + certificates[array] = ( + lower, + upper, + min(values), + max(values), + len(set(values)) == len(table), + ) + return certificates + + def lemmas(self, conditions) -> tuple[z3.BoolRef, ...]: + conditions = tuple(c for c in conditions if not isinstance(c, bool)) + if not conditions or not all(isinstance(c, z3.BoolRef) for c in conditions): + return () + context = conditions[0].ctx + if any(c.ctx != context for c in conditions): + raise z3.Z3Exception("snapshot conditions have different contexts") + if self._context != context: + # A solver normally uses one context. A reused helper may switch, + # but equal-looking ASTs from different contexts never share facts. + self._children.clear() + self._cells.clear() + self._candidates.clear() + self._summaries.clear() + self._fact_summaries.clear() + self._fact_joins.clear() + self._certificates.clear() + self._guarded_reads.clear() + self._injectivity.clear() + self._context = context + if not any(self._has_facts(condition) for condition in conditions): + return () + summaries = [self._summary(condition) for condition in conditions] + actual_reads = dict.fromkeys(r for s in reversed(summaries) for r in s.reads) + if not actual_reads: + # Certificates cannot produce a lemma without a nonliteral read. + # Cached read summaries allow this exit before assembling facts. + return () + relevant_arrays = frozenset(self._node_children(r)[0] for r in actual_reads) + if not any( + self._has_facts(condition, relevant_arrays) for condition in conditions + ): + return () + by_array: dict[z3.ArrayRef, list[_CellFacts]] = {} + for condition in conditions: + for array, facts in self._fact_summary(condition): + if array in relevant_arrays: + by_array.setdefault(array, []).append(facts) + certificates = {} + for array_roots in by_array.values(): + # Each key contains every current asserted cell for this array, + # including conflicting or incomplete facts. Neither read changes + # nor unrelated arrays can turn stale premises into a certificate. + roots = tuple(dict.fromkeys(array_roots)) + if roots not in self._certificates: + self._certificates[roots] = self._certify(roots) + certificates.update(self._certificates[roots]) + if not certificates: + return () + reads: dict[z3.ArrayRef, list[z3.ArithRef]] = { + array: [] for array in certificates + } + for read in actual_reads: + array = self._node_children(read)[0] + if array in certificates: + reads[array].append(read) + lemmas = [] + for array, table_reads in reads.items(): + certificate = certificates[array] + lower, upper, minimum, maximum, injective = certificate + guarded = [] + for read in table_reads: + key = read, certificate + if key not in self._guarded_reads: + index = self._node_children(read)[1] + guard = z3.And(index >= lower, index <= upper) + lemma = z3.Implies(guard, z3.And(read >= minimum, read <= maximum)) + self._guarded_reads[key] = guard, lemma + guard, lemma = self._guarded_reads[key] + guarded.append((read, guard)) + lemmas.append(lemma) + if injective and len(guarded) <= _MAX_INJECTIVITY_READS: + for (read_a, guard_a), (read_b, guard_b) in combinations(guarded, 2): + pair_key = read_a, read_b, certificate + if pair_key not in self._injectivity: + self._injectivity[pair_key] = z3.Implies( + z3.And(guard_a, guard_b, read_a == read_b), + self._node_children(read_a)[1] + == self._node_children(read_b)[1], + ) + lemmas.append(self._injectivity[pair_key]) + return tuple(lemmas) + + +def _conjuncts(expression): + pending = [expression] + while pending: + node = pending.pop() + if z3.is_and(node): + pending.extend(reversed(node.children())) + else: + yield node + + +def _nodes(expression): + pending, seen = [expression], set() + while pending: + node = pending.pop() + if node in seen: + continue + seen.add(node) + # A read with a bound index cannot be lifted out of its binder. + if z3.is_quantifier(node): + continue + yield node + pending.extend(node.children()) + + +def snapshot_table_lemmas(expression) -> tuple[z3.BoolRef, ...]: + """Return independently entailed lemmas, without solving or new premises. + + For each original table, completeness is checked by comparing the number + of distinct keys to the inclusive interval's size. Every recorded value + is checked when deriving the range; injectivity additionally requires all + those values to differ. Conflicting equations and holes decline the table. + Duplicate values retain only the valid range facts. + """ + if not isinstance(expression, z3.BoolRef): + return () + tables: dict[z3.ArrayRef, dict[int, int]] = {} + inconsistent: set[z3.ArrayRef] = set() + for atom in _conjuncts(expression): + if not z3.is_eq(atom): + continue + for read, value in (atom.children(), tuple(reversed(atom.children()))): + if not ( + z3.is_select(read) + and read.num_args() == 2 + and z3.is_int_value(read.arg(1)) + and z3.is_int_value(value) + ): + continue + array = read.arg(0) + if ( + array.sort().domain().kind() != z3.Z3_INT_SORT + or array.sort().range().kind() != z3.Z3_INT_SORT + ): + continue + index, number = read.arg(1).as_long(), value.as_long() + table = tables.setdefault(array, {}) + if index in table and table[index] != number: + inconsistent.add(array) + table[index] = number + + certificates = {} + for array, table in tables.items(): + lower, upper = min(table), max(table) + if array in inconsistent or len(table) != upper - lower + 1: + continue + values = tuple(table.values()) + certificates[array] = ( + lower, + upper, + min(values), + max(values), + len(set(values)) == len(table), + ) + if not certificates: + return () + + reads: dict[z3.ArrayRef, list[z3.ArithRef]] = {array: [] for array in certificates} + for node in _nodes(expression): + if ( + z3.is_select(node) + and node.num_args() == 2 + and node.arg(0) in certificates + and not z3.is_int_value(node.arg(1)) + ): + reads[node.arg(0)].append(node) + + lemmas: list[z3.BoolRef] = [] + for array, actual_reads in reads.items(): + lower, upper, minimum, maximum, injective = certificates[array] + guarded = [ + (read, z3.And(read.arg(1) >= lower, read.arg(1) <= upper)) + for read in actual_reads + ] + lemmas.extend( + z3.Implies(guard, z3.And(read >= minimum, read <= maximum)) + for read, guard in guarded + ) + if injective and len(guarded) <= _MAX_INJECTIVITY_READS: + lemmas.extend( + z3.Implies( + z3.And(guard_a, guard_b, read_a == read_b), + read_a.arg(1) == read_b.arg(1), + ) + for (read_a, guard_a), (read_b, guard_b) in combinations(guarded, 2) + ) + return tuple(lemmas) diff --git a/tilelens/clients/race_detector/two_copy_symbolic_hb_solver.py b/tilelens/clients/race_detector/two_copy_symbolic_hb_solver.py new file mode 100644 index 000000000..7481d3a9c --- /dev/null +++ b/tilelens/clients/race_detector/two_copy_symbolic_hb_solver.py @@ -0,0 +1,2626 @@ +"""Two-copy symbolic HB solver. + +The race detector's race-finder. The solver duplicates each +recorded access into two symbolic program-instances ``A`` and ``B`` (alpha- +renaming PIDs, ``tl.arange`` lane vars, and per-record copy-local vars such as +the CAS return), then asks Z3 whether any pair of cross-copy events is +unordered, in conflict, and aliasing. + +Model boundary (closed-world atomic source assumption): + When an initial scalar source is identifiable AND no unmodeled write (plain + store or atomic RMW) can overlap the location, source choices are closed + over: (initial source) + (modeled CAS writers in the two selected copies). + Otherwise ``rf_unknown_R`` is introduced but does NOT enable a + synchronizes-with edge — an overlapping plain-store/RMW can publish a value + outside the closed world (e.g. a flag set via ``tl.atomic_xchg``), so the + reader's old value must not be over-constrained or every conflict gated on + it silently disappears. Synchronization through a third program instance is + not modeled. The guarded acquire/release CAS no-race result depends on the + closed world, which holds whenever the flag is only ever written by modeled + CAS. + +Address-domain invariant: + ``record.addr_expr`` consumed by this solver MUST be a byte address matching + ``tensor.data_ptr()``. ``byte_overlap`` and ``initial_atomic_source`` rely on + this. Capture-side normalisation must convert element / tensor-relative + offsets to byte addresses BEFORE the records reach the solver. + +Z3 context: + Every term lives in Z3's main context. Records must be lowered there (a + term from another context fails with Z3's "Context mismatch"), and since + that context is shared and not thread-safe, the caller serializes solves. + +Intra-instance duplicate lanes: + Cross-copy queries assert ``different_blocks``, so they can never witness + two lanes of one store colliding inside a single program instance — and a + grid=(1,1,1) launch makes ``different_blocks`` UNSAT outright. A separate + same-instance query pins ``pid_a == pid_b`` and every launch-level + copy-local var equal, leaving the arange lane vars as the only + alpha-difference between the copies; requiring a lane-identity difference + then asks whether two DISTINCT lanes of the same dynamic access conflict. + Distinct operations of one instance are concurrently in flight unless the + caller's ``fence_between`` hook or a dependency orders them, so unordered + pairs of distinct operations enter the same query. + +Z3 ``unknown`` policy: + Every query runs on its own Solver with a per-Solver timeout + (``timeout_ms``); no global Z3 parameter is changed. ``unknown`` (a + timeout included) is never treated as unsat. A race query that comes back + undecided raises :class:`UnsupportedSymbolicRaceQuery` (the launch reports + ``unsupported`` instead of a silent clean verdict), and an undecided + overlap in the closed-world escape check opens the ``rf_unknown`` escape. + +RMW value modeling: + An integer AtomicRMW with a modeled op (``add``/``max``/``min``/``xchg``) + gets a fresh observation symbol ``o_r`` (``record.old_value``, alpha- + renamed per copy exactly like the CAS return) and a modeled write part + ``f_op(o_r, v)`` (``written_value``). ``o_r`` is justified like a CAS + observation: rf candidates are the value-modeled atomic writers, the + initial-value source, and the unknown source when an unmodeled writer can + overlap. Value-modeled atomics join the per-location atomic order, which + makes RMW **atomicity/immediacy** structural: one order position covers + the read AND the write part, and the existing "no successful same-address + writer strictly between rf source and reader" constraint is exactly the + immediacy axiom. Two extensions build on it: + + - **Reads-through (release sequences over RMW chains)**: sw(w, r) also + holds when r reads-through w via a bounded chain of modeled RMW write + parts (each link an rf edge). Chains through UNMODELED grid instances + are covered only by the counting axiom below. + - **Counting axiom** (guarded): for a location L touched by EXACTLY ONE + always-active scalar constant-increment ``add`` RMW record with a known + initial value and no other possible writer, per-copy rank variables + r ∈ [0, |G|) satisfy ``o = init + c·rank``, rank equality iff same + block, and ``co ⇔ rank<``. Under those guards every write to L between + two instances is a link of the same RMW chain, so reads-through is + equivalent to coherence order — giving last-block-done and work-queue + disjointness. A counted reader also gets an ``rf_chain`` source choice + (an unmodeled instance at rank-1) so real races at non-adjacent ranks + are not squeezed out of the closed world; ``rf_chain`` itself never + enables synchronizes-with. If ANY guard fails the axiom is omitted + entirely (over-report direction), and an observation variable used in + an ADDRESS position without counting support raises + ``UnsupportedSymbolicRaceQuery`` instead of widening silently. + +Limitations (current): + - **Initial atomic source covers scalar tensors and small contiguous flag + arrays** (``numel <= _MAX_INITIAL_ATOMIC_ELEMENTS = 1024``). Larger or + non-contiguous tensors fall through to ``rf_unknown_R``, which + deliberately does NOT enable synchronizes-with; guarded acq/rel CAS over + them is reported as races conservatively. + - **Two program instances only** — synchronization that travels through a + third block (writer-via-third-block CAS chains) is not modeled directly; + the counting axiom is the one guarded exception. + - **Float-typed RMW returns and bitwise/unsigned RMW ops are not value- + modeled** (``fadd``, float max, ``and``/``or``/``xor``, ``umax``/ + ``umin``): they get no modeled write part, so the record's write stays + in the unmodeled-writer set. +""" + +from __future__ import annotations + +from collections.abc import Callable +from dataclasses import dataclass +from typing import TYPE_CHECKING, Any, ClassVar + +if TYPE_CHECKING: + from .guarded_division import GuardedDivisionApplicabilityCache + from .snapshot_lemmas import SnapshotLemmaCache + +from z3 import ( + And, + AtMost, + Bool, + BoolVal, + Const, + ExprRef, + If, + Implies, + Int, + IntVal, + Not, + Or, + Solver, + is_false, + is_true, + sat, + simplify, + unsat, +) +from z3.z3 import BoolRef, IntNumRef, ModelRef + +from .conflict_simplification import ( + _PureSelectExpressionCache, + conflict_impossible, + conflict_precheck_features, +) +from .data import AccessEventRecord, RaceReport, RaceType +from .hb_common import ( + CountingScopeUnsupported, + UnsupportedSymbolicRaceQuery, + apply_sub, + as_bool, + build_transitive_hb, + conflicting_access_modes, + is_acquire_sem, + is_release_sem, + iter_constraints, + lane_value, + modeled_atomic_read_from, + normalize_copy_local_vars, + to_lanes, +) +from .report_diagnostics import append_missing_fence_diagnostic + + +@dataclass(frozen=True) +class CopyContext: + label: str # "a" or "b" + pid: tuple[Any, Any, Any] + pid_substitutions: tuple[tuple[Any, Any], ...] + arange_substitutions: tuple[tuple[Any, Any], ...] + arange_constraints: tuple[Any, ...] + copy_local_substitutions: tuple[tuple[Any, Any], ...] # launch-level + + +def _immutable_precheck_source(value: Any) -> bool: + """Admit only immutable leaves and containers for identity-based reuse.""" + if type(value) in (bool, int, float): + return True + if isinstance(value, ExprRef): + # User-defined subclasses can override coercion with mutable state. + # Standard z3py expression classes represent immutable ASTs. + return type(value).__module__ == ExprRef.__module__ + if type(value) is tuple: + return all(_immutable_precheck_source(item) for item in value) + if type(value) is CopyContext: + # Frozen records can still contain mutable fields supplied by callers. + # These are exactly the fields read by the common precheck below. + return all( + _immutable_precheck_source(field) + for field in ( + value.pid, + value.copy_local_substitutions, + value.arange_substitutions, + ) + ) + return False + + +@dataclass +class _ConflictPrecheckCommon: + # Retaining the source objects makes identity checks safe against id reuse. + sources: tuple[Any, ...] + expression: BoolRef + shared: tuple[tuple[Any, Any], ...] + correspondence: tuple[tuple[Any, Any], ...] + has_snapshot: bool | None = None + intra_expression: BoolRef | None = None + + +@dataclass(frozen=True) +class _BaseConstraintCache: + # Keep the objects alive: comparisons use Python identity, never Z3 equality. + snapshot: tuple[tuple[Any, ...], ...] + expression: BoolRef + + +@dataclass(frozen=True) +class SymbolicMemoryEvent: + idx: int + copy: str + record: AccessEventRecord + name: str + lane: int + event_id: int + program_seq: int + pid: tuple[Any, Any, Any] + addr: Any + elem_size: int + active: BoolRef + reads: BoolRef + writes: BoolRef + is_atomic: bool + atomic_kind: str + sem: str + scope: str | None + old_value: Any = None + written_value: Any = None + # The substituted RMW operand v (None for non-RMW / unmodeled RMW); + # the counting axiom reads the constant increment off it. + rmw_operand: Any = None + # Substituted operational conditions, excluding proof-domain premises. + # Reads/writes retain those premises for all execution constraints; + # causality must not mistake them for observation dependencies. + causal_inputs: tuple[Any, ...] = () + + +def _import_symbolic_expr_pids(): + # Local import: SymbolicExpr is a heavy module; keep tests cheap. + from ..symbolic_engine import SymbolicExpr + + return (SymbolicExpr.PID0, SymbolicExpr.PID1, SymbolicExpr.PID2) + + +def _is_symbolic_dim(d: Any) -> bool: + """A grid dim that is a Z3 expression rather than a Python int. + + Must be an isinstance check: duck-typing on ``sort`` misfires on numpy + scalars (ndarray.sort) and would leave them un-coerced where the old + ``int(d)`` handled them.""" + return isinstance(d, ExprRef) + + +@dataclass(frozen=True) +class _CountingInfo: + """The counting axiom fired for one RMW record: per-copy + rank variables tied to the observation values and the atomic order.""" + + idx_a: int + idx_b: int + rank_a: Any + rank_b: Any + init: int + inc: int + loc: int + + +def _rmw_written_value(op: str | None, old: Any, v: Any) -> Any: + """The modeled write part f_op(old, v) of an RMW, or ``None`` when the + op has no Int-sort model: non-identity bitwise and/or/xor need + bitvectors, unsigned umax/umin diverge from the signed Int order, and + float ops are outside the integer model. The one bitwise case with an + exact Int model is the identity or/xor of a provably-zero operand + (f(old, 0) = old), the write-back shape of an identity-RMW await poll; + a symbolic or nonzero operand keeps ``None``. ``None`` keeps the + record's write in the unmodeled-writer set (rf_unknown escape) — the + over-report direction.""" + if op is None or old is None or v is None: + return None + if op == "add": + return old + v + if op == "max": + return If(old >= v, old, v) + if op == "min": + return If(old <= v, old, v) + if op == "xchg": + return v + if op in ("or", "xor") and _as_numeral(v) == 0: + return old + return None + + +def _as_numeral(v: Any) -> int | None: + """``v`` as a concrete int if it simplifies to one, else None.""" + if v is None: + return None + if isinstance(v, (bool, int)): + return int(v) + try: + s = simplify(v) + except Exception: + return None + if isinstance(s, IntNumRef): + return s.as_long() + return None + + +def _z3_var_key(v: Any) -> tuple[int, str, str]: + # Mirrors the dedup key used by hb_common.normalize_copy_local_vars. + return (v.hash(), str(v.sort()), v.decl().name()) + + +def _collect_z3_var_keys(values: tuple[Any, ...]) -> set[tuple[int, str, str]]: + """Keys of every 0-ary leaf in ``values``. Numeral leaves are included + but can never collide with a variable's key.""" + seen: set[tuple[int, str, str]] = set() + stack: list[Any] = list(values) + while stack: + v = stack.pop() + if v is None or isinstance(v, (bool, int, float, str)): + continue + if isinstance(v, (list, tuple)): + stack.extend(v) + continue + if not hasattr(v, "num_args"): + continue + if v.num_args() == 0: + try: + seen.add(_z3_var_key(v)) + except Exception: + pass + continue + stack.extend(v.children()) + return seen + + +class TwoCopySymbolicHBSolver: + """Two-copy symbolic happens-before solver. + + Construct it over one launch's records, then call :meth:`find_races` + (and :meth:`check_feasibility` before claiming race freedom). Both the + constructor and the queries raise :class:`UnsupportedSymbolicRaceQuery` + (or its subclass :class:`CountingScopeUnsupported`) when a record cannot + be lowered or a query is undecided. See the module docstring for the + model boundary and address-domain invariants. + """ + + # Per-Solver Z3 budget of every query this solver creates (milliseconds). + # The enumeration's per-case and retry limits below only ever shorten + # it. Never a global Z3 parameter: a solve must not change Z3's + # defaults for other clients. + TIMEOUT_MS: ClassVar[int] = 180_000 + ENUM_MAX_CASES: ClassVar[int] = 1024 + ENUM_CASE_TIMEOUT_MS: ClassVar[int] = 5000 + ENUM_TOTAL_BUDGET_S: ClassVar[float] = 60.0 + # Once one query has been decided by enumeration the launch's claim + # is already scoped to its extent, so a LATER query's long symbolic + # attempt can no longer buy a stronger claim: it gets this short + # budget instead and falls through to the (near-free) enumeration. + # Applied only when the cross case split fits ENUM_MAX_CASES, so a + # query whose split would overflow keeps its full symbolic budget. + ENUM_RETRY_TIMEOUT_MS: ClassVar[int] = 10_000 + + def __init__( + self, + records: list[AccessEventRecord], + *, + grid: tuple[Any, ...], + arange_dict: dict[Any, Any] | None = None, + extra_assumptions: tuple[Any, ...] = (), + only_pairs: frozenset[tuple[int, int]] | None = None, + enum_fallback_grid: tuple[int, int, int] | None = None, + launch_ceiling: bool = False, + fence_between: Callable[[AccessEventRecord, AccessEventRecord], bool] + | None = None, + timeout_ms: int | None = None, + ) -> None: + self.records = list(records) + # Fence-ordered intra-instance semantics: program order between two + # records of one instance is a happens-before edge only when a + # fence orders them, and same-instance pairs of distinct operations + # that no fence orders enter the intra-instance race query. Which fence orders which pair is the + # caller's rule: ``fence_between(first, second)`` is asked for two + # records of one instance with ``first.program_seq < + # second.program_seq``. None: no fence orders any pair. + self.fence_between = fence_between + self._fence_cache: dict[tuple[int, int], bool] = {} + self.timeout_ms = self.TIMEOUT_MS if timeout_ms is None else int(timeout_ms) + if self.timeout_ms <= 0: + # Z3 reads timeout=0 as "no limit". + raise ValueError(f"timeout_ms must be positive, got {timeout_ms}") + # Dependency order: unordered record pairs (load, dependent) whose + # same-position accesses are ordered by causality. + self.dep_pairs: frozenset[tuple[int, int]] = frozenset( + (int(d), int(r.event_id)) + for r in self.records + for d in getattr(r, "dep_loads", ()) + ) + self.grid = self._normalize_grid(grid) + self.arange_dict = dict(arange_dict or {}) + self.extra_assumptions = tuple(extra_assumptions) + # Enumeration fallback: when a race query returns Z3-unknown and + # a concrete launch grid was provided, the query is re-asked as + # an exhaustive case split over concrete pid assignments at that + # extent. All-UNSAT decides the query AT THE LAUNCH EXTENT ONLY + # (the caller must degrade the claim to launch scope: enum_used + # is set); a SAT case is a normal witness with in-extent pids. + # Refused (the original unknown propagates) when the case + # count exceeds ENUM_MAX_CASES, a case is itself undecided, + # or ENUM_TOTAL_BUDGET_S is exhausted: fail-closed to the + # pre-fallback behavior. + self.enum_fallback_grid = enum_fallback_grid + self.enum_used = False + self._enum_deadline: float | None = None + # True when this solver's strongest possible claim is ALREADY + # launch-scoped (the pinned requery): then a long symbolic + # attempt can never buy more than the enumeration fallback + # delivers, so the short budget applies from the first query, + # not only after the first enumeration. + self.launch_ceiling = launch_ceiling + # Requery restriction (sound by UNSAT monotonicity): when set, + # only event pairs whose UNORDERED record-id pair is listed are + # queried. The caller may use this ONLY when every omitted pair + # is already known UNSAT under a WEAKER system (fewer + # assumptions): adding constraints (here: grid pins in + # extra_assumptions) cannot turn an UNSAT query SAT, so the + # omitted pairs contribute no reports either way. Keyed by + # record event_id and unordered, so every lane and both + # orientations of a listed record pair are still queried. + self.only_pairs = only_pairs + # The launch's premises after per-copy substitution (loop-iterator + # ranges and, decisively, the awaited exit predicates): the + # feasibility query asserts them, because activity gating folds + # them into every event, so the bare base system is always + # satisfiable through the all-inactive (non-terminating) + # valuation, which does not satisfy the premises. Filled during + # record lowering, before any constraint family is built. + self.launch_premises: list[BoolRef] = [] + + # 1. PID vars + substitutions for both copies. + pid_a, pid_b = self._make_pid_vars() + pid_subs_a, pid_subs_b = self._make_pid_subs(pid_a, pid_b) + + # 2. Grid bounds + different-block constraints. + ( + self.grid_constraints, + self.different_blocks, + ) = self._make_grid_and_diff_block_constraints(pid_a, pid_b) + + # 3. Arange substitutions + range constraints from the snapshot. + ( + arange_subs_a, + arange_subs_b, + arange_consts_a, + arange_consts_b, + ) = self._make_arange_subs_and_constraints() + self.arange_constraints_a = tuple(arange_consts_a) + self.arange_constraints_b = tuple(arange_consts_b) + + # 4. LAUNCH-LEVEL copy-local substitutions (union over all records). + copy_local_subs_a, copy_local_subs_b = self._make_launch_copy_local_subs() + + # 5. Build the two CopyContexts (frozen). + self.ctx_a = CopyContext( + label="a", + pid=tuple(pid_a), + pid_substitutions=tuple(pid_subs_a), + arange_substitutions=tuple(arange_subs_a), + arange_constraints=self.arange_constraints_a, + copy_local_substitutions=tuple(copy_local_subs_a), + ) + self.ctx_b = CopyContext( + label="b", + pid=tuple(pid_b), + pid_substitutions=tuple(pid_subs_b), + arange_substitutions=tuple(arange_subs_b), + arange_constraints=self.arange_constraints_b, + copy_local_substitutions=tuple(copy_local_subs_b), + ) + + # 6. Lower every record under both contexts. + self.events: list[SymbolicMemoryEvent] = self._lower_two_copies() + + # 7. Atomic-order vars, counting axioms, RF source booleans, and the + # reads-through relation, BEFORE building the HB closure (HB reads + # self.reads_through for synchronizes_with). Order matters: the + # counting axiom's applicability is consulted while building rf + # choices (it adds the rf_chain source), and the reads-through + # closure folds in both the direct rf edges and the counting pairs. + self.atomic_order: dict[int, Any] = self._make_atomic_order_vars() + self.rf_source: dict[tuple[int, int], BoolRef] = {} + self.rf_init_source: dict[int, BoolRef] = {} + self.rf_unknown_source: dict[int, BoolRef] = {} + self.rf_chain_source: dict[int, BoolRef] = {} + self.rf_constraints: list[BoolRef] = [] + self.atomic_coherence_constraints: list[BoolRef] = [] + self.counting_constraints: list[BoolRef] = [] + self._counting_grid_restricted: set[int] = set() + self._counting: dict[int, _CountingInfo] = self._build_counting_axioms() + self._build_read_from_choices() + self._build_atomic_coherence_constraints() + # wf-vc (value causality / no out-of-thin-air): its own family — + # coherence is per-location order, value causality is a + # cross-location well-formedness axiom of the value model itself. + self.vc_read_rank: dict[int, Any] = {} + self.vc_write_rank: dict[int, Any] = {} + self.value_causality_constraints: list[BoolRef] = [] + self._build_value_causality_constraints() + self._assert_no_uncounted_observation_addresses() + self.reads_through: dict[tuple[int, int], BoolRef] = self._build_reads_through() + + # 8. Build HB transitive closure (synchronizes_with reads + # reads_through). + self.hb = build_transitive_hb(self.events, self._edge) + + # 9. Coherence hb-consistency axiom (co-hb) — needs self.hb, hence + # after step 8; appended to atomic_coherence_constraints, which is + # consumed only at query time in _base_solver. + self._build_coherence_hb_constraints() + + # ──────────────────────── Public API ──────────────────────── + + _CROSS_INSTANCE_REASON: str = ( + "unordered conflicting memory accesses across two symbolic " + "program instances under the current symbolic assumptions" + ) + _INTRA_INSTANCE_REASON: str = ( + "conflicting lanes of a single program instance touch the same " + "bytes with no defined intra-instance order" + ) + + def find_races(self) -> list[RaceReport]: + """Race witnesses across two instances and within one, one report + per unordered (record, lane) pair whose race query is SAT.""" + import time as _time + + events_a = [e for e in self.events if e.copy == "a"] + events_b = [e for e in self.events if e.copy == "b"] + # (kind, seconds, sat) per executed query. + self.query_stats: list[tuple[str, float, bool]] = [] + # Only full symbolic UNSAT results are reusable. Keep their ASTs + # alive, and limit the cache to this race-finding invocation. + self._unsat_race_queries: dict[tuple[int, int], BoolRef] = {} + self._guarded_query_cache: dict[BoolRef, BoolRef] = {} + # Structural summaries retain immutable ASTs only for this invocation. + self._guarded_division_applicability_cache: GuardedDivisionApplicabilityCache | None = None + self._snapshot_lemma_cache: SnapshotLemmaCache | None = None + + candidates: list[tuple[SymbolicMemoryEvent, SymbolicMemoryEvent, ModelRef, str]] + candidates = [] + for a in events_a: + for b in events_b: + if self._pair_excluded(a, b): + continue + precheck_start = _time.perf_counter() + if self._conflict_precheck(a, b): + self.query_stats.append( + ("cross", _time.perf_counter() - precheck_start, False) + ) + continue + precheck_s = _time.perf_counter() - precheck_start + race_expression = self._race_expr(a, b) + normalization_start = _time.perf_counter() + normalized = self._normalized_race_query( + race_expression, (self.different_blocks,) + ) + known_unsat = self._known_unsat_race_query(normalized) + precheck_s += _time.perf_counter() - normalization_start + if known_unsat: + self.query_stats.append(("cross", precheck_s, False)) + continue + + def _build(a=a, b=b, normalized=normalized) -> Solver: + if normalized is None: + s = self._new_solver() + s.add(self._race_expr(a, b)) + else: + s = self._solver() + s.add(normalized) + return s + + solver = _build() + self._cap_symbolic_retry(solver) + t0 = _time.perf_counter() + model: ModelRef | None = None + try: + is_sat = self._race_query_is_sat(solver, a, b) + if is_sat: + model = solver.model() + else: + self._remember_unsat_race_query(normalized) + except UnsupportedSymbolicRaceQuery as exc: + is_sat, model = self._enumerate_pair(_build, False, exc) + self.query_stats.append( + ("cross", precheck_s + _time.perf_counter() - t0, is_sat) + ) + if is_sat: + candidates.append((a, b, model, self._CROSS_INSTANCE_REASON)) + + candidates.extend(self._find_intra_instance_candidates(events_a, events_b)) + return self._dedupe_reports(candidates) + + def check_feasibility(self, extra: tuple[Any, ...] = ()) -> bool: + """Feasibility half of the race-freedom certificate: does the base + system admit any execution at all? + + The m^2 per-pair race queries are all UNSAT even when the + premises themselves are unsatisfiable (an await's termination + premise no execution can meet), and a proof claimed over an + empty set of executions would be vacuous. The certificate is + feasibility AND race freedom, and this one satisfiability query + of the base constraints WITH the launch's premises asserted + discharges the first conjunct. The premises + must be asserted explicitly: activity gating folds them into + every event, so the bare base system always admits the + all-inactive valuation (the non-terminating execution), and a bare + check would be trivially satisfiable. + Deliberately WITHOUT ``different_blocks``: a + single-instance launch is feasible even though the + cross-instance constraint is unsatisfiable on its grid. + + Z3 ``unknown`` must not certify feasibility — escalate to + :class:`UnsupportedSymbolicRaceQuery` exactly like a race + query, so the caller reports the launch as unsupported rather + than certified. + """ + solver = self._base_solver() + for p in self.launch_premises: + solver.add(p) + for c in extra: + solver.add(as_bool(c)) + result = solver.check() + if result == sat: + return True + if result == unsat: + return False + detail = solver.reason_unknown() + raise UnsupportedSymbolicRaceQuery( + "Z3 could not decide the feasibility query" + + (f" ({detail})" if detail else "") + ) + + def _enum_pid_cases( + self, same_instance: bool + ) -> list[tuple[tuple[int, int, int], tuple[int, int, int]]] | None: + """Concrete pid assignments covering the fallback grid, or None + when no fallback grid is set or the case count exceeds + ENUM_MAX_CASES.""" + g = self.enum_fallback_grid + if g is None: + return None + n = g[0] * g[1] * g[2] + count = n if same_instance else n * (n - 1) + if count <= 0 or count > self.ENUM_MAX_CASES: + return None + pids = [ + (x, y, z) for z in range(g[2]) for y in range(g[1]) for x in range(g[0]) + ] + if same_instance: + return [(p, p) for p in pids] + return [(pa, pb) for pa in pids for pb in pids if pa != pb] + + def _enumerate_pair( + self, + build_solver: Any, + same_instance: bool, + original: Exception, + ) -> tuple[bool, ModelRef | None]: + """Decide one Z3-undecided pair by exhaustive concrete-pid case + split at the fallback grid's extent. + + ``build_solver`` rebuilds the pair's solver exactly as the + querying loop did (base system + pair constraints + race + expression); each case then pins both copies' pid triples to + concrete values, so the disjunction of the cases is exactly the + original query WITH the grid bounded to the fallback extent. + All cases UNSAT therefore decides the query AT THAT EXTENT (the + caller must scope the claim accordingly); any SAT case yields a + normal model whose witness pids are in-extent by construction. + ``original`` (the symbolic attempt's unknown) is re-raised + whenever the split cannot be completed: too many cases, a case + itself undecided, or the total budget exhausted — fail-closed + to the pre-fallback behavior. + """ + import time as _time + + cases = self._enum_pid_cases(same_instance) + if cases is None: + raise original + self.enum_used = True + if self._enum_deadline is None: + self._enum_deadline = _time.monotonic() + self.ENUM_TOTAL_BUDGET_S + deadline = self._enum_deadline + pid_a = [Int(f"pid_a_{i}") for i in range(3)] + pid_b = [Int(f"pid_b_{i}") for i in range(3)] + for pa, pb in cases: + if _time.monotonic() > deadline: + raise original + solver = build_solver() + assignments = tuple( + (pid, IntVal(value, ctx=pid.ctx)) + for pids, values in ((pid_a, pa), (pid_b, pb)) + for pid, value in zip(pids, values) + ) + # Substitute into EVERY original assertion, including activity, + # HB/rf, array and domain premises. Constant PIDs can eliminate + # nested address div/mod before the arithmetic solver sees them. + # Rebuilding first also observes any changed source constraints. + expression = simplify(apply_sub(And(*solver.assertions()), assignments)) + solver.reset() + solver.add(expression) + # Keep the original PID symbols in SAT models. Together these + # pins and the substituted assertions are equivalent to the old + # assertions plus pins, including all non-PID witness variables. + solver.add(*(pid == value for pid, value in assignments)) + solver.set(timeout=min(self.timeout_ms, self.ENUM_CASE_TIMEOUT_MS)) + result = solver.check() + if result == sat: + return True, solver.model() + if result != unsat: + raise original + return False, None + + def _cap_symbolic_retry(self, solver: Solver) -> None: + """Cap this symbolic attempt's budget (ENUM_RETRY_TIMEOUT_MS) + once a long attempt can no longer buy a stronger claim: after + the first enumeration (the claim is degraded to launch scope), + or from the start when the solver's claim ceiling is launch + scope by construction (the pinned requery). Gated on the CROSS + split fitting ENUM_MAX_CASES: then every possible unknown in + this solver is enumerable, so the cap cannot lose a decision.""" + if (self.enum_used or self.launch_ceiling) and self._enum_pid_cases( + False + ) is not None: + solver.set(timeout=min(self.timeout_ms, self.ENUM_RETRY_TIMEOUT_MS)) + + def _pair_excluded(self, a: SymbolicMemoryEvent, b: SymbolicMemoryEvent) -> bool: + """True when an ``only_pairs`` restriction is active and this + record pair is not in it (see ``__init__``); the pair's queries + are then skipped as already-known UNSAT.""" + if self.only_pairs is None: + return False + lo, hi = sorted((a.event_id, b.event_id)) + return (lo, hi) not in self.only_pairs + + def _normalized_race_query( + self, race_expression: BoolRef, pair_constraints: tuple[Any, ...] + ) -> BoolRef | None: + """Normalize the complete query before constructing a fresh solver. + + All base premises, the cross/same-instance conditions, lane identity, + and the original race expression are retained. Unsupported container + or coercion inputs use the original construction path instead. + """ + if not all( + isinstance(c, BoolRef) or type(c) is bool # noqa: E721 (only immutable builtin scalars) + for c in (race_expression, *pair_constraints) + ): + return None + base = self._base_constraint_conjunction() + if base is None: + return None + from .guarded_division import ( + GuardedDivisionApplicabilityCache, + guarded_division_normal_form, + ) + + original = simplify(And(base, *pair_constraints, race_expression)) + cache = getattr(self, "_guarded_query_cache", None) + if cache is None: + self._guarded_query_cache = cache = {} + if original not in cache: + applicability_cache = getattr( + self, "_guarded_division_applicability_cache", None + ) + if applicability_cache is None: + applicability_cache = ( + self._guarded_division_applicability_cache + ) = GuardedDivisionApplicabilityCache() + cache[original] = guarded_division_normal_form( + original, applicability_cache=applicability_cache + ) + return cache[original] + + @staticmethod + def _race_query_cache_key(expression: BoolRef) -> tuple[int, int]: + # AST ids are unique only within a context. The cache retains the + # expression (and its context), preventing either id from recycling. + return id(expression.ctx), expression.get_id() + + def _known_unsat_race_query(self, expression: BoolRef | None) -> bool: + if expression is None: + return False + cached = getattr(self, "_unsat_race_queries", None) + return cached is not None and self._race_query_cache_key(expression) in cached + + def _remember_unsat_race_query(self, expression: BoolRef | None) -> None: + if expression is None: + return + cached = getattr(self, "_unsat_race_queries", None) + if cached is None: + self._unsat_race_queries = cached = {} + cached[self._race_query_cache_key(expression)] = expression + + @staticmethod + def _race_query_is_sat( + solver: Solver, a: SymbolicMemoryEvent, b: SymbolicMemoryEvent + ) -> bool: + """``solver.check()`` with Z3 ``unknown`` made conservative. + + ``unknown`` (timeout, nonlinear give-up) must not collapse into + unsat: dropping the pair would turn an undecided query into a + silent clean "ok" verdict. There is no witness model to report + either, so escalate to :class:`UnsupportedSymbolicRaceQuery`; the + caller reports the launch as unsupported instead of race-free. + """ + result = solver.check() + if result == sat: + return True + if result == unsat: + return False + detail = solver.reason_unknown() + raise UnsupportedSymbolicRaceQuery( + f"Z3 could not decide the race query for {a.name} vs {b.name}" + + (f" ({detail})" if detail else "") + ) + + def _find_intra_instance_candidates( + self, + events_a: list[SymbolicMemoryEvent], + events_b: list[SymbolicMemoryEvent], + ) -> list[tuple[SymbolicMemoryEvent, SymbolicMemoryEvent, ModelRef, str]]: + """Duplicate-lane conflicts inside a single program instance. + + See the module docstring: cross-copy queries assert + ``different_blocks`` and therefore cannot witness these (under + grid=(1,1,1) they are vacuously unsat). An atomic op's lanes + serialize, so the intra-instance hazards are duplicate addresses + across the lanes of a single non-atomic store, plus pairs of + distinct operations that neither the caller's fence rule + (``fence_between``) nor a dependency orders, including pairs with + equal or unset sequence numbers. + """ + import time as _time + + same_instance = self._same_instance_constraints() + out: list[tuple[SymbolicMemoryEvent, SymbolicMemoryEvent, ModelRef, str]] + out = [] + for a in events_a: + for b in events_b: + if self._pair_excluded(a, b): + continue + lane_cond = self._intra_pair_lane_condition(a, b) + if lane_cond is None: + continue + precheck_start = _time.perf_counter() + if self._conflict_precheck( + a, b, same_instance=True, lane_cond=lane_cond + ): + if hasattr(self, "query_stats"): + self.query_stats.append( + ("intra", _time.perf_counter() - precheck_start, False) + ) + continue + precheck_s = _time.perf_counter() - precheck_start + race_expression = self._race_expr(a, b) + normalization_start = _time.perf_counter() + normalized = self._normalized_race_query( + race_expression, (*same_instance, lane_cond) + ) + known_unsat = self._known_unsat_race_query(normalized) + precheck_s += _time.perf_counter() - normalization_start + if known_unsat: + if hasattr(self, "query_stats"): + self.query_stats.append(("intra", precheck_s, False)) + continue + + def _build( + a=a, b=b, lane_cond=lane_cond, normalized=normalized + ) -> Solver: + if normalized is None: + s = self._base_solver() + for c in same_instance: + s.add(c) + s.add(lane_cond) + s.add(self._race_expr(a, b)) + else: + s = self._solver() + s.add(normalized) + return s + + solver = _build() + self._cap_symbolic_retry(solver) + t0 = _time.perf_counter() + model: ModelRef | None = None + try: + is_sat = self._race_query_is_sat(solver, a, b) + if is_sat: + model = solver.model() + else: + self._remember_unsat_race_query(normalized) + except UnsupportedSymbolicRaceQuery as exc: + is_sat, model = self._enumerate_pair(_build, True, exc) + if hasattr(self, "query_stats"): + self.query_stats.append( + ("intra", precheck_s + _time.perf_counter() - t0, is_sat) + ) + if is_sat: + out.append((a, b, model, self._INTRA_INSTANCE_REASON)) + return out + + def _conflict_precheck( + self, + a: SymbolicMemoryEvent, + b: SymbolicMemoryEvent, + *, + same_instance: bool = False, + lane_cond: BoolRef | None = None, + ) -> bool: + """Prove a necessary conflict condition UNSAT without changing HB. + + The single private entry point of the precheck. It never changes + enumeration state or participates in feasibility certification. + Actual byte overlap and activity stay in the weaker condition; + only the full solver supplies SAT witnesses. + """ + if is_false(a.writes) and is_false(b.writes): + return True + # Read/read pairs (and structurally exempt atomic pairs) have no + # conflict independently of their potentially large address DAGs. + if ( + self._ordinary_access_mode(a) is None + or self._ordinary_access_mode(b) is None + ) and is_true(simplify(Not(conflicting_access_modes(a, b)))): + return True + features = getattr(self, "_conflict_precheck_events", None) + if features is None: + features = self._conflict_precheck_events = { + event.idx: conflict_precheck_features(event.addr) + for event in self.events + } + common = self._conflict_precheck_common() + # Even linear addresses otherwise enter array solving when shared + # snapshot premises contain Selects. The same necessary-condition + # precheck can prove them disjoint without the full array/HB query. + if not any(features[a.idx]) and not any(features[b.idx]): + if common.has_snapshot is None: + common.has_snapshot = conflict_precheck_features(common.expression)[1] + if not common.has_snapshot: + return False + simplify_first = not (features[a.idx][0] or features[b.idx][0]) + conflict = self._conflict(a, b) + if same_instance: + assert lane_cond is not None + # In one instance, pids and copy-local observations/iterations + # agree. Lane variables MUST remain independent. + if common.intra_expression is None: + common.intra_expression = apply_sub(common.expression, common.shared) + conditions = [ + common.intra_expression, + apply_sub(conflict, common.shared), + apply_sub(lane_cond, common.shared), + ] + else: + conditions = [common.expression, conflict, self.different_blocks] + expression_cache = None + if simplify_first: + expression_cache = getattr(self, "_conflict_expression_cache", None) + if expression_cache is None: + expression_cache = ( + self._conflict_expression_cache + ) = _PureSelectExpressionCache() + from .snapshot_lemmas import SnapshotLemmaCache + + snapshot_cache = getattr(self, "_snapshot_lemma_cache", None) + if snapshot_cache is None: + snapshot_cache = self._snapshot_lemma_cache = SnapshotLemmaCache() + return conflict_impossible( + conditions, + common.correspondence, + same_instance=same_instance, + simplify_first=simplify_first, + expression_cache=expression_cache, + snapshot_cache=snapshot_cache, + ) + + def _conflict_precheck_common(self) -> _ConflictPrecheckCommon: + """Reuse the immutable common conjunction, never a query decision. + + The constructor stores constraint sequences as tuples and contexts + as frozen records. Attribute replacement invalidates the cached + conjunction, including removal of launch pins. Cache admission also + checks their contents: mutable or custom coercible conditions must + be read on every call, even inside an unchanged tuple. Admission is + checked only when building a new entry, preserving cheap cache hits. + """ + sources = ( + self.grid_constraints, + self.arange_constraints_a, + self.arange_constraints_b, + self.extra_assumptions, + self.ctx_a, + self.ctx_b, + ) + cached = getattr(self, "_conflict_common_cache", None) + if cached is not None and all( + current is old for current, old in zip(sources, cached.sources) + ): + return cached + self._conflict_common_cache = None + shared = tuple(zip(self.ctx_b.pid, self.ctx_a.pid)) + tuple( + (bvar, avar) + for (_, avar), (_, bvar) in zip( + self.ctx_a.copy_local_substitutions, + self.ctx_b.copy_local_substitutions, + ) + ) + correspondence = shared + tuple( + (bvar, avar) + for (_, avar), (_, bvar) in zip( + self.ctx_a.arange_substitutions, self.ctx_b.arange_substitutions + ) + ) + expression = And( + self.grid_constraints, + *self.arange_constraints_a, + *self.arange_constraints_b, + *[as_bool(condition) for condition in self.extra_assumptions], + ) + cached = _ConflictPrecheckCommon(sources, expression, shared, correspondence) + if all(_immutable_precheck_source(source) for source in sources): + self._conflict_common_cache = cached + return cached + + def _intra_pair_lane_condition( + self, a: SymbolicMemoryEvent, b: SymbolicMemoryEvent + ) -> BoolRef | None: + """Lane-identity constraint for an intra-instance pair, or ``None`` + when the pair cannot race within one instance (fence-ordered, + serialized, never writes, or the symmetric duplicate of an + already-queried pair). + """ + if a.record is b.record: + # Lanes of one atomic op serialize against each other; a + # load's duplicate lanes read-read and cannot conflict. + if a.record.is_atomic or a.record.access_mode != "write": + return None + if a.lane > b.lane: + return None # symmetric duplicate + if a.lane < b.lane: + return BoolVal(True) # explicitly distinct lanes + return self._lane_identity_differs(a) + # Distinct ops of one instance are concurrently in flight unless + # fence_between or a dependency orders them. + if a.event_id > b.event_id: + return None # symmetric duplicate + if (a.record.pre_exit or b.record.pre_exit) and a.program_seq == b.program_seq: + # The pre-exit representative vs its OWN awaited record (they + # share the poll's seq): a thread's poll does not race its own + # failed iterations. Do NOT rely on the conflict exemption — + # for a cta-scoped poll it is void and the equal-seq pair + # would surface as a same-instance race against itself; for + # device-scoped polls the pair is exempt-UNSAT anyway, so + # skipping is uniform and cheaper. + return None + if a.program_seq >= 0 and b.program_seq >= 0 and a.program_seq != b.program_seq: + if self._fence_orders(a, b): + return None + if (a.event_id, b.event_id) in self.dep_pairs or ( + b.event_id, + a.event_id, + ) in self.dep_pairs: + # Dependency order: the same position is ordered by + # causality, so only DISTINCT positions can race. + return self._lanes_differ(a, b) + # Fence-ordered semantics: two distinct operations of one + # instance with no fence between them are concurrently in + # flight, so the pair is queried like any conflicting pair. + return BoolVal(True) + return BoolVal(True) + + def _lanes_differ( + self, a: SymbolicMemoryEvent, b: SymbolicMemoryEvent + ) -> BoolRef | None: + """Constraint that the a-copy lane of ``a`` and the b-copy lane of + ``b`` are DIFFERENT positions, over the arange vars either event + uses; ``None`` when neither has a lane (scalar accesses: one + position, dependency-ordered, never queried).""" + occurring = _collect_z3_var_keys((a.addr, a.active, b.addr, b.active)) + diffs = [ + var_a != var_b + for (_, var_a), (_, var_b) in zip( + self.ctx_a.arange_substitutions, self.ctx_b.arange_substitutions + ) + if _z3_var_key(var_a) in occurring or _z3_var_key(var_b) in occurring + ] + if not diffs: + return None + return diffs[0] if len(diffs) == 1 else Or(*diffs) + + def _lane_identity_differs(self, e: SymbolicMemoryEvent) -> BoolRef | None: + """Constraint that the a/b copies of ``e`` denote two DIFFERENT + lanes of its record, or ``None`` for a true scalar access (no + second lane exists). + + Each arange summary var is injective in the lane index, so any one + of the record's arange vars differing across the copies witnesses + two distinct lanes. Vars in the activity condition count too: a + store whose address ignores the lane still has its lanes + distinguished by the mask. + """ + occurring = _collect_z3_var_keys((e.addr, e.active, e.writes)) + diffs = [ + var_a != var_b + for (_, var_a), (_, var_b) in zip( + self.ctx_a.arange_substitutions, self.ctx_b.arange_substitutions + ) + if _z3_var_key(var_a) in occurring or _z3_var_key(var_b) in occurring + ] + if not diffs: + return None + return diffs[0] if len(diffs) == 1 else Or(*diffs) + + def _same_instance_constraints(self) -> tuple[BoolRef, ...]: + """Pin the b copy onto the a copy's program instance. + + ``pid_a == pid_b`` makes the two copies the same block. Copy-local + vars (loop iterators, CAS returns) are pinned equal because within + one instance the two lane roles share each dynamic op's iteration + and return value — leaving them free would let an ordered + cross-iteration pair masquerade as an intra-instance lane conflict. + """ + cons: list[BoolRef] = [self.ctx_a.pid[i] == self.ctx_b.pid[i] for i in range(3)] + for (_, var_a), (_, var_b) in zip( + self.ctx_a.copy_local_substitutions, self.ctx_b.copy_local_substitutions + ): + cons.append(var_a == var_b) + return tuple(cons) + + # ──────────────────────── Construction ──────────────────────── + + @staticmethod + def _normalize_grid(grid: tuple[Any, ...]) -> tuple[Any, Any, Any]: + """Concrete launches pass ints; a static front-end passes Z3 + Ints so the verdict covers EVERY grid (each symbolic dim gets a + ``>= 1`` bound in the grid constraints).""" + dims = [d if _is_symbolic_dim(d) else int(d) for d in grid] + while len(dims) < 3: + dims.append(1) + return (dims[0], dims[1], dims[2]) + + @staticmethod + def _make_pid_vars(): + pid_a = [Int(f"pid_a_{i}") for i in range(3)] + pid_b = [Int(f"pid_b_{i}") for i in range(3)] + return pid_a, pid_b + + @staticmethod + def _make_pid_subs(pid_a, pid_b): + orig = _import_symbolic_expr_pids() + sub_a = tuple((orig[i], pid_a[i]) for i in range(3)) + sub_b = tuple((orig[i], pid_b[i]) for i in range(3)) + return sub_a, sub_b + + def _make_grid_and_diff_block_constraints(self, pid_a, pid_b): + grid_constraints = And( + *[And(pid_a[i] >= 0, pid_a[i] < self.grid[i]) for i in range(3)], + *[And(pid_b[i] >= 0, pid_b[i] < self.grid[i]) for i in range(3)], + # A symbolic dim needs its own lower bound or a zero/negative + # grid would make every pid constraint vacuously unsat and turn + # any query into a false proof. + *[d >= 1 for d in self.grid if _is_symbolic_dim(d)], + ) + different_blocks = Or( + pid_a[0] != pid_b[0], + pid_a[1] != pid_b[1], + pid_a[2] != pid_b[2], + ) + return grid_constraints, different_blocks + + def _make_arange_subs_and_constraints(self): + sub_a, sub_b = [], [] + cons_a, cons_b = [], [] + for key, value in self.arange_dict.items(): + # ARANGE_DICT entry shape: key=(start, end) or + # (start, end, filename, lineno) — the engine keys interned vars + # by creation site so independent same-range arange instances stay + # distinct. value=(orig_var, _). Per-copy names derive from the + # original var's name so every dict entry renames uniquely. + try: + start, end = key[0], key[1] + orig_var = value[0] if isinstance(value, (list, tuple)) else value + base_name = orig_var.decl().name() + except Exception: + continue + var_a = Int(f"{base_name}__a") + var_b = Int(f"{base_name}__b") + sub_a.append((orig_var, var_a)) + sub_b.append((orig_var, var_b)) + cons_a.append(And(var_a >= start, var_a < end)) + cons_b.append(And(var_b >= start, var_b < end)) + return sub_a, sub_b, cons_a, cons_b + + def _make_launch_copy_local_subs(self): + all_vars = normalize_copy_local_vars( + v for r in self.records for v in r.copy_local_vars + ) + subs_a, subs_b = [], [] + for i, v in enumerate(all_vars): + base = f"{v.decl().name()}__{i}__{v.hash()}" + subs_a.append((v, Const(f"{base}__a", v.sort()))) + subs_b.append((v, Const(f"{base}__b", v.sort()))) + return tuple(subs_a), tuple(subs_b) + + # ──────────────────────── Lowering ──────────────────────── + + def _lower_two_copies(self) -> list[SymbolicMemoryEvent]: + events: list[SymbolicMemoryEvent] = [] + for ctx in (self.ctx_a, self.ctx_b): + for record in self.records: + events.extend(self._lower_record(record, ctx, len(events))) + return events + + @staticmethod + def _active_access_mode(active: BoolRef, condition: BoolRef) -> BoolRef: + """Fold literal mode conditions while retaining the full activity guard.""" + if is_true(condition): + return active + if is_false(condition): + return condition + return And(active, condition) + + def _lower_record( + self, + record: AccessEventRecord, + ctx: CopyContext, + start_idx: int, + ) -> list[SymbolicMemoryEvent]: + if record.addr_expr is None: + raise UnsupportedSymbolicRaceQuery( + "AccessEventRecord.addr_expr is required for two-copy lowering" + ) + + sub = ( + ctx.pid_substitutions + + ctx.arange_substitutions + + ctx.copy_local_substitutions + ) + + addr_all = apply_sub(record.addr_expr, sub) + active_all = apply_sub(record.active, sub) + local_all = apply_sub(record.local_constraints, sub) + prem_all = apply_sub(record.premises, sub) + causal_all = ( + (local_all, prem_all) + if record.causal_constraints is None + else apply_sub(record.causal_constraints, sub) + ) + + addr_lanes = to_lanes(addr_all) + n_lanes = len(addr_lanes) or 1 + + # Per-record CAS substitutions are needed in cas_cmp/new/old. + cas_old_all: Any = None + cas_cmp_all: Any = None + cas_new_all: Any = None + if record.atomic_kind == "cas": + cas_old_all = apply_sub(record.old_value, sub) + cas_cmp_all = apply_sub(record.cas_cmp_value, sub) + cas_new_all = apply_sub(record.cas_new_value, sub) + + # local_constraints / premises are FLAT lists of globally applicable + # constraints (mask conditions, address-validity, loop iterators); they + # are NOT lane-indexed. Per-lane variation lives in record.active / + # record.reads / record.writes. + local_terms = tuple(as_bool(c) for c in iter_constraints(local_all)) + prem_terms = tuple(as_bool(c) for c in iter_constraints(prem_all)) + self.launch_premises.extend(prem_terms) + causal_terms = tuple(as_bool(c) for c in iter_constraints(causal_all)) + + out: list[SymbolicMemoryEvent] = [] + for lane, addr in enumerate(addr_lanes): + causal_inputs = ( + as_bool(lane_value(active_all, lane, n_lanes)), + *causal_terms, + ) + active = And( + as_bool(lane_value(active_all, lane, n_lanes)), + *local_terms, + *prem_terms, + ) + + rmw_operand: Any = None + if record.atomic_kind == "cas": + old = lane_value(cas_old_all, lane, n_lanes) + cmp_ = lane_value(cas_cmp_all, lane, n_lanes) + new = lane_value(cas_new_all, lane, n_lanes) + if old is None or cmp_ is None or new is None: + raise UnsupportedSymbolicRaceQuery( + "CAS record missing old_value / cas_cmp_value / cas_new_value" + ) + success = old == cmp_ + # Preserve the compare dependency in the write condition, + # without importing execution-domain premises into vdep. + causal_inputs += (success,) + reads = active + writes = And(active, success) + written = If(success, new, old) + old_value: Any = old + written_value: Any = written + elif record.is_atomic: + # AtomicRMW: always reads and always writes when active. + # Exception: the pre-exit representative of a CAS poll + # carries record-level statically-False writes (a FAILED + # CAS writes nothing) — honor it. + reads = active + writes = ( + BoolVal(False) + if (record.pre_exit and record.writes is False) + else active + ) + old_value = None + written_value = None + if record.old_value is not None: + # Value-modeled RMW: the observation symbol + # o_r lives in copy_local_vars, so `sub` already alpha- + # renamed it per copy; the write part is f_op(o_r, v). + old_value = lane_value( + apply_sub(record.old_value, sub), lane, n_lanes + ) + if record.rmw_operand is not None: + rmw_operand = lane_value( + apply_sub(record.rmw_operand, sub), lane, n_lanes + ) + written_value = _rmw_written_value( + record.rmw_op, old_value, rmw_operand + ) + else: + if record.reads is None: + read_cond: Any = record.access_mode == "read" + else: + read_cond = lane_value(apply_sub(record.reads, sub), lane, n_lanes) + if record.writes is None: + write_cond: Any = record.access_mode == "write" + else: + write_cond = lane_value( + apply_sub(record.writes, sub), lane, n_lanes + ) + reads = self._active_access_mode(active, as_bool(read_cond)) + writes = self._active_access_mode(active, as_bool(write_cond)) + old_value = None + written_value = None + + name = record.debug_name or f"e{record.event_id}" + if n_lanes > 1: + name = f"{name}.lane{lane}" + name = f"{name}.{ctx.label}" + + out.append( + SymbolicMemoryEvent( + idx=start_idx + len(out), + copy=ctx.label, + record=record, + name=name, + lane=lane, + event_id=record.event_id, + program_seq=record.program_seq, + pid=ctx.pid, + addr=addr, + elem_size=max(1, int(record.elem_size)), + active=active, + reads=reads, + writes=writes, + is_atomic=record.is_atomic, + atomic_kind=record.atomic_kind, + sem=record.sem, + scope=record.scope, + old_value=old_value, + written_value=written_value, + rmw_operand=rmw_operand, + causal_inputs=causal_inputs, + ) + ) + return out + + # ──────────────────────── Edges & HB closure ──────────────────────── + + def _fence_orders(self, e1: SymbolicMemoryEvent, e2: SymbolicMemoryEvent) -> bool: + """The caller's fence rule for two operations of one instance at + distinct known positions, asked in program order.""" + if self.fence_between is None: + return False + first, second = (e1, e2) if e1.program_seq < e2.program_seq else (e2, e1) + key = (id(first.record), id(second.record)) + cached = self._fence_cache.get(key) + if cached is None: + cached = self._fence_cache[key] = bool( + self.fence_between(first.record, second.record) + ) + return cached + + def _program_order( + self, e1: SymbolicMemoryEvent, e2: SymbolicMemoryEvent + ) -> BoolRef: + if e1.copy != e2.copy: + return BoolVal(False) + if e1.program_seq < 0 or e2.program_seq < 0: + return BoolVal(False) + if e1.program_seq >= e2.program_seq: + return BoolVal(False) + if not self._fence_orders(e1, e2): + if (e1.event_id, e2.event_id) in self.dep_pairs: + # Dependency order: within one copy the two records share + # their position variables, so this is the same-position + # edge (cross-position pairs are the intra-instance + # query's business). + return And(e1.active, e2.active) + # Fence-ordered semantics: source order alone carries no + # happens-before between distinct operations of one instance. + return BoolVal(False) + return And(e1.active, e2.active) # active-gated + + @staticmethod + def _exact_atomic_addr(w: SymbolicMemoryEvent, r: SymbolicMemoryEvent) -> BoolRef: + """Same-location predicate for the VALUE-MODELED atomic machinery + (rf, coherence order). Membership is presence of an observation + symbol: CAS always has one, an RMW exactly when its value semantics + are modeled).""" + if not (w.is_atomic and r.is_atomic): + return BoolVal(False) + if w.old_value is None or r.old_value is None: + return BoolVal(False) + if w.elem_size != r.elem_size: + return BoolVal(False) + return w.addr == r.addr + + def _same_dynamic_op( + self, e: SymbolicMemoryEvent, f: SymbolicMemoryEvent + ) -> BoolRef: + """Predicate: the two events denote ONE dynamic operation — the + cross-copy alpha-twins of a record (same record, same lane) with + both copies pinned to the same block. The same-instance query pins + pids equal, so without this identification the coherence machinery + would demand two distinct order positions and two distinct rf + sources for what is a single real operation, making e.g. the + rank-0 winner's world structurally UNSAT (counterexample: + single-winner duplicate-lane WAW silently proved clean).""" + if e.record is not f.record or e.lane != f.lane or e.copy == f.copy: + return BoolVal(False) + pid_a, pid_b = self.ctx_a.pid, self.ctx_b.pid + return And(*[pid_a[i] == pid_b[i] for i in range(3)]) + + @staticmethod + def _scope_ok(w: SymbolicMemoryEvent, r: SymbolicMemoryEvent) -> BoolRef: + for scope in (w.scope, r.scope): + if scope not in (None, "cta", "gpu", "sys"): + # Never widen an unknown scope to device-wide moral + # strength; the capture normalizes and refuses first, + # this guards events arriving by other routes. + raise UnsupportedSymbolicRaceQuery( + f"unsupported memory scope {scope!r}" + ) + if w.scope == "cta" or r.scope == "cta": + return And( + w.pid[0] == r.pid[0], + w.pid[1] == r.pid[1], + w.pid[2] == r.pid[2], + ) + return BoolVal(True) + + def _synchronizes_with( + self, w: SymbolicMemoryEvent, r: SymbolicMemoryEvent + ) -> BoolRef: + """sw goes through READS-THROUGH, not bare rf: a release + write also synchronizes with an acquire read that reads the tail of + an RMW chain rooted at it. ``rf_unknown`` / ``rf_chain`` sources are + deliberately absent from reads_through — an unmodeled source must + never manufacture an hb edge.""" + rt = self.reads_through.get((w.idx, r.idx)) + if rt is None: + return BoolVal(False) + return And( + BoolVal(is_release_sem(w.sem)), + BoolVal(is_acquire_sem(r.sem)), + self._scope_ok(w, r), + rt, + ) + + def _edge(self, e1: SymbolicMemoryEvent, e2: SymbolicMemoryEvent) -> BoolRef: + if e1.idx == e2.idx: + return BoolVal(False) + # Without a reads-through source, sw is identically False. Avoid + # constructing Or(po, False) for every pair in a large capture. + if (e1.idx, e2.idx) not in self.reads_through: + return self._program_order(e1, e2) + return Or( + self._program_order(e1, e2), + self._synchronizes_with(e1, e2), + ) + + # ──────────────────────── Read-from / RF source choices ──────────────── + + def _can_be_rf_candidate( + self, w: SymbolicMemoryEvent, r: SymbolicMemoryEvent + ) -> bool: + if w.idx == r.idx: + return False + # A same-instance writer at or after the reader is no rf source. + if w.copy == r.copy and w.program_seq >= r.program_seq: + return False + return True + + # Cap on initial-source disjunction size. Above this, the solver falls + # back to rf_unknown (no synchronizes-with) — keeps formulas tractable. + _MAX_INITIAL_ATOMIC_ELEMENTS: int = 1024 + + @classmethod + def _initial_atomic_source(cls, r: SymbolicMemoryEvent) -> Any: + """Predicate that ``r`` reads the launch-time initial value. + + Supports scalar tensors and small contiguous flag arrays. For large or + non-contiguous tensors, returns ``None`` so the solver falls back to + ``rf_unknown`` without synchronizes-with. + """ + t = r.record.tensor + if t is None or r.old_value is None: + return None + # The value model is integer-only, so a float-valued flag must + # fall back to rf_unknown rather than be silently truncated — + # int(0.7) == 0 would let the modeled CAS succeed where the real one fails (or + # mask a real race behind a fabricated single-winner lock). + dtype = getattr(t, "dtype", None) + if dtype is not None and ( + bool(getattr(dtype, "is_floating_point", False)) + or bool(getattr(dtype, "is_complex", False)) + ): + return None + try: + numel = int(t.numel()) + if numel <= 0 or numel > cls._MAX_INITIAL_ATOMIC_ELEMENTS: + return None + if hasattr(t, "is_contiguous") and not bool(t.is_contiguous()): + return None + base = int(t.data_ptr()) + elem_size = ( + int(t.element_size()) if hasattr(t, "element_size") else r.elem_size + ) + elem_size = max(1, elem_size) + tensor_for_read = t.detach() if hasattr(t, "detach") else t + tensor_for_read = ( + tensor_for_read.cpu() + if hasattr(tensor_for_read, "cpu") + else tensor_for_read + ) + values = tensor_for_read.reshape(-1).tolist() + except Exception: + return None + + clauses = [] + for i, value in enumerate(values): + # bool is an int subclass; anything else (a duck-typed tensor + # without a dtype attribute yielding floats) must not be + # truncated — fall back to rf_unknown. + if not isinstance(value, int): + return None + clauses.append( + And( + r.addr == IntVal(base + i * elem_size), + r.old_value == IntVal(int(value)), + ) + ) + + if not clauses: + return None + if len(clauses) == 1: + return clauses[0] + return Or(*clauses) + + def _template_solver(self) -> Solver: + """A solver holding only the template bounds (grid + arange) — used + for guard checks that must stay CONSERVATIVE (fewer assumptions → + more guard failures → axioms omitted, never fabricated).""" + solver = self._solver() + solver.add(self.grid_constraints) + for c in self.arange_constraints_a: + solver.add(c) + for c in self.arange_constraints_b: + solver.add(c) + return solver + + def _has_unmodeled_overlapping_writer(self, r: SymbolicMemoryEvent) -> bool: + """True when a write the rf model does not include — a plain store, + or an atomic whose WRITTEN VALUE is not modeled (float RMW, + non-identity bitwise RMW, unsigned umax/umin) — can overlap the + location ``r`` reads. + + Such a writer can publish a value the closed-world choice set + excludes; without an escape hatch the reader's ``old_value`` would be + over-constrained and every conflict gated on it silently vanishes + (e.g. a guard flag set via an unmodeled ``tl.atomic_xchg``). Overlap + is decided by Z3 on the symbolic addresses under grid/arange bounds + AND both events' activity (``e.writes`` / ``r.reads`` — masks, path + conditions, in-bounds premises): a writer only publishes a value + when it actually writes, and only reads that actually happen need a + source. Without the activity gate, an address expression drifting + arithmetically past its tensor under an unbounded symbolic grid + would open the escape for writers of a DIFFERENT tensor. Writers to + other tensors (distinct concrete bases) never weaken the closed + world. A VALUE-MODELED atomic is excluded from this set only to the + extent its overlap is COVERED by rf candidacy — exact address at + equal width (_exact_atomic_addr). A torn overlap (different widths, + or same width at a misaligned unequal address) can publish bytes + the rf model never delivers, so it must open the escape like any + unmodeled write (counterexample: an 8-byte modeled xchg over a + 4-byte reader was excluded from BOTH channels and pinned the reader + to the initial value — a false proof). + """ + # Pre-exit representatives are excluded (load-bearing: the + # identity-RMW rep's write half sits AT the awaited location and + # would otherwise open rf_unknown for its own poll, flipping clean + # producer-consumer baselines to false data races). Soundness of + # the exclusion: an identity write-back republishes only a value + # some other write already put there; if that value's writer is + # weak, THAT writer opens the escape itself. The CAS-poll and + # plain-load reps are excluded by the feasibility check anyway + # (their writes are statically False). + candidates = [ + e + for e in self.events + if ((not e.is_atomic and e.record.access_mode == "write") or e.is_atomic) + and e.idx != r.idx + and not e.record.pre_exit + and self._can_be_rf_candidate(e, r) + ] + if not candidates: + return False + solver = self._template_solver() + solver.add(r.reads) + for e in candidates: + solver.push() + solver.add(e.writes) + solver.add(self._byte_overlap(e, r)) + if e.is_atomic and e.written_value is not None: + # An ADD write's modeled value old+v is unbounded-Int + # arithmetic, but the machine wraps: unless the record + # carries the counting certificate (guard (f) bounded every + # reachable value inside the dtype range) or provably adds + # zero, the published value may be one the model cannot + # express — treat the write as unmodeled (counterexample: + # an INT32_MAX counter's wrap-gated store was proved dead + # through the closed-world value chain). + # max/min never leave the operands' range and xchg/CAS + # write user values, so only `add` is wrap-capable. + wrap_capable = ( + (e.record.rmw_op or "") == "add" + and _as_numeral(e.rmw_operand) != 0 + and id(e.record) not in self._counting + ) + if not wrap_capable and e.elem_size == r.elem_size: + # rf covers exactly the equal-width same-address + # overlap; only the residual TORN overlap counts as + # unmodeled. (Width mismatch: no rf edge exists at all + # — any overlap is uncovered.) + solver.add(e.addr != r.addr) + # Z3 ``unknown`` must open the escape: keeping the closed world + # on an undecided overlap would over-constrain the reader's old + # value and silently hide every conflict gated on it. + feasible = solver.check() != unsat + solver.pop() + if feasible: + return True + return False + + def _build_read_from_choices(self) -> None: + # Closed-world atomic source model. + # If the initial scalar source is identifiable, source choices are + # closed over: (initial source) + (value-modeled atomic writers — + # CAS and modeled RMW write parts incl. identity or/xor-of-zero). + # If the initial source is not identifiable — or an UNMODELED write + # (plain store, float RMW, non-identity bitwise RMW) can overlap the + # location, publishing a value the closed world does not contain — + # rf_unknown is introduced and does NOT enable synchronizes-with. + # This is intentionally NOT a + # full coherence/read-from model over all program instances; the + # guarded acq_rel CAS no-race result depends on this closed-world + # assumption holding whenever the flag is only ever written by + # modeled atomics. For a COUNTED record the closed world is + # widened by rf_chain: the reader may take its value from an + # unmodeled grid instance at rank-1 (the counting equations already + # pin the value), so real races at non-adjacent ranks are not + # squeezed out. rf_chain never enables synchronizes-with either — + # the counted sw edge rides on coherence order via reads_through. + modeled_writers = [ + e for e in self.events if e.is_atomic and e.written_value is not None + ] + for r in self.events: + if not r.is_atomic or r.old_value is None: + continue + choices: list[BoolRef] = [] + init_pred = self._initial_atomic_source(r) + + if init_pred is not None: + rf_init = Bool(f"rf_init_{r.idx}") + self.rf_init_source[r.idx] = rf_init + choices.append(rf_init) + self.rf_constraints.append(Implies(rf_init, And(r.reads, init_pred))) + if init_pred is None or self._has_unmodeled_overlapping_writer(r): + rf_unknown = Bool(f"rf_unknown_{r.idx}") + self.rf_unknown_source[r.idx] = rf_unknown + choices.append(rf_unknown) + self.rf_constraints.append(Implies(rf_unknown, r.reads)) + + counting = self._counting.get(id(r.record)) + if counting is not None: + rank_r = counting.rank_a if r.copy == "a" else counting.rank_b + rf_chain = Bool(f"rf_chain_{r.idx}") + self.rf_chain_source[r.idx] = rf_chain + choices.append(rf_chain) + # Source = the unmodeled instance at rank-1; rank >= 1 or + # the only source with the matching value is the initial + # one, which rf_init already covers. + self.rf_constraints.append(Implies(rf_chain, And(r.reads, rank_r >= 1))) + + for w in modeled_writers: + if not self._can_be_rf_candidate(w, r): + continue + rf = Bool(f"rf_{w.idx}_to_{r.idx}") + choices.append(rf) + self.rf_source[(w.idx, r.idx)] = rf + self.rf_constraints.append( + Implies( + rf, + modeled_atomic_read_from( + w, r, same_atomic_addr_fn=self._exact_atomic_addr + ), + ) + ) + + if choices: + self.rf_constraints.append(Implies(r.reads, Or(*choices))) + self.rf_constraints.append( + Implies(Not(r.reads), And(*(Not(c) for c in choices))) + ) + if len(choices) > 1: + self.rf_constraints.append(AtMost(*choices, 1)) + + # ──────────────────────── Conflict / race query ──────────────────────── + + @staticmethod + def _byte_overlap(a: SymbolicMemoryEvent, b: SymbolicMemoryEvent) -> BoolRef: + if a.elem_size == 1 and b.elem_size == 1: + return a.addr == b.addr + return And( + a.addr < b.addr + b.elem_size, + b.addr < a.addr + a.elem_size, + ) + + def _conflict(self, a: SymbolicMemoryEvent, b: SymbolicMemoryEvent) -> BoolRef: + mode_a = self._ordinary_access_mode(a) + mode_b = self._ordinary_access_mode(b) + if mode_a is not None and mode_b is not None: + if not (mode_a or mode_b): + return BoolVal(False) + # Lowering already includes activity in the ordinary read/write + # mode. Under the two activity guards the mode predicate is True. + return And(a.active, b.active, self._byte_overlap(a, b)) + return And( + a.active, + b.active, + self._byte_overlap(a, b), + conflicting_access_modes(a, b), + ) + + @staticmethod + def _ordinary_access_mode(event: SymbolicMemoryEvent) -> bool | None: + """Recognize exact lowered plain modes, without assuming an op's kind. + + Identity with the immutable activity expression is sufficient; unknown + or conditional modes and atomics retain the general conflict formula. + """ + if event.is_atomic: + return None + if event.writes is event.active and is_false(event.reads): + return True + if event.reads is event.active and is_false(event.writes): + return False + return None + + def _race_expr(self, a: SymbolicMemoryEvent, b: SymbolicMemoryEvent) -> BoolRef: + forward, reverse = self.hb[a.idx][b.idx], self.hb[b.idx][a.idx] + if is_true(forward) or is_true(reverse): + return BoolVal(False) + terms = [self._conflict(a, b)] + if not is_false(forward): + terms.append(Not(forward)) + if not is_false(reverse): + terms.append(Not(reverse)) + return terms[0] if len(terms) == 1 else And(*terms) + + # ──────────────────── modeled-atomic coherence ──────────────────── + + def _modeled_atomic_events(self) -> list[SymbolicMemoryEvent]: + """Events in the per-location atomic order: every VALUE-MODELED + atomic — CAS always, RMW exactly when its observation is modeled.""" + return [e for e in self.events if e.is_atomic and e.old_value is not None] + + def _make_atomic_order_vars(self) -> dict[int, Any]: + """One symbolic atomic-order position per value-modeled atomic. + + The variable denotes the position of the WHOLE operation in the + per-location atomic order — the read and the write part share it, + which is what makes RMW atomicity/immediacy + structural: no write can sit between an RMW's read and its write + because they occupy one position, and the rf constraints below + forbid a writer strictly between the source and the reader. + """ + return { + e.idx: Int(f"atomic_order_{e.idx}") + for e in self.events + if e.is_atomic and e.old_value is not None + } + + def _build_atomic_coherence_constraints(self) -> None: + """Closed-world atomic coherence for the two modeled program copies. + + Without these constraints, two CAS try-locks at the same flag could + both read the initial value and both succeed — producing a false WAW + on guarded stores; likewise two modeled RMWs could both observe the + initial counter. The coherence model (over value-modeled atomics): + + * Active actions get bounded atomic-order positions. + * Same-address active actions are distinct in the per-location + order. + * Same-copy program order is preserved for same-address actions. + * If a reader reads the initial source, no modeled successful + writer at the same address may precede it. + * If r reads from modeled writer w, w must be before r in the order + and no modeled same-address successful writer may sit between + them — with the shared read/write position this is exactly the + RMW immediacy axiom: what makes two successful lock + acquisitions of the same "0" unsatisfiable. + + This is not a full GPU memory model, but it suffices to suppress the + most obvious unsoundness around atomic synchronization patterns. + """ + atomic_events = self._modeled_atomic_events() + if not atomic_events: + return + + n_orders = max(1, len(atomic_events)) + cons = self.atomic_coherence_constraints + + for e in atomic_events: + ord_e = self.atomic_order[e.idx] + cons.append(Implies(e.reads, And(ord_e >= 0, ord_e < n_orders))) + + for i, e in enumerate(atomic_events): + for f in atomic_events[i + 1 :]: + same_addr = self._exact_atomic_addr(e, f) + both_active_same_addr = And(e.reads, f.reads, same_addr) + ord_e = self.atomic_order[e.idx] + ord_f = self.atomic_order[f.idx] + + # Distinct positions apply to distinct dynamic operations; + # a record's cross-copy twins under pinned-equal pids are + # ONE operation and share the position instead. + same_op = self._same_dynamic_op(e, f) + cons.append( + Implies(And(both_active_same_addr, Not(same_op)), ord_e != ord_f) + ) + cons.append(Implies(same_op, ord_e == ord_f)) + + if e.copy == f.copy and e.program_seq >= 0 and f.program_seq >= 0: + if e.program_seq < f.program_seq: + cons.append(Implies(both_active_same_addr, ord_e < ord_f)) + elif f.program_seq < e.program_seq: + cons.append(Implies(both_active_same_addr, ord_f < ord_e)) + + # rf_init: no modeled successful writer at the same address may + # precede the reader in the per-location order. The reader's own + # cross-copy twin (same dynamic op when pids coincide) is not a + # DISTINCT writer and must not block rf_init. + for r in atomic_events: + rf_init = self.rf_init_source.get(r.idx) + if rf_init is None: + continue + ord_r = self.atomic_order[r.idx] + for w in atomic_events: + if w.idx == r.idx: + continue + ord_w = self.atomic_order[w.idx] + cons.append( + Implies( + And( + rf_init, + w.writes, + self._exact_atomic_addr(w, r), + Not(self._same_dynamic_op(w, r)), + ), + ord_r < ord_w, + ) + ) + + # rf from modeled writer w to reader r: w precedes r and no modeled + # same-address successful writer sits strictly between w and r + # (immediacy — the reader's write part shares its position). + # Twins of w or r (same dynamic op) share the endpoints' positions + # and are not "between". + for r in atomic_events: + ord_r = self.atomic_order[r.idx] + for w in atomic_events: + rf = self.rf_source.get((w.idx, r.idx)) + if rf is None: + continue + ord_w = self.atomic_order[w.idx] + cons.append(Implies(rf, ord_w < ord_r)) + # An operation never reads-from itself: forbid the rf edge + # between cross-copy twins when they denote one op. + cons.append(Implies(rf, Not(self._same_dynamic_op(w, r)))) + + for v in atomic_events: + if v.idx in (w.idx, r.idx): + continue + ord_v = self.atomic_order[v.idx] + cons.append( + Implies( + And( + rf, + v.writes, + self._exact_atomic_addr(v, r), + Not(self._same_dynamic_op(v, r)), + Not(self._same_dynamic_op(v, w)), + ), + Or(ord_v < ord_w, ord_r < ord_v), + ) + ) + + def _build_coherence_hb_constraints(self) -> None: + """Coherence hb-consistency axiom (co-hb): hb-ordered distinct + same-location value-modeled atomics take increasing per-location + positions. This extends co-po's antecedent from same-copy program + order to the full hb closure; co-po stays asserted on its own, + since program order between unfenced operations is no hb edge. + Without it, a relaxed atomic read that + is hb-after a same-location write can still source the initial + value (the message-passing counterexample). Together with the + no-intervening-writer clauses of rf/rf_init, the four C++ + coherence shapes (write-write, read-write, write-read, read-read) + follow. Gating mirrors co-po (activity via ``reads``, location via + the exact-atomic-address predicate); cross-copy twins under + pinned-equal pids denote ONE operation sharing a position and are + exempt, as in the uniqueness clause.""" + atomic_events = self._modeled_atomic_events() + cons = self.atomic_coherence_constraints + for e in atomic_events: + ord_e = self.atomic_order[e.idx] + for f in atomic_events: + if f.idx == e.idx: + continue + if e.copy == f.copy and 0 <= e.program_seq < f.program_seq: + continue # co-po already asserts this pair without the hb antecedent + cons.append( + Implies( + And( + self.hb[e.idx][f.idx], + e.reads, + f.reads, + self._exact_atomic_addr(e, f), + Not(self._same_dynamic_op(e, f)), + ), + ord_e < self.atomic_order[f.idx], + ) + ) + + # ──────────────────── value causality (wf-vc) ──────────────────── + + def _build_value_causality_constraints(self) -> None: + """wf-vc: value-causality axiom (no out-of-thin-air values). + + Rationale (PTX causality / Tile-IR no-thin-air): the hardware + memory model never lets a relaxed atomic load observe a value whose + only justification is a write that itself depends on that very + observation — two relaxed reads each observing the value the other + thread's dependent write produced is forbidden even without any + acquire/release ordering. Formally the model requires rf ∪ vdep to + be acyclic, where vdep(r, e) holds when read r's observation + reaches event e's written value, operand, activity, or address. + + Encoding: every value-modeled atomic event e (the per-location + atomic-order membership set) gets a PAIR of fresh Int causality + ranks vc_r(e) <= vc_w(e) — value flows read-to-write within one + operation, which also orders an identity write-back after its own + observation. Two edge families then rule the cycles out: + + * rf edge: for each MODELED-writer selector rf(w, r), assert + rf(w, r) -> vc_w(w) < vc_r(r): a read's value exists only + after its source write produced it. rf_init / rf_unknown / + rf_chain sources get NO edge — a reader sourced there has an + unconstrained vc_r and roots the graph, so cycles through the + initial value, the open world, or the counted chain are NOT + excluded (conservative: those values may be justified outside + the two modeled copies). + * static vdep edge: if r's observation symbol occurs in another + value-modeled event e's written value or RMW operand (a CAS's + cmp/new terms live inside its written_value If-term), assert + vc_r(r) < vc_w(e); if it occurs in e's activity (reads/writes + conditions) or address, assert vc_r(r) < vc_r(e) — the value + is needed before e's read part can even issue. + + Operational conditions are preserved separately from the lowered + reads/writes predicates. Those predicates also contain global + execution premises (including every await's exit condition) and + source-domain restrictions, which are not value dependencies. + Scanning them would invent reciprocal dependencies between two + independent awaits and make even the bare base inconsistent. + Frontends distinguish actual loop/mask control from domain facts; + records without causal_constraints use local_constraints/premises + as operational conditions, including interpreter loop-control + premises. + + Gating: genuine static vdep edges remain UNCONDITIONAL. Captured + operational expressions refer to earlier observations within one + copy, and alpha-renaming separates the copies. Global termination + conditions do not meet that ordering argument and are excluded + from dependency extraction, while remaining in event activity and + the independent feasibility check. Cycle-closing rf edges remain + activity-gated through their selectors. A preceding await's exit + is a genuine control dependency of later operations: these explicit + edges require both same-copy endpoints to execute, so mutually + exclusive branches do not constrain each other's causality ranks. + + Occurrence is checked on GENUINE observation symbols only: the keys + of r.old_value intersected with the copy-local rename targets (the + observation vars live in copy_local_vars, like the CAS return). + Anything that leaks other vars into old_value yields an empty key + set and simply drops the vdep edge — the over-report direction. + + Plain stores and non-value-modeled atomics carry no ranks: a + causality cycle through them would need an rf edge FROM them, which + the closed world never provides (they open the rf_unknown escape + instead), so their omission is conservative. + """ + atomic_events = self._modeled_atomic_events() + if not atomic_events: + return + cons = self.value_causality_constraints + for e in atomic_events: + self.vc_read_rank[e.idx] = Int(f"vc_r_{e.idx}") + self.vc_write_rank[e.idx] = Int(f"vc_w_{e.idx}") + cons.append(self.vc_read_rank[e.idx] <= self.vc_write_rank[e.idx]) + + # rf edges: modeled-writer selectors only (never rf_init / + # rf_unknown / rf_chain — those readers root the graph). + for (w_idx, r_idx), rf in self.rf_source.items(): + cons.append( + Implies(rf, self.vc_write_rank[w_idx] < self.vc_read_rank[r_idx]) + ) + + # Static vdep edges, by observation-symbol occurrence. + copy_local_targets = { + _z3_var_key(var) + for subs in ( + self.ctx_a.copy_local_substitutions, + self.ctx_b.copy_local_substitutions, + ) + for (_, var) in subs + } + for r in atomic_events: + obs_keys = _collect_z3_var_keys((r.old_value,)) & copy_local_targets + if not obs_keys: + continue + exit_sources = ( + [ + source + for source in atomic_events + if source.copy == r.copy + and source.event_id in r.record.await_observations + ] + if r.record.await_observations + else [r] + ) + for e in atomic_events: + if e.idx == r.idx: + continue + if obs_keys & _collect_z3_var_keys((e.written_value, e.rmw_operand)): + cons.append(self.vc_read_rank[r.idx] < self.vc_write_rank[e.idx]) + if obs_keys & _collect_z3_var_keys((e.causal_inputs, e.addr)): + cons.append(self.vc_read_rank[r.idx] < self.vc_read_rank[e.idx]) + # Exiting a preceding await controls later operations, but a + # poll in another branch does not. The encoder supplies + # source-earlier candidates; both same-copy path/activity + # predicates decide whether that control edge actually exists. + if r.copy == e.copy and r.event_id in e.record.await_dependencies: + # An exit may compare the poll with another read's value. + # Both are control inputs; retaining only the poll would + # allow an expected value to come from a future publication. + for source in exit_sources: + cons.append( + Implies( + And(r.reads, e.reads, source.reads), + self.vc_read_rank[source.idx] + < self.vc_read_rank[e.idx], + ) + ) + + # ──────────────────── counting axiom ──────────────────── + + def _build_counting_axioms(self) -> dict[int, _CountingInfo]: + """Per-copy rank variables for each RMW record whose guards hold. + + Guards, all checked on the TEMPLATE (Z3 ``unknown`` fails a guard — + the axiom is then OMITTED, never approximated): + (a) the record is a value-modeled ``add`` RMW with exactly one + lane per copy, and its address simplifies to ONE numeral in + both copies (a fixed scalar location L); + (b) its activity is provably true for every instance; + (c) the increment is a constant c > 0; + (d) L's initial value is known via the rf-init machinery's own + side conditions; + (e) no OTHER event's write part can overlap L (which also keeps + the rf_unknown escape closed for the counted readers). + The grid-size product must stay linear: at most one symbolic dim. + + Justification of the emitted constraints: under (a)-(e) every write + to L is an instance of this one always-active RMW, so the + per-location coherence order is exactly the arrival order; the k-th + arriver observes init + c·k (induction over the chain, using + atomicity/immediacy), distinct instances have distinct ranks, and + coherence order agrees with rank order. Consequences the solver + derives for free: distinct observations across blocks (work-queue + disjointness) and "o = init + c·(|G|-1) forces coherence-after- + everyone" (last-block-done). + """ + out: dict[int, _CountingInfo] = {} + by_record: dict[int, list[SymbolicMemoryEvent]] = {} + for e in self.events: + if e.is_atomic and e.atomic_kind == "rmw" and e.old_value is not None: + by_record.setdefault(id(e.record), []).append(e) + if not by_record: + return out + # |G| must stay linear (rank < g0·g1·g2): >1 symbolic dim is + # Z3-unknown bait, so the axiom is omitted for such grids. + if sum(1 for d in self.grid if _is_symbolic_dim(d)) > 1: + return out + grid_size = self.grid[0] * self.grid[1] * self.grid[2] + + for rec_key, evts in by_record.items(): + if len(evts) != 2: + continue # multi-lane record (or a missing copy) + e_a = next((e for e in evts if e.copy == "a"), None) + e_b = next((e for e in evts if e.copy == "b"), None) + if e_a is None or e_b is None: + continue + if (e_a.record.rmw_op or "") != "add": + continue + info = self._counting_guards(e_a, e_b, grid_size) + if info is not None: + out[rec_key] = info + return out + + def _counting_guards( + self, + e_a: SymbolicMemoryEvent, + e_b: SymbolicMemoryEvent, + grid_size: Any, + ) -> _CountingInfo | None: + # (a) fixed scalar location: both copies' addresses are the SAME + # numeral (no pid/arange/copy-local dependence survives simplify). + loc = _as_numeral(e_a.addr) + if loc is None or _as_numeral(e_b.addr) != loc: + return None + # (c) constant increment > 0, identical in both copies. + inc = _as_numeral(e_a.rmw_operand) + if inc is None or inc <= 0 or _as_numeral(e_b.rmw_operand) != inc: + return None + # (b) activity provably true for every instance of the grid. + solver = self._template_solver() + for e in (e_a, e_b): + solver.push() + solver.add(Not(e.active)) + always_active = solver.check() == unsat + solver.pop() + if not always_active: + return None + # (d) known initial value, via the rf-init machinery's own side + # conditions (so rf_init is guaranteed to exist as a choice). + if self._initial_atomic_source(e_a) is None: + return None + init = self._initial_value_at(e_a, loc) + if init is None: + return None + # (f) no machine-integer wraparound on any LAUNCHABLE grid: the + # value model is unbounded-Int, so pinning o = init + c·rank is + # sound only while the largest reachable observation stays inside + # the element type's signed range (counterexample: an + # INT32_MAX-initialized counter really wraps on hardware while the + # model proved its wrap-gated store dead). Symbolic dims are + # bounded by the CUDA launch caps (2^31-1 on x, 65535 on y/z) — + # no real launch exceeds them, so certifying up to the cap + # certifies every execution the claim covers. + elem = max(1, e_a.elem_size) + max_g = 1 + caps = (2**31 - 1, 65535, 65535) + for axis, d in enumerate(self.grid): + max_g *= caps[axis] if _is_symbolic_dim(d) else max(1, int(d)) + signed_max = (1 << (8 * elem - 1)) - 1 + # The largest reachable value is the LAST WRITE, init + inc·|G| + # (the last observation plus one increment) — the certificate must + # cover it, since it is what the escape hatch trusts to stay + # representable. + if init + inc * max_g > signed_max: + if any(_is_symbolic_dim(d) for d in self.grid): + self._counting_grid_restricted.add(id(e_a.record)) + return None + # (e) no other event's write part can overlap [L, L+elem). The + # check runs under the axiom's own PROVISIONAL observation bounds + # (init <= o <= init + c·(|G|-1)) — sound by first-violation + # induction over L's coherence order: before the first foreign + # write, every observation is a bounded chain value, so a foreign + # write whose address needs an out-of-bound o cannot be first + # (work-queue stores addressed by the observation would otherwise + # alias everything and kill the axiom that pins them). + own = {e_a.idx, e_b.idx} + lo = IntVal(init) + hi = IntVal(init) + IntVal(inc) * (grid_size - 1) + for e in self.events: + if e.idx in own: + continue + if not e.is_atomic and e.record.access_mode != "write": + continue + solver.push() + for o in (e_a.old_value, e_b.old_value): + solver.add(o >= lo, o <= hi) + solver.add(e.writes) + solver.add(e.addr < IntVal(loc + elem)) + solver.add(IntVal(loc) < e.addr + e.elem_size) + overlap_possible = solver.check() != unsat + solver.pop() + if overlap_possible: + return None + + rank_a = Int(f"rmw_rank_{e_a.idx}_a") + rank_b = Int(f"rmw_rank_{e_b.idx}_b") + pid_a, pid_b = self.ctx_a.pid, self.ctx_b.pid + same_block = And(*[pid_a[i] == pid_b[i] for i in range(3)]) + ord_a = self.atomic_order[e_a.idx] + ord_b = self.atomic_order[e_b.idx] + cons = self.counting_constraints + cons.append(And(rank_a >= 0, rank_a < grid_size)) + cons.append(And(rank_b >= 0, rank_b < grid_size)) + # rank is the instance's position in L's coherence order: equal iff + # the two copies denote the same block. + cons.append(same_block == (rank_a == rank_b)) + cons.append(e_a.old_value == IntVal(init) + IntVal(inc) * rank_a) + cons.append(e_b.old_value == IntVal(init) + IntVal(inc) * rank_b) + cons.append((ord_b < ord_a) == (rank_b < rank_a)) + return _CountingInfo( + idx_a=e_a.idx, + idx_b=e_b.idx, + rank_a=rank_a, + rank_b=rank_b, + init=init, + inc=inc, + loc=loc, + ) + + @classmethod + def _initial_value_at(cls, r: SymbolicMemoryEvent, loc: int) -> int | None: + """The launch-time integer value stored at byte address ``loc`` in + the reader's tensor, under the same side conditions as + ``_initial_atomic_source`` (integer contents, aligned, in range).""" + t = r.record.tensor + if t is None: + return None + try: + base = int(t.data_ptr()) + elem = max( + 1, int(t.element_size()) if hasattr(t, "element_size") else r.elem_size + ) + off = loc - base + if off < 0 or off % elem != 0: + return None + idx = off // elem + if idx >= int(t.numel()): + return None + tensor_for_read = t.detach() if hasattr(t, "detach") else t + tensor_for_read = ( + tensor_for_read.cpu() + if hasattr(tensor_for_read, "cpu") + else tensor_for_read + ) + value = tensor_for_read.reshape(-1).tolist()[idx] + except Exception: + return None + if not isinstance(value, int): # bool is an int subclass; floats fail + return None + return int(value) + + # ──────────────────── reads-through ──────────────────── + + def _build_reads_through(self) -> dict[tuple[int, int], BoolRef]: + """rt(w, r): r reads-through w — directly (rf), via a bounded chain + of value-modeled RMW write parts (each link an rf edge, so each + intermediate's write part is implied active), or — for a counted + record — via coherence order between its two copies (justified in + ``_build_counting_axioms``: every write to the counted location is a + link of the same RMW chain). Chain length over MODELED events is + bounded by their count; chains through unmodeled grid instances are + exactly what the counting pairs cover. + + Every rf hop of a chain must be morally strong (PTX observation + order recurses over ``morally_strong ∩ rf``; scoped-RC11 release + sequences use ``incl ∩ rf`` at every relay), so each link — the + seed rf included — conjoins ``_scope_ok`` of ITS OWN endpoints. + Ordering stays endpoint-only: interior relays may be relaxed. A + scope-incompatible interior hop breaks the chain even when the + chain's two endpoints are mutually inclusive (counterexample: + a cta-scoped relay CAS in another block let a release publish + through it, certifying a PTX-racy launch race-free). A counted + record's chain runs through unmodeled ranks of its one textual + operation, so a ``cta``-scoped counted record cannot guarantee + per-hop inclusion across ranks and contributes no chain edge. + """ + by_idx = {e.idx: e for e in self.events} + rt: dict[tuple[int, int], BoolRef] = { + (w_idx, r_idx): And(rf, self._scope_ok(by_idx[w_idx], by_idx[r_idx])) + for (w_idx, r_idx), rf in self.rf_source.items() + } + n_modeled = len(self._modeled_atomic_events()) + frontier: dict[tuple[int, int], BoolRef] = dict(rt) + for _ in range(max(0, n_modeled - 1)): + grown: dict[tuple[int, int], BoolRef] = {} + for (w_idx, m_idx), pred in frontier.items(): + for (m2_idx, r_idx), rf2 in self.rf_source.items(): + if m2_idx != m_idx or r_idx == w_idx: + continue + step = And( + pred, + rf2, + self._scope_ok(by_idx[m2_idx], by_idx[r_idx]), + ) + key = (w_idx, r_idx) + grown[key] = Or(grown[key], step) if key in grown else step + if not grown: + break + for key, pred in grown.items(): + rt[key] = Or(rt[key], pred) if key in rt else pred + frontier = grown + for info in self._counting.values(): + if by_idx[info.idx_a].scope == "cta": + continue + ord_a = self.atomic_order[info.idx_a] + ord_b = self.atomic_order[info.idx_b] + for w_idx, r_idx, before in ( + (info.idx_b, info.idx_a, ord_b < ord_a), + (info.idx_a, info.idx_b, ord_a < ord_b), + ): + key = (w_idx, r_idx) + rt[key] = Or(rt[key], before) if key in rt else before + return rt + + def _assert_no_uncounted_observation_addresses(self) -> None: + """An observation variable may feed an ADDRESS only when its + record's counting axiom fired (the address is then affine in the + pinned rank — the work-queue pattern). Anything else raises: an unconstrained + observation in an address would alias everything, and silently + widening is the forbidden failure mode — unsupported is the honest + verdict.""" + counted: set[int] = set() + for info in self._counting.values(): + counted.update((info.idx_a, info.idx_b)) + obs_keys: dict[tuple[int, str, str], SymbolicMemoryEvent] = {} + for e in self._modeled_atomic_events(): + if e.idx in counted: + continue + for key in _collect_z3_var_keys((e.old_value,)): + obs_keys[key] = e + if not obs_keys: + return + for e in self.events: + hit = _collect_z3_var_keys((e.addr,)) & set(obs_keys) + if hit: + src = obs_keys[next(iter(hit))] + error = ( + CountingScopeUnsupported + if id(src.record) in self._counting_grid_restricted + else UnsupportedSymbolicRaceQuery + ) + raise error( + f"the observation of atomic {src.name} feeds the address " + f"of {e.name}, and the counting axiom's guards do not " + "hold for it — an atomic return in address position is " + "only modeled under the counting axiom" + ) + + def _base_constraint_conjunction(self) -> BoolRef | None: + """Reuse immutable assertions, with snapshots of every mutable source. + + Constraint lists and the HB matrix are public and may be changed in + place. Checking their actual elements costs only Python work on a + cache hit; no Boolean coercion or Z3 construction is repeated. The + cache is first populated at query time, after co-hb has been built. + """ + containers = ( + self.arange_constraints_a, + self.arange_constraints_b, + self.rf_constraints, + self.atomic_coherence_constraints, + self.counting_constraints, + self.value_causality_constraints, + self.extra_assumptions, + ) + # Do not consume a one-shot iterable before the original add path. + if not all(isinstance(source, (list, tuple)) for source in containers): + self._base_constraint_cache = None + return None + families = ( + (self.grid_constraints,), + tuple(self.arange_constraints_a), + tuple(self.arange_constraints_b), + tuple(self.rf_constraints), + tuple(self.atomic_coherence_constraints), + tuple(self.counting_constraints), + tuple(self.value_causality_constraints), + tuple(self.extra_assumptions), + ) + rows = tuple(self.hb[i] for i in range(len(self.events))) + diagonal = tuple(row[i] for i, row in enumerate(rows)) + sources = ( + self.grid_constraints, + self.arange_constraints_a, + self.arange_constraints_b, + self.rf_constraints, + self.atomic_coherence_constraints, + self.counting_constraints, + self.value_causality_constraints, + self.extra_assumptions, + self.events, + self.hb, + *rows, + ) + snapshot = (sources, *families, diagonal) + cached = getattr(self, "_base_constraint_cache", None) + if cached is not None and all( + len(current) == len(previous) + and all(a is b for a, b in zip(current, previous)) + for current, previous in zip(snapshot, cached.snapshot) + ): + return cached.expression + + self._base_constraint_cache = None + # Solver.add also accepts nested containers and custom coercible + # values. Their contents may change without changing object identity; + # retain the original add path for those nonstandard inputs. + if ( + not all( + isinstance(c, BoolRef) or type(c) is bool # noqa: E721 (only immutable builtin scalars) + for family in families[:-1] + for c in family + ) + or not all( + isinstance(c, ExprRef) or type(c) in (bool, int, float) + for c in families[-1] + ) + or not all( + isinstance(c, BoolRef) or type(c) is bool # noqa: E721 (immutable builtin scalars) + for c in diagonal + ) + ): + return None + + constraints = [c for family in families[:-1] for c in family] + constraints.extend(as_bool(c) for c in families[-1]) + # Only syntactic False diagonals can be omitted: a True or + # conditional cycle must still exclude its valuation from executions. + constraints.extend(Not(c) for c in diagonal if not is_false(c)) + expression = And(*constraints) + self._base_constraint_cache = _BaseConstraintCache(snapshot, expression) + return expression + + def _base_solver(self) -> Solver: + """Assertions shared by every race query; the caller adds the + cross-instance (``different_blocks``) or same-instance constraints. + """ + solver = self._solver() + conjunction = self._base_constraint_conjunction() + if conjunction is not None: + solver.add(conjunction) + return solver + solver.add(self.grid_constraints) + for c in self.arange_constraints_a: + solver.add(c) + for c in self.arange_constraints_b: + solver.add(c) + for c in self.rf_constraints: + solver.add(c) + for c in self.atomic_coherence_constraints: + solver.add(c) + for c in self.counting_constraints: + solver.add(c) + for c in self.value_causality_constraints: + solver.add(c) + for c in self.extra_assumptions: + solver.add(as_bool(c)) + # HB irreflexivity: H = TC(po ∪ sw) must be acyclic in any valuation + # that models an execution; without Not(H[i][i]) the solver may + # witness race queries with cyclic po ∪ sw valuations. + for i in range(len(self.events)): + solver.add(Not(self.hb[i][i])) + return solver + + def _solver(self) -> Solver: + """A fresh Z3 solver with this solver's per-query budget.""" + solver = Solver() + solver.set(timeout=self.timeout_ms) + return solver + + def _new_solver(self) -> Solver: + solver = self._base_solver() + solver.add(self.different_blocks) + return solver + + # ──────────────────────── Reports ──────────────────────── + + @staticmethod + def _canonical_pair( + a: SymbolicMemoryEvent, b: SymbolicMemoryEvent + ) -> tuple[SymbolicMemoryEvent, SymbolicMemoryEvent]: + if (a.event_id, a.lane) <= (b.event_id, b.lane): + return a, b + return b, a + + def _dedupe_reports( + self, + candidates: list[ + tuple[SymbolicMemoryEvent, SymbolicMemoryEvent, ModelRef, str] + ], + ) -> list[RaceReport]: + seen: set[tuple[tuple[int, int], tuple[int, int]]] = set() + reports: list[RaceReport] = [] + for a, b, model, reason in candidates: + first, second = self._canonical_pair(a, b) + key = ( + (first.event_id, first.lane), + (second.event_id, second.lane), + ) + if key in seen: + continue + seen.add(key) + reports.append(self._make_report(first, second, model, reason)) + return reports + + def _make_report( + self, + first: SymbolicMemoryEvent, + second: SymbolicMemoryEvent, + model: ModelRef, + reason: str, + ) -> RaceReport: + fw = bool(is_true(model.evaluate(first.writes, model_completion=True))) + sw = bool(is_true(model.evaluate(second.writes, model_completion=True))) + if fw and sw: + race_type: RaceType = RaceType.WAW + elif fw: + race_type = RaceType.RAW + else: + race_type = RaceType.WAR + + addr_a_val = model.evaluate(first.addr, model_completion=True).as_long() + addr_b_val = model.evaluate(second.addr, model_completion=True).as_long() + if first.elem_size > 1 or second.elem_size > 1: + witness_addr = max(addr_a_val, addr_b_val) + else: + witness_addr = addr_a_val + + witness_grid_a = tuple( + model.evaluate(first.pid[i], model_completion=True).as_long() + for i in range(3) + ) + witness_grid_b = tuple( + model.evaluate(second.pid[i], model_completion=True).as_long() + for i in range(3) + ) + + if reason == self._INTRA_INSTANCE_REASON: + positioned = ( + first.program_seq >= 0 + and second.program_seq >= 0 + and first.program_seq != second.program_seq + ) + reason = append_missing_fence_diagnostic( + reason, + same_instance=witness_grid_a == witness_grid_b, + distinct_operations=first.record is not second.record, + first_seq=first.program_seq, + second_seq=second.program_seq, + fenced=positioned and self._fence_orders(first, second), + first_site=first.record.source_location, + second_site=second.record.source_location, + first_mode="write" if fw else "read", + second_mode="write" if sw else "read", + pre_exit=first.record.pre_exit or second.record.pre_exit, + ) + + assert race_type is not None, "race_type_value must always be populated" + return RaceReport( + first=first, + second=second, + model=self._model_to_dict(model), + reason=reason, + race_type_value=race_type, + witness_addr=int(witness_addr), + witness_grid_a=witness_grid_a, + witness_grid_b=witness_grid_b, + ) + + @staticmethod + def _model_to_dict(model: ModelRef) -> dict[str, str]: + return {decl.name(): str(model[decl]) for decl in model.decls()} + + +__all__ = [ + "CopyContext", + "SymbolicMemoryEvent", + "TwoCopySymbolicHBSolver", +]