Auto merge of #3054 - Vanille-N:spurious-fail, r=RalfJung

Browse source

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.

...

This commit is contained in:

bors 2023-09-19 15:46:28 +00:00

parent d6b53ac9af 96abd4a06f

commit b0d36cb6cb

Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL

Show stats Download patch file Download diff file Expand all files Collapse all files

Diff content is not available