Skip to content
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

Make Atomic RMWs always fail on read-only memory #2463

Closed
RalfJung opened this issue Aug 5, 2022 · 11 comments · Fixed by #2464
Closed

Make Atomic RMWs always fail on read-only memory #2463

RalfJung opened this issue Aug 5, 2022 · 11 comments · Fixed by #2464
Labels
A-concurrency Area: affects our concurrency (multi-thread) support C-bug Category: This is a bug. I-misses-UB Impact: makes Miri miss UB, i.e., a false negative (with default settings)

Comments

@RalfJung
Copy link
Member

RalfJung commented Aug 5, 2022

This example should probably fail even with Stacked Borrows disabled. (It also segfaults at runtime.)

@RalfJung
Copy link
Member Author

RalfJung commented Aug 5, 2022

That said, doing this the "obvious" way will also trigger all the other write hooks, and I am not sure that would be correct. See rust-lang/unsafe-code-guidelines#355 for that discussion.

@RalfJung
Copy link
Member Author

RalfJung commented Aug 5, 2022

In particular this becomes relevant for the Stacked Borrows successor, where we want to see rust-lang/unsafe-code-guidelines#303 fixed -- that would also "fix" Miri to accept the original example, which we don't want.

@taiki-e
Copy link
Member

taiki-e commented Aug 5, 2022

I think (at least DW) atomic load also needs to fail on read-only memory.

The instructions generated by Atomic*128::load for aarch64 without lse2, Atomic*128::load for x86_64, and Atomic*64::load for x86 without sse&x87 all always write to memory: godbolt

Also, on pre-v6 ARM linux, atomic load calls __sync_val_compare_and_swap_N, which calls __kuser_cmpxchg. I have not read the implementation of __kuser_cmpxchg, but this may have a similar problem because the value is written if the comparison is successful.

@RalfJung
Copy link
Member Author

RalfJung commented Aug 5, 2022

I think (at least DW) atomic load also needs to fail on read-only memory.

What's DW?

The instructions generated by Atomic128::load for aarch64 without lse2, Atomic128::load for x86_64, and Atomic*64::load for x86 without sse&x87 all always write to memory

Uh wtf what?^^

@RalfJung
Copy link
Member Author

RalfJung commented Aug 5, 2022

I can't read assembly very well but it seems this is using a compare_exchange to implement a load? Interesting.

But that's a hardware architecture thing, so I think it is enough to just reject this on read-only memory, but it doesn't mean we need to consider this a write for any other part of the memory model. Stacked Borrows treating this as read-only should still be sound, right?

For example, if another thread does non-atomic loads concurrently with the first thread doing a failing compare_exchange, or one of these u128 atomic loads -- can anything strange happen, are there ever "wrong values" in memory for some intermediate moment in time, or is this really just a strange quirk of the x86 page tables we have to work around?

this may have a similar problem because the value is written if the comparison is successful.

But the value written is the same as the value that was there, i.e., it is guaranteed to be a NOP write, right? On the hardware level this then should mean it's not really observable by other threads?

@taiki-e
Copy link
Member

taiki-e commented Aug 5, 2022

What's DW?

double-width

But that's a hardware architecture thing, so I think it is enough to just reject this on read-only memory, but it doesn't mean we need to consider this a write for any other part of the memory model. Stacked Borrows treating this as read-only should still be sound, right?

Yeah, IMO, the problem is using atomic operations on read-only memory, and since the value is not changed, things like concurrent non-atomic loads from other threads should be fine. (If not, things like emulating 8-bit CAS using 32-bit CAS used on mips, powerpc, riscv, etc. would also be unsound. Since they also write to the memory around the target memory)

is this really just a strange quirk of the x86 page tables we have to work around?

I believe this is a read-only memory-specific problem, but I don't believe this should be considered an x86-specific problem -- I tested a 128-bit atomic load into read-only memory on aarch64 linux and I got SIGSEGV.

On the hardware level this then should mean it's not really observable by other threads?

Probably depends on the architecture; architectures that implement CAS using LL/SC may cause weak CAS in other threads to fail (I can confirm this on aarch64).

@RalfJung
Copy link
Member Author

RalfJung commented Aug 5, 2022

emulating 8-bit CAS using 32-bit CAS

The things you learn...

may cause weak CAS in other threads to fail

Legally speaking it could have failed anyway even if no other thread did anything, so that is fine.
(And also now I finally understand why weak CAS even exists, it's for LL/SC architectures -- thanks for enlightening me :D )

@taiki-e
Copy link
Member

taiki-e commented Aug 5, 2022

Legally speaking it could have failed anyway even if no other thread did anything, so that is fine.

Yeah, that is definitely okay.

emulating 8-bit CAS using 32-bit CAS

Well, I should probably have said, "emulate 8-bit/16-bit atomic RMWs using 32-bit atomic operations" to be exact. (Some architectures lack instructions for atomic RMWs that are smaller than the word size (32-bit). On such architectures, 8-bit and 16-bit atomic RMWs are emulated using 32-bit CAS loop or LL/SC loop. Rounded down the address of the pointer to a multiple of 4, load the 32-bit value, mask the value as only to operate a part of it, and store it by 32-bit CAS or SC...)

If the memory model considers a write that is guaranteed to be no-op as "write", it should not be possible to implement atomic in such a way, because concurrent non-atomic reads to memory around an atomic value will be considered data race.

@RalfJung
Copy link
Member Author

RalfJung commented Aug 5, 2022

If the memory model considers a write that is guaranteed to be no-op as "write"

The Rust memory model does, so this would not be a legal implementation in Rust.

But if this is done at the end of the pipeline when generating assembly, it is fine -- hardware memory models AFAIK don't have a problem with this.

@taiki-e
Copy link
Member

taiki-e commented Aug 5, 2022

If the memory model considers a write that is guaranteed to be no-op as "write"

The Rust memory model does, so this would not be a legal implementation in Rust.

But if this is done at the end of the pipeline when generating assembly, it is fine -- hardware memory models AFAIK don't have a problem with this.

You are right. I should have said something like "If hardware memory models consider a write to non-read-only memory that is guaranteed to be no-op as write..."

@RalfJung
Copy link
Member Author

RalfJung commented Aug 5, 2022

Yes. I hope the targets that emulate small CAS using larger CASes don't have problems with concurrent non-mutating writes. :D

@RalfJung RalfJung added C-bug Category: This is a bug. I-misses-UB Impact: makes Miri miss UB, i.e., a false negative (with default settings) A-concurrency Area: affects our concurrency (multi-thread) support labels Aug 6, 2022
matthiaskrgr added a commit to matthiaskrgr/rust that referenced this issue Aug 8, 2022
…ackh726

add method to get the mutability of an AllocId

Miri needs this for rust-lang/miri#2463.
Dylan-DPC added a commit to Dylan-DPC/rust that referenced this issue Aug 9, 2022
…ackh726

add method to get the mutability of an AllocId

Miri needs this for rust-lang/miri#2463.
@bors bors closed this as completed in 5aef34c Aug 9, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-concurrency Area: affects our concurrency (multi-thread) support C-bug Category: This is a bug. I-misses-UB Impact: makes Miri miss UB, i.e., a false negative (with default settings)
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants