The augment of "Unifying borrow and reborrow (conceptually) via access"

I read this Unifying borrow and reborrow (conceptually) via access tutorial, and I think it is very useful to understand the rule about general borrowing(including reborrowing). It introduced two principles with that:

  • Access of values may be bororwed, according to the diagram above
  • When a value is moved, assigned or is dropping out of scope, it must take back all of its access.

It seems an oversight that the rule didn't talk about borrowing/reborrowing, even though the topic mentioned them in the comments of the examples.

I think for borrowing/reborrowing, we may say

  • When a value is borrowed/reborrowed immutably, it must take back its write access if it ever had.
  • When a value is borrowed/reborrowed mutably, it must take back all of its access.
  • No requirement is imposed if the access is to a static value.
let mut i = 0;
let mrf = & mut i;
let rf = &i; // i should take back its write access since it ever had, hence mrf should drop here
println!("{mrf}"); // error
let mut i = 0;
let mrf = & mut i;
let reborrow = & mut *mrf;
let im_rf = &*reborrow;
let m_rf = & mut *reborrow;  // mutably reborrowed here, so `reborrow` should take back all of its access(including read access), hence `im_rf` should drop here
println!("{im_rf}"); // error

Finally, if a value didn't ever have the write access and it is borrowed/reborrowed immutable, no requirement will be imposed.

I think this augment should complete the "Unifying borrow and reborrow (conceptually) via access" principle. The exception is access the static value seems not to be governed by these rules.

	static mut i:i32 = 0;
	let mrf = unsafe {
		& mut i
	};
	let rf = unsafe {
		&i
	};
	println!("{mrf}"); //Ok

The example would have been an error if i had declared a non-static.

Update

Accesses are categorized to

1. move access
2. deallocation access

  1. owner access
  2. write access
  3. read access

Only read and write access can be (re)borrowed and the borrowee shall have the access it borrows. Borrowing read access borrows the copied one. Borrowing the write access transfers the access from borrowee to the borrower.

For any operation, the following rules are required:

  • For the move(semantically) or destruction operation, the operated value must at least have {move, deallocation} { owner } accesses.
  • For the assignment operation, the (LHS)assigned value must at least have { write } access.
  • For a read operation, the value must at least have {read} access.

For a value, they have the accesses as the following:

  • The owner value has {owner, write, read} accesses to the value.
  • The mutable borrowing value has { write, read } accesses to the referent.
  • The immutable borrowing has only { read } accesses to the referent.
  • When a value is moved(semantically), assigned, or is dropping out of scope, it must take back all of the accesses it has borrowed
  • When a value is borrowed/reborrowed immutably, it must take back its write access if it ever had.
  • When a value is borrowed/reborrowed mutably, it must take back all of its access it has borrowed.

All accesses mentioned in the above list refer to:

  • When the value is borrowed, the accesses to the value
  • When the value is reborrowed, the accesses to the referent of the value

When the borrowee tasks back the access, the borrower that borrows the access from the borrowee gives back that access. [Note: "borrowee" means the lender or the value from which the borrower borrows the access].

Reborrow occurs when we want to acquire access from a borrowing value B to access the referent of B.

Statics are still governed by this kind of rule, but the compiler doesn't check that you're following the rules. If you violate the rules, your program is simply incorrect, and the compiler might make optimizations that change the behavior of your program.

This is why accessing a static mut is unsafe.

You can try running your program under miri to see the problem. Open the playground and select miri under the tools dropdown, and you will get an error about having used unsafe incorrectly.

error: Undefined Behavior: trying to retag from <3058> for SharedReadOnly permission at alloc1[0x0], but that tag does not exist in the borrow stack for this location
    --> /playground/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs:2382:1
     |
2382 | fmt_refs! { Debug, Display, Octal, Binary, LowerHex, UpperHex, LowerExp, UpperExp }
     | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
     | |
     | trying to retag from <3058> for SharedReadOnly permission at alloc1[0x0], but that tag does not exist in the borrow stack for this location
     | this error occurs as part of retag at alloc1[0x0..0x4]
     |
     = help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
     = help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <3058> was created by a Unique retag at offsets [0x0..0x4]
    --> src/main.rs:4:3
     |
4    |         & mut i
     |         ^^^^^^^
help: <3058> was later invalidated at offsets [0x0..0x4] by a SharedReadOnly retag
    --> src/main.rs:7:3
     |
7    |         &i
     |         ^^
     = note: BACKTRACE:
     = note: inside `<&mut i32 as std::fmt::Display>::fmt` at /playground/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs:2376:71: 2376:78
     = note: inside `std::fmt::write` at /playground/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs:1208:17: 1208:59
     = note: inside `<std::io::StdoutLock<'_> as std::io::Write>::write_fmt` at /playground/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/io/mod.rs:1682:15: 1682:43
     = note: inside `<&std::io::Stdout as std::io::Write>::write_fmt` at /playground/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/io/stdio.rs:716:9: 716:36
     = note: inside `<std::io::Stdout as std::io::Write>::write_fmt` at /playground/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/io/stdio.rs:690:9: 690:33
     = note: inside `std::io::stdio::print_to::<std::io::Stdout>` at /playground/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/io/stdio.rs:1008:21: 1008:47
     = note: inside `std::io::_print` at /playground/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/io/stdio.rs:1075:5: 1075:37
note: inside `main`
    --> src/main.rs:9:2
     |
9    |     println!("{mrf}");
     |     ^^^^^^^^^^^^^^^^^
     = note: this error originates in the macro `fmt_refs` which comes from the expansion of the macro `println` (in Nightly builds, run with -Z macro-backtrace for more info)
2 Likes

That would sound like RefCell and mutable borrowing, multiple mutable borrowing can make the borrowing checker fail while multiple mutable borrowing from RefCell will make a panic in runtime but it does not cause the borrowing checker to fail.

Well, the thing is that a panic is defined behaviour. Mutating a static mut almost always (but not always) leads to UB, which is really bad.

1 Like

See the updated part.

Yes, UnsafeCell has a relaxation on some of these rules. In particular, having an &UnsafeCell<T> doesn't imply to the compiler that the data pointed to it cannot be mutated.

1 Like

Generally, modifying a RefCell is considered a read operation for the purposes of the borrow-checker.

This kind of thing where you can modify stuff using only immutable access is called interior mutability.

I think the conclusion I have summarized is suitable for checking common borrowing and owner, which does not consider interior mutability.

Generally, move and deallocation access is the same thing, so you always have both or neither.

Another thing to note is that std::mem::swap requires only write access, and not move access, even though you might want to consider it to be a move. Similarly, overwriting a value with a new one also only requires write access even though the old value is destroyed.

We may simplify move and deallocation access to a single one, called owned access.

Another thing to note is that std::mem::swap requires only write access, and not move access, even though you might want to consider it to be a move.

The move here means the move semantic in the compile-time, swap two values is not considered the move here.

Similarly, overwriting a value with a new one also only requires write access even though the old value is destroyed.

Yes, so, I said

*For the assignment operation, the assigned value must at least have {write} access.