weak memory: fix non-atomic read clearing store buffer #4658
Conversation
|
Thank you for contributing to Miri! |
RalfJung
force-pushed
the
weak-mem-na-reads
branch
3 times, most recently
from
930b74f to
f3cba0b
Compare
| self.write_type = write_type; | ||
| self.read.set_zero_vector(); | ||
| // This is not an atomic location any more. | ||
| self.atomic_ops = None; |
There was a problem hiding this comment.
@cbeuw do you know if there is a particular reason why we kept the atomic_ops around even after a non-atomic write?
RalfJung
force-pushed
the
weak-mem-na-reads
branch
from
f3cba0b to
5ac282c
Compare
| data_race.read(alloc_id, range, NaReadType::Read, None, machine)?; | ||
| if let Some(weak_memory) = weak_memory { | ||
| weak_memory.memory_accessed(range, machine.data_race.as_vclocks_ref().unwrap()); | ||
| } |
There was a problem hiding this comment.
@cbeuw is it correct to do absolutely nothing with the store buffers on a non-atomic read? I would think so, but better to double-check.^^
RalfJung
force-pushed
the
weak-mem-na-reads
branch
from
5ac282c to
e8233b5
Compare
|
This PR was rebased onto a different master commit. Here's a range-diff highlighting what actually changed. Rebasing is a normal part of keeping PRs up to date, so no action is needed—this note is just to help reviewers. |
|
I'm going to land this for now to fix the bug; we can always adjust more later. |
2 participants
We used to clear the store buffer on every non-atomic read, which made sense back when non-atomic accesses were not allowed to race with atomic accesses -- but these days, this makes little sense, and it prevents legal behaviors from being explored (see the change in the
weak.rstest). Furthermore, when we reconstruct the store buffer on the next atomic store, we assume that the "prior" state we are inserting corresponds to a non-atomic write, and thus we do not give it a sync clock -- but if we cleared the store buffer, that prior state might in fact be an atomic write, so the incorrect sync clock then leads to incorrect vector clocks which causes wrong UB and potentially also wrong behavior.Fixes #4655