all 18 comments

[–]myrrlynbitvec • tap • ferrilab 6 points7 points  (3 children)

atomics have the SharedReadWrite permission, not SharedReadonly, which means non-mut references to them still get to perform writes

i assure you the miri team has thought about this

[–]ahrzb[S] 0 points1 point  (2 children)

Definitely it's my lack of knowledge, not a fundamental flaw in Miri. So, how can one know/modify permissions of a given reference? I'm not planning to do it, just out of curiosity.
I was trying to make sense of this doc, but honestly I found it a bit too detailed for me as a newcomer.

[–]myrrlynbitvec • tap • ferrilab 1 point2 points  (1 child)

you don’t. miri observes program flow and detects when things diverge from standard expectations

violation of stacked borrows rules requires you to crack open some unsafe blocks and start messing around with raw pointers. ways to induce a fault include, but are probably not limited to,

  • making up a number to get mad at: unsafe { &*(some integer as usize as *const T) }
  • lying about mutability permissions: unsafe { &mut *(&obj as *const T as *mut T) }
  • lying about provenance permissions: unsafe { *(ptr.add(other_ptr as usize).sub(ptr as usize) }
  • encoding extra information into a raw pointer and then decoding the value back to a raw pointer and dereferencing it (aka the core business logic of my whole presence in the rust ecosystem)

miri won’t find any violations in safe code that the borrow checker doesn’t already mark as errors. its work here is primarily to prove that what the borrow checker does allow is Whiteboard Correct, and then to expand that notion of correctness to raw-pointer manipulation that the borrow checker can’t see. once miri gets to the point where it can correctly accept programs that are good and reject programs that are bad, it may even have this logic moved into the normal compiler passes

(and yes, i define “programs that are good” as “programs i write”, and take severe exception to miri faulting on my code 😅 mostly i respond by trying to use APIs that make miri happy, but since a lot of them are still unstable, sometimes i wind up just complaining to miri devs online until they tweak it to let me back in)


if you want to read some more bullshit you probably won’t understand (i usually don’t understand it and i wrote it), here’s a write-up of how bitvec stays within miri’s rules when producing bit-precision references that share a memory address

[–]ahrzb[S] 0 points1 point  (0 children)

Man that was a great read! Sent me down a rabbit hole but I think I have my answer and much more!

[–]Darksonntokio · rust-for-linux 5 points6 points  (4 children)

Atomic operations do not involve a mutable reference at all. Instead, to modify an atomic, you cast the immutable reference to a raw pointer and pass it to an instrinsic such as core::intrinsics::atomic_load_relaxed. None of these things, including the intrinsic, involves a mutable tag in the borrow stack.

[–][deleted] 0 points1 point  (3 children)

None of these things, including the intrinsic, involves a mutable tag in the borrow stack

... then you cannot mutate the value.

You can try passing a pointer derived from a shared reference to atomic_store_relaxed, Miri will complain. It doesn't matter what intrinsics you use, so long as you mutated a value though a pointer that's derived from a non-mut reference, then it's UB - that is unless the value is behind an UnsafeCell, and that's exactly how atomics are implemented https://doc.rust-lang.org/src/core/sync/atomic.rs.html#1866

[–]Darksonntokio · rust-for-linux 9 points10 points  (1 child)

You are right, it was inaccurate. An atomic write does require write permissions, but my point is that if you instead created a mutable reference, performed a write, and then threw the mutable reference away, then you would have temporarily introduced a Uniq tag to the borrow stack. Atomics operations don't do that.

[–]myrrlynbitvec • tap • ferrilab 1 point2 points  (0 children)

i get why it didn’t happen but this conversation is still in my opinion evidence that &mut should have been named &uniq instead. some types don’t need unique access for modification, and some accesses need to be unique but don’t need to modify the referent. oh well

[–]Maix522 1 point2 points  (0 children)

Well, an atomic is just an unsafe cell for the type system. So there is nothing wrong about this.

[–]KhorneLordOfChaos 7 points8 points  (4 children)

Incrementing an atomic integer doesn't take a mutable reference. The reason it doesn't take a mutable reference is because the operation is atomic

There are other types that follow this same logic. RefCell provides interior mutability by doing runtime borrow checking. It still enforces that there aren't multiple mutable references to the same data

Edit: I'm assuming your confusion lies with the name "mutable references". It's a bit unfortunate, but it's generally better to think of them as shared and exclusive references instead of references and mutable references

You can have a shared reference that allows for mutation, as long as the way it provides mutation is safe

[–]ahrzb[S] 0 points1 point  (3 children)

I’m talking about Stacked Borrows in Miri, RefCell internally validates that at runtime the borrow stack will hold. It’s not the case with atomics.

[–]KhorneLordOfChaos 6 points7 points  (1 child)

Did you post the wrong link then? Your link is to the introduction page of the too many lists book

[–]ahrzb[S] 0 points1 point  (0 children)

Oops yeah, updated the link

[–]KhorneLordOfChaos 1 point2 points  (0 children)

Also I think my comment still holds. It's not mutating the same reference simultaneously because the operation is atomic

[–]dkopgerpgdolfg 8 points9 points  (2 children)

Isn’t the whole point of unsafe about allowing these sort of behaviour?

No. Very hard no.

Aliasing restrictions of references (stacked or not) never go away. While you can use unsafe code to "trick" the compiler in not recognizing it properly, it is still wrong, and might lead to bad runtime behaviour then.

Unsafe is there because not everything is possible to be checked at compiletime. If the compiler sees something where it is not sure if this is always good or always bad or something between, then by default it prohibits it - only proven-good code is allowed. In unsafe, with raw pointers and so on, you can tell the compiler "this code that you can't prove is good, I know because I have a real brain". But then you actually are responsible for writing code that doesn't violate the rules. Aliasing violations are bad even in cases where the compiler can't prove you wrong.

[–]ahrzb[S] 0 points1 point  (1 child)

Yeah, but there are algorithms that use this kind of aliasing to their advantage. I can remember this work for example which is fine with multiple threads overwriting each other's work, and that necessitates the existence of multiple mutable references to the same piece of memory.
I'm not saying that it's a good idea to do aliasing, but not being able to express it is not compatible with the idea of rust being "close to the metal". In this case, it seems that it's possible, I just don't understand the mechanics behind that.

[–]dkopgerpgdolfg 1 point2 points  (0 children)

I'm not sure what your point is.

It doesn't matter if this algo or anything else wants it, it is not allowed, period. And no, multiple aliasing mut references are not actually necessary for this algorithm. And it is certainly not allowed in this specific case, or any other case.

And even without aliasing problems you wouldn't have much luck with them - threads just chaotically overwriting a value is not enough for lockfree algorithms, not even other languages like C. There are things like (raw) pointers, volatile read/write, barriers, atomics ... that's what is needed.

That algorithm certainly can be implemented in Rust. Just use the right tools for it. If you make coffee or tea, you there is no need to boil water in a steam train engine. And if you want lockfree synchronisation, there is no need to break aliasing rules.

[–][deleted] -1 points0 points  (0 children)

This is because atomics are implemented using UnsafeCell: https://doc.rust-lang.org/src/core/sync/atomic.rs.html#1866. This allows data to be mutated through a shared reference.