SymbolicHBSolver currently never suppresses races; PR #346 behavior does not match the stated goal

[mark14wu]

Problem

PR #346 description states: "Integrate into _check_symbolic_races to suppress races proven ordered by release/acquire synchronization in the symbolic analysis path."

However, SymbolicHBSolver.check_race_possible() unconditionally returns True:

def check_race_possible(self) -> bool:
    """Return True -- symbolic HB cannot currently prove ordering.

    Sound suppression requires both:
    1. Must-alias proof (not just signature equality)
    2. Reads-from proof (atomic_old unavailable in symbolic accesses)

    Until the symbolic engine provides these, conservatively report all
    candidate races and let the concrete fallback handle suppression.
    """
    return True

The tests in test_race_detector_symbolic_hb.py correctly expect True for all cases — including textbook release/acquire patterns — confirming that no suppression ever occurs.

This means _check_symbolic_races() always falls through to concrete execution when sync metadata is present, making the symbolic HB solver effectively a no-op.

Options

1. Update PR [FEAT][RACE DETECTOR] Add symbolic path HB solver #346 scope — Change description to "Add SymbolicHBSolver stub that conservatively defers to concrete fallback" and mark symbolic suppression as future work.
2. Implement concrete fallback gating — When _has_symbolic_sync_metadata() returns True, explicitly skip the symbolic race check and defer to the concrete path, rather than running a no-op solver.
3. Implement actual symbolic suppression — Requires must-alias proof and symbolic reads-from, which are non-trivial.

Affected files

• triton_viz/clients/race_detector/hb_solver.py — SymbolicHBSolver.check_race_possible()
• triton_viz/clients/race_detector/race_detector.py — _check_symbolic_races() integration
• tests/unit/test_race_detector_symbolic_hb.py — all tests expect no suppression

Priority

Merge blocker for PR #346.