Add regressions for same-value ABA reads-from ambiguity and single-SM symbolic HB false positives

[mark14wu]

Context

PR #347 added regression E2E tests for 3 bugs:

1. Multi-lane CAS single-lane bug (test_duplicate_lane_same_address_aggregation)
2. Wrong-old-value / failed acquire (test_failed_acquire_no_sw_edge)
3. Private sync address / ptr signature (test_per_block_private_sync_no_spurious_suppress)

Two additional high-risk scenarios lack dedicated E2E coverage:

Gap 1: Same-value ABA concrete E2E

Status: Already covered — test_aba_same_value_no_spurious_suppress_e2e and test_acquire_cas_same_value_poll_still_races_with_third_party_same_value_writer were added in recent commits on #347.

Gap 2: Single-SM symbolic path (SymbolicHBSolver never suppresses)

When num_sms == 1, the race detector takes the symbolic analysis path. SymbolicHBSolver.check_race_possible() always returns True, so it never suppresses — but this behavior isn't pinned by an E2E test.

Without a regression test, a future change to SymbolicHBSolver that incorrectly starts suppressing could go unnoticed. The test should:

• Set up a num_sms=1 scenario with release/acquire pattern
• Verify that races are still reported (symbolic path cannot prove ordering)
• Serve as a canary for when symbolic suppression is actually implemented (test expectations would flip)

Suggested test

def test_symbolic_path_release_acquire_still_reports_race():
    """num_sms=1 → symbolic path → SymbolicHBSolver returns True → race reported."""
    # Producer-consumer pattern via symbolic path
    # Assert races > 0 (symbolic HB cannot suppress)

Related

• SymbolicHBSolver currently never suppresses races; PR #346 behavior does not match the stated goal #349 (SymbolicHBSolver no-op)
• Downstream PRs are not restacked onto the latest #345 HB fixes; same-value ABA / ambiguous reads-from remains reproducible #350 (ABA restack status)

Priority

Test gap — ties into #349 resolution.