-
-
Notifications
You must be signed in to change notification settings - Fork 2.6k
Data race in multi-threaded runtime #6155
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Comments
As I mentioned in the email you quoted, this isn't something that we will consider to be a security vulnerability. Still, thank you for following our process to disclose potential security issues privately first. The easiest way to fix the MIRI failure is to change this function to do a relaxed load instead: tokio/tokio/src/loom/std/atomic_usize.rs Lines 19 to 27 in 7b55518
We could even do that conditionally only on MIRI if this turns out to matter for performance. Either way, we probably want to keep it as an unsynchronized load under loom to keep code valid under that assumption. cc @RalfJung |
I'd rather offer a flag in Miri that allows read-read races. We currently reject them because they are documented as forbidden, which follows C++. If making this load synchronized is an issue for Tokio, that's a good argument for working towards allowing such code. We shouldn't just paper over the fact that Tokio breaks rules that are written down explicitly in our docs. :) (The docs change is fairly new, but that's because until recently there wasn't even any way to cause such read-read races without basically transmuting the memory.) |
"no sane compiler would optimize atomics," but note that this race AIUI would still be considered UB at the LLVM level; an "unordered atomic" load has stronger guarantees than a "not atomic" load. On the other hand, my very quick scan suggested the only codegen difference is that "unordered" won't compile if it could tear, but otherwise lower identically to "not." Since Rust doesn't expose access to "unordered atomic", using a "not atomic" read (when it only ever races with atomic reads) is still formally incorrect but does seem at least a reasonable concession to reality. Personally I would just use a relaxed load to avoid needing to answer the weird questions and avoid giving LLVM justification to dislike me. But asserting the stronger proof under loom still remains useful even if it doesn't get communicated to the codegen. |
That would have the unfortunate effect that you would no longer be able to run programs using Tokio under miri in the playground. I think there is a lot of value for Tokio to work under the default miri configuration. |
I don't think so. LLVM has no UB from data races. It considers read-write races to make the read return undef, and write-write races to change the memory contents to undef. Reading the LLVM docs on this, I think this is completely well-defined. A read that is part of such a read-read race still sees only a single possible write, so we end up in this clause: "Otherwise, if Rbyte may see exactly one write, Rbyte returns the value written by that write." |
Using
tokio
1.34.0 with featuresmacros
andrt-multi-threaded
(without default features enabled), I have a trivial async program:Using the
nightly-2023-11-16
toolchain with themiri
component on thex86_64-unknown-linux-gnu
target, I executedMIRIFLAGS="-Zmiri-num-cpus=2" cargo miri run
. This results in a data race.For completeness, this is
Cargo.lock
.Cargo.lock
contentsFrom @Darksonn via email (in part)
The text was updated successfully, but these errors were encountered: