Commit Graph

6227 Commits

Author SHA1 Message Date
Ralf Jung
295e18df0d document how to get a toolchain with clippy 2022-06-08 08:12:20 -04:00
Ralf Jung
a310ccc9a4 some clippy-induced cleanup 2022-06-08 08:06:32 -04:00
Ralf Jung
e62e09ac17 rustup 2022-06-08 07:57:43 -04:00
bors
eedc78d216 Auto merge of #2213 - RalfJung:clippy, r=RalfJung
make clippy mandatory for bors, and silence another clippy lint

We don't currently trigger this but I saw it in a PR and I'd rather evaluate this on a case-by-case basis during review, thank you clippy.
2022-06-07 21:08:56 +00:00
Ralf Jung
2b35dd514e linux-futex test: ensure we join all threads 2022-06-07 17:03:11 -04:00
Ralf Jung
aa68111c60 gate bors on clippy 2022-06-07 16:03:32 -04:00
Ralf Jung
7a5de0c98a silence another clippy lint 2022-06-07 16:01:44 -04:00
bors
ba15da4018 Auto merge of #2212 - RalfJung:cargo-miri, r=RalfJung
update and move cargo-miri operational description
2022-06-07 18:14:33 +00:00
Ralf Jung
cca3dea379 update and move cargo-miri operational description 2022-06-07 13:59:47 -04:00
bors
4d7258076d Auto merge of #2211 - InfRandomness:typo, r=RalfJung
Fix typo
2022-06-07 17:47:27 +00:00
InfRandomness
4758ce74ef Fix typo 2022-06-07 17:43:45 +00:00
bors
4756be8aee Auto merge of #2210 - RalfJung:tls-drop-test, r=RalfJung
add stdlib test for TLS dtor order
2022-06-07 11:59:47 +00:00
Ralf Jung
61f5680da0 add stdlib test for TLS dtor order 2022-06-07 07:58:21 -04:00
bors
ad576d8f9e Auto merge of #2208 - RalfJung:preempt, r=RalfJung
Make scheduler preemptive

This is actually fairly easy. :D I just roll the dice on each terminator to decide whether we want to yield the active thread. I think with this we are also justified to no longer show "experimental" warnings when a thread is spawned. :)

Closes https://github.com/rust-lang/miri/issues/1388
2022-06-07 01:48:57 +00:00
Ralf Jung
11a8b3a00b bless tests 2022-06-06 20:17:39 -04:00
Ralf Jung
bf372a8fbc remove warning about thread support being experimental 2022-06-06 20:16:02 -04:00
Ralf Jung
b64c9a0a83 make scheduler preemptive, with configurable preemption rate 2022-06-06 20:16:02 -04:00
Ralf Jung
dac95a3ad8 rename AllocationMap → RangeObjectMap 2022-06-06 20:16:02 -04:00
bors
d98bd98385 Auto merge of #2209 - RalfJung:if-only, r=RalfJung
hotfix for incorrect only- logic

This hacks around https://github.com/rust-lang/miri/issues/2206. We don't currently use `only-32bit` or so, which is why this works.
2022-06-06 23:48:52 +00:00
Ralf Jung
89edc355e8 bless Windows 2022-06-06 19:48:21 -04:00
Ralf Jung
66d3ee157b hotfix for incorrect only- logic 2022-06-06 19:11:59 -04:00
bors
e6d3d9888d 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 (https://github.com/crossbeam-rs/crossbeam/pull/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
2022-06-06 19:30:38 +00:00
Andy Wang
1b32d14255
Make racy imperfectly overlapping atomic access unsupported instead of UB
Co-authored-by: Ralf Jung <post@ralfj.de>
2022-06-06 19:16:02 +01:00
Andy Wang
bf7a5c4154
Add more backgrounds on lazy store buffers
Co-authored-by: Ralf Jung <post@ralfj.de>
2022-06-06 19:16:02 +01:00
Andy Wang
6fb7c131ed
Remove unused lifetimes 2022-06-06 19:16:02 +01:00
Andy Wang
1379036713
Simplify known C++20 inconsistency test 2022-06-06 19:16:01 +01:00
Andy Wang
65f39bd5cf
Move tests to new directories 2022-06-06 19:16:01 +01:00
Andy Wang
6d0c76ea1b
Specify only perfectly overlapping accesses can race 2022-06-06 19:16:01 +01:00
Andy Wang
c731071640
Give flag temp disabling race detector a better name 2022-06-06 19:16:00 +01:00
Andy Wang
8215702d5a
Refer to GitHub issue on overwritten init value 2022-06-06 19:16:00 +01:00
Andy Wang
4a07f78dad
Forbade all racing mixed size atomic accesses 2022-06-06 19:16:00 +01:00
Andy Wang
ceb173d647
Move logic out of machine.rs 2022-06-06 19:15:59 +01:00
Andy Wang
a7c832b04a
Wording improvements
Co-authored-by: Ralf Jung <post@ralfj.de>
2022-06-06 19:15:59 +01:00
Andy Wang
6a73dedb36
Update experimental threading warning 2022-06-06 19:15:59 +01:00
Andy Wang
bfa56454e9
Split extra_cpp tests into sound and unsafe 2022-06-06 19:15:58 +01:00
Andy Wang
613d60db0b
Allow non-racy mixed size accesses 2022-06-06 19:15:58 +01:00
Andy Wang
226ed41cca
Destroy store buffers on non-racy non-atomic accesses 2022-06-06 19:15:58 +01:00
Andy Wang
2321b15342
Differentiate between not multithreading and temp disabling race detection 2022-06-06 19:15:57 +01:00
Andy Wang
7dcb19ead4
Add rust-only operation tests 2022-06-06 19:15:57 +01:00
Andy Wang
dafd813c16
Move transmute into a separate function 2022-06-06 19:15:57 +01:00
Andy Wang
6d27f188c2
Update src/concurrency/weak_memory.rs
Co-authored-by: Ralf Jung <post@ralfj.de>
2022-06-06 19:15:56 +01:00
Andy Wang
5ddd4eff03
Spelling, punctuation and grammar
Co-authored-by: Ralf Jung <post@ralfj.de>
2022-06-06 19:15:56 +01:00
Andy Wang
31c01415cb
Replace yield_now() with spin loop hint 2022-06-06 19:15:55 +01:00
Andy Wang
e2002b4c65
Amend experimental thread support warnings 2022-06-06 19:15:55 +01:00
Andy Wang
92145373c3
Put the initialisation value into the store buffer 2022-06-06 19:15:55 +01:00
Andy Wang
577054c6de
Rename variables in AllocationMap 2022-06-06 19:15:54 +01:00
Andy Wang
6b54c92377
Throw UB on imperfectly overlapping access 2022-06-06 19:15:54 +01:00
Andy Wang
5a4a1bfccc
Remove incorrect comment 2022-06-06 19:15:54 +01:00
Andy Wang
335667c774
Move buffered functions into their own ext trait 2022-06-06 19:15:53 +01:00
Andy Wang
8739e45bef
Move data_race and weak_memory into a submodule 2022-06-06 19:15:53 +01:00