Skip to content

Relax Immutable semantics #1155

Open
Open
@joshlf

Description

@joshlf

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions