google/zerocopy

Relax `Immutable` semantics

Opened this issue · 2 comments

Overview

Progress

  • Restrict Immutable documentation so that it requires recursive freedom from interior mutability, not just shallow
  • Relax Immutable documentation so that it refers only to interior mutability
  • Relax Immutable documentation so that it promises nothing to callers outside of zerocopy
  • Update this issue description based on this comment
  • Once Freeze is stabilized, consider whether or not Immutable needs to have the same semantics as Freeze
  • Once Freeze is stabilized, add section to Immutable documentation entitled something like "Why not Freeze?"
  • Get formal semantics of "interior mutability" documented in the Rust reference or stdlib docs
  • Document in the reference or stdlib docs that certain operations are guaranteed sound depending only on whether interior mutation happens at runtime, and not on whether the type system believes that UnsafeCells exist at certain offsets or covering certain ranges
  • Update Immutable documentation to refer to this formal notion of interior mutability
  • Update use sites to rely only on this soundness guarantee
  • Permit UnsafeCells in some places as appropriate (e.g., introduce a wrapper type which "disables" interior mutability)

Details

Intuitive definition of interior mutability + compiler optimizations

TODO:

  • Provide an intuitive description of interior mutability and discuss how it relates to the compiler's right to make certain assumptions or optimizations
  • Mention that there is currently no formal definition of interior mutability

Interior mutability vs UnsafeCells

TODO: Describe how interior mutability is implemented via UnsafeCells today, and justify our intention to relax Immutable's requirements in the future to only mention interior mutability, not UnsafeCells in particular.

Stacked Borrows, UnsafeCell overlap, and Ralf's future plans

TODO:

  • Describe how Stacked Borrows reasons about UnsafeCell overlap
  • Describe Ralf's intended formal semantics and how it diverges from Stacked Borrows

Immutable vs Freeze

EDIT: Maybe not? #1155 (comment)

TODO:

  • Explain why, in order to support general Safe Transmute, Immutable must be recursive, while the stdlib Freeze will not be recursive
  • Conclude that we can never replace Immutable with Freeze

@joshlf I'm a little confused why we need the different semantics from Freeze. If we have a type like:

struct Foo<'a> {
  a: u32,
  b: &'a UnsafeCell<u64>,
}

It will be Immutable, but not FromBytes or IntoBytes, so it doesn't seem like we would run into problems with the various transmute methods? Or am I missing something?

Second unrelated question: do we need a Self: Immutable bound for something like IntoBytes::as_mut_bytes()? It seems like IntoBytes and FromBytes would be enough. Obviously, Immutable is needed for something like IntoBytes::as_bytes().

EDIT: Are the current bounds related to rust-lang/unsafe-code-guidelines#495 ?

@joshlf I'm a little confused why we need the different semantics from Freeze. If we have a type like:

struct Foo<'a> {
  a: u32,
  b: &'a UnsafeCell<u64>,
}

It will be Immutable, but not FromBytes or IntoBytes, so it doesn't seem like we would run into problems with the various transmute methods? Or am I missing something?

TLDR: You've prompted @jswrenn and me to reconsider, and we might actually go back to considering Immutable to be shallow, and thus equivalent to Freeze.

The reason has to do with future compatibility with safe transmute, which will permit T -> U transmutation on types which are not IntoBytes or FromBytes on their own. E.g. while your Foo is not FromBytes, safe transmute would permit transmuting some types into Foo, and so we'd need a way of banning certain transmutations which are valid except for interior mutability.

The reason we've considered walking this back is that safe transmute will have its own trait (such as this one) which is completely separate from FromBytes/IntoBytes/etc, and the interior mutability analysis will be built-in to the compiler support for that trait. For that reason, Immutable/Freeze will be entirely redundant in the context of full safe transmute, and so we only need to consider Immutable in relation to the traits we have today. In today's world, your argument holds, so we're considering reverting to shallow rather than recursive analysis.

Second unrelated question: do we need a Self: Immutable bound for something like IntoBytes::as_mut_bytes()? It seems like IntoBytes and FromBytes would be enough. Obviously, Immutable is needed for something like IntoBytes::as_bytes().

EDIT: Are the current bounds related to rust-lang/unsafe-code-guidelines#495 ?

Exactly. In particular:

  • Stacked borrows treats it as UB to change your mind about whether a given byte range is covered by UnsafeCell even if you never load or store from that memory
  • Per rust-lang/unsafe-code-guidelines#495, we don't currently know how to prove that something like &mut UnsafeCell<T> -> &mut T is sound, or even whether it's possible to prove that it's sound based on what's currently guaranteed by the language docs. That conversation is ongoing, and I owe Ralf a response to his latest comment 😛