Skip to content

Commit e6d3d98

Browse files
committed
Auto merge of #1963 - cbeuw:weak-memory, r=RalfJung
Weak memory emulation using store buffers This implements the second half of the [Lidbury & Donaldson paper](https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/POPL.pdf): weak memory emulation using store buffers. A store buffer is created over a memory range on atomic access. Stores will push store elements into the buffer and loads will search through the buffer in reverse modification order, determine which store elements are valid for the current load, and pick one randomly. This implementation will never generate weak memory behaviours forbidden by the C++11 model, but it is incapable of producing all possible weak behaviours allowed by the model. There are certain weak behaviours observable on real hardware but not while using this. Note that this implementation does not take into account of C++20's memory model revision to SC accesses and fences introduced by [P0668](https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0668r5.html). This implementation is not fully correct under the revised C++20 model and may generate behaviours C++20 disallows. Rust follows the C++20 memory model (except for the Consume ordering and some operations not performable through C++'s std::atomic<T> API). It is therefore possible for this implementation to generate behaviours never observable when the same program is compiled and run natively. Unfortunately, no literature exists at the time of writing which proposes an implementable and C++20-compatible relaxed memory model that supports all atomic operation existing in Rust. The closest one is [A Promising Semantics for Relaxed-Memory Concurrency](https://www.cs.tau.ac.il/~orilahav/papers/popl17.pdf) by Jeehoon Kang et al. However, this model lacks SC accesses and is therefore unusable by Miri (SC accesses are everywhere in library code). Safe/sound Rust allows for more operations on atomic locations than the C++20 atomic API was intended to allow, such as non-atomically accessing a previously atomically accessed location, or accessing previously atomically accessed locations with a differently sized operation (such as accessing the top 16 bits of an `AtomicU32`). These scenarios are generally left undefined in formalisations of C++ memory model, even though they [became possible](https://lists.isocpp.org/std-discussion/2022/05/1662.php) in C++20 with `std::atomic_ref<T>`. In Rust, these operations can only be done through a `&mut AtomicFoo` reference or one derived from it, therefore these operations can only happen after all previous accesses on the same locations. This implementation is adapted to accommodate these. ---------- TODOs: - [x] Add tests cases that actually demonstrate weak memory behaviour (even if they are scheduler dependent) - [x] Change `{mutex, rwlock, cond, srwlock}_get_or_create_id` functions under `src/shims` to use atomic RMWs instead of separate read -> check if need to create a new one -> write steps - [x] Make sure Crossbeam tests still pass (crossbeam-rs/crossbeam#831) - [x] Move as much weak-memory related code as possible into `weak_memory.rs` - [x] Remove "weak memory effects are not emulated" warnings - [x] Accommodate certain mixed size and mixed atomicity accesses Rust allows on top of the C++ model
2 parents 3361eab + 1b32d14 commit e6d3d98

File tree

93 files changed

+1848
-126
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

93 files changed

+1848
-126
lines changed

README.md

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,8 @@ for example:
2020
or an invalid enum discriminant)
2121
* **Experimental**: Violations of the [Stacked Borrows] rules governing aliasing
2222
for reference types
23-
* **Experimental**: Data races (but no weak memory effects)
23+
* **Experimental**: Data races
24+
* **Experimental**: Emulation of weak memory effects (i.e., reads can return outdated values)
2425

2526
On top of that, Miri will also tell you about memory leaks: when there is memory
2627
still allocated at the end of the execution, and that memory is not reachable
@@ -61,9 +62,11 @@ in your program, and cannot run all programs:
6162
not support networking. System API support varies between targets; if you run
6263
on Windows it is a good idea to use `--target x86_64-unknown-linux-gnu` to get
6364
better support.
64-
* Threading support is not finished yet. E.g., weak memory effects are not
65-
emulated and spin loops (without syscalls) just loop forever. There is no
66-
threading support on Windows.
65+
* Threading support is not finished yet. E.g. spin loops (without syscalls) just
66+
loop forever. There is no threading support on Windows.
67+
* Weak memory emulation may produce weak behaivours unobservable by compiled
68+
programs running on real hardware when `SeqCst` fences are used, and it cannot
69+
produce all behaviors possibly observable on real hardware.
6770

6871
[rust]: https://www.rust-lang.org/
6972
[mir]: https://github.com/rust-lang/rfcs/blob/master/text/1211-mir.md
@@ -317,7 +320,7 @@ to Miri failing to detect cases of undefined behavior in a program.
317320
can focus on other failures, but it means Miri can miss bugs in your program.
318321
Using this flag is **unsound**.
319322
* `-Zmiri-disable-data-race-detector` disables checking for data races. Using
320-
this flag is **unsound**.
323+
this flag is **unsound**. This implies `-Zmiri-disable-weak-memory-emulation`.
321324
* `-Zmiri-disable-stacked-borrows` disables checking the experimental
322325
[Stacked Borrows] aliasing rules. This can make Miri run faster, but it also
323326
means no aliasing violations will be detected. Using this flag is **unsound**
@@ -327,6 +330,8 @@ to Miri failing to detect cases of undefined behavior in a program.
327330
as out-of-bounds accesses) first. Setting this flag means Miri can miss bugs
328331
in your program. However, this can also help to make Miri run faster. Using
329332
this flag is **unsound**.
333+
* `-Zmiri-disable-weak-memory-emulation` disables the emulation of some C++11 weak
334+
memory effects.
330335
* `-Zmiri-measureme=<name>` enables `measureme` profiling for the interpreted program.
331336
This can be used to find which parts of your program are executing slowly under Miri.
332337
The profile is written out to a file with the prefix `<name>`, and can be processed

src/bin/miri.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -318,6 +318,7 @@ fn main() {
318318
miri_config.stacked_borrows = false;
319319
} else if arg == "-Zmiri-disable-data-race-detector" {
320320
miri_config.data_race_detector = false;
321+
miri_config.weak_memory_emulation = false;
321322
} else if arg == "-Zmiri-disable-alignment-check" {
322323
miri_config.check_alignment = miri::AlignmentCheck::None;
323324
} else if arg == "-Zmiri-symbolic-alignment-check" {
@@ -340,6 +341,8 @@ fn main() {
340341
isolation_enabled = Some(false);
341342
}
342343
miri_config.isolated_op = miri::IsolatedOp::Allow;
344+
} else if arg == "-Zmiri-disable-weak-memory-emulation" {
345+
miri_config.weak_memory_emulation = false;
343346
} else if let Some(param) = arg.strip_prefix("-Zmiri-isolation-error=") {
344347
if matches!(isolation_enabled, Some(false)) {
345348
panic!("-Zmiri-isolation-error cannot be used along with -Zmiri-disable-isolation");

src/concurrency/allocation_map.rs

Lines changed: 278 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,278 @@
1+
//! Implements a map from allocation ranges to data.
2+
//! This is somewhat similar to RangeMap, but the ranges
3+
//! and data are discrete and non-splittable. An allocation in the
4+
//! map will always have the same range until explicitly removed
5+
6+
use rustc_target::abi::Size;
7+
use std::ops::{Index, IndexMut, Range};
8+
9+
use rustc_const_eval::interpret::AllocRange;
10+
11+
#[derive(Clone, Debug)]
12+
struct Elem<T> {
13+
/// The range covered by this element; never empty.
14+
range: AllocRange,
15+
/// The data stored for this element.
16+
data: T,
17+
}
18+
19+
/// Index of an allocation within the map
20+
type Position = usize;
21+
22+
#[derive(Clone, Debug)]
23+
pub struct AllocationMap<T> {
24+
v: Vec<Elem<T>>,
25+
}
26+
27+
#[derive(Clone, Debug, PartialEq)]
28+
pub enum AccessType {
29+
/// The access perfectly overlaps (same offset and range) with the exsiting allocation
30+
PerfectlyOverlapping(Position),
31+
/// The access does not touch any exising allocation
32+
Empty(Position),
33+
/// The access overlaps with one or more existing allocations
34+
ImperfectlyOverlapping(Range<Position>),
35+
}
36+
37+
impl<T> AllocationMap<T> {
38+
pub fn new() -> Self {
39+
Self { v: Vec::new() }
40+
}
41+
42+
/// Finds the position of the allocation containing the given offset. If the offset is not
43+
/// in an existing allocation, then returns Err containing the position
44+
/// where such allocation should be inserted
45+
fn find_offset(&self, offset: Size) -> Result<Position, Position> {
46+
// We do a binary search.
47+
let mut left = 0usize; // inclusive
48+
let mut right = self.v.len(); // exclusive
49+
loop {
50+
if left == right {
51+
// No element contains the given offset. But the
52+
// position is where such element should be placed at.
53+
return Err(left);
54+
}
55+
let candidate = left.checked_add(right).unwrap() / 2;
56+
let elem = &self.v[candidate];
57+
if offset < elem.range.start {
58+
// We are too far right (offset is further left).
59+
debug_assert!(candidate < right); // we are making progress
60+
right = candidate;
61+
} else if offset >= elem.range.end() {
62+
// We are too far left (offset is further right).
63+
debug_assert!(candidate >= left); // we are making progress
64+
left = candidate + 1;
65+
} else {
66+
// This is it!
67+
return Ok(candidate);
68+
}
69+
}
70+
}
71+
72+
/// Determines whether a given access on `range` overlaps with
73+
/// an existing allocation
74+
pub fn access_type(&self, range: AllocRange) -> AccessType {
75+
match self.find_offset(range.start) {
76+
Ok(pos) => {
77+
// Start of the range belongs to an existing object, now let's check the overlapping situation
78+
let elem = &self.v[pos];
79+
// FIXME: derive Eq for AllocRange in rustc
80+
if elem.range.start == range.start && elem.range.size == range.size {
81+
// Happy case: perfectly overlapping access
82+
AccessType::PerfectlyOverlapping(pos)
83+
} else {
84+
// FIXME: add a last() method to AllocRange that returns the last inclusive offset (end() is exclusive)
85+
let end_pos = match self.find_offset(range.end() - Size::from_bytes(1)) {
86+
// If the end lands in an existing object, add one to get the exclusive position
87+
Ok(inclusive_pos) => inclusive_pos + 1,
88+
Err(exclusive_pos) => exclusive_pos,
89+
};
90+
91+
AccessType::ImperfectlyOverlapping(pos..end_pos)
92+
}
93+
}
94+
Err(pos) => {
95+
// Start of the range doesn't belong to an existing object
96+
match self.find_offset(range.end() - Size::from_bytes(1)) {
97+
// Neither does the end
98+
Err(end_pos) =>
99+
if pos == end_pos {
100+
// There's nothing between the start and the end, so the range thing is empty
101+
AccessType::Empty(pos)
102+
} else {
103+
// Otherwise we have entirely covered an existing object
104+
AccessType::ImperfectlyOverlapping(pos..end_pos)
105+
},
106+
// Otherwise at least part of it overlaps with something else
107+
Ok(end_pos) => AccessType::ImperfectlyOverlapping(pos..end_pos + 1),
108+
}
109+
}
110+
}
111+
}
112+
113+
/// Inserts an object and its occupied range at given position
114+
// The Position can be calculated from AllocRange, but the only user of AllocationMap
115+
// always calls access_type before calling insert/index/index_mut, and we don't
116+
// want to repeat the binary search on each time, so we ask the caller to supply Position
117+
pub fn insert_at_pos(&mut self, pos: Position, range: AllocRange, data: T) {
118+
self.v.insert(pos, Elem { range, data });
119+
// If we aren't the first element, then our start must be greater than the preivous element's end
120+
if pos > 0 {
121+
debug_assert!(self.v[pos - 1].range.end() <= range.start);
122+
}
123+
// If we aren't the last element, then our end must be smaller than next element's start
124+
if pos < self.v.len() - 1 {
125+
debug_assert!(range.end() <= self.v[pos + 1].range.start);
126+
}
127+
}
128+
129+
pub fn remove_pos_range(&mut self, pos_range: Range<Position>) {
130+
self.v.drain(pos_range);
131+
}
132+
133+
pub fn remove_from_pos(&mut self, pos: Position) {
134+
self.v.remove(pos);
135+
}
136+
}
137+
138+
impl<T> Index<Position> for AllocationMap<T> {
139+
type Output = T;
140+
141+
fn index(&self, pos: Position) -> &Self::Output {
142+
&self.v[pos].data
143+
}
144+
}
145+
146+
impl<T> IndexMut<Position> for AllocationMap<T> {
147+
fn index_mut(&mut self, pos: Position) -> &mut Self::Output {
148+
&mut self.v[pos].data
149+
}
150+
}
151+
152+
#[cfg(test)]
153+
mod tests {
154+
use rustc_const_eval::interpret::alloc_range;
155+
156+
use super::*;
157+
158+
#[test]
159+
fn empty_map() {
160+
// FIXME: make Size::from_bytes const
161+
let four = Size::from_bytes(4);
162+
let map = AllocationMap::<()>::new();
163+
164+
// Correctly tells where we should insert the first element (at position 0)
165+
assert_eq!(map.find_offset(Size::from_bytes(3)), Err(0));
166+
167+
// Correctly tells the access type along with the supposed position
168+
assert_eq!(map.access_type(alloc_range(Size::ZERO, four)), AccessType::Empty(0));
169+
}
170+
171+
#[test]
172+
#[should_panic]
173+
fn no_overlapping_inserts() {
174+
let four = Size::from_bytes(4);
175+
176+
let mut map = AllocationMap::<&str>::new();
177+
178+
// |_|_|_|_|#|#|#|#|_|_|_|_|...
179+
// 0 1 2 3 4 5 6 7 8 9 a b c d
180+
map.insert_at_pos(0, alloc_range(four, four), "#");
181+
// |_|_|_|_|#|#|#|#|_|_|_|_|...
182+
// 0 ^ ^ ^ ^ 5 6 7 8 9 a b c d
183+
map.insert_at_pos(0, alloc_range(Size::from_bytes(1), four), "@");
184+
}
185+
186+
#[test]
187+
fn boundaries() {
188+
let four = Size::from_bytes(4);
189+
190+
let mut map = AllocationMap::<&str>::new();
191+
192+
// |#|#|#|#|_|_|...
193+
// 0 1 2 3 4 5
194+
map.insert_at_pos(0, alloc_range(Size::ZERO, four), "#");
195+
// |#|#|#|#|_|_|...
196+
// 0 1 2 3 ^ 5
197+
assert_eq!(map.find_offset(four), Err(1));
198+
// |#|#|#|#|_|_|_|_|_|...
199+
// 0 1 2 3 ^ ^ ^ ^ 8
200+
assert_eq!(map.access_type(alloc_range(four, four)), AccessType::Empty(1));
201+
202+
let eight = Size::from_bytes(8);
203+
// |#|#|#|#|_|_|_|_|@|@|@|@|_|_|...
204+
// 0 1 2 3 4 5 6 7 8 9 a b c d
205+
map.insert_at_pos(1, alloc_range(eight, four), "@");
206+
// |#|#|#|#|_|_|_|_|@|@|@|@|_|_|...
207+
// 0 1 2 3 4 5 6 ^ 8 9 a b c d
208+
assert_eq!(map.find_offset(Size::from_bytes(7)), Err(1));
209+
// |#|#|#|#|_|_|_|_|@|@|@|@|_|_|...
210+
// 0 1 2 3 ^ ^ ^ ^ 8 9 a b c d
211+
assert_eq!(map.access_type(alloc_range(four, four)), AccessType::Empty(1));
212+
}
213+
214+
#[test]
215+
fn perfectly_overlapping() {
216+
let four = Size::from_bytes(4);
217+
218+
let mut map = AllocationMap::<&str>::new();
219+
220+
// |#|#|#|#|_|_|...
221+
// 0 1 2 3 4 5
222+
map.insert_at_pos(0, alloc_range(Size::ZERO, four), "#");
223+
// |#|#|#|#|_|_|...
224+
// ^ ^ ^ ^ 4 5
225+
assert_eq!(map.find_offset(Size::ZERO), Ok(0));
226+
assert_eq!(
227+
map.access_type(alloc_range(Size::ZERO, four)),
228+
AccessType::PerfectlyOverlapping(0)
229+
);
230+
231+
// |#|#|#|#|@|@|@|@|_|...
232+
// 0 1 2 3 4 5 6 7 8
233+
map.insert_at_pos(1, alloc_range(four, four), "@");
234+
// |#|#|#|#|@|@|@|@|_|...
235+
// 0 1 2 3 ^ ^ ^ ^ 8
236+
assert_eq!(map.find_offset(four), Ok(1));
237+
assert_eq!(map.access_type(alloc_range(four, four)), AccessType::PerfectlyOverlapping(1));
238+
}
239+
240+
#[test]
241+
fn straddling() {
242+
let four = Size::from_bytes(4);
243+
244+
let mut map = AllocationMap::<&str>::new();
245+
246+
// |_|_|_|_|#|#|#|#|_|_|_|_|...
247+
// 0 1 2 3 4 5 6 7 8 9 a b c d
248+
map.insert_at_pos(0, alloc_range(four, four), "#");
249+
// |_|_|_|_|#|#|#|#|_|_|_|_|...
250+
// 0 1 ^ ^ ^ ^ 6 7 8 9 a b c d
251+
assert_eq!(
252+
map.access_type(alloc_range(Size::from_bytes(2), four)),
253+
AccessType::ImperfectlyOverlapping(0..1)
254+
);
255+
// |_|_|_|_|#|#|#|#|_|_|_|_|...
256+
// 0 1 2 3 4 5 ^ ^ ^ ^ a b c d
257+
assert_eq!(
258+
map.access_type(alloc_range(Size::from_bytes(6), four)),
259+
AccessType::ImperfectlyOverlapping(0..1)
260+
);
261+
// |_|_|_|_|#|#|#|#|_|_|_|_|...
262+
// 0 1 ^ ^ ^ ^ ^ ^ ^ ^ a b c d
263+
assert_eq!(
264+
map.access_type(alloc_range(Size::from_bytes(2), Size::from_bytes(8))),
265+
AccessType::ImperfectlyOverlapping(0..1)
266+
);
267+
268+
// |_|_|_|_|#|#|#|#|_|_|@|@|_|_|...
269+
// 0 1 2 3 4 5 6 7 8 9 a b c d
270+
map.insert_at_pos(1, alloc_range(Size::from_bytes(10), Size::from_bytes(2)), "@");
271+
// |_|_|_|_|#|#|#|#|_|_|@|@|_|_|...
272+
// 0 1 2 3 4 5 ^ ^ ^ ^ ^ ^ ^ ^
273+
assert_eq!(
274+
map.access_type(alloc_range(Size::from_bytes(6), Size::from_bytes(8))),
275+
AccessType::ImperfectlyOverlapping(0..2)
276+
);
277+
}
278+
}

0 commit comments

Comments
 (0)