Changes to pass Miri test with the stacked borrows model #46
Conversation
ratmice
changed the title
The `swap` function passed with `MIRIFLAGS=-zmiri-tree-borrows` But failed when ran through the stacked borrows model, because `get_unchecked_mut` returns `&mut` references which we need two of. by using `as_mut_ptr()` we can avoid creating multiple mutable references from a single one satisfying uniqueness.
This clone impl would sucessfully run under `MIRIFLAGS=-Zmiri-tree-borrows` but failed with stacked borrows. Instead of cloning the extra capacity into the new vec. Create a new vector with the correct capacity then extend it with the cloned contents of the other vector. This can be done safely.
ratmice
force-pushed
the
miri_stacked_borrows
branch
from
aaa349b to
254c1ec
Compare
|
Rebased, and all green now. |
src/core/option.rs
Outdated
| // To fix both issues, we get a slice to the complete memory of the | ||
| // original `Vec` and create a `Vec` from it. Then we reset the length | ||
| // to the old value. Both is safe as all the elements that are included | ||
| // and excluded by the "fake length" are `None`. | ||
| let data = unsafe { | ||
| let mut data_clone = self.data.get_unchecked(0..self.data.capacity()).to_vec(); | ||
| data_clone.set_len(self.data.len()); | ||
| data_clone | ||
| }; | ||
| // To fix both issues, we create a new vec with the appopriate capacity | ||
| // and extend it with the values of the other. | ||
| let mut data = Vec::with_capacity(self.data.capacity()); | ||
| data.extend(self.data.iter().cloned()); |
There was a problem hiding this comment.
I don't think this is correct, as it does not initialize elements beyond self.data.len(), right? But this is required. See realloc that initializes all those elements to None. And the docs on the data field say so as well. I suppose has_element_at was one of the methods relying on this behavior.
But I think this implementation relying that elements beyond vec.len() can be initialized and stay that way is... dubious? The easy way to do this properly is to actually initialize all elements and have the Vec's len == cap at all times. But that wastes a usize of course and would require us to store a separate len field. So I think this implementation should use a pointer and do everything manually like bitvec. I don't think Vec can give us the guarantees that we need. Or, alternatively, we could find all the methods that rely on the current "initialized beyond len" behavior and rewrite them. Hopefully without making them slower.
There was a problem hiding this comment.
Oof I think many methods rely on the "initialized beyond len". Lots call self.data.get_unchecked_mut(idx) where idx is only guaranteed to be <= cap. Vec::get_unchecked_mut specifically says that calling it with an out of bounds index is immediately UB. So I think this whole implementation is super broken... sigh
There was a problem hiding this comment.
Yeah, the key point here is this line in the std docs for Slice::get_unchecked and Slice::get_uncheckec_mut
Calling this method with an out-of-bounds index is undefined behavior even if the resulting reference is not used.
There was a problem hiding this comment.
I think with the has_element_at change that we committed though, we aren't hitting that anymore.
because those get_unchecked_mut calls seem to be predicated on has_element_at, it is very much a can of worms though.
There was a problem hiding this comment.
So yes, that means it has to be completely rewritten to either waste a usize and keep the vec's len == cap or not use Vec at all, but raw pointers. Ouch.
I assume you are not volunteering? :D
I don't know when I'll have the time but of course I'd try it asap. I wonder if I should release your other patch already. Or release a new major version where the OptionCore is removed until I get time to re-add it. And then of course yank the old ones.
There was a problem hiding this comment.
I think it is a bit involved and a diversion for me, I mostly wanted to compare the performance of Lox vs a naive doubly linked list approach for cases where we are adding/removing lots of elements like decimation and subdivision.
And I was pondering whether modified RRB-vectors could be used in any way that improves the deletion/insertion with the vector stability guarantees but without having to keep the entire vector gaps.
(Not that I have any actual ideas yet that would work, but it is part of the thinking that lead to me playing with these crates)
There was a problem hiding this comment.
Looking through github at least I don't see anywhere that OptionCore/InlineStableVec gets used outside of
this benchmark1, so removing it until it can be re-added does seem like a viable option.
I don't have any particular preferences between that and releasing with my patch, so both seem like viable options to me.
Footnotes
There was a problem hiding this comment.
I suppose one other thing we could consider doing rather than abandoning the approach the crate currently takes is to override clear to for item in self.data.iter_mut() { item.take() }, then replace the uses of get_unchecked* with their vec.ast_ptr().offset(idx) which has the weaker precondition the current implementation assumes.
This would probably require quite a bit of auditing of anything in the implementation that removes elements though so they take().
There was a problem hiding this comment.
Regarding your initial comment in this thread I did push a fix that initializes the extra capacity with None values, but in a way that doesn't read the extra capacity of the other vector.
There was a problem hiding this comment.
So i've gone ahead and come to the conclusion that there were 2 problems,
the failure to maintain the invariant, in clear, and the get_unchecked usage in has_element_at.
Subsequently, I've changed the clear implementation and avoided get_unchecked,
and now because calls to get_unchecked* are predicated on the return value of has_element_at all the current usage I believe should be correct.
This should allow keeping the current implementation intact, while removing that bounds check from my previous patch
|
So this is now revisiting my previous patch, at which point it is probably good to make things clear that we're
The first case I believe should be entirely handled by a1ce91b As far as I can see and the testsuite covers, the rest are predicated on having called |
|
Sorry for my delay getting to this and thanks for your analysis and this amazing work. I believe the But yes it seems like I can just release it then. I still think it should be eventually rewritten as Vec's guarantees regarding memory behind |
|
Just released v0.4.1 and yanked v0.4.0. I also created #47. Thanks again! |
Indeed indeed, I entirely agree, but I was a bit hesitant to do so myself, considering it seems like it requires changing |
I broke these patches out separately, but when run on top of my pr #45
mirinow passes the testsuite with both stacked borrows andMIRIFLAGS=-Zmiri-tree-borrows. Previously it would only pass when running with tree borrows.I don't consider myself terribly well versed in unsafe rust so a healthy skepticism is probably prudent.