Commit 5910517
committed
Auto merge of rust-lang#3054 - Vanille-N:spurious-fail, r=RalfJung
Issue discovered in TB: spurious reads are not (yet) possible in a concurrent setting
We discovered a week ago that in general, the current model of TB does not allow spurious reads because although reads provably never invalidate other reads, they migh invalidate writes.
Consider the code
```rs
fn f1(x: &u8) {}
fn f2(y: &mut u8) -> &mut u8 { &mut *y }
let mut data = 0;
let _ = thread::spawn(|| {
f1(&mut data)
};
let _ = thread::spawn(|| {
let y = f2(&mut data);
*y = 42;
});
```
of which one possible interleaving is
```rs
1: retag x (&, protect) // x: [P]Frozen
2: retag y (&mut, protect) // y: [P]Reserved, x: [P]Frozen
1: return f1 // x: [P]Frozen -> Frozen, y: [P]Reserved
2: return f2 // x: Frozen, y: [P]Reserved -> Reserved
2: write y // x: Disabled, y: Active
```
that does not have UB.
Assume enough barriers to force this specific interleaving, and consider that the compiler could choose to insert a spurious read throug `x` during the call to `f1` which would produce
```rs
1: retag x (&, protect) // x: [P]Frozen
2: retag y (&mut, protect) // y: [P]Reserved, x: [P]Frozen
1: spurious read x // x: [P]Frozen, y: [P]Reserved -> [P]Frozen
1: return f1 // x: [P]Frozen -> Frozen, y: [P]Frozen
2: return f2 // x: Frozen, y: [P]Frozen -> Frozen
2: write y // UB
```
Thus the target of the optimization (with a spurious read) has UB when the source did not.
This is bad.
SB is not affected because the code would be UB as early as `retag y`, this happens because we're trying to be a bit more subtle than that, and because the effects of a foreign read on a protected `&mut` bleed outside of the boundaries of the protector. Fortunately we have a fix planned, but in the meantime here are some `#[should_panic]` exhaustive tests to illustrate the issue.
The error message printed by the `#[should_panic]` tests flags the present issue in slightly more general terms: it says that the sequence `retag x (&, protect); retag y (&mut, protect);` produces the configuration `C_source := x: [P]Frozen, x: [P]Reserved`, and that inserting a spurious read through `x` turns it into `C_target := x: [P]Frozen, y: [P]Reserved`.
It then says that `C_source` is distinguishable from `C_target`, which means that there exists a sequence of instructions applied to both that triggers UB in `C_target` but not in `C_source`.
It happens that one such sequence is `1: return f1; 2: return f2; 2: write y;` as shown above, but it is not the only one, as for example the interleaving `1: return f1; 2: write y;` is also problematic.File tree
6 files changed
+917
-146
lines changed- src/tools/miri
- src/borrow_tracker/tree_borrows
- tree
- tests/fail/tree_borrows/reserved
6 files changed
+917
-146
lines changedLines changed: 111 additions & 0 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
| 11 | + | |
| 12 | + | |
| 13 | + | |
| 14 | + | |
| 15 | + | |
| 16 | + | |
| 17 | + | |
| 18 | + | |
| 19 | + | |
| 20 | + | |
| 21 | + | |
| 22 | + | |
| 23 | + | |
| 24 | + | |
| 25 | + | |
| 26 | + | |
| 27 | + | |
| 28 | + | |
| 29 | + | |
| 30 | + | |
| 31 | + | |
| 32 | + | |
| 33 | + | |
| 34 | + | |
| 35 | + | |
| 36 | + | |
| 37 | + | |
| 38 | + | |
| 39 | + | |
| 40 | + | |
| 41 | + | |
| 42 | + | |
| 43 | + | |
| 44 | + | |
| 45 | + | |
| 46 | + | |
| 47 | + | |
| 48 | + | |
| 49 | + | |
| 50 | + | |
| 51 | + | |
| 52 | + | |
| 53 | + | |
| 54 | + | |
| 55 | + | |
| 56 | + | |
| 57 | + | |
| 58 | + | |
| 59 | + | |
| 60 | + | |
| 61 | + | |
| 62 | + | |
| 63 | + | |
| 64 | + | |
| 65 | + | |
| 66 | + | |
| 67 | + | |
| 68 | + | |
| 69 | + | |
| 70 | + | |
| 71 | + | |
| 72 | + | |
| 73 | + | |
| 74 | + | |
| 75 | + | |
| 76 | + | |
| 77 | + | |
| 78 | + | |
| 79 | + | |
| 80 | + | |
| 81 | + | |
| 82 | + | |
| 83 | + | |
| 84 | + | |
| 85 | + | |
| 86 | + | |
| 87 | + | |
| 88 | + | |
| 89 | + | |
| 90 | + | |
| 91 | + | |
| 92 | + | |
| 93 | + | |
| 94 | + | |
| 95 | + | |
| 96 | + | |
| 97 | + | |
| 98 | + | |
| 99 | + | |
| 100 | + | |
| 101 | + | |
| 102 | + | |
| 103 | + | |
| 104 | + | |
| 105 | + | |
| 106 | + | |
| 107 | + | |
| 108 | + | |
| 109 | + | |
| 110 | + | |
| 111 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
15 | 15 | | |
16 | 16 | | |
17 | 17 | | |
| 18 | + | |
| 19 | + | |
| 20 | + | |
| 21 | + | |
18 | 22 | | |
19 | 23 | | |
20 | 24 | | |
| |||
271 | 275 | | |
272 | 276 | | |
273 | 277 | | |
| 278 | + | |
| 279 | + | |
| 280 | + | |
| 281 | + | |
274 | 282 | | |
275 | 283 | | |
276 | 284 | | |
| |||
283 | 291 | | |
284 | 292 | | |
285 | 293 | | |
286 | | - | |
| 294 | + | |
287 | 295 | | |
288 | 296 | | |
289 | 297 | | |
| |||
0 commit comments