[FEAT][RACE DETECTOR] Add symbolic path HB solver#346
Open
mark14wu wants to merge 2 commits intoadd_effect_based_race_classification_and_28bcfrom
Open
[FEAT][RACE DETECTOR] Add symbolic path HB solver#346mark14wu wants to merge 2 commits intoadd_effect_based_race_classification_and_28bcfrom
mark14wu wants to merge 2 commits intoadd_effect_based_race_classification_and_28bcfrom
Conversation
mark14wu
changed the title
mark14wu
changed the title
mark14wu
force-pushed
the
add_effect_based_race_classification_and_28bc
branch
from
6de4922 to
fbb62ce
Compare
mark14wu
force-pushed
the
add_symbolic_path_hb_solver_for_race_det_e62c
branch
3 times, most recently
from
eb2f289 to
993a5c5
Compare
Add SymbolicHBSolver that models two copies of the symbolic program (block A and B) with separate po chains and cross-block sw edges. Integrate into _check_symbolic_races to suppress races proven ordered by release/acquire synchronization in the symbolic analysis path. git-pr-chain: add_symbolic_path_hb_solver_for_race_det_e62c
SymbolicHBSolver used string equality of symbolic ptr signatures to prove same-address and built unconditional sw edges. This is unsound for flag+pid patterns where signatures match but concrete addresses differ. Symbolic accesses also lack atomic_old, so reads-from can't be proven. Replace with conservative `return True` so all candidate races are reported and the concrete fallback handles suppression. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
mark14wu
force-pushed
the
add_symbolic_path_hb_solver_for_race_det_e62c
branch
from
993a5c5 to
fc284e1
Compare
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 symbolic path HB solver for race detector
Add SymbolicHBSolver that models two copies of the symbolic program
(block A and B) with separate po chains and cross-block sw edges.
Integrate into _check_symbolic_races to suppress races proven ordered
by release/acquire synchronization in the symbolic analysis path.
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.