Transitiveness in Pinning

language design
1

After think about this a little while, I think the problem is unsoundness of Cell is the source of the evil. Just think about this, having a &Cell<Option<T>> is pretty much having a &mut T, since we can do the following thing:

fn abuse_cell_ref<T>(cell_ref: &Cell<Option<T>>,  op: impl FnOnce(&mut T)) {
    if let Some(mut inner) = cell_ref.replace(None) {
        op(&mut inner);
        cell_ref.replace(Some(inner));
    }
}

But the evil part is the compiler will treat this reference as normal immutable reference. You don't really have a way to clone a &mut T, but you definitely can have &Cell<Option<T>> cloned as it's just a immutable reference. And this makes multiple &mut T effectively possible in safe Rust.

So there's actually a lot of different way to exploit this. For example, I believe this code is definitely an UB, but it's completely safe code. Even without Pin, I believe.

https://play.rust-lang.org/?version=stable&mode=debug&edition=2018&gist=aff2b95898bfce703616d5c186928903

In the code above, you are ending up a malformed b-tree data structure.

So my point is Cell really safe, the problem of Cell is it makes &T not a guarantee of immutability any more. Furthermore, most of other part of the code just believe the contract that everything behind &T is really immutable and this gives malicious code so many ways to break borrowing contract even without unsafe block.

Unsoundness in `Pin`
2

FYI: Not that well versed in Cell.

However, I don't think that is broken since the checking is done at run time.

Also, there are many other ways to get a &mut from &: Mutex, RefCell, ...

3

But &T doesn't mean immutable, it means shared. Anything built on top of UnsafeCell is allowed to mutate things behind a shared reference.

That is fine, a malformed BTreeMap is easy to create with any form of shared mutability.

This isn't the concern here, the problem right now is unsafe code relying on safe traits directly, which is unsound.

Cell doesn't do any runtime checks, it just forbids references to the inner value while it value is inside the Cell

3 Likes
4

There's definitely no UB here. BTreeMap is completely able to handle "incorrectly ordered" trees. You just discovered why that is important!

You don't even need Cell for this, you can just have a type for which PartialOrd returns random results, and different results each time it is called.

6 Likes
5

Ok,but is a shared mutable still fine ? Since as I said &Cell<Option<T>> is effectively a &mut T already, isn't this breaking the contract?

6

Yes, that is the entire point of anything built ontop of UnsafeCell, like Cell and Mutex. They just guard access to the value inside to prevent UB. This can be done with runtime checks (like Mutex), or by removing ways of accessing the inner data (like Cell).

Being isomorphic to &mut T does not mean that they are the same. (In this case &Cell<T> is isomorphic to &mut T, not &Cell<Option<T>>)

4 Likes
7

Yes, you are right, I was wrong about &Cell<Option<T>>, this is actually something like a RefCell, which means once you mut borrowed the inner data, the cell is temporarily invalidated until the borrow is end.

But still, this breaks the assumption for Pin, which makes anything logically similar to Pin<Cell<T>> isn't actually pinned.

8

As has been said a few time in this discussion, pinning is not transitive. So having a pinned Cell<T> does not mean that the T inside the Cell<T> is pinned. This is exactly because of Cell<T> and other types like it.

3 Likes
9

Nor does it need to be...is that not the case?

The only reason something need to be pinned is so that I can have a weak pointer to it and still guarantee that when I deref my weak pointer the "thing" is still at the location of my pointer (even though I don't own the pointed to thing, nor, do I hold a borrow). All I have is a weak pointer that is "guaranteed" to still point to the head of the object it refers to when it comes time for me to deref that pointer. Any pointers or anything else inside the "thing" being pointed to can move around however is permitted by that type. That has nothing to do with Pin.

Is that not correct? Do I have the correct understanding?

So, is this "unsoundness" due to the fact that I can somehow coerce the type system to give me ownership of the object, which then allows me to move that object in memory elsewhere after a Pin has been given to someone else?

Is the thing being moved the same thing being pointed to by the Pin? Or, is it internal movement?

Is the problem basically:

  1. Bill has a book
  2. Bill let's Sally Borrow the Book by putting it on a picnic table in the park. He tells Sally she is free to grab the book off the table whenever she wants, update or read it, then put it back on the table. Bill promises not to remove it from the picnic table until Sally lets him know she is done with it. (this is in essence a Pin....you are not taking possession, but, we've agreed where you can get it when you need it and I promise not to move it somewhere else until you let me know you are done with it)
  3. Bill also lets Jezebel Borrow the Book under the same terms (assuming a shared as opposed to a mutable borrows)
  4. Now, Bill, Jezebel, and Sally can all walk over to the table anytime they want, and look at the book. It may require them to wait in line (Arc) but, they know that if they need to look at the book, the can find it on the picnic table unless someone else is at the moment looking at it, but, it'll still be on the picnic table. I may or may not be able to look over their shoulder and read at the same time, but, at worst I have to wait in line. Th book will always be there for me.
  5. Bill decides to renege on the deal and take the book home, but, when he tries to do that the Watchman (Rust), says, "Lookie here numnutz, you promised not to take the book off the table until Sally and Jezebel let you know they are done with it". But, the watchman doesn't actually sit and watch to ensure that Bill doesn't remove the book from the table, instead, Bill files a plan of action with the Watchman and the watchman ensures that his plan will not violate the agreement made with Sally and Jezebel.
  6. Now, Bill, being a particularly devious and clever lawyer, writes a really complicated plan of action with lots of confusing terms and circuitous explanations. He might even include a few Escher-Style diagrams that demonstrate the Book being in two places at once through the magic of extra dimensions (i.e. Playing complicated tricks with the type system and traits).
  7. The watchmen, being really good at his job, checks out Bill's plan and everything seems to check out, but, in the plan, Bill has filed, what he is actually guaranteeing to leave on the table is a paper grocery bag book-cover that he first puts on the book, but, Sally and Jezebel believe he has promised to leave the Book on the table. The watchman approves the plan, because it looks correct to the Watchman that Bill has promised to leave a book-cover on the table, and, Sally and Jezebel, are duped into thinking he has promised to leave the book there.
  8. Now, Bill takes the book (maybe right away, maybe later) and leave the cover, but, the cover is coated with self-destructing nanites that detect when the cover no longer holds a book and so the cover too evaporates from existence.
  9. Bill strolls away ominously twirling is mustache ready to dupe his next victim.
  10. Sally gets a call to look up the answer to life, the world, and everything, so that the inevitable apocalypse can be avoided. When she goes to the table, she can't find the book, so she reads the scrawl that has accumulated over the years from the table, and, then all hell breaks loose because the message she returns as the answer to the dilemma is, "Joey :heart_decoration: Bobby" instead of "42". As a result, the universe folds in on itself and reboots into a new world with randomly new laws of nature.

So, in this story, the "Contract" as written by Bill, is so confusing that the Watchman's understanding of what Bill is promising doesn't correspond to what Sally and Jezebel believe Bill is promising. The "Contract" is the types and traits that are being given to Sally and Jezebel pinned. They don't realize that the "Book Cover" is not the "Book" and that the "Book Cover" includes self-destructing chemicals and that cover permits Bill to pull out the Book without notice.

But, you may ask, why couldn't Bill just file a correct plan/contract and still remove the book anyways? Well, in this story, if you haven't figured it out, Bill is a Jinn or Demon (C/C++ Compiler) that isn't permitted to outright lie (i.e. use "Unsafe") by his code of honor, but, he is permitted by his own "morality" to twist words and sow confusion (make complicated trait interactions that obfuscate the promise being made) in the hopes of condemning his next victim.

Is this a good summary of the situation? If so, it seems like the options are:

  1. Make the Watchman (compiler/borrow-checker) more intelligent, careful, thorough so that nefarious plans cannot be mistakenly approved.
  2. Make the "language" the plans can be written in have sufficient limits and precise definitions so that there cannot be legitimate misunderstanding.
  3. Allow the Watchmen to actually monitor the situation after the plan is approved and throw down the penalty flag if the understanding the Watchman has is violated after the plan is approved.

These options seem to correspond to:

  1. Make the Borrow Checker/Compiler smarter.
  2. Add "Marker" traits that clarify requirements by asserting certain promises that are unambiguous.
  3. Have some run-time overhead to ensure the promises of Pin are kept.

Is that right? If so, it seems like 3 should be avoided if possible, and 1 is asking for an Omniscient Magic Eight Ball, while 2 seems somewhat tractable.

Do I have a correct understanding of the situation? If not, where is my understanding flawed?

3 Likes
10

So if this is the case, it seems the usage of Pin in Future::poll cannot guarantee anything, as long as it's still possible that the actual future is in a Cell which just make Pin can't guarantee the actual data isn't touched by a third-party . So my understand why poll API uses pin is to enforce the state of the async invocation won't be modified (or moved) by anyone other than the async itself.

So I am wondering if this is by design, I just feel this isn't something by design, since this may make the Pin pointless as long as we have safe way to break the property it try to enforce.

This is exactly what I am asking, since I think it should be transitive otherwise there must some way to break the contract.

11

This won't work in this case, because it isn't a problem with lifetimes, but the semantics of pin.

This seems to be what @RalfJung is proposing

I don't think this is even possible, given that we can't track moves.

When I said that pinning isn't transitive, I should have said "pinning is not transitive by default". A specific type T can say that pinning type T also pins a field of T, but this isn't the default. Cell keeps the default, a lot of future combinators don't keep the default and say that pinning the combinator also pins the future inside the combinator.

Non-transitive pins was by design, to make the implementation simpler. If you want transitive pins you must have true immovable types. This doesn't exist in Rust, and would be a monumental effort to put into Rust, larger than the scale of async/await because you will also have to adjust all generic code to work with truely immovable types.

12

The thing being moved is the same thing being pointed to by the Pin.

Anything inside the type can move around as normal.

The exception is if the type exposes Pin accessors, which requires unsafe code but is a common pattern:

struct Foo { bar: Bar }
impl Foo {
    fn get_bar(self: Pin<&Self>) -> Pin<&Bar> {
        unsafe { Pin::new_unchecked(&self.bar) }
    }
}

In that case, once you call the method and get a Pin<&Bar>, the pin guarantee obviously applies to the Bar as well.

That's roughly correct, but note that you don't actually need ownership. You only need a non-pinned mutable reference, &mut T, at which point you can use, e.g., std::mem::replace to move the T while supplying a replacement value.

13

So, would you say that the contract described by the Traits promised to keep "THE Book" on the able, and then it was able to be violated, or, are you saying that the promise made was actually to keep "A Book" of similar size, dimensions on the table at all times?

In other word, did these "Trait Games" boil down to promising something different that seemingly promised, or promising one thing and doing another?

Doesn't std:mem:swap require that the things being swapped are type compatible? If so, is Pin really promising the presence of "A Book" instead of "THE Book". "A Book" would not be undefined behavior in my mind because there would still be a valid book there when I went there. It just wouldn't be the book I was expecting. But, if I someone swap "THE Book" with "A Zamboni", and I didn't know how to deal with "A Zamboni", that would be UB. Especially if I just pretended like the "A Zamboni" was "A Book" even if "A Book" wouldn't be correct when I expected "THE Book", I would at least still now how to read from and write to the "Book" even though it isn't "THE Book" I started with?

Is that not right? So, is this a case, not of unsoundness, but, a case of promises kept literally, but, not in Spirit?

Would it / does it make sense to say that all Pin guarantees is there will be a valid T there, not necessarily THE T I was originally given? But, that there can't be a Q there instead. Nor can there be an almost T with some of its invariants compromised.

I think, from what I'm reading, that this problem is a case of the promise of Pin being kept, but, having an idea of what that promise is that is not what is being promised.

So, my question is, Does Pin guarantee "THE T" given originally or "A T" which is a valid "T" to be pinned at that location.

It seems like the notion of "THE T" is suspect because it would be difficult to have any real meaning there.

So, if I promise to put a book cover on the table with a 100 pages, and then, when you aren't looking, I swap it with another 100 page book, have I violated the Promise of Pin?

I would think not. However, if I swap it with a bag of Doritos, I've definitely violated the Promise.

True / False?

EDIT: I guess I'm wondering is Pin really promising the original T or is it just making a promise that whatever is there is Lishkov Substitutable/Compatible T? As I think about it, to not have UB, the latter is sufficient, and the ability to do mem::swap doesn't violate that.

14

If you don't care about identity, then &mut is enough.

Pin does require the same instance remaining there (logically), because that guarantee is what allows self pointers to exist within the pin, because what they point to won't change out from underneath them, due to the identity pinning guarantee.

15

The T, though it doesn’t usually matter. Suppose you have this code:

async fn foo(opt: Option<String>) {
	if let Some(ref string) = opt {
		// string: &String
		some_future().await; // suspend here
		println!("{}", *string);
	}
}

This will desugar to a Future type looking something like this:

struct Foo {
    state: u8, // where did we suspend?
    opt: Option<String>,
    string: *const String,
}

(Actually, some fields might not be initialized depending on the state, but ignore that.) Based on the behavior of the function, for a given object my_foo: Foo, if my_foo.state corresponds to the await point, my_foo.string will point to the interior of my_foo.opt (within the same object).

Let's say you do

let mut my_foo: Foo = foo(Some(42));
my_foo.poll(ctx); // Imagine pinning weren't required.
// Now my_foo.string points into my_foo.opt.
let old_foo = mem::replace(my_foo, foo(None));

[edit: fixed example]

Now old_foo.string points to the interior of my_foo.opt, and old_foo upon resumption will dereference that and print the result. And you have two problems:

  1. The borrow checker has no way to enforce that you don't go on to free my_foo altogether, in which case there would no longer be "a Foo" there.
  2. But even if you don't free it, the new value of my_foo has opt == None, so the interior of the Option contains undefined bytes. It would be very bad if you went on to access it as a String! This is the consequence of not ensuring you still have "the Foo".

Anyway, this is all a bit off topic; is there a way for mods to split it into a different thread?

4 Likes
16

OK, so, are we saying that Pin needs to guarantee this?

===memory (A)===
b : B;
c : &C; // points to C below

===elsewhere in memory (C)===
d : D;
e : E;
a : &A; // points to A above

Now, I do a mem::swap for (A) to end up with this:

===memory (A)===
b : B;
c : &D;
===

Is this wrong to do to the thing relying on Pin? Yes. But, is it UB? I'd think not. It's bad in the way leaking memory is bad, or, having a "Race Condition", or similar "Safe", but, not good things.

How is doing the mem::swap different from me just mutating the "c" reference?

Or am I completely misunderstanding? This doesn't seem like UNSOUND or UB to me, it just seems like logical failure. I promise there to be a valid A there, there is. I also am not supposed to mess with it, but, if it somehow allows internal mutability, because the type allows that directly or transitively, then, all that I've promised you is that you will have a valid value of the type there, but, I have not promised you that I (or someone else) won't modify it. If you need that promise, then I need to Pin something to you with no internal mutability. Is that not the case?

17

see @comex's example of a self-referential type. Moving such a type would definitely be UB

1 Like
18

Yeah, that clears it up. I see now where my thinking was awry.

19

See this blog post for more details about &mut _ vs. &{Unsafe}Cell<_>: Mutation - part 2: To mut or not to mut · Another one bytes the Rust!

By the way, this whole thread belongs to URLO, imho.

2 Likes
20

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.