BTree: lighten the load on Miri #68781

ssomers · 2020-02-02T20:51:28Z

Reduce the amount of work Miri ploughs through in btree code, in particular on test_clone_from (which takes up 5 minutes on my machine).

r? @crgl

Mark-Simulacrum · 2020-02-02T21:09:15Z

src/liballoc/tests/btree/map.rs

    let size = 30;
+    #[cfg(miri)]
+    let size = 13;


I'm not really sure that testing 900 different variations of clone_from is buying us anything anyway, so maybe just go with 13 always?

I agree. 0, 1, 10, 11 and 12 are the only interesting sizes for size=30 (note that size itself isn't tested). Next stop would be 144 (3 levels, not all edges pointing to leaves).

Also, as an aside, by always adding greater elements on both sides, I think (am not quite sure) that some kinds of trees are ignored (as in right leaf bigger than left leaf or so). I am pretty sure that you can have an 11 element tree packed in a lonely root or spread over 2 levels, depending on whether you remove the 6th or 7th element from a 12 element tree. But it's hard to diagnose since tests can't tell the difference. So other test cases don't try to go there either.

The same can be said about test_clone (possibly an inspiration for this or future tests): if we can clone a 12 element (2 level, 2 leaf) tree, surely we can handle every bigger 2 level tree... but can we handle bigger? Yes, we can, and Miri can handle it fine too. Just don't ask it to clone every size of tree in between.

src/liballoc/tests/btree/map.rs

JohnTitor · 2020-02-16T04:31:22Z

r? @RalfJung

RalfJung · 2020-02-16T11:21:22Z

src/liballoc/collections/btree/map.rs

@@ -250,8 +250,7 @@ impl<K: Clone + Ord, V: Clone> BTreeClone for BTreeMap<K, V> {
        // the BTree invariants are maintained at the end of the loop
        while !siter.is_empty() {
            if let Some((ok, ov)) = oiter.next() {
-                // SAFETY: This is safe because the `siter.front != siter.back` check
-                // ensures that `siter` is nonempty
+                // SAFETY: This is safe because `siter` is nonempty


Why is there a safety comment being changed in a PR that's labelled to be about tests?

It's something I noticed that wasn't adapted in the history of the already merged change, related to most of the test tweaks. I can do that commit in a separate PR or forget about it.

I am not deeply familiar with the code, and unfortunately next_unchecked doesn't have a comment explaining its unsafe precondition. But the change makes sense to me, so we can keep it. Just please add a trailing . :)

Gladly, but to this one only or to all similar comments in the file?

Having a trailing . after a proper sentence is the recommended comment style in rustc (AFAIK...), but there's no need to increase the diff to port everything. Just, whatever you touch should follow the style.

OTOH if you want to add a few more trailing ., it's not like that's hard to review.^^

next_unchecked doesn't have a comment explaining its unsafe precondition

True. But when I work my way up from the recently documented underlying implementation, the precondition is unhelpful or convoluted. Calling Range::next_unchecked is safe if (besides another thing) whoever initialized the range instance, gave it "good" data. Or constructing a valid Range is an unsafe operation itself but I don't find information on marking constructors unsafe. So, short unhelpful comment coming in.

Well I was trying to review the SAFETY comment and that is hard when the precondition is unclear. ;) But that is not your fault, and your PR doesn't make it worse, so I am still fine with the diff here.

Or constructing a valid Range is an unsafe operation itself but I don't find information on marking constructors unsafe.

There is no such thing; we make them private. A constructor can never by itself cause UB.

I was adding comments on the next_unchecked touched here, because it seems a waste to keep the underlying documentation work hidden.

Range::next_unchecked is private too, but we still mark it unsafe (which I found surprising,). Okay, the constructor cannot cause UB itself, but there's an implicit "class invariant" on Range (and many others), i.e. front and back are leaf edges (that's in their type already), point into the same tree (duh...) and front is not right of back (obviously?). If we don't specify how the constructor should be used, can we silently assume that the class invariant is honoured in Range::next_unchecked?

Ideally, the invariant should be documented at the type, and everything acting on its fields directly should have SAFETY comments explaining why this preserves the invariant. For unsafe methods, well it's up to them whether they require the invariant to already hold or not.

But the code here isn't yet up to that kind of standard. Also if this becomes more documentation changes I would ask you to split the PR, because I don't feel comfortable to review those.

Ideally, the invariant should be documented at the type

Where at the type? For a public type like Range, with private fields and safe public methods, the usual struct documentation seem a bad place to bother people with internal invariants. string/vec::from_raw_parts and vec::set_len also list invariants (actually, they are the only places in string and vec listing them), but these are unsafe methods. Finally I found in librustc/ty/free_region_map.rs a pub struct FreeRegionMap that features an invariant in the comments of a field.

src/liballoc/tests/btree/map.rs

ssomers · 2020-02-16T17:27:23Z

So I mixed 3 themes here:

the main problem and description (test_clone_from drags down Miri), i.e. a post-Implement clone_from for BTreeMap and BTreeSet #66648 patch
another post-Implement clone_from for BTreeMap and BTreeSet #66648 comment patch
other ways in which Miri is slowed down.

Which ones (if any) should I keep here?

RalfJung · 2020-02-16T17:33:02Z

I'm fine keeping them all, I just asked for a few more comments explaining your choices.

src/liballoc/tests/btree/map.rs

src/liballoc/collections/btree/map.rs

RalfJung · 2020-02-16T19:57:35Z

The PR LGTM now, except that it adds a few comments for which I cannot say if they are correct.

src/liballoc/tests/btree/map.rs

RalfJung · 2020-02-16T21:50:48Z

All right, that also does it. Thanks for bearing with me!

@bors r+

bors · 2020-02-16T21:50:49Z

📌 Commit da226dd has been approved by RalfJung

bors · 2020-02-17T03:24:59Z

⌛ Testing commit da226dd with merge 3c4590f...

@crgl

BTree: lighten the load on Miri Reduce the amount of work Miri ploughs through in btree code, in particular on `test_clone_from` (which takes up 5 minutes on my machine). r? @crgl

bors · 2020-02-17T06:44:29Z

☀️ Test successful - checks-azure
Approved by: RalfJung
Pushing 3c4590f to master...

Mark-Simulacrum reviewed Feb 2, 2020

View reviewed changes

JohnTitor added the S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. label Feb 3, 2020

ssomers force-pushed the btree_miri_relief branch from 2c85753 to b23f8e0 Compare February 3, 2020 16:58

RalfJung reviewed Feb 3, 2020

View reviewed changes

src/liballoc/tests/btree/map.rs Show resolved Hide resolved

rust-highfive assigned RalfJung Feb 16, 2020