Unsoundness using experimental-multiple-mutable-borrows

[noamtashma]

Recently, looking at wackbyte's pull request made me look into this code again.

I found out this counterexample:

fn main() {
  GhostToken::new(|mut token| {
      let cell_of_array: GhostCell<[i32; 2]> = GhostCell::new([3, 7]);
      let array_of_cells = (&cell_of_array as &GhostCell<[i32]>).as_slice_of_cells();
      let second_cell = &array_of_cells[1];
      let (second_val, array) =
          GhostBorrowMut::borrow_mut((second_cell, &cell_of_array), &mut token).unwrap();
      println!("{}", *second_val);
      array[1] = -4;
      println!("{}", *second_val);
  });
}

[noamtashma]

I think this might be solved by ensuring that borrowed cells are nonoverlapping, instead of just ensuring that their first byte is different.

I also conjecture that the code would also be sound if the as_slice_of_cells method was removed.

However now I'm less sure that either of these is actually correct than I used to be sure that my original code was correct when I wrote it.

[matthieu-m]

First of all, thanks for the slew of soundness issues you opened!

In the wake of the discussions on sound projections, I had been thinking about how to implement projection for GhostCell, and the difficulties in ensuring the absence of overlap between the reachability graphs of various "roots" in the presence of projection.

I had not realized we already had a limited form of projection under the form of as_slice_of_cells, and that we were already in trouble in that regard.

In particular, while as_slice_of_cells is limited in the transformation it achieves, I only think its impact is, but I am not so sure. Specifically, I do not think that it is possible to obtain a pointer to an object outside the memory area of the backing array (following a pointer).

If the impact is limited, then the overlap between reachability graphs check is limited to an overlap between memory ranges check, which is fairly simple. If the impact is NOT limited, then we need to think about a more generic solution. Thus I believe our (known) options are:

1. Limited impact - projection within memory:
   • Remove as_slice_of_cells, and forego projections for now.
   • Switch check_distinct to an array of memory ranges (either pointer+pointer or pointer+size).
   • Enhance check_distinct with an array of ranges, on top of the array of single values.
2. Full impact:
   • Remove as_slice_of_cells, and forego projections for now.
   • Remove impl of GhostBorrowMut for slices.
   • Implement projection (and thus as_slice_of_cells) in a way compatible with GhostBorrowMut, somehow.

I do note that as_slice_of_cells being a limited projection (single-step) means that it may be possible to implement solutions for it that would not be generalizable for full projection: it would be possible to project & check distinctness at the same time, for example.

[noamtashma]

In the wake of the discussions on sound projections

Can you please elaborate on these discussions? Are you referring to this thread?

I do think that we only have "Limited Impact". In fact, I don't think we need to remove as_slice_of_cells at all.
I believe the essential problem, from the beginning, was assuming that checking the distinctness of the pointer was enough.
However, as I said before, I do think that checking distinctness of memory ranges is enough.

[noamtashma]

Here is an informal argument as to why it's probably correct: suppose you have

// Assume we have some inputs from somewhere
a_cell : &GhostCell<'brand, T1>;
b_cell : &GhostCell<'brand, T2>;
token : GhostToken<'brand>;
// We do a multiple mutable borrow:
let (a, b) = GhostBorrowMut::borrow_mut((a_cell, b_cell), &mut token);

And we want to know that a, b are recursively non overlapping, to convince ourselves that this is safe.
If a, b do overlap, then either

1. a, b overlap directly.
2. a overlaps with something reachable indirectly from b.
3. b overlaps with something reachable indirectly from a.
   There's a fourth option, of something indirectly reachable from a overlapping with something indirectly reachable from b. However, that should be impossible, since that would violate rust's single-ownership invariants.

For option 1. we can check directly (Not forgetting to check for the type's width this time around).
If we're in option 2, (and w.l.o.g. option 3), consider this code:

// Assume we have some inputs from somewhere
a_cell : &GhostCell<'brand, T1>;
b_cell : &GhostCell<'brand, T2>;
token : GhostToken<'brand>;
let b = b_cell.borrow_mut(&mut token);
let b_indirect_descendant = ... /* b's indirect descendant, overlapping with `a` */

At this point, we have access to both a_cell and b_indirect_descendant, which is overlapping with a_cell's interior. Which probably shouldn't be possible.

This almost shows that the original code was already unsound without GhostBorrowMut. That would imply that either option 2 is impossible in the first place, or that GhostCell itself is unsound, And therefore, that GhostBorrowMut is sound assuming GhostCell is sound.

However, There are multiple holes in this argument, some assumptions and some omissions.

[matthieu-m]

At this point, we have access to both a_cell and b_indirect_descendant, which is overlapping with a_cell's interior. Which probably shouldn't be possible.

I don't think that whether it overlaps with a_cell's interior is problematic, because as token is mutably borrowed, it's impossible to peek into a_cell's interior for as long as b (and therefore b_indirect_descendant) exists.

It is perfectly fine in Rust to have multiple references (both immutable and mutable) to the same piece of memory; the restriction is only about which of those references can be used at a time, and the GhostToken enforces this restriction in the absence of GhostBorrowMut.

I believe the essential problem, from the beginning, was assuming that checking the distinctness of the pointer was enough.

Indeed. In fact, even in the absence of ?Sized bounds on GhostBorrowMut, it was already problematic with fixed-size arrays.

However, as I said before, I do think that checking distinctness of memory ranges is enough.

I can't think of any situation where it wouldn't be -- absent "deep" projections -- so I'll experiment with range-checking.

[matthieu-m]

I created a "potential" fix in PR #26 however the branch is somewhat lackluster, and it's not clear it's the best approach to the problem.

I invite you to review the PR; and I'll leave this issue open in case the PR doesn't cut it, so this problem doesn't get lost.

[matthieu-m]

Fixed.