[FEAT][RACE DETECTOR] Add effect-based race classification and concrete HB solver#345
Open
mark14wu wants to merge 5 commits intoadd_atomic_metadata_plumbing_and_return__bec4from
Conversation
mark14wu
changed the title
mark14wu
changed the title
Replace hard-coded _classify_race with effects_at_addr for mixed atomic/plain pairs (e.g. failed CAS = read-only). Add HBSolver using graph reachability over po+sw edges to suppress races proven ordered by release/acquire synchronization. Integrate into detect_races with caching and legacy_atomic exclusion. git-pr-chain: add_effect_based_race_classification_and_28bc
sw edges were created for any release/acquire pair on the same address, over-suppressing races when the acquire didn't observe the release's write. Now sw edges require reads-from proof: the acquire's atomic_old must match the value written by the release. Also updates RaceType enum from RW/WAW to RAW/WAR/WAW for finer-grained classification, and adds reads-from helper functions. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
mark14wu
force-pushed
the
add_effect_based_race_classification_and_28bc
branch
from
6de4922 to
fbb62ce
Compare
- _written_value_at_addr now computes the actual written value for RMW ops (e.g., add(5) with old=10 → written=15) instead of returning the operand - sw edges are only created when the written value uniquely identifies the writer, preventing unsound edges when multiple writers produce the same value - Add _rmw_op_suffix and _compute_rmw_written helpers for all RMW op types - Add 3 regression tests: ABA ambiguity, add written value, operand mismatch Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The ambiguity scan in check_race_possible() only skipped the candidate writer (wi) but not the reader (ri). For a polling CAS like cas(1,1), _written_value_at_addr() returns the reader's own writeback value, which the scan treated as a third-party same-value writer, marking it ambiguous and blocking the sw edge. This broke producer-consumer patterns using CAS polling on the acquire side. Fix: extract _has_ambiguous_writer() helper that skips both wi and ri, and reorder to check _reads_from first as a cheap gate. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
CTA scope is block-local and cannot synchronize across blocks, but
_detect_global_barrier_addresses(), _is_barrier_atomic(), and
_detect_symbolic_barrier_keys() only checked op kind + address, not
scope. This caused CTA-scoped add+cas at a shared address to be
misidentified as a global barrier, incorrectly splitting epochs and
altering the race candidate set.
Fix: filter to scope in ("gpu", "sys", None) in all three functions,
consistent with the HB solver's _scope_ok() gate.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
4 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Add effect-based race classification and concrete HB solver
Replace hard-coded _classify_race with effects_at_addr for mixed
atomic/plain pairs (e.g. failed CAS = read-only). Add HBSolver using
graph reachability over po+sw edges to suppress races proven ordered
by release/acquire synchronization. Integrate into detect_races with
caching and legacy_atomic exclusion.
PR chain
you're doing. This PR is part of a chain of PRs, and clicking the merge
button will not merge it into master.