4 ms·
> There's an implicit assumption here that all the values returned from the iterator at > for i in &mut v > are disjoint. But iterators, in general, do no
by herbstein 5y ago
> There's an implicit assumption here that all the values returned from the iterator at
> for i in &mut v
> are disjoint. But iterators, in general, do not guarantee disjoint outputs. An iterator which returned each reference value twice, for example, is a valid iterator. But used in the context above, two threads would receive mutable access to the same element of a vector. That seems to violate a core Rust safety assumption.
Your assumptions here are wrong. "An iterator which returned each reference value twice" could only be implemented using unsafe Rust, and code emitting multiple co-occuring mutable references to the same value are instant-UB. In other words, a "safe abstraction" being able to do this is actually not a safe abstraction at all. This would be a bug in the implementation of the custom iterator.
In fact, if you tried to prove such an implementation using the formal tools (Iris) from RustBelt you wouldn't be able to do it. I know, because I've done it as part of my course work under Lars Birkedal.
I'm not sure if you misunderstanding how `&mut v` turns into an iterator, which values it spits out etc, or what is happening. Let's look at how that code is translated into a program and typechecked. First, let's look at the for-loop itself. Anything on the form of
for x in y
must have an implementation of the `IntoIterator` trait for the type of the expression `y`. Whatever that type might be. In this case `y` is actually `&mut v`, where `v`'s type is `Vec<i32>`. Luckily enough, an implementation of `IntoIterator` exists for any `&mut Vec<T>`. [0]
Looking at the expanded signature we can see that the associated type `Item` is `&mut T`. This tells us that the types the resulting iterator will produce are `&mut i32`. Keep in mind that this reference is into the backing memory store of the `Vec<i32>` of `v`. This is where Rust's semantic help us.
You say the following:
> But iterators, in general, do not guarantee disjoint outputs.
The issue with that statement is that iterators don't have to. Rust guarantees that condition. Safe Rust can't return multiple mutable references to the same value. Further, any unsafe implementation, even when exposed through a safe interface, giving this behavior is a bug. It would be great if the compiler could statically verify unsafe code too, but if it could there wouldn't be a need to call it unsafe.
> The question is whether a piece of encapsulated code is always memory-safe for all uses. There's no guarantee of that from the language.
That is ultimately impossible to prove completely and statically. Turing and Gödel made sure of that. However, some things that the compiler can't prove we can still prove as outside observers. Often these things will boil down to controlling and checking the states of several variables before performing an unsafe operation, but knowing that in a given context the operation is safe.
The first part of the above quote is partially true. However, if we assume a given unsafe implementation is indeed safe then the rules of Rust's semantics make the composition of any number of safe APIs a completely safe composition. This is a strong, useful statement because it means the very few places where unsafe is required can be easily checked, and every other piece of code doesn't have to spend mental energy for the programmer to consider the safety of their implementation.
[0] https://doc.rust-lang.org/std/iter/trait.IntoIterator.html#impl-IntoIterator-19
- Animats 5y agoThe issue with that statement is that iterators don't have to. Rust guarantees that condition. Safe Rust can't return multiple mutable references to the same value. So how does Vec return mutable references to elements? Unsafe code, apparently. You can't write your own safe collection class with an iterator and return mutable references. You'd need a proof of disjointness system to do that. The question is whether a piece of encapsulated code is always memory-safe for all uses. There's no guarantee of that from the language. That is ultimately impossible to prove completely and statically. One can construct code for which memory safety is not decidable. That's a good reason to reject it. The Microsoft Static Driver Verifier has a simple solution - if symbolic execution can't verify safety within some time limit, it rejects the driver.
- herbstein 5y ago> So how does Vec return mutable references to elements? Unsafe code, apparently. You can't write your own safe collection class with an iterator and return mutable references. You'd need a proof of disjointness system to do that. If you have a mutable binding to a vector `v` you can get a single mutable reference to one of the elements of that vector at a time. Because getting a single mutable reference to an element requires taking a mutable reference to the vector the disjointedness invariant is upheld. This is the core of the Rust borrow checker. If you're unsure about the semantics you should be reading about it, not trying to sus them out from a fairly surface level discussion on HackerNews. This code: for x in &mut v { *x = // ... } is perfectly valid. For every iteration of the loop only a single mutable reference to an element exists, and the reference is dropped before the next mutable reference is taken. This following piece of code is a full example that showcases how taking two mutable references is not allowed. struct ComplexNonCopyClone { a: u32, } fn main() { let mut v = vec![ ComplexNonCopyClone { a: 1 }, ComplexNonCopyClone { a: 2 }, ComplexNonCopyClone { a: 3 }, ]; let mut_one = v.get_mut(0).unwrap(); let mut_two = v.get_mut(0).unwrap(); mut_two.a = 4; println!("{}", mut_one.a); } Do note that using `mut_one` after `mut_two` is important, as otherwise the compiler will infer that `mut_one` can be dropped before `mut_two` is create, removing the clash. > So how does Vec return mutable references to elements? Unsafe code, apparently. The implementation can be found quite easily[0]. It's essentially invariants upheld by runtime checks and knowledge about the state of the given references/pointers. Notice the comments starting with "SAFETY". They explain the assumptions/conditions/reasons that make the code inside the `unsafe` block safe. If these assumptions can never be violated with malicious input or calling patterns then the code is actually safe and it can be a safe wrapper. [0]: https://doc.rust-lang.org/src/core/slice/index.rs.html#149-190