Should validity of a reference depend on the *contents* of memory in any way?

[RalfJung]

This discussion presupposes that "Do we have full recursive validity for references" (#412) is answered "no".

As @digama0 points out, lots of weaker variants of "validity depending on memory contents" are conceivable. Probably the most strict one is "full recursive validity except inside shared UnsafeCell". We could also imagine "only follow one indirection" and all sorts of other variants.

[RalfJung]

My own opinion is that no, validity should not depend on the contents of memory in any way. It might (at least effectively) depend on whether there is dereferenceable memory at a given location at all (see the issues tagged A-dereferenceable), but that is all we should have.

My main argument is that I want to keep reasoning about whether code has UB as local as possible, so other threads changing the contents of memory shouldn't make a reference suddenly be invalid. Deallocation being able to invalidate references is bad enough, but that falls out of the aliasing model fairly naturally. (I view dangling references as causing UB on the next retag, not the next typed copy.) I don't see a strong enough reason to also let any write possibly invalidate references, and I don't see an elegant way that this requirement would even arise (considering a MiniRust-like framework).

(Some of) the arguments in #346 also apply. In particular, even 1-level validity behind &mut would make a lot of existing uses of Read UB; we should have a really good reason to break such code and a good plan to helping people find and fix such code. We did something like that with mem::uninitialized and it was not pleasant.

[RalfJung]

Anyway this issue is not about retags! This issue is about whether we want to require any kind of validity of in-memory data beyond what is imposed by retags (which is just dereferencability).

[chorman0773]

Anyway this issue is not about retags! This issue is about whether we want to require any kind of validity of in-memory data beyond what is imposed by retags (which is just dereferencability).

I'd argue that the only place it makes sense to assert validity is on retags and activation (except maybe #84 stuff at invalidation of certain references), so that would make retags relevant to the discussion.

[RalfJung]

Are you saying that retagging should do more than what is necessary for the alias model (which amounts to checking dereferencability)?

[chorman0773]

Are you saying that retagging should do more than what is necessary for the alias model (which amounts to checking dereferencability)?

I'm saying that if we are requiring the validty of referents, then retags are the most logical place for them. Otherwise, if you project: &Cell<Option<T>> into Option<&Cell<T>>, which I could see as being a perfectly valid unsafe operation, we have to ask what happens to the &Cell<T> when you do orig.set(None). Under TB IIRC, It's still Reserved after the other Cell becomes Active, but if that Reserved still actively requires validity, we've introduced UB into the code by keeping the reference valid. So if that projection is sound provided the static lifetime is enforced, validity of references only can be be a finite number of times per - IMO, retags are the place that most makes sense to happen.
This could just as easily be an argument against recursive validity, as well.

[RalfJung]

which I could see as being a perfectly valid unsafe operation,

(In general this is wildly unsafe because Cell blocks niches, so the layout could be entirely different.)

t if that Reserved still actively requires validity, we've introduced UB into the code by keeping the reference valid

I have no idea what you mean by "actively requiring validity" here or how there is UB here.

Again, this issue is about contents being valid, so the aliasing state shouldn't even come in. Is it insta-UB to have a &bool that points to 3? That's the kind of question we are considering here. Such insta-UB usually arises (in my view) from doing a typed load (converting the in-memory representation into a higher-level "value" representation). I don't think we want to have that value representation being recursive through references though.

I guess we could have retagging create such a high-level value representation of the pointee. Is that what you mean? With interior mutability however we'd have to "leave a hole" in that representation at any place where there is an UnsafeCell, so it'd not be a proper value either.

[python-ast-person]

Is it insta-UB to have a &bool that points to 3?

I would say yes because my definition of the validity requirement of a shared reference is that, at any point while the reference is live:

• it must be sound to load the value behind the reference.
• the loaded value must satisfy all validity requirements.

This definition would require UnsafeCell to downgrade all validity requirements to safety requirements to allow Mutex<bool> to be sound.

[Nadrieril]

Something I have not seen mentioned: any kind of recursive validity implies that a self-referential struct would have a coinductive validity invariant. That sounds unpleasant to model.

[RalfJung]

Yeah, one could use interior mutability to set up a cycle of shared references and then transmute the Cell away -- that should be sound and validity would then be cyclic.