[FEAT][RACE DETECTOR] Add atomic sync examples and end-to-end tests#347
Open
mark14wu wants to merge 4 commits intoadd_symbolic_path_hb_solver_for_race_det_e62cfrom
Open
Conversation
2b4bbe8 to
f827523
Compare
025dbbd to
6fa79f5
Compare
f827523 to
eb2f289
Compare
3cca866 to
212fa5c
Compare
eb2f289 to
993a5c5
Compare
Add integration tests for producer-consumer release/acquire, CAS spinlock, failed CAS mixed access, atomic xchg handoff, and epoch barrier preservation. Add example scripts demonstrating spinlock and producer-consumer flag patterns. git-pr-chain: add_atomic_sync_examples_and_end_to_end__a9fd
Add 3 regression E2E tests locking the 3 correctness bugs: 1. Multi-lane CAS aggregation (Issue 1: single-lane bug) 2. Failed acquire with wrong old value (Issue 2: unconditional sw) 3. Per-block private sync addresses (Issue 3: ptr signature unsoundness) Also updates existing E2E tests to provide atomic_val/atomic_old fields needed for reads-from sw edge gating, and resolves remaining rebase conflict markers in hb_solver.py. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- Barrier test CAS now has explicit write_mask (only block 3 succeeds) - Add test_aba_same_value_no_spurious_suppress_e2e: two writers same value → race - Add test_add_written_value_correctness_e2e: add operand ≠ written value → race - Fix residual conflict marker in hb_solver.py from rebase Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Reproducer: release xchg(1) + acquire cas(1,1) must establish sw edge (reader's own writeback excluded from ambiguity scan). Guardrail: same pattern + third-party relaxed xchg(1) must remain ambiguous and report a race. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
993a5c5 to
fc284e1
Compare
212fa5c to
73b9379
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
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 atomic sync examples and end-to-end race detector tests
Add integration tests for producer-consumer release/acquire, CAS
spinlock, failed CAS mixed access, atomic xchg handoff, and epoch
barrier preservation. Add example scripts demonstrating spinlock
and producer-consumer flag patterns.
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.