Skip to content

Commit

Permalink
fix SC fence logic
Browse files Browse the repository at this point in the history
  • Loading branch information
RalfJung committed Dec 6, 2024
1 parent 8b26f5c commit 7b51f77
Showing 1 changed file with 8 additions and 4 deletions.
12 changes: 8 additions & 4 deletions src/concurrency/data_race.rs
Original file line number Diff line number Diff line change
Expand Up @@ -874,23 +874,27 @@ pub trait EvalContextExt<'tcx>: MiriInterpCxExt<'tcx> {
// Either Acquire | AcqRel | SeqCst
clocks.apply_acquire_fence();
}
if atomic != AtomicFenceOrd::Acquire {
// Either Release | AcqRel | SeqCst
clocks.apply_release_fence();
}
if atomic == AtomicFenceOrd::SeqCst {
// Behave like an RMW on the global fence location. This takes full care of
// all the SC fence requirements, including C++17 §32.4 [atomics.order]
// paragraph 6 (which would limit what future reads can see). It also rules
// out many legal behaviors, but we don't currently have a model that would
// be more precise.
// Also see the second bullet on page 10 of
// <https://www.cs.tau.ac.il/~orilahav/papers/popl21_robustness.pdf>.
let mut sc_fence_clock = data_race.last_sc_fence.borrow_mut();
sc_fence_clock.join(&clocks.clock);
clocks.clock.join(&sc_fence_clock);
// Also establish some sort of order with the last SC write that happened, globally
// (but this is only respected by future reads).
clocks.write_seqcst.join(&data_race.last_sc_write_per_thread.borrow());
}
// The release fence is last, since both of the above could alter our clock,
// which should be part of what is being released.
if atomic != AtomicFenceOrd::Acquire {
// Either Release | AcqRel | SeqCst
clocks.apply_release_fence();
}

// Increment timestamp in case of release semantics.
interp_ok(atomic != AtomicFenceOrd::Acquire)
Expand Down

0 comments on commit 7b51f77

Please sign in to comment.