Skip to content

[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
add_atomic_sync_examples_and_end_to_end__a9fd
Open

[FEAT][RACE DETECTOR] Add atomic sync examples and end-to-end tests#347
mark14wu wants to merge 4 commits intoadd_symbolic_path_hb_solver_for_race_det_e62cfrom
add_atomic_sync_examples_and_end_to_end__a9fd

Conversation

@mark14wu
Copy link
Copy Markdown
Collaborator

@mark14wu mark14wu commented Mar 17, 2026

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

  1. [FEAT][RACE DETECTOR] Add atomic metadata plumbing and return value capture #344
  2. [FEAT][RACE DETECTOR] Add effect-based race classification and concrete HB solver #345
  3. [FEAT][RACE DETECTOR] Add symbolic path HB solver #346
  4. 👉 [FEAT][RACE DETECTOR] Add atomic sync examples and end-to-end tests #347 👈 YOU ARE HERE

⚠️⚠️ Please do not click the green "merge" button unless you know what
you're doing. This PR is part of a chain of PRs, and clicking the merge
button will not merge it into master. ⚠️⚠️

@mark14wu mark14wu changed the title Add atomic sync examples and end-to-end race detector tests [FEAT][RACE DETECTOR] PR4: Add atomic sync examples and end-to-end tests Mar 17, 2026
@mark14wu mark14wu changed the title [FEAT][RACE DETECTOR] PR4: Add atomic sync examples and end-to-end tests [FEAT][RACE DETECTOR] Add atomic sync examples and end-to-end tests Mar 17, 2026
@mark14wu mark14wu force-pushed the add_symbolic_path_hb_solver_for_race_det_e62c branch from 2b4bbe8 to f827523 Compare March 18, 2026 20:14
@mark14wu mark14wu force-pushed the add_atomic_sync_examples_and_end_to_end__a9fd branch from 025dbbd to 6fa79f5 Compare March 18, 2026 20:14
@mark14wu mark14wu force-pushed the add_symbolic_path_hb_solver_for_race_det_e62c branch from f827523 to eb2f289 Compare March 18, 2026 23:41
@mark14wu mark14wu force-pushed the add_atomic_sync_examples_and_end_to_end__a9fd branch 2 times, most recently from 3cca866 to 212fa5c Compare March 19, 2026 01:36
@mark14wu mark14wu force-pushed the add_symbolic_path_hb_solver_for_race_det_e62c branch from eb2f289 to 993a5c5 Compare March 19, 2026 01:36
mark14wu and others added 4 commits March 19, 2026 15:53
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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant