Tracking issue for Ref/RefMut::map_split

[joshlf]

Tracking issue for Ref::map_split and RefMut::map_split (feature refcell_map_split), implemented in #51466.

Blocking stabilization

• Performance (Optimize RefCell refcount tracking #51630)
• Proof of soundness (Add Ref/RefMut map_split method #51466 (comment))

cc @RalfJung @jhjourdan

[RalfJung]

Can I just say how awesome it is for people to actually be willing to block something on a proof of soundness? I love this community <3

[jhjourdan]

I have just completed the proof of soundness of this new feature:

https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/70db5cbf1f63879ff8171218d4ba679e8e4c69a2

Note, however, that our model do not model machine integer. Therefore, it is possible that our proof would not spot an overflow in the borrow counter that would cause an unsoundness. That said, causing an overflow in the borrow counter is very hard anyway.

[joshlf]

That's fantastic! Thanks so much for doing that! In your opinion, is integer overflow something we should be concerned about, or are you comfortable that it's not an issue even though the proof doesn't technically cover it?

@joshtriplett @dtolnay Anything left to do before proposing stabilization?

[joshtriplett]

Given recent events, I think it's rather reasonable to want to carefully examine the assumptions that integer overflow can't happen here.

Looking over the code, it appears that several of the overflow checks occur in a debug_assert! rather than an assert!, for instance.

[jhjourdan]

That's fantastic! Thanks so much for doing that! In your opinion, is integer overflow something we should be concerned about, or are you comfortable that it's not an issue even though the proof doesn't technically cover it?

Of course, a thorough review of the code cannot hurt. But actually, I cannot imagine a realistic scenario where this overflow would occur without causing an out of memory first (or using a lot of mem::forget calls for each of the created Ref/RefMut, which is also a weird thing to do).

[jhjourdan]

Looking over the code, it appears that several of the overflow checks occur in a debug_assert! rather than an assert!, for instance.

What overflow check are you speaking about? Reading the current state of the code, all the overflow checks are either is_reading(...) or is_writing(...) or self.borrow.get() == UNUSED, none of which check for overflow.

As far as I can tell, each incrementation or decrementation of the counter in this code is either guarded by an overflow check or cannot overflow because of the current sate of the counter.

[joshlf]

That's fantastic! Thanks so much for doing that! In your opinion, is integer overflow something we should be concerned about, or are you comfortable that it's not an issue even though the proof doesn't technically cover it?

Of course, a thorough review of the code cannot hurt. But actually, I cannot imagine a realistic scenario where this overflow would occur without causing an out of memory first (or using a lot of mem::forget calls for each of the created Ref/RefMut, which is also a weird thing to do).

Unsoundness is unsoundness, regardless of how pathological the program would have to be :)

But regardless, I don't think it's an issue. All overflow is checked by assert!s. The debug_assert!s only check for conditions which we, the programmers, believe should always be true. In particular:

• This one is in BorrowRef::drop, and asserts that the borrow is a reading borrow. BorrowRef is a reading borrow, so if it weren't true, it'd be a bug.
• This one is in BorrowRef::clone, and asserts that the borrow is a reading borrow. It's safe for the same reason as the previous one.
• This one and this one are in BorrowRefMut::drop and BorrowRefMut::clone respectively, check that the borrow is a writing borrow, and are safe for the same reason.

[joshtriplett]

@joshlf Thanks for clarifying! With that clarification on the debug_assert! calls, this LGTM.

[joshtriplett]

That said: could someone add a note to the comment at the top of that file, regarding checking for overflow, that any such overflow checks must be assert! and not debug_assert!, just to make it less likely that future changes accidentally make that mistake?

[Centril]

@sfackler shall we stabilize this perhaps?

[SimonSapin]

We previously had Ref::filter_map and removed it in #27746. If map_split is deemed useful enough for inclusion in the standard library, should filter_map be brought back? @rust-lang/libs what do you think?