From 21e2ac55d74474e79efbe610cb00f7453807c9cf Mon Sep 17 00:00:00 2001 From: HeroicKatora Date: Thu, 19 May 2022 19:47:54 +0200 Subject: [PATCH] Note on shared references to Pod-like types (#106) * Note on shared references to Pod-like types * Expand explanation of no-interior-mutability --- src/anybitpattern.rs | 9 ++++++++- src/no_uninit.rs | 7 +++++++ src/pod.rs | 7 +++++++ 3 files changed, 22 insertions(+), 1 deletion(-) diff --git a/src/anybitpattern.rs b/src/anybitpattern.rs index 2984db2..5e1fb88 100644 --- a/src/anybitpattern.rs +++ b/src/anybitpattern.rs @@ -3,7 +3,7 @@ use crate::{Pod, Zeroable}; /// Marker trait for "plain old data" types that are valid for any bit pattern. /// /// The requirements for this is very similar to [`Pod`], -/// except that it doesn't require that the type contains no uninit (or padding) bytes. +/// except that the type can allow uninit (or padding) bytes. /// This limits what you can do with a type of this kind, but also broadens the /// included types to `repr(C)` `struct`s that contain padding as well as `union`s. Notably, you can only cast /// *immutable* references and *owned* values into [`AnyBitPattern`] types, not @@ -37,6 +37,13 @@ use crate::{Pod, Zeroable}; /// [Infallible](core::convert::Infallible)). /// * The type must be valid for any bit pattern of its backing memory. /// * Structs need to have all fields also be `AnyBitPattern`. +/// * It is disallowed for types to contain pointer types, `Cell`, `UnsafeCell`, atomics, and any +/// other forms of interior mutability. +/// * More precisely: A shared reference to the type must allow reads, and *only* reads. RustBelt's +/// separation logic is based on the notion that a type is allowed to define a sharing predicate, +/// its own invariant that must hold for shared references, and this predicate is the reasoning +/// that allow it to deal with atomic and cells etc. We require the sharing predicate to be +/// trivial and permit only read-only access. /// * There's probably more, don't mess it up (I mean it). pub unsafe trait AnyBitPattern: Zeroable + Sized + Copy + 'static {} diff --git a/src/no_uninit.rs b/src/no_uninit.rs index 8aeed66..ae628cb 100644 --- a/src/no_uninit.rs +++ b/src/no_uninit.rs @@ -42,6 +42,13 @@ use crate::Pod; /// all other rules end up being followed. /// * Enums need to have an explicit `#[repr(Int)]` /// * Enums must have only fieldless variants +/// * It is disallowed for types to contain pointer types, `Cell`, `UnsafeCell`, atomics, and any +/// other forms of interior mutability. +/// * More precisely: A shared reference to the type must allow reads, and *only* reads. RustBelt's +/// separation logic is based on the notion that a type is allowed to define a sharing predicate, +/// its own invariant that must hold for shared references, and this predicate is the reasoning +/// that allow it to deal with atomic and cells etc. We require the sharing predicate to be +/// trivial and permit only read-only access. /// * There's probably more, don't mess it up (I mean it). pub unsafe trait NoUninit: Sized + Copy + 'static {} diff --git a/src/pod.rs b/src/pod.rs index 085f8d3..a612f0f 100644 --- a/src/pod.rs +++ b/src/pod.rs @@ -26,6 +26,13 @@ use super::*; /// * The type needs to be `repr(C)` or `repr(transparent)`. In the case of /// `repr(C)`, the `packed` and `align` repr modifiers can be used as long as /// all other rules end up being followed. +/// * It is disallowed for types to contain pointer types, `Cell`, `UnsafeCell`, atomics, and any +/// other forms of interior mutability. +/// * More precisely: A shared reference to the type must allow reads, and *only* reads. RustBelt's +/// separation logic is based on the notion that a type is allowed to define a sharing predicate, +/// its own invariant that must hold for shared references, and this predicate is the reasoning +/// that allow it to deal with atomic and cells etc. We require the sharing predicate to be +/// trivial and permit only read-only access. pub unsafe trait Pod: Zeroable + Copy + 'static {} unsafe impl Pod for () {}