Repository navigation
Challenge 4: Memory safety of BTreeMap's btree::node module #77
Description
Tracking issue for Challenge 4: Memory safety of BTreeMap's btree::node module.
btree::node module #77Tracking issue for Challenge 4: Memory safety of BTreeMap's btree::node module.
Activity
btj commentedon Jan 29, 2025
Anyone looking into this might be puzzled initially by the ValMut borrow type. The description says there may be any number of outstanding mutable references to values, but if you just look at the API of node.rs, you would think the
NodeRef<ValMut>gets consumed whenever a mutable reference to a value gets created. To understand ValMut, it is useful to look at how it's used in client code, specifically here, in the implementation of the BTreeMap iterator. Notice that theHandle<NodeRef<ValMut>>gets duplicated through unsafe code. In general, of course, duplicating mutable references of any kind is a big no-no. In this case, it's safe provided that the client never tries to get two mutable references to the same value.btj commentedon Jan 30, 2025
I've started looking into this challenge. I've made a first stab at a separation logic predicate (plus supporting definitions) defining what it means to own a NodeRef. Note: for now, this is completely untested; I have not yet attempted to use it to verify any code.
btj commentedon Jan 30, 2025
OK, I've looked some more at the codebase. If I'm not mistaken, borrow type ValMut is being used (only) to implement IterMut, and borrow type Dying is used (only) to implement IntoIter. In both cases, two NodeRef values of this type are used, to point to the start and end of the iterator, which is a DoubleEndedIterator and can therefore be consumed from both ends. Any given key-value pair can be returned from either end, depending on which end reaches that pair first. Therefore, it does not work to assign ownership of a given key-value pair to one of these NodeRefs. My idea for how these iterators could perhaps be verified is then that, when in rest, ownership of the not-yet-consumed part of the tree is held just once by the iterator, separately from the two NodeRefs, which themselves are in a kind of dormant state. When
nextornext_backis called, one of the NodeRefs is awoken and takes hold of that ownership. (These "go to sleep" and "awaken" transitions are not explicit in the code; they would show up in the separation logic proof only.)I have improved my NodeRef predicate to take this new insight into account. The predicate now asserts ownership of only the part of the tree between two leaf edges. When the borrow type is Immut, Mut, or Owned, that range is in fact the full range, i.e. the entire tree. Only with borrow type ValMut or Dying could the range be less. The node.rs functions that are polymorphic over the borrow type, mostly navigation functions, will need to take a precondition saying that the navigation does not exit the "active" range. Even the non-
unsafeones will need to take such a precondition. This reflects the fact that calling certain safe functions on a ValMut or Dying NodeRef can cause UB. Therefore, initially I will not attempt to prove RustBelt semantic well-typedness of any of the functions; rather, I will prove only correctness with respect to a custom separation logic spec. The goal will be that these specs are sufficient to, in turn, prove safety (and correctness) of the rest of the BTreeMap implementation. The safety of the BTreeMap implementation (map.rs,navigate.rs, etc.) will not follow from its well-typedness; in any case, it uses lots ofunsafeblocks so it's not well-typed in the RustBelt sense anyway.Note: the doc comment for NodeRef says that ValMut is like a shared reference as far as the tree structure is concerned. But as far as I can tell, it is only used in IterMut, where always only these exactly two NodeRefs exist, so there is not really any arbitrary sharing going on. Therefore, it seemed more logical to have ValMut own a full borrow of the tree and the keys rather than a fractured borrow. (This also jives better with the fact that node.rs implements Send for
NodeRef<ValMut, K, V>if K is Send (as opposed to if K is Sync).)Challenge 4: Verify memory safety of BTreeMap node module