Miri subtree update #116138
Merged
Miri subtree update #116138
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Automatic sync from rustc
triagebot exclude_labels -> exclude_titles rust-lang/triagebot#1720
Automatic sync from rustc
This occurs because in some interleavings, inserting a spurious read turns a Reserved into Frozen. We show here an exhaustive test (including arbitrary unknown code in two different threads) that makes this issue observable.
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.
disable no-merges check for now It leads to false warnings on sync PRs until rust-lang/triagebot#1720 lands.
Automatic sync from rustc
…obk,saethlin deprecate -Zmiri-disable-abi-check This was added in rust-lang/miri#1776 but I couldn't find any discussion or motivation.
Tested through x86 avx512vpopcntdq and avx512bitalg functions.
run the cron job a bit earlier
Automatic sync from rustc
Implement `llvm.ctpop.v*` intrinsics Tested through x86 avx512vpopcntdq and avx512bitalg functions. I picked them from rust-lang/miri#2057 (comment), which looked easy.
Automatic sync from rustc
Automatic sync from rustc
Put AVX512 tests together
…` to make it generic
The input carry is an 8-bit value that is interpreted as 1 when it is non-zero. The output carry is an 8-bit value that will be 0 or 1. https://www.intel.com/content/www/us/en/docs/cpp-compiler/developer-guide-reference/2021-8/addcarry-u32-addcarry-u64.html
…lfJung
Move `llvm.x86.*` shims into `shims::x86` and implement `_addcarry_u32` and `_subborrow_u{32,64}`
This PR moves all `llvm.x86.*` shims into `shims::x86` and adds `llvm.x86.addcarry.32`, `llvm.x86.subborrow.32` and `llvm.x86.subborrow.64`.
Additionally, it fixes the input carry semantics of `llvm.x86.addcarry.32`. The input carry is an 8-bit value that is interpreted as 1 when it is non-zero.
https://www.intel.com/content/www/us/en/docs/cpp-compiler/developer-guide-reference/2021-8/addcarry-u32-addcarry-u64.html
and add a comment in the AVX test
remove some dead code and add a comment in the AVX test
rustbot
added
the
S-waiting-on-review
|
The Miri subtree was changed cc @rust-lang/miri |
|
@bors r+ p=1 |
bors
added
S-waiting-on-bors
|
☀️ Test successful - checks-actions |
|
Finished benchmarking commit (96ab09d): comparison URL. Overall result: no relevant changes - no action needed@rustbot label: -perf-regression Instruction countThis benchmark run did not return any relevant results for this metric. Max RSS (memory usage)ResultsThis is a less reliable metric that may be of interest but was not used to determine the overall result at the top of this comment.
CyclesThis benchmark run did not return any relevant results for this metric. Binary sizeThis benchmark run did not return any relevant results for this metric. Bootstrap: 631.29s -> 630.752s (-0.09%) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
r? @ghost