Tracking Issue for feature(pin_static_ref): Pin::{static_ref,static_mut}

[m-ou-se]

Tracking issue for #![feature(pin_static_ref)], as added by #77726.

Interface:

impl<T: ?Sized> Pin<&'static T> {
    pub const fn static_ref(r: &'static T) -> Pin<&'static T>;
}

impl<T: ?Sized> Pin<&'static mut T> {
    pub const fn static_mut(r: &'static mut T) -> Pin<&'static mut T>;
}

@rustbot modify labels: +B-unstable +C-tracking-issue +T-libs

[Lucretiel]

Sorry for my ignorance, but how is this sound? It seems to trade on the idea that &'static mut can never be moved out of, but I don't see any reason that should be case? Can you not mem::swap a pair of &'static mut T?

EDIT: Thanks for your help everyone, it turned out I had a flawed understanding of how reborrowing works. Cheers

[eddyb]

This has been resolved elsewhere, but effectively you cannot both call Pin::static_mut(r) and use r ever again - that would (roughly) amount to copying r, which would never be allowed for &mut T in general.

It's a bit subtle, but once you create a &'a mut U (or even &'a U) from a &'a mut T, since the 'a is the same in both, they cannot be distinguished at the typesystem level, and so the original has to be considered "perma-borrowed for 'a" (which when 'a = 'static means "forever") to be able to disallow one (the original) and allow the other (the new one), since otherwise the types look the same.

(I would love to have a compiler with one specific borrow exception, to demonstrate what exactly would be broken)

Also, IIRC there was a soundness issue with &'static mut T at some point (largely due to it not being a type you could ever really have values of, pre-Box::leak), but I'm pretty sure it got resolved long ago.

[tmandry]

Can you not mem::swap a pair of &'static mut T?

I had this question as well.. the answer is that you can. But once you put your &'static mut T in a Pin you can never "get it out" again. Nor can you have any other reference to the original value, crucially, since (as @eddyb described) a &'static mut T reference must be the only valid reference to that value.

[RalfJung]

Pin::static_mut is fine, I think

Pin::static_ref, on the other hand, I think is potentially problematic. You can think of pinning as a "typestate", and the type can have its own separate custom invariants for the "pinned" and "unpinned" typestates. The Pin::static_ref function may assume that &'static T points to something that satisfies the "unpinned" typestate invariant, and has to now prove that it also satisfies the "pinned" typestate invariant. I don't see any way to justify this. I haven't constructed a counterexample yet, either, but I would tread very carefully around this method.

[m-ou-se]

Hm, interesting. Pin::static_ref was the one I needed. I only added Pin::static_mut for completeness.

Use case (e.g. in the standard library):

static MUTEX: MutexThatGetsVeryAngryIfItIsMoved = ...;

impl MutexThatGetsVeryAngryIfItIsMoved {
    pub fn lock(self: Pin<&Self>) -> ... { ... }
}

fn something() {
    let guard = Pin::static_ref(&MUTEX).lock();
    ...
}

Instead of having all its methods unsafe with the requirement that it hasn't been moved, the methods require Pin<&Self> and can be safe. Pin::static_ref can be used on statics, because the 'static lifetime already promises that the thing won't move.

[RalfJung]

I think this is a (contrived) counterexample, demonstrating that Pin::static_ref is a breaking change:

// Invariant: the integer is 0, except behind shared *unpinned* references it can be whatever.
// There is no `&self` operation so we do not care about those values.
struct Nasty(i32);

impl Nasty {
    pub fn new() -> Self {
        Nasty(0)
    }
    
    pub fn new_shared() -> &'static Self {
        // We seem to violate the invariant here, but there is no operation
        // on `&self` so this is not a problem.
        &Nasty(1)
    }
    
    pub fn check(self: Pin<&Self>) {
        // It would be sound to cause UB for non-0 values here.
        // IOW, this assertion can never fail (for safe callers).
        assert!(self.0 == 0);
    }
}

With Pin::static_ref I can make the assertion fail: Pin::static_ref(Nasty::new_shared()).check().

The example is somewhat similar in spirit to those examples which show that Sync does not imply Send: if there is no operation on &self, the invariant associated with those values can be degenerate.

Of course this is a contrived example, but it does demonstrate that adding Pin::static_ref alters the logical contract associated with pinning.

[m-ou-se]

Is that really a promise that Pin makes though?

https://doc.rust-lang.org/stable/std/pin/struct.Pin.html#safety does not really explicitly state that.

It only says:

A value, once pinned, must remain pinned forever

where pinned is defined a bit above as

pinned, meaning that the data will not be moved or its storage invalidated until it gets dropped

By that definition, the T in a &'static T is pinned, regardless of whether there's a Pin<> wrapper around it.

[RalfJung]

The current docs don't say either way. Being English-language as opposed to formal docs, they don't make sufficiently explicit what exactly the requirement is.

Adding Pin::static_ref imposes a new proof obligation on all unsafe code that defines custom pinning-related invariants for types it exports: if the unpinned shared invariant is satisfied for lifetime 'static, then the pinned shared invariant must be satisfied for lifetime 'static. Nothing in the current docs indicates that this might be a proof obligation unsafe code has to uphold. Hence I argue my example is fine under current Pin.

This would also be the first proof obligation that special-cases the 'static lifetime -- so I don't think I like it. It feels like an ad-hoc hack to me.

(FWIW, I agree that the current docs also don't rule out Pin::static_ref. This situation is known as "independence" in mathematics: the rules as stated do not suffice to confirm or deny the statement. Famously, the axiom of choice is independent from Zermelo–Fraenkel set theory. However, adding a new proof obligation to custom type invariants is a big deal as it affects all code.)

[m-ou-se]

With your example, someone can currently already do

let r = Nasty::new_shared();
// SAFETY: We know for sure *r is never invalidated or moved (or even modified at all).
let p = unsafe { Pin::new_unchecked(r) };
p.check();

Which should be perfectly fine according to the current documentation, right?

[RalfJung]

The docs for new_unchecked say

If the constructed Pin<P> does not guarantee that the data P points to is pinned, that is a violation of the API contract and may lead to undefined behavior in later (safe) operations.

new_shared returns a shared reference that is not "pinned", in the sense that it does not satisfy the pinning invariant. You don't get to assume what it means for other types to be "pinned", this can vary greatly depending on the type. (This is similar to "shared", where what it means to share an i32 is very different from what it means to share a Cell<i32>. You don't get to assume what it means for other types to be "shared".)

Is that really a promise that Pin makes though?

The thing is, what you rely on with Pin::shared_ref is also a promise that Pin does not make.

[m-ou-se]

new_shared returns a shared reference that is not "pinned",

'Pinned' is defined both here and here as a property of a pointee (not of a pointer), specifically that it won't be moved/invalidated/deallocated. So the object referred to by the reference returned by new_shared() is pinned. Therefore we're allowed to wrap references/pointers to that object in Pin<>. I don't see how to read the Pin documentaiton in any other way.

[RalfJung]

it won't be moved/invalidated/deallocated

This is sufficient but not necessary for something to be pinned. This describes consequences of the entire pinning setup. But the underlying concept of the "invariant of the pinned typestate" is what makes this actually precise. And the notion of "moving data" does not come up there. Since data consists just of a-priori meaningless bytes, it is entirely unclear what "moving data" should even mean.

The pointee returned by new_shared is not pinned, and this statement has nothing to do with whether data is moved around or anything like that. The data is just 1 anyway, so "moving" this data is equivalent to storing a 1 somewhere. But it's not the data that matters, it's the invariants and the ownership they attach to this data.

By the arguments you are using (in very broad analogy), interior mutability is unsound because "data behind a shared reference is read-only" so I can always memcpy it away. (For non-Copy types I cannot use both the original and the copy, but I am allowed to do the copy.) But in practice this memcpy can lead to UB because types like AtomicI32 exploit the concept of "sharing" for their own purpose, making shared data actually not read-only but attaching their own meaning to the idea of "sharing". Nasty does the exact same thing with pinning -- it exploits the structure of the type system and Pin type to attach its own meaning to "pinning".
What I am trying to say is that it is very dangerous to make statements of the form "all types satisfy X" -- statements such as "for all types, when you share them they are read-only", or "for all types, when you have a 'static shared reference to them they are pinned".

[RalfJung]

FWIW, the principle behind this your example

let r = Nasty::new_shared();
// SAFETY: We know for sure *r is never invalidated or moved (or even modified at all).
let p = unsafe { Pin::new_unchecked(r) };
p.check();

is even stronger -- I think you are basically saying that for shared data (types behind a shared reference), "pinned" or "not-pinned" must be equivalent. At this point we might as well add a safe method to turn &T into Pin<&T> -- for any lifetime, not just 'static. That would at least be less ad-hoc than doing this only for 'static. Basically we'd say there are just 3 typestates: owned, pinned, shared -- no separate "shared pinned" vs "shared unpinned".

I'm not on the top of my game today, but on first sight it seems to me this is what happens... also see chapter 3 of this blog post where I mused about the "shared pinned" typestate. Back then my model did not have it, but that post contains an example that needs it.

[m-ou-se]

By the arguments you are using (in very broad analogy), interior mutability is unsound because "data behind a shared reference is read-only"

No, we don't document shared references like that. Where is that quote from?

---

On your blog post you say:

The core piece of the pinning API is a new reference type Pin<'a, T> that guarantees that the data it points to will remain at the given location, i.e. it will not be moved.

which matches with the definition of 'pinned' in the std documentation.

At this point we might as well add a safe method to turn &T into Pin<&T> -- for any lifetime, not just 'static.

Huh, that makes no sense to me. Pin implies that the thing it points to does not get moved until it is dropped. No lifetime other than 'static is gauranteed to last until an object is dropped.

I think you are basically saying that for shared data (types behind a shared reference), "pinned" or "not-pinned" must be equivalent.

Shared data with a static lifetime. And as far as I know, we don't define 'not-pinned' or 'unpinned' anywhere, other than just the possible absence the guarantee that something is pinned.

[RalfJung]

On your blog post you say:

"Pin guarantees X" does not mean "Pin is equivalent to X". It means "Pin implies X".

So this does not define Pin to be X, not at all.

For example: bool guarantees that the byte of that type does not have the value 0xFF.

[m-ou-se]

This discussion is going nowhere. I give up for today.

[RalfJung]

No, we don't document shared references like that. Where is that quote from?

Many Rust tutorials explain shared references as read-only. For example, from the Rust book.

Just as variables are immutable by default, so are references. We’re not allowed to modify something we have a reference to.

Note that the reference docs link there.
"Data is either mutable or shared, but never both" is the first thing we teach people about the Rust type system. And then later we explain there is an exception. But the thing is, if we just consider the core language (without any library code), "Data is either mutable or shared, but never both" is a strictly correct statement! It is a library-only concept to make sharing "interesting".

It was one of the key insights of RustBelt that sharing really is its own invariant. The very same happens with pinning.

Huh, that makes no sense to me. Pin implies that the thing it points to does not get moved until it is dropped. No lifetime other than 'static is gauranteed to last until an object is dropped.

I might have spoken nonsense here, I'll re-think this once I am of a fresh mind.

[RalfJung]

This discussion is going nowhere. I give up for today.

Ah, you wrote this while I was typing. ;) I agree we need to change our approach.

Taking a step back here, we are using entirely different vocabulary to talk about the same thing. So each of us repeating ourselves over and over is not going to lead anywhere. I am not sure how to make progress, but I will think about finding more examples -- I've found those to be a great vehicle for conveying all the subtleties that surround a formal model of a type system like Rust's.

You have articulated why you think Pin::static_ref is a correct addition, and while I do not agree with the arguments since I think they are based on a too informal reading of our docs (to be fair, we only have informal docs), I think I understand them. I am just trying (and clearly failing) to explain that those arguments do not work any more once one translates everything into a formal language -- or rather, they only work after making an extra assumption. "Pinned data cannot be moved" might be a great intuition, but I think it is entirely useless as a formal definition -- I literally have no idea how to make it formal.

What would help me is if you could try to explain what you think is wrong with this type. Which part of the pinning docs is violated by defining a type like this, and performing this kind of reasoning? This is the same kind of reasoning that underpins all formal soudness arguments for Rust types with internal unsafety.

What I claim is that both Nasty and Pin::static_ref violate no part of the pinning docs -- but together, they are clearly unsound. This is not the first time that such a situation has come up in Rust, for example when ManuallyDrop was added that resulted in an existing crate becoming unsound -- neither ManuallyDrop nor that crate violated any docs (they were fine on their own), but putting them together leads to unsoundness. Each time that happens, we are at a fork in the road and need to make a choice for the languages as a whole, and that choice will affect the fundamental structure of Rust type invariants. So far, we always erred on the side of requiring less from Rust type invariants, giving more freedom to which kinds of invariants a type can define. If we accept Pin::static_ref, that would be the first time that we restrict Rust type invariants (ruling out, in particular, the invariant underlying Nasty). I'm not saying this is bad, I am just pointing out the consequences for formal reasoning here.

[eddyb]

(EDIT: I'm adding this note before sending the comment, but do note that I started writing it a few comments earlier in the thread)

@RalfJung I'm trying to understand this thread, so correct me if I'm wrong, but it sounds like:

• you have a model where pinning is typestate
• the docs don't strongly agree or disagree with that model necessarily
• users relying on the model could have made a library using unsafe code in the vein of Nasty from upthread
• Pin::static_ref is not sound under that model

Now, there are three things I think we can all agree are important:

1. the documentation is as clear as we can make it, and we don't leave room for ambiguity
2. formal models (RustBelt/Stacked Borrows) have to be able to distinguish what we consider "correct Rust code"
3. not breaking existing unsafe code out there needlessly

And given the above discussion I have these questions:

1. is there any way to document the additional restrictions/guarantees that the model appears to have?
   • at a glance, it seems like starting with having ownership of the value is sufficient, but I doubt it's necessary?
2. how hard would it be to allow Pin::static_ref into the model? (this is even more relevant because of 3.)
3. what are the chances users came to the conclusion that Nasty is correct, as opposed to Pin::static_ref?
   • the existence of this feature and my own informal reading align with Pin::static_ref way more than Nasty
   • Pin::static_ref itself already has unstable uses, and its definition may have been copied by stable users
   • Nasty strongly resembles some other examples I've seen in the past (&NotSync promotion to 'static), and they have in common the fact that "constructability of types referring to StrangeInvariants, but not owning it" is being assumed to be fixed based on what's possible in the language at the time, to an extent I personally would probably avoid (tho I can't speak for the community as a whole, or anyone in particular, really)

[Lucretiel]

"Data is either mutable or shared, but never both" is a strictly correct statement!

No, I'm sorry, but it's not. Formally, references are either shared or unique; mutability is orthogonal to this. There are several types that are safe to mutate through shared references (the cells, atomics, mutexes), and in general shared mutability is fine so long as the other rust soundness guarantees are upheld. Shared references being immutable is basically only a convention, albeit one that's assumed by the compiler and optimizer and requires UnsafeCell as an escape hatch.

[RalfJung]

@Lucretiel I am well aware. And yet, the borrow checker is entirely based on the idea that shared data is immutable; that is the justification for allowing shared references to be accessible from many functions and even threads. It just happens to be the case that we can slightly break that rule, and mutate some shared state under careful restrictions. The justification for this is extremely tricky -- the only proposal so far that properly justifies this is based on a form of "typestate" where shared data is subject to a separate invariant that needs to be suitably related to the "fully owned" "default" typestate. Almost all formal models of Rust ignore this, and just declare shared data to be read-only -- which is entirely correct if you only consider the borrow checker itself; it only breaks down once you also consider the standard library! (I am ignoring noalias-based optimizations here so we do not have to worry about UnsafeCell/Freeze -- those are relevant for the optimizer but not the type checker.)

So, what essentially happens here is that types like Cell "abuse" the type system and slightly bend the ways it usually works. Rust without Cell and friends is perfectly conceivable, and the type system would be exactly the same -- just its interpretation would b slightly different.

Shared references being immutable is basically only a convention, albeit one that's assumed by the compiler and optimizer and requires UnsafeCell as an escape hatch.

If it's assumed by the compiler then it's not a convention, it's part of the fudamentals of the language. :)

So really, it's the other way around: the fact that we can mutate shared data is just a convention, and it works as long as we are sneaky enough about it such that the type checker doesn't have to notice.

@eddyb

you have a model where pinning is typestate

Indeed, we follow the same approach that already worked so well for shared references to explain interior mutability. I don't know any other way to model pinning (or interior mutability), so I think it is fair to say that both of them are typestate in disguise -- even if their designers might not have realized this.

is there any way to document the additional restrictions/guarantees that the model appears to have?

I assume "let people learn Iris and show them the formal definition" is not an acceptable answer? ;)
FWIW, we have the same problem with shared references. But either people are less creative in how those are (ab)used, or design space is more "tied down" there due to the compiler knowing more about shared references than it does about Pin.

I have sketched what I think the model should be in a blog post. That model is enough to give rise to guarantees like "pinned data cannot be moved" (for some reasonable interpretation(s) of what that statement actually means). It is also enough to justify safe API encapsulation for some simple self-referential data structures. I think it appropriately captures the intuition behind Pin, but this discussion shows that there is some wiggle room left.

how hard would it be to allow Pin::static_ref into the model? (this is even more relevant because of 3.)

It basically requires adding another "axiom" to the set of rules that the typestate needs to satisfy. This is allowing static_ref "by fiat": we directly require each and every author of a type that uses pinning to justify static_ref for their type. I don't know a better way to do this -- I don't know some other, nicer principle from which this would be a consequence.

Nasty strongly resembles some other examples I've seen in the past (&NotSync promotion to 'static), and they have in common the fact that "constructability of types referring to StrangeInvariants, but not owning it" is being assumed to be fixed based on what's possible in the language at the time, to an extent I personally would probably avoid (tho I can't speak for the community as a whole, or anyone in particular, really)

I mentioned this is similar to examples showing that Send does not imply Sync -- is that what you had in mind? Rust could totally have just declared "by fiat" that Send implies Sync, which would have been another typestate axiom (probably a rather awkward one). It did not though, the counterexample(s) were enough to stop those suggestions. Now with static_ref the situation is very similar, except it seems this time there is more demand for actually adding the required axiom.

The rules that these typestates need to satisfy are necessarily a two-sided contract -- whoever defines a type with a custom invariant needs to ensure their typestate is sufficiently well-behaved; whoever is working with other people's types needs to not make any assumptions about their typestate beyond that basic notion of "well-behavedness". I think it is natural to make the list of axioms the typestate needs to satisfy as small as possible -- interior mutability shows that this provides a fertile breeding ground for creative (ab)use of existing types; and we could spend a lot of time thinking of more or less "reasonable" axioms we could add without any idea if those could ever be useful. (Also more axioms means more proof obligations for unsafe code authors.)

So I think I want to push back on this 'assumed to be fixed based on what is possible in the language at the time' -- we have to fix the axioms somehow, so we make a kind of survey to see what axioms are needed and then cut that down to the barest minimum possible. I think this leads to much more informative and useful models than the alternatives (I am not even really sure what those alternatives would be).

[RalfJung]

All that said, I don't feel like I have understood Pin<&T> well enough yet. So I'd like to solicit some help from the pinning experts in the room. :)

Future, the original motivation for Pin, only involves Pin<&mut T>. The small examples we considered in our formal model, including an intrusive linked list, also don't use Pin<&T>. So it would be great if someone could point me to examples where Pin<&T> is used in interesting ways.

Concretely, my question is: would anything go wrong if we added an operation that converts &'a T to Pin<&'a T>? I can certainly imagine examples where that would go wrong, but as my previous example shows me imagining something is not sufficient. ;) So, is there any real-world use of Pin that would have a problem with such a conversion function?

This may sound like a strange question when the intuition is entirely around whether "data is moved", but from a typestate perspective this is actually a rather obvious question: are there two separate "shared unpinned" and "shared pinned" typestates, or are those the same? This is not a question that the formal model can answer, it is a question that Rust has to decide about and then the formal model can reflect that answer. If the two typestates are identical -- if converting &'a T to Pin<&'a T> indeed does not cause problems -- then of course static_ref would also be trivially sound.

In the past, I felt like that conversion should probably be disallowed, but now that there is some desire to allow the conversion specifically for the 'static lifetime, I think it would be good to consider whether we want to allow that conversion in general -- and the examples against us wanting to do this will also be interesting examples to consider for static_ref. At least I think so -- I don't know such an example after all. So I hope someone can supply one. :)

[eddyb]

I believe the usecase is having resources with "stable addresses" (such as C libraries that may keep their own pointers to the Rust-managed data), without having to always Box them, and while not needing &mut access.

(@m-ou-se can explain better, but AFAIK the standard library already uses this feature in that way, for OS-provided synchronization primitives that require a stable address even when not in a "locked" state)

For this usecase, &'a T -> Pin<&'a T> means Pin<&'a T> serves no purpose, because once the 'a borrow expires, the original T value is owned again (since the borrowing side only saw a regular reference), can be moved with safe code, and so cannot soundly keep any kind of pinned typestate it may have had for the duration of the Pin<&'a T> being in use.

Or in other words, &'a T -> Pin<&'a T> makes Pin<&'a T> not let you know more than &'a T, making them effectively "almost isomorphic" (even if there aren't conversions in both directions).

Whereas &'static T -> Pin<&'static T> can serve a similar purpose to &'static mut T -> Pin<&'static mut T> (especially when T: !Freeze), since there is no original borrow that can ever be revoked, and the pinning typestate can be kept forever.

[m-ou-se]

ReentrantMutex is a bit of a weird one, because it needs a const constructor, but the implementations do require having init() called before it's actually used.

A better example is RwLock: #77865 (Which I apparently forgot about and should probably be merged.)

However, even with that... would anything actually become unsound if we had a safe way to convert &'a T into Pin<&'a T>? So far I can't see any good reason for why the shared pinned and shared unpinned invariants would be different here.

Yes, lock() would no longer be able to guarantee the lock wasn't moved since the last call to lock() or any other method, which pthread requires. In the case of ReentrantMutex we just hackily stick that requirement into the safety requirements for init(), but for RwLock the interface is safe. (Also, for ReentrantMutex we had UB in the standard library before we use Pin to enforce this rule. (See also #77801))

And more generally: A function taking a Pin<&T> (for T: !Unpin) can assume the T won't be moved anymore, such that internal pointers can be stored in cells inside T, or that pointers to it can be stored in some other data structure. Making Pin<&T> meaningless would break all that.

[RalfJung]

And more generally: A function taking a Pin<&T> (for T: !Unpin) can assume the T won't be moved anymore, such that internal pointers can be stored in cells inside T, or that pointers to it can be stored in some other data structure. Making Pin<&T> meaningless would break all that.

Yeah I am aware of the general point, but without a concrete example it is hard to tell how relevant that is.

RwLock looks to be such an example then; I'll take a look at that when I find some more time.

[RalfJung]

RwLock is indeed an interesting example, thanks! I think I can make sense of how Pin<&T> is different from &T while it is still okay to convert &'static T to Pin<&'static T>.

Details of my formal reasoning (probably not very comprehensible)

• We model the requirement that an rwlock cannot move once the first call is made by imagining that the first call does a CAS from 0 ("uninit") to 1 ("init") and spawns a background thread that does something on this memory location. That explains why it cannot be moved.
• To coordinate ownership of the memory location between the background thread and everyone else, we put the points-to into a &at{static} (which is basically isomorphic to an inv but integrates better with the lifetime logic). The invariant in that borrow says something like CoreInvariant := l ↦ 0 ∗ BackgroundThreadToken ∨ l ↦ 1 .... The background thread owns the token while it is running.
• The owned unpinned invariant says that the current value is 0.
• The shared pinned invariant is &at{static} CoreInvariant.
• The shared unpinned invariant is &at{static} CoreInvariant) ∨ (\kappa != static ∗ &at{\kappa} l ↦ 0)
• The owned pinned invariant is... probably (&at{static} CoreInvariant)? Seems a bit strange for it to be equivalent to the shared pinned but OTOH having an Pin<&mut RwLock> does not actually help... the background thread might already exist so all interactions need to follow CoreInvariant.

The key is that the shared unpinned invariant is a disjunction supporting both the case where the lock is already initialized and the lock where we are just a regular shared borrow of a fully owned uninitialized lock. Having a syntactic equality test in \kappa != static is ugly but seems unsurprising given the proposed special casing of the static lifetime. Crucially, if \kappa=static, then shared pinned and unpinned are equivalent. The sharing rule has to also special case the static lifetime and actually initiates the CoreInvariant protocol if the lifetime is static. (Otherwise the protocol is initialized when pinning starts, as usual, as part of the "owned unpinned → owned pinned" transition. In the lifetime of an RwLock, one or the other can happen, but never both: if the sharing rule if used for static, sharing never ends, so this lock will never be fully owned again and cannot take the regular transition for starting pinning.)

Basically, pinning actually starts immediately when sharing starts for the static lifetime; calling Pin::static_ref just witnesses that this already happens. I am not sure if this is necessary, and it seems a little odd, but it should work. The alternative is problematic because once sharing started for the static lifetime, we can duplicate that shared reference many times, and any one of them has to start pinning and then somehow coordinate with all the others that pinning just started mid-way through the sharing...

So, I don't think I have any fundamental objections left here.

I am still not particularly happy about having to add another axiom though, and looking at those PRs made me wonder if it would not be a reasonable alternative to have a macro that creates a pinned static? We have macros for creating pinned local variables (not yet in the standard library, but I assume that will happen at some point). That would also avoid having to write Pin::static_ref(&HOOK_LOCK) all the time.

[m-ou-se]

looking at those PRs made me wonder if it would not be a reasonable alternative to have a macro that creates a pinned static? We have macros for creating pinned local variables (not yet in the standard library, but I assume that will happen at some point).

I'm not sure how comfortable I feel with macros that provide safety guarantees based on shadowing etc. I guess it's commonly used by now so we'll just have to accept it.

As for pinned statics specifically, I don't think it makes sense to add a macro. Avoiding having to explicitly call Pin::static_ref would be nice, but the same holds for usages of Pin::new. This just seems like a special case of Pin::new to me.

[m-ou-se]

So, I don't think I have any fundamental objections left here.

@rfcbot merge

[rfcbot]

Team member @m-ou-se has proposed to merge this. The next step is review by the rest of the tagged team members:

• @Amanieu
• @BurntSushi
• @dtolnay
• @joshtriplett
• @m-ou-se
• @yaahc

No concerns currently listed.

Once a majority of reviewers approve (and at most 2 approvals are outstanding), this will enter its final comment period. If you spot a major issue that hasn't been raised at any point in this process, please speak up!

See this document for info about what commands tagged team members can give me.

[BurntSushi]

I have no particular objection to these APIs, but I have to say, after reading the discussion above, I don't actually have a firm conceptual grasp of either why static_ref was thought to be problematic and how exactly it has been resolved. I don't have any interest in re-litigating that conversation, but is there a way to... ELIANRUWHUPY? ("Explain Like I'm A Novice Rust User Who Hasn't Used Pin Yet")

[BurntSushi]

Also, these routines do not appear to be documented. Examples would be helpful for why someone might want to use them.

[m-ou-se]

Basically, this whole things comes down to the question of whether a static X is considered 'pinned' or not. From a very theoretical perspective it is not (yet, depending on if we stabilize this), since something being static (or 'static) doesn't technically say anything about pinnedness, since we don't strictly define what it means for something to be pinned. From a more practical perspective, one (me) might say that static X is clearly pinned, because it can't move anywhere. It's perfectly fine to store pointers into that X and assume they won't be invalidated, it's perfectly fine for X to be self-referential, etc. Which to me is what Pin is all about, in practice.

Stabilizing this means accepting this and making those practical expectations match the theoretical promises about Pin. It means we accept that it's possible to make Ralf's example fail the assertion with only safe code. (Imagine there's a PhantomPinned in Nasty, which seems to be missing there.)

---

Edit: Note that the current standard library documentation (both here and here) already says that something that doesn't 'move'* is considered 'pinned', (vaguely?) implying that static X is 'pinned'. (*For some not entirely well-defined definition of 'move'.) Due to this, many users of Pin probably already assume that Pin::static_ref is something they can soundly do in an unsafe block.

[RalfJung]

Basically, this whole things comes down to the question of whether a static X is considered 'pinned' or not. From a very theoretical perspective it is not (yet, depending on if we stabilize this), since something being static (or 'static) doesn't technically say anything about pinnedness, since we don't strictly define what it means for something to be pinned. From a more practical perspective, one (me) might say that static X is clearly pinned, because it can't move anywhere. It's perfectly fine to store pointers into that X and assume they won't be invalidated, it's perfectly fine for X to be self-referential, etc. Which to me is what Pin is all about, in practice.

More specifically we are saying that anything that has a 'static lifetime is "pinned". There is no way to know that this comes from a static, it might just as well be a Box::leak or any other way to obtain a 'static reference. That's what makes this tricky and an expansion of the axioms of pinning.

Edit: Note that the current standard library documentation (both here and here) already says that something that doesn't 'move'* is considered 'pinned',

I would say the docs say that for something to be pinned, it must not move -- which is an implication the other way around than what you claim.

"Something doesn't move" is a rather vague term to pin down (heh), so we cannot reasonably use it as the definition of pinning, just in informal documentation.

Due to this, many users of Pin probably already assume that Pin::static_ref is something they can soundly do in an unsafe block.

If they do it for local statics that they control all access to, that's easy. Adding Pin::static_ref is a totally different game though since it says we can do this for an reference with the right lifetime, no matter where we got it and no matter what else is happening to the referent earlier or later. That is very hard to justify. I think it can only be justified "by fiat", by adding a new axiom that all unsafe pinning-related invariants need to satisfy. This puts a burden on anyone who wants to argue precisely that their pinned type is implemented correctly, even if they never care to use this method.
Maybe that burden is worth it, that is not for me to judge -- but I think saying that this is just a consequence of things we already decided about pinning is a misrepresentation. Pinning may look like a library-only concept but it has far-reaching consequences for the language, affecting all proofs of trusted libraries even if they don't use pinning themselves -- and adding Pin::static_ref slightly expands what exactly is happening here. IOW, this, too, is not just a library-only change but fundamentally affects the model of the language and what it means for unsafe code to be safely encapsulated behind an abstraction barrier.

[rfcbot]

🔔 This is now entering its final comment period, as per the review above. 🔔

[rfcbot]

The final comment period, with a disposition to merge, as per the review above, is now complete.

As the automated representative of the governance process, I would like to thank the author for their work and everyone else who contributed.

This will be merged soon.