Tracking Issue for feature(pin_static_ref): Pin::{static_ref,static_mut} · Issue...
source link: https://github.com/rust-lang/rust/issues/78186
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
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
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.
Can you not
mem::swapa 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.
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.
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.
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.
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.
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.)
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?
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.
new_sharedreturns 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.
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".
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.
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.
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.
This discussion is going nowhere. I give up for today.
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.
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.
(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
unsafecode in the vein ofNastyfrom upthread Pin::static_refis not sound under that model
Now, there are three things I think we can all agree are important:
- the documentation is as clear as we can make it, and we don't leave room for ambiguity
- formal models (RustBelt/Stacked Borrows) have to be able to distinguish what we consider "correct Rust code"
- not breaking existing
unsafecode out there needlessly
And given the above discussion I have these questions:
- 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?
- how hard would it be to allow
Pin::static_refinto the model? (this is even more relevant because of 3.) - what are the chances users came to the conclusion that
Nastyis correct, as opposed toPin::static_ref?- the existence of this feature and my own informal reading align with
Pin::static_refway more thanNasty Pin::static_refitself already has unstable uses, and its definition may have been copied by stable usersNastystrongly resembles some other examples I've seen in the past (&NotSyncpromotion to'static), and they have in common the fact that "constructability of types referring toStrangeInvariants, 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)
- the existence of this feature and my own informal reading align with
"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.
@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.
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).
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. :)
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.
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).
Yes that is exactly what I meant when I said that "shared unpinned" and "shared pinned" become the same typestate: &T and Pin<&T> become the same type.
It'd be nice to have concrete examples for use-cases this would break -- do you have links for those?
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.
Sadly, this does not work: even a static shared borrow is still shared, so you can't just access its data as if it was not borrowed.
RustBelt provides very strong reasoning principles for static exclusive borrows, like &'static mut. That's why Pin::static_mut is fine. But the same reasoning principles for static shared borrows are a lot weaker since they have to account for sharing.
I am not sure what you mean by "the pinning typestate can be kept forever" -- an &'static T is not in the pinned typestate; static_ref needs to somehow transition it to that state. That is exactly the problem.
Yes that is exactly what I meant when I said that "shared unpinned" and "shared pinned" become the same typestate:
&TandPin<&T>become the same type.
There's a crucial difference here: we don't want a "shared pinned" -> "shared unpinned" transition (assuming !Unpin), nor "shared unpinned" -> any kind of ownership (modulo details around how Drop is handled).
Sadly, this does not work: even a static shared borrow is still shared, so you can't just access its data as if it was not borrowed.
Is the concern that accessing the T through a &'static T, independently of the Pin<&'static T>, requires the undesired "shared pinned" -> "shared unpinned" state transition? Could that state transition "just" not exist? There'd be no difference in limitations around accessing the T value via Pin<&T> vs &T, but it would be UB to e.g. ever obtain a &mut T to the same T.
It'd be nice to have concrete examples for use-cases this would break -- do you have links for those?
I mean, if something is taking Pin<&'a Self> and passes the address through FFI to something that escapes it, that's broken if the pinning can be revoked, isn't it?
Anyway, I wasn't sure which part of std used it, so I searched around and found at least one example:
/// Initializes this mutex so it's ready for use.
///
/// # Unsafety
///
/// Unsafe to call more than once, and must be called after this will no
/// longer move in memory.
pub unsafe fn init(self: Pin<&mut Self>) {
self.get_unchecked_mut().inner.init()
}
/// Acquires a mutex, blocking the current thread until it is able to do so.
///
/// This function will block the caller until it is available to acquire the mutex.
/// Upon returning, the thread is the only thread with the mutex held. When the thread
/// calling this method already holds the lock, the call shall succeed without
/// blocking.
///
/// # Errors
///
/// If another user of this mutex panicked while holding the mutex, then
/// this call will return failure if the mutex would otherwise be
/// acquired.
pub fn lock(self: Pin<&Self>) -> ReentrantMutexGuard<'_, T> {
unsafe { self.inner.lock() }
ReentrantMutexGuard { lock: self }
}
I am not sure what you mean by "the pinning typestate can be kept forever" -- an
&'static Tis not in the pinned typestate;static_refneeds to somehow transition it to that state. That is exactly the problem.
Could a 2-step &'static mut T -> Pin<&'static mut T> -> Pin<&'static T> conversion achieve the necessary state transition?
If so, is the uniquness in the first step required? As in, is the issue with the shared version kind of like a "typestate race"?
The other idea we could rely on is that &'static T can only come from either "shared forever" things like const/static or by revoking all ownership rights (e.g. Box<T> -> &'static mut T -> &'static T, and both steps are "consuming"). Sadly I doubt that trying to be exhaustive about all the mechanisms through which a &'static T can be obtained, is a good path (e.g. how could that allow &*raw_ptr?), so we're probably stuck with "shared pinned" typestate needing to (somehow?) be entered by Pin::static_ref.
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 TtoPin<&'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 ofPinthat would have a problem with such a conversion function?
See my comment at the start of this discussion: #78186 (comment)
There's a crucial difference here: we don't want a "shared pinned" -> "shared unpinned" transition
Eh, too late for that.^^ One can safely convert Pin<&T> to &T.
"shared unpinned" → "shared pinned" currently does not exist; static_ref proposes to add it specifically for the 'static lifetime.
Could a 2-step &'static mut T -> Pin<&'static mut T> -> Pin<&'static T> conversion achieve the necessary state transition?
If so, is the uniquness in the first step required? As in, is the issue with the shared version kind of like a "typestate race"?
I'm not sure yet if there is a deep issue with the new "static shared unpinned" → "static shared pinned" that is being proposed for addition -- I just know that it does require a new axiom that all invariants need to prove, and I am worried that we do not have sufficient reasoning principles for this (since shared references being static is much "less useful" than mutable references being static). The reason for this is that other parties might also access this shared thing and you have to ensure that whatever you do (to turn the typestate into "pinned") is compatible with whatever they do.
&'static mut T -> Pin<&'static mut T> is fine, as I mentioned. Pin<&'static mut T> -> Pin<&'static T> is also already possible I think? So yeah if that is enough for the usecase here, then moving to that would resolve all my concerns. :)
Sadly I doubt that trying to be exhaustive about all the mechanisms through which a &'static T can be obtained, is a good path
Indeed, that path is pretty much the antithesis to the "semantic model" approach of RustBelt.
@m-ou-se thanks, I'll take a closer look tomorrow.
I had a closer look at ReentrantMutex (took a bit longer than expected, sorry for that). It's a tricky one because even with Pin, there is no entirely safe way to use this type... this means the invariant we use for the safety proof is much less constrained than it would be in a proper safe API. So I imagined that we would add the following function:
impl<T> ReentrantMutex<T> {
pub fn new_boxed() -> Pin<Box<Self>> { unsafe {
let mut m = Box::pin(Self::new());
m.as_mut().init();
m
}
}I hope I got this right and this function is actually safe. This helps a lot since now the safe API surface of this type is useful, so we can't pick entirely silly invariants.
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.
It would really help to have an example of an API that would be made unsound by a safe fn(&'a T) -> Pin<&'a T>. This operation might go strongly against your intuition, but without a more concrete argument it's hard for me to attempt to underpin that intuition with a formal argument.
(My quest here is to understand why fn(&'a T) -> Pin<&'a T> would be bad when fn(&'static T) -> Pin<&'static T> is allowed. I can construct sensible formal universes in which both are allowed, or both are forbidden, but having the latter without the former is not something I can make much sense of formally, at this point -- I can write down a definition, but without an example I can't evaluate if it makes any sense, and my own intuition says it does not make a lot of sense.)
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.
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.
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)
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.
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.
So, I don't think I have any fundamental objections left here.
@rfcbot merge
Team member @m-ou-se has proposed to merge this. The next step is review by the rest of the tagged team members:
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.
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")
Also, these routines do not appear to be documented. Examples would be helpful for why someone might want to use them.
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.
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.
Copy link
rfcbot commented 10 days ago
This is now entering its final comment period, as per the review above.
Copy link
rfcbot commented 1 hour ago
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.
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK