Stacked Borrows: How precise should UnsafeCell be tracked?

Currently, when looking for UnsafeCell behind shared references, Miri descends through arrays, structs and the like, but does not descend through enums. Instead, when it sees an enum, it checks if T: Freeze, and if not, treats the entire enum as an UnsafeCell.

The benefit of this is that finding UnsafeCell does not require reading from memory (rust-lang/miri#931), which makes formal reasoning about Stacked Borrows a lot simpler. Accessing memory during UnsafeCell search opens all sorts of nasty questions, such as whether those accesses are themselves subject to Stacked Borrows rules or not (and if yes, which tag they use). Not reading enum discriminants also avoids potential confusion from Stacked Borrows partially checking the validity invariant of the referenced data.

On the other hand, being more precise with UnsafeCell search could help optimizations. When a function works on &Result<Cell<i32>, i32>, and the compiler somehow can know that the Err variant is active, we would be able to rely on this shared reference being read-only -- currently, that is not an assumption that the compiler can make. (But note that once a shared reference gets created to the i32 in the Err variant, that is already guaranteed to be read-only.)

This is somewhat related to #204.

Some posts with useful datapoints (not exhaustive):

Other parts of this question:

If we don't have strict subobject provenance, then what is the mutability of bytes outside the range of T?
Does UnsafeCell inside PhantomData have any effect?

To be precise, here is currently how we compute the permissions associated with a shared reference &T: we do recursive descend over T.

If we hit an UnsafeCell, the memory it covers is writable.
If we hit a field of type U such that U: Freeze, we stop searching for UnsafeCell here. This is purely an optimization, we could equivalently continue our descend, but we know that U: Freeze guarantees the absence of UnsafeCell.
If we hit a union or a type where variants is Variants::Multiple, and since we already checked Freeze, we treat memory this type covers as writable.
For other types (Variants::Single), we descend recursively through its fields.

Every location not marked as writable in the above procedure is marked as read-only.

For reasons similar to those brought up in #77, #84, and #253, I think the multiple variants case should consider the active variant, when determining runtime writability.
Consider the type Result<Cell<i32>,i32>, brought up in the original example. Under the model presented by lccc, in an object of that type, reguardless of the variant, there is a subobject of type i32. However, that subobject has the mutable characteristic (used to implement UnsafeCell) only when the result is Ok. Behind a shared reference, it should be reasonable to conclude that the value of this subobject does not change if you have the Err variant. This allows the movement/removal of reads behind a shared reference of this type when the variant is known to be Err (without loss of generality).

I cannot think of a particular example where this distinction would have an effect (one would probably use an external UnsafeCell, which does fun things anyways, and I've pretty much given up trying to optimize things inside an UnsafeCell, and focus my efforts on things outside of one).

FWIW, making UnsafeCell "maximally imprecise" would also help with issues like rust-lang/rust#98498, where currently the obvious fix is not sound because one of the fields of Scope is not an UnsafeCell.

In fact, even just making each field be in an UnsafeCell is not always sufficient to allow deallocating that reference, since the padding between the fields is not in an UnsafeCell.

So making use of the exception that is being added in rust-lang/rust#98017 is rather fragile currently, but would fairly very well if we don't attempt to track where inside a type the UnsafeCell are.

There is still a possible axiomatic alternative: treat padding even more weakly. All fields being UnsafeCell can be sufficient to say the whole struct is in UnsafeCell if you explicitly don't care about padding. Treating the answer to “is this padding byte in an UnsafeCell” as undefined isn't strong enough; that could resolve to always say no and be the same as today; I think you'd need to somehow say the answer is always yes but still somehow justify Freeze from lack of non-padding UnsafeCell.

I don't know exactly what this would look like, and it would probably break some important properties of Stacked Borrows — the simplest interpretation is probably to have a “padding” permission tag on the borrow stack for a byte reborrowed as padding, and then reading through a padding permission both returns an uninitialized byte and stores uninit. (Making a read perform a write is the certainly broken bit.)

Ultimately I'm also in favor of the weakening applied by UnsafeCell (and by analogy, PhantomPinned) applying to the entire pointee if the pointee type contains any UnsafeCell. As chorman has pointed out, this greatly limits the reasoning the compiler¹ can make about generic code, but giving that up this seems justified² by the operational specification simplifications gained.

What might be beneficial under such a model is splitting the UnsafeCell weakening into parts, so that you can remove the dereferencable_always(n) and noalias qualities individually.

But I want to point out that code authors can still make these assumptions in a generic environment due to privacy, encapsulation, and generally the concept of soundness of an API not considering outside uses of unsafe that break such. ↩
Especially since for better or for worse Rust already relies heavily on monomorphizations for performance. ↩

There is still a possible axiomatic alternative: treat padding even more weakly. All fields being UnsafeCell can be sufficient to say the whole struct is in UnsafeCell if you explicitly don't care about padding.

We could do something operational where if all fields of a struct are entirely UnsafeCell, then its padding is considered UnsafeCell, too.

What might be beneficial under such a model is splitting the UnsafeCell weakening into parts, so that you can remove the dereferencable_always(n) and noalias qualities individually.

Basically, separating its effect on protectors and permissions? Sure, that would be easy to represent.

As chorman has pointed out, this greatly limits the reasoning the compiler can make about generic code, but giving that up this seems justified

I actually think there might be a more insidious problem, if this includes the fact that you can get a &mut T to those fields (while the exterior can still be freely moved as a shared reference). If it's just mutability, then the loss in generic contexts actually affects non-generic contexts as well, since non-trivial validity attributes are salient parts of pointer types in XIR (if they weren't the same problem I mentioned before is trivial to recreate, since it basically involves smuggling a unique pointer into a function as a trivially-valid pointer type, which doesn't cause implicit derives, and thus allows you to alias it to another unique pointer passed into the same function, since the raw pointer in the second parameter is its direct parent).

We could do something operational where if all fields of a struct are entirely UnsafeCell, then its padding is considered UnsafeCell, too.

I'd be even fine with a more expansive restriction: Any contiguous extent of padding bytes that preceeds or follows an UnsafeCell gets SRW as well. Unlike actual fields, XIRs model doesn't let you just point to padding bytes the same way as a subobject (I mean, you can have a pointer to it, but not a pointer to it), which is where the problem would arrise.

If it's just mutability, then the loss in generic contexts actually affects non-generic contexts as well,

I don't see why that has to be the case, or why it would be the case in MIR+LLVM.

I'd be even fine with a more expansive restriction: Any contiguous extent of padding bytes that preceeds or follows an UnsafeCell gets SRW as well. Unlike actual fields, XIRs model doesn't let you just point to padding bytes the same way as a subobject (I mean, you can have a pointer to it, but not a pointer to it), which is where the problem would arrise.

Even precisely defining the notion of "padding byte" is super hard (and subtle), on top of the already subtle rules for how far we traverse looking for UnsafeCell, on top of the already super subtle aliasing rules... I think this is way overspending our complexity budget.

On Tue, Jun 28, 2022 at 09:52 Ralf Jung ***@***.***> wrote: If it's just mutability, then the loss in generic contexts actually affects non-generic contexts as well, I don't see why that has to be the case, or why it would be the case in MIR.

In XIR, pointer types consistent of a number of validity attributes and some definition attributes (pointer kind and syntax declaration kinds), and pointee type. Different attributes forms different pointer types that are incompatible with each other. An explicit conversion (called the derive operation) is necessary. This is because an implicit conversion is otherwise needed (else you can get a *T that is the same pointer as a *unique T, and which allows both to be passed to the same function) and I don't like doing non-trivial operations implicitly.

I'd be even fine with a more expansive restriction: Any contiguous extent of padding bytes that preceeds or follows an UnsafeCell gets SRW as well. Unlike actual fields, XIRs model doesn't let you just point to padding bytes the same way as a subobject (I mean, you can have a pointer to it, but not a pointer to it), which is where the problem would arrise. Even precisely defining the notion of "padding byte" is super hard (and subtle), on top of the already subtle rules for how far we traverse looking for UnsafeCell, on top of the already super subtle aliasing rules... I think this is way overspending our complexity budget.

Fair, though it encompasses the previous proposal. Since searching for Freeze itself is structural on a type, though, couldn't it just use the implicit Pad fields?

…

— Reply to this email directly, view it on GitHub <#236 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABGLD26CJRDU24DNQR672N3VRL7RTANCNFSM4N4GIRZQ> . You are receiving this because you commented.Message ID: ***@***.***>

In XIR,

Can you explain this without going into the specifics of XIR? As in, is there actually something fundamental here, or just a design quirk of XIR?

Fair, though it encompasses the previous proposal. Since searching for
Freeze itself is structural on a type, though, couldn't it just use the
implicit Pad fields?

There are no implicit Pad fields. Padding is the absence of a field at a given offset into a struct. (And something more complicated for enums.) At least that's how I prefer to think of it.

Can you explain this without going into the specifics of XIR? As in, is there actually something fundamental here, or just a design quirk of XIR?

It's fundamental, part of the type system. Especially for non-trivial validity, it changes how the pointers interact with certain operations, like being moved (particularily into a function, local, or a static, the same way that &mut T and &T do. And there are no implicit conversions in XIR, only weak ones with the convert instruction, especially when the conversion is as non-trivial as an implicit derive operation (which can best be described as being equivalent to a generalization of the reborrow operation - although as an instruction, derive is "Change pointer attributes and produce new pointer value").

There are no implicit Pad fields. Padding is the absence of a field at a given offset into a struct

Yeah, that's how I'd think of it as well. Parts of the object-representation that don't participate in determining the value.

I don't mean fundamental to XIR. I mean fundamental in a way that does not depend on the details of the language this is formalized in.

Context: I am mostly interested in XIR insofar as it teaches us general lessons that we might miss by taking a MIR/LLVM view, due to the quirks of those languages. I am much less interested in XIR itself. So if there is a lesson here that transcends XIR, I would like to learn it.

const analyzes how the value is constructed in many cases, so e.g. Option<Cell> = None is allowed.

TBH, this might have issues with the question presented here.

Or hmm... Miri at least seems to think that mutating a promoted constant, even an impl !Freeze one, is UB.

Promoted constants are put in read-only memory, so yeah their mutation is definitely UB. That's a different "source of UB" that &T-readonly-ness.

TBH, this might have issues with the question presented here.

Yeah there are definitely some interesting potential interactions.

There are at least 2 creates that rely on PhantomData being always Freeze, at least for the purpose of creating references in const-eval.

This doesn't necessarily impact the aliasing rules, I think, but it is still certainly useful to know.

Auto merge of rust-lang#128543 - RalfJung:const-interior-mut, r=fee1-…

Auto merge of #128543 - RalfJung:const-interior-mut, r=fee1-dead

I wonder if we could get most of the optimization benefits of precise UnsafeCell tracking without relying on runtime reads by making use of the information provided by some sort of pattern types mechanism to track the active variant statically.

use std::cell::UnsafeCell;

enum Enum {
    Freeze(u8),
    Unfreeze(UnsafeCell<u8>),
}

fn foo(e: &Enum) {
    match e {
        f @ Enum::Freeze(_) => { /* f statically known to not have `UnsafeCell` here, optimization can depend on it */ }
        u @ Enum::Unfreeze(_) => { /* u has `UnsafeCell` here */ }
    }
}

Potentially we could interpret Enum @ Freeze(u8) as a type without UnsafeCell, yeah.

I don't know whether what I am going to point out is necessarily 100% aligned with the topic of this issue or whether it is a bit orthogonal, but I was wondering about the interaction between static promotion of an enum instantiated with a "Freeze variant" despite there being other variant(s) which may be non-Freeze/containing UnsafeCells and whatnot.

let _: &Option<Cell<u8>> = &None; // the `None` is `static`-promoted

This is:

a stable Rust guarantee (we can 'static-annotate the aforementioned ref);
and very convenient;

but then I wondered about the interaction between this, and:

fn write_to_some_payload(
    opt: &Option<Cell<u8>>,
    value: u8,
)
{ unsafe {
    UnsafeCell::<u8>::raw_get(
        (&raw const *opt)
            .byte_add(mem::offset_of!(Option<Cell<u8>>, Some.0))
            .cast()
     ).write(value)
}}

// could be useful with a companion `unsafe fn read_from_some_payload`

if targeting a #[repr(Rust)] enum such as Option feels too dirty, we could easily imagine replacing these things with a #[repr(C and/or int)] enums, all the way down to unions (which do not get static-promoted even when instantiated with Freeze fields exclusively)<

Is write_to_some_payload():

blatantly unsound, as in, able to cause UB every time a (reference to a) None is fed to it?
or mildly unsound, as in, able to cause UB when fed a (reference to a) static-located None?

Running it with miri as of now seems to accept it when given a non-static-located None, whereas a static-promoted one does cause UB:

write_to_some_payload(&identity(None), 0); // No UB reported;
write_to_some_payload(&{ None }, 0); // UB! (and segfault when actually executed).

Playground

I can't find the source at the moment, but I do vaguely recall there being a decision that it's fine to forbid writes to values just based on that safe code can't write to it. To break the soundness of your example, consider that I could alias &None::<Cell<i32>> with &[MaybeUninit<u8>; 8] even for non-static places in order to retag the memory as immutably shared.

So I'd say somewhere between your blatant and mildly unsound: something untypical needs to be done, but those things are more useful and less surprising to allow.

But that only really covers const { &None }. In the case of static promoted &None, the promotion does change semantics¹, which promotion isn't supposed to do. For that, I recall discussing potentially deprecating !Freeze and requiring such to use const blocks, although I think with even just informal justification of that the type of a literal is more precise than the full type is sufficient to leave it as a default allow restriction style lint.

Assuming None is a literal of type Option<Cell<i32>> and not of refined type Option<Cell<i32>> is None, which as noted can potentially be treated as being Freeze. ↩

@danielhenrymantilla

@danielhenrymantilla I think you might be talking about #493?

Auto merge of #128543 - RalfJung:const-interior-mut, r=fee1-dead

Navigation Menu

Repository navigation

Stacked Borrows: How precise should UnsafeCell be tracked? #236

47 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Stacked Borrows: How precise should UnsafeCell be tracked? #236

Description

Activity

RalfJung commented on Jun 13, 2020

chorman0773 commented on Nov 2, 2020

RalfJung commented on Jun 26, 2022

RalfJung commented on Jun 26, 2022

CAD97 commented on Jun 26, 2022

Footnotes

RalfJung commented on Jun 26, 2022

chorman0773 commented on Jun 28, 2022

RalfJung commented on Jun 28, 2022

chorman0773 commented on Jun 28, 2022

RalfJung commented on Jun 28, 2022

chorman0773 commented on Jun 28, 2022

RalfJung commented on Jun 28, 2022

RalfJung commented on Jun 28, 2022

47 remaining items

chorman0773 commented on Aug 6, 2023

chorman0773 commented on Aug 6, 2023

RalfJung commented on Aug 6, 2023

RalfJung commented on Aug 14, 2023

Jules-Bertholet commented on Mar 20, 2025

RalfJung commented on Mar 20, 2025

danielhenrymantilla commented on Mar 20, 2025

CAD97 commented on Mar 20, 2025

Footnotes

RalfJung commented on Mar 20, 2025

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions