Unsoundness in `Pin`

There's also a guarantee that the memory location will not be reclaimed before running Drop. I don't think anything in the std library relies on that, thus the requirement of using PinCell to observe the unsoundness.

As a semi-general workaround, we could instead implement Hash, PartialEq, Eq, PartialOrd, and Ord when T: Trait instead of when Ptr<T>: Trait, using the Deref implementation manually. This would limit the places we expose &Ptr<T> to only Deref, DerefMut, and Clone. This makes both approaches (additional proof obligations on new_unchecked or an added unsafe trait) a bit more scalable: we could later add trait implementations that manually call deref without having to worry as much about the trait implementation being correct. After all, we already have impl<P: Deref> Deref for Pin<P>.

I suppose there are places where this would create a change in behavior, but I can't see a useful example of that: even tricks like pointer equality can still be used, since the underlying PartialEq impls still get references.

(I'll throw my hat in to say that I much prefer the obligations being on new_unchecked, i.e. at construction time, instead of being at use time: my fuzzy intuition is that this places the minimal burden on users of Pin, since they don't need to follow any complicated unsoundness decisions to understand what this weird PinDeref trait is.)

7 Likes

Would this even change stable std behavior? (I know it could break custom pin-capable pointers.) IIUC, the only pinned types that you can build soundly are Pin<&>, Pin<&mut>, Pin<Box>, Pin<Rc>, and Pin<Arc> (and any impl Deref<Target: !Unpin>).

All of these implement {Hash, PartialEq, Eq, PartialOrd, Ord} by delegating to the deref target.

I guess the breakage could be observed via a smart pointer wrapper that implements PartialEq as identity equivalence rather than structural equivalence. Then, for T: Unpin, we'd have P: PartialEq while T: ?PartialEq, and the two impls don't give the same result.

Well, it's breaking, but this seems like to me the best way to bound the guarantees required by Pin::new_unchecked. Pin only needs to interact with Deref(Mut) and Clone to do its job; the other impls are really just convenience impls that turned into an attack vector.

2 Likes

That said, we control the full set of trait implementations on Pin (that can access &P<T>). To be less breaking, we can just list all trait implementations that convert from &Pin<P<T>> to &P<T> rather than Pin<&P<T>> or &T, and require that they always treat the &P<T > as if it were Pin<&P<T>> if it's going to be used with Pin::new_unchecked. That handles the trait leakage in theory, even if it still requires reasoning about external impls (and doesnt handle the impl for #[fundamental] or CoerceUnsized cases).

I think due to the pain of reasoning negatively about external impls (especially as we relax coherence rules!) we should avoid negative reasoning of such as much as possible. Unfortunately, Pin's guarantee is intherantly negative, so that's difficult.

I think my current preference is to tighten up all impls except Copy/Clone/Deref/DerefMut to directly apply the deref first, prevent nonsense impls of Deref/DerefMut/Clone on #[fundamemtal] types, and be very careful with CoerceUnsized.

Hi, author of stable_deref_trait here.

When originally creating the crate, I chose the gaurentees based on a review of the existing crates owning_ref, rental, and shawshank, and which invariants they appeared to be relying on. The fact that you can impl DerefMut for &T means that shawshank is very likely unsound, and owning_ref and rental probably are as well (which is more alarming, since owning_ref is a much more popular crate).

Regardless of what else we do, I think we should prevent impls of DerefMut on &T. The fact that this was even possible came as a surprise to me, and presumably to the authors of many other unsafe crates as well.

9 Likes

Has there been any work on formalizing Rust's trait system? Or some "well-known" reasons why it's impossible or unwise to do so? I didn't see anything about traits in https://plv.mpi-sws.org/rustbelt/#publications.

Wow, you managed to weaponize this, nice. :smiley:

I think this confirms my suspicion that we are making assumptions about every one of these traits and that so far, we do not have a clear handle on what these assumptions are -- let alone how to enforce them. I also see it as another argument for using unsafe marker traits, to make these assumptions more explicit.

Agreed. Everything that has direct access to the private field of Pin is highly suspicious.

I'd even consider moving out code like this that just safely composes the core API into a separate module, to make sure it doesn't access said field. But there might not be enough code to warrant this.

I don't think it is inherently negative. I mean, we have a WIP positive formalization of it in Coq. It's just very hard to turn that into something intuitive, into something that can be explained without all the formal boilerplate around it.

Interesting proposal, I like that idea. If we go with unsafe marker traits, this would mean we need fewer of those.

This goes well with my proposed module separation: we could impl PartialEq for Pin (and all the others) outside the module that has access to the private field of Pin. That can be done no matter whether we put the obligation on new_unchecked or on as_mut.

By users, I assume you mean people using Pin with existing smart ptr types? For them nothing changes with my proposal as the existing pin-supporting smart ptr types will implement the right trait bounds. I doubt many users will write code that uses Pin and is generic over the smart ptr type.

Then there are also those users that use Pin with their own smart ptr type. I do not know how common that is. But for those users, I think the "complicated unsoundness decision" are crucial for them to understand to make their use of the API sound. I think explicit unsafe marker traits will help with that.

No and no, to my knowledge. It's just hard. But I know several research groups have an interest in doing this. We are just all still busy with the borrow checker. :wink:

Of course, then combining the trait system with reasoning about unsafe code is yet another totally different game.

5 Likes

Yea I agree with this: I think we should "shore up" our pointer types so they work the way we believe they would work (specifically the issue with references) and then continue to place the burden on whoever implements constructors to pinned pointers.

So, this is exactly the sort of thing I was worried about. In my opinion probably Pin::new was too ambitious and we should not have any safe constructor for Pin generic over P. Deprecating Pin::new will be a bummer, though. Possibly we should have a marker trait for Pin::new implemented by all our pointer types. Just one marker trait though, which asserts correctness for all of the behavior of pin.

1 Like

I don't see how Pin::new is at fault here. It's the PartialEq impl for Pin that is wrong. It unsoundly creates a &Rc<T> from a &Pin<Rc<T>>, and we should prevent it from doing so.

What would be the contract that Pin::new violates here? Its only "fault" is the bad combination of Pin<Apple<T>> with Pin<Rc<T>>, but these could be defined in independent parts of the crate tree. We'd have to change our contract for Pin::new_unchecked to cover PartialEq for all combinations of all pinning smart ptr types. Surely that is not a solution.

Instead, we have to require, in impl PartialEq for Pin, that the concrete PartialEq impl we are using is well-behaved. That is the assumption that we are missing currently. (Or, as has been proposed above, we could use Pin::as_ref to step over the smart ptr PartialEq and directly use the one for T, which does not require any extra assumption in the PartialEq beyond what as_ref needs.)

I think blaimg Pin::new here is a big mistake, and will not lead to a reasonable safety contract. We end up having to reason about a combinatorial explosion of any two pinning ptrs that might be compared with each other.

The issue here is making a promise for a trait that's not a super-trait of the unsafe trait. Like, a DerefPin trait that wants to make a promise about the DerefMut impl for the same type if it exists -- we couldn't currently legally implement that trait for &T as we have seen. This is exactly what underpins the soundness holes we saw here.

7 Likes

Suppose we agree to change the PartialEq etc. impls so that we only depend on the correctness of DerefMut and Clone, and we also agree to somehow make &mut T: Clone and &T: DerefMut affirmatively impossible. (Both of these sound like good ideas to me.) And then the remaining question is whether to also add unsafe marker traits.

What would the contract for those traits be? "Don't try any funny business"? Is there any contract we could spell out which it would be possible to violate; is there any example we could point to of what not to do? Having to write unsafe impls to certify that you're not doing anything which, to the best of our knowledge, isn't even possible to do, feels like a faintly bizarre state of affairs to me.


My second thought is a bit fuzzier. Some time ago there was a debate over whether to add traits such as unsafe trait TrustedOrd: Ord to the standard library, with the purpose that data structures like BTreeMap would be able to assume that these traits were correctly implemented, allowing simpler and more efficient implementations of methods for the data structure, instead of having to account for the possibility of pathological impls like ones which invoke random(). The outcome of this debate (which makes a lot of sense to me) was that we shouldn't, because the purpose of Rust is not to be able to say "well, it's your fault -- you wrote unsafe!" when something goes wrong, but to reduce the risk of things going wrong outright.

These situations are very different. But a common element is the unsafe trait -- it strikes me that adding an unsafe trait is a very easy way to obtain a system which is sound in the technical sense, while not necessarily having an impact on the likelihood of code going wrong.

(In the extreme, we could add a marker trait unsafe trait Safe, remove all other unsafe annotations, bound all methods by where Safe<()>, and make the contract of Safe be that it may only be implemented for () if one's program is safe! This would be sound, but not in any useful way.)


Above, Ralf wrote:

I don't know if this is true, but it's at least a good motivation. If we can formulate sensible and comprehensible contracts for these traits, and believe that their presence will reduce the risk of people writing programs that go wrong, then let's add them. Which circles back to the first part of my comment, which was, "can we?".

4 Likes

This made me think about unsafe fields. It wouldn't have prevented this problem, but having

pub struct Pin<P> {
  unsafe pointer: P
}

would have required manual implementations of all relevant traits on Pin, with an unsafe block. This makes them extra visible when auditing the code, and preferably requiring an explaination of the impls safety. But even then, the problem is still difficult as

impl<P, Q> PartialEq<Pin<Q>> for Pin<P>
where
    P: PartialEq<Q>,
{
    fn eq(&self, other: &Pin<Q>) -> bool {
        unsafe { self.pointer == other.pointer }
    }
    // [...]
}

doesn't look very dangerous to me, and the subtle details of this thead easily overlooked.

5 Likes

Is it feasible to start by determining some non-minimal, but sufficient conditions for Pin safety? We can then backwards-compatibly determine more permissive sufficient conditions until we find the necessary conditions.

3 Likes

I'm concerned that this would make Pin much more confusing when custom pointer types are involved. Currently, it's possible to treat Pin<P<T>> (in safe code) as 'just' a restricted version of P<T>. There are methods that you cannot call for !Unpin types, like Pin::get_mut, but the methods that you can call just pass through to the underlying type.

I think this is a good thing - it shouldn't be necessary to understand the details of Pin if you're just using a Pin in safe code. A Pin just (conceptually) acts as an another wrapper type, like Box, Rc, Cell, etc.

Making trait impls bypass the wrapper type would (as far as I'm aware) make Pin unique as far as ats wrapper types go. Of course, Pin is already unique in terms of its constructor requirements - but this only affects people using the new_unchecked constructor. I'm worried that this will create problems with custom wrapper types with unusual (but valid) impls of PartialEq and other traits. Users will essentially have to remember, 'wrapper types usually just pass through trait impls, except for Pin, which does something different'.

I think we should aim to make using an existing Pin as straightforward and unsurprising as possible. The 'weirdness' of Pin should only be noticeable when you need to use new_unchecked, or make a custom wrapper type for use with Pin These are the cases where you actually need to understand what Pin means.

3 Likes

Yes. For Deref and DerefMut, the contract is something like "if the argument is in the pinned typestate, then the result must be in the pinned typestate, too". We'd obviously need a bunch of docs to explain all this typestate business, but there is a contract here, and we even have a rough formalization of it in an under-development Coq mechanization.

This is exactly what "method 1" violates: it returns something unpinned even if the argument is pinned.

For Clone and PartialEq, I don't know the details yet, but I expect them to be similar.

The comparison does not actually work. With BTreeMap, we obtain a data structure that is correct under more circumstances, i.e., we actually reduce the proof burden on clients. On the other hand, the "coherence-based assumptions" proposal (the one where Pin::new_unchecked and friends impose requirements on traits they don't depend on) does not mean that a user has to prove less than they would have to prove with an unsafe marker trait. The things I said above about Deref preserving the pinned typestate all still apply in this proposal. The only different to unsafe marker trait is the part of the pinning API where the proof obligation has to be checked by the other:

  • With unsafe marker traits, the proof obligation arises when calling Pin::as_mut or Pin::clone or one of the other methods that actually invoke the trait method that is mentioned in the proof obligation.
  • With coherence-based assumptions, the same proof obligation arises when calling Pin::new_unchecked (or when otherwise constructing a Pin).

In other words, avoiding unsafe marker traits here does nothing to alleviate the issue you are raising.

I know this is a strawman, but I have to push back on this. Every proposal we discussed here still allows modular reasoning, i.e., you can verify some piece of code once and then make it re-usable as a library. This is the key to making type systems useful, and it is the key for why safe typed abstractions of unsafe code are so useful: you can safely compose everything.

Safe<()> is not an extreme variant of a marker trait, it is qualitatively different by giving up on modularity and composition.

With unsafe marker traits, we are still modular. With coherence-based assumptions, we need a modular way to reason about the trait system, which is exactly what we got wrong so far. We certainly hope that there is a way to reason modularly about the trait system, but this demonstrably is a hard problem. For me it also makes a bit difference that we have no formal guidance whatsoever so far for doing this.

This is a valid concern, but I feel the alternative of having to make up contracts for each of these traits is worse.

5 Likes

I found this line of reasoning convincing. I don't have time to write more right now.

11 Likes

I think this whole argument is wrong, since this statement is wrong.

Pin does not wrap any type, or any smart pointer, but only smart pointers that are well-behaved, and that being well-behaved can certainly include implementing PartialEq, etc. in the obviously correct way of delegating to the PartialEq on &T where T is the pointer target.

Also in general behavior equivalent to the PartialEq implementation should be implementable in safe code outside of the module, and thus the PartialEq implementation should not require access to private fields or unsafe code, which means that the "bypassing" implementation is the correct one (since safe non-private code cannot access the smart pointer itself) and the current unsound implementation is wrong.

3 Likes

I agree with this, and I think the use case we're excluding seems so exceedingly niche:

  • A user has defined a smart pointer type that can be validly pinned (already a rare case).
  • A user actually wants to use that with the std Pin API.
  • That smart pointer type has a custom PartialEq/etc impl that they need to get called.

However, we are talking about losing some optimizations. For example, Rc == Rc currently does an addr comparison before comparing the value for types that implement Eq and so does Pin<Rc> == Pin<Rc> today. But these can be recovered with secret specializations.

Also, users can, in the most extreme case, recover whatever behavior they want by creating their own type for the code where they need equality checks (using an unsafe partialeq marker or non-generic pointer types, etc), converting between that and Pin whenever they want.

1 Like

This is only true for !Unpin types. With an Unpin type, I can use Pin::new with any smart pointer, without a (safety) requirement that it be well-behaved in any way whataoever.

I don't think we should be determining what 'obviously correct' means for user code, without providing any way to override this assumption. The PartialEq trait only requires (as a logical contract, not a safety requirement) that the implementation uphold reflexivity, symmetry, and transitivity. I don't think we should be assuming anything else about what a 'correct' PartialEq implementation looks like.

I'm not quite sure what you mean here.

If you're talking about the PartialEq implementation on Pin itself, I don't think it should necessarily be implementable outside the module. While it would make the correctness of Pin easier to verify, I think we should prioritize making Pin flexible with respect to custom pointer types.

If you're referring to the user-supplied PartialEq impl on the pointer type, I strongly disagree. One of the core ideas behind writing unsafe code is that it should (whenever feasible) be used to build a safe abstraction, which does not require users to even be aware of the existence of the underlying unsafe code.

We should not making any kind of assumptions as to where unsafe code 'should' exist. While it might be unusual for a PartialEq implementation to require it, there's no reason why it couldn't.

1 Like

Could such specializations be written in user code after specialization gets stabilized, or would they be a special kind of perma-unstable specialization for libstd only.

If it's the latter, I'm somewhat uncomfortable with the idea of giving libstd types this kind of 'special power' that will never be available to user code (assuming that a specialization trick is the only way of recovering performance in this case).

This will not help users relying on other crates which expect a Pin. I don't think this will be a common (or even very useful) thing to do, but I think it's worth pointing out that this change will impose some loss of functionality, even if it's still a net improvement.

Users could use the specialization to write unsound impls unless we introduced an unsafe marker trait as a part of exposing the specialization. There's nothing "perma-unstable" about adding private specializations to add safe optimizations without exposing an unsound API.

Sure no one is disputing that its a loss of functionality, just that it outweighs the cost of maintaining that functionality. Making it impossible to impl DerefMut for &MyType is a loss of functionality also. Only the "separate unsafe marker trait for each trait involved in Pin" solution involves no loss of functionality.

1 Like