[FEAT] Add the eager race detector

tests/unit/test_race_detector.py

@@ -1,12 +1,18 @@
+import pytest
+import torch
 import triton
 import triton.language as tl
+from z3 import substitute
 
 import tilelens
 from tilelens.clients import RaceDetector
 from tilelens.clients.race_detector.race_detector import (
     SymbolicRaceDetector,
     NullRaceDetector,
 )
+from tilelens.clients.race_detector.two_copy_symbolic_hb_solver import (
+    TwoCopySymbolicHBSolver,
+)
 from tilelens.core.config import config as cfg
 
 
@@ -25,6 +31,13 @@ def test_race_detector_factory_toggle():
         cfg.enable_race_detector = saved
 
 
+def test_compile_mode_is_not_available_yet(monkeypatch):
+    monkeypatch.setattr(cfg, "enable_race_detector", True)
+    for make in (RaceDetector, SymbolicRaceDetector):
+        with pytest.raises(NotImplementedError, match="compiled race detector"):
+            make(compile=True)
+
+
 @triton.jit
 def _dispatch_kernel(x_ptr, BLOCK: tl.constexpr):
     offs = tl.arange(0, BLOCK)
@@ -76,3 +89,26 @@ def test_flag_off_returns_raw_kernel_for_factory_instance():
         assert traced is _dispatch_kernel
     finally:
         cfg.enable_race_detector = saved
+
+
+# ======== Solver Contract ========
+
+
+@triton.jit
+def _pid_store_kernel(x_ptr):
+    tl.store(x_ptr + tl.program_id(0), 1)
+
+
+def test_solver_renames_the_captured_pid_per_copy():
+    """The two-copy solver renames SymbolicExpr's pid vars per copy; a
+    captured pid-dependent address must change under that rename, or both
+    copies would be one program and every cross-program race would be
+    missed."""
+    detector = SymbolicRaceDetector()
+    tilelens.trace(client=detector)(_pid_store_kernel)[(2,)](torch.zeros(2))
+    (record,) = detector.records
+    solver = TwoCopySymbolicHBSolver(detector.records, grid=(2, 1, 1))
+    for ctx in (solver.ctx_a, solver.ctx_b):
+        renamed = substitute(record.addr_expr, *ctx.pid_substitutions)
+        assert not renamed.eq(record.addr_expr)
+        assert f"pid_{ctx.label}_0" in str(renamed)

tilelens/clients/__init__.py

@@ -9,6 +9,9 @@
     "LoadStoreBytes": ("tilelens.clients.profiler.data", "LoadStoreBytes"),
     "OpTypeCounts": ("tilelens.clients.profiler.data", "OpTypeCounts"),
     "RaceDetector": ("tilelens.clients.race_detector.race_detector", "RaceDetector"),
+    "RaceType": ("tilelens.clients.race_detector.data", "RaceType"),
+    "RaceRecord": ("tilelens.clients.race_detector.data", "RaceRecord"),
+    "RaceAccess": ("tilelens.clients.race_detector.data", "RaceAccess"),
     "Sanitizer": ("tilelens.clients.sanitizer.sanitizer", "Sanitizer"),
     "CompiledSanitizer": (
         "tilelens.clients.sanitizer.compiled.client",

tilelens/clients/race_detector/data.py

@@ -1,7 +1,7 @@
 from __future__ import annotations
 
 from dataclasses import dataclass, field
-from enum import Enum, auto
+from enum import Enum
 from typing import Any, Literal
 
 import torch
@@ -13,10 +13,11 @@
 AtomicKind = Literal["none", "cas", "rmw"]
 
 
-class RaceType(Enum):
-    RAW = auto()  # Read-After-Write
-    WAR = auto()  # Write-After-Read
-    WAW = auto()  # Write-After-Write
+class RaceType(str, Enum):
+    # str-valued, so a RaceRecord holds (and a saved trace keeps) the name.
+    RAW = "RAW"  # Read-After-Write
+    WAR = "WAR"  # Write-After-Read
+    WAW = "WAW"  # Write-After-Write
 
 
 @dataclass
@@ -89,8 +90,15 @@ class AccessEventRecord:
     # 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.
+    # these pairs. A block anchor is listed only when it has a
+    # lane_position.
     dep_loads: tuple[int, ...] = ()
+    # The block position of a lane, one coordinate per dimension of the
+    # access's block (the arange feeding that dimension, minus its start).
+    # When both records of a dependency-ordered pair carry one, the
+    # dependency edge and the DISTINCT-position query compare positions
+    # through it. None: not derived.
+    lane_position: tuple[Any, ...] | None = None
 
     # Operational control conditions used for value-causality dependencies,
     # before execution-domain premises are conjoined into event activity.
@@ -124,6 +132,9 @@ class RaceReport:
     reason: str = ""
     race_type_value: RaceType | None = None
     witness_addr: int | None = None
+    # Each access's own address in the witness (they differ when the two
+    # element sizes do).
+    witness_addrs: tuple[int, int] | None = None
     witness_grid_a: tuple[int, int, int] | None = None
     witness_grid_b: tuple[int, int, int] | None = None
 
@@ -142,10 +153,46 @@ def race_type(self) -> RaceType:
         return self.race_type_value
 
 
+@dataclass(frozen=True)
+class RaceAccess:
+    """One access of a race witness."""
+
+    op: str  # the Op's name: "load", "store", "atomic_cas" or "atomic_rmw"
+    writes: bool  # whether it writes in the witness
+    tensor_name: str | None
+    source_location: tuple[str, int, str] | None  # (filename, lineno, func)
+    # The element it touches in the witness, counted in elements from the
+    # tensor's data pointer (the flat index for a contiguous tensor); None
+    # when the tensor is unknown.
+    element: int | None
+
+
+@dataclass(frozen=True)
+class RaceRecord:
+    """A race the race detector found, as ``Launch.records`` holds it.
+
+    Plain data, so ``tilelens.save()`` keeps it: no Z3 terms, no tensors.
+    ``programs`` are the program ids of the two accesses in the witness
+    (equal for a race inside one program instance).
+    """
+
+    race_type: str  # a RaceType value
+    first: RaceAccess
+    second: RaceAccess
+    programs: tuple[tuple[int, int, int], tuple[int, int, int]]
+    reason: str
+
+    def __post_init__(self) -> None:
+        # A RaceType member is held as its plain string, as a load returns it.
+        object.__setattr__(self, "race_type", RaceType(self.race_type).value)
+
+
 __all__ = [
     "AccessEventRecord",
     "AtomicKind",
     "MemorySem",
+    "RaceAccess",
+    "RaceRecord",
     "RaceReport",
     "RaceType",
 ]

tilelens/clients/race_detector/hb_common.py

@@ -14,8 +14,15 @@ class UnsupportedSymbolicRaceQuery(Exception):
     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.
+
+    ``reason_unknown`` is Z3's ``reason_unknown()`` (e.g. ``"timeout"``) when
+    an undecided query raised it, None otherwise.
     """
 
+    def __init__(self, *args: object, reason_unknown: str | None = None) -> None:
+        super().__init__(*args)
+        self.reason_unknown = reason_unknown
+
 
 class CountingScopeUnsupported(UnsupportedSymbolicRaceQuery):
     """An atomic address needs a counter whose symbolic-grid bound may wrap.