Rust 1.20 caused pinning to become incorrect

[asajeffrey]

I guess this is an issue of what the implicit contract for Drop is. Is it expected to drop all of its owned data? Even in the presence of drop code panic? Is it allowed to panic? Is it allowed to abort? Is there any contract at all?

[RalfJung]

@asajeffrey

The only thing I’d ask for is please can we give ourselves some wiggle room and define two invariants for rely-guarantee reasoning (code can rely on R and should guarantee G, where G implies R). That way there’s some room for strengthening R and weakening G. If we just have one invariant (i.e. R=G) we’re stuck never being able to change them!

This is a great point. However, rely-guarantee is (AFAIK) terminology from concurrency research and describes modular (thread-per-thread) verification of concurrent interactions. I'm not actually aware of any research for type system invariants that provide "wiggle room". Somehow, this would have to make a difference between the types that are produced by an unsafely implemented library (where it has to show the stronger invariant) and types that are consumed (where it can only rely on the weaker invariant). But given this is all higher-order and we can both produce and consume closures, I will only believe this really works once I see it worked out.

So, while I agree with the goal, I actually have no idea how to formally do that. I know I should write this down as a future research project though

@asajeffrey

I think my main point still stands, which is that the contextual definition of correctness is brittle, and that this is an interesting example of it producing problems “in the wild”.

It's not just brittle. It's anti-modular: Two libraries can be correct independently but break in combination. Just imagine VecDeque not being in libstd; then VecDeque and Pin form such a pair.

So, I'd say the contextual definition is plain broken.

@asajeffrey

@RalfJung: this might be a way to tie the contextual definition of correctness back to rely-guarantee reasoning, if the contracts are themselves stated using rely-guarantee.

Could you elaborate? I don't follow. This doesn't help with the anti-modularity, right?

@asajeffrey

I guess this is an issue of what the implicit contract for Drop is. Is it expected to drop all of its owned data? Even in the presence of drop code panic? Is it allowed to panic? Is it allowed to abort? Is there any contract at all?

I agree with what has been said above that ever sine the leakpocalypse, the contract is something like "drop is called on a best-effort basis; you can't ever rely on it for safety" (EDIT: except if it's all your code. You can rely on your own stack objects getting dropped). But probably this has not been documented clearly enough.

[arielb1]

Pinning is unsafe in the presence of arena-allocated Rc data anyway, which is something we want to allow one day:

struct Cyclic<A, T> {
    cycle: RefCell<Option<Rc<Cyclic<T, A>, A>>,
    data: T
}

fn foo(arena: &ArenaAllocator) {
    let rc1 = arena <- Cyclic {
        cycle: Default::default(),
        data: Pin::new(),
    };
    
    // make a cycle    
    *rc1.cycle.borrow_mut() = Some(rc1.clone());
    rc1.data.pin();

    // no destructors are run, but the arena (and its containing Rc) is eventually free-ed.
}

[asajeffrey]

Arena-allocated data doesn’t get its destructor called? That’s annoying. It would be nice if there were a way to call the destructors for data that was marked may_dangle or some similar marker for drop code that is safe in the presence of cycles. But that’s a different topic!

[asajeffrey]

Yes, more research is needed!

We might need some kind of Kleisli semantics future world trick, that is you don’t just show rely/guarantee for the current R and G, but for all future R’ and G’. This is the usual trick for getting monotonicity in the presence of contravariance (in particular for higher-order functions).

For contextual correctness, I was wondering if there’s a way to interpret the defn “for all safe C . C[P] has no UB” as something like “for all safe C . for all implementations I . (I satisfies appropriate contracts) implies (C[P] linked against I has no UB)”. There is lots of handwaving here, but this might be a way to recover a defn of correctness based on invariants (assuming that’s how the contracts for I are defined).

[atagunov]

@asajeffrey

Arena-allocated data doesn't get its destructor called?

guess in the example

• the counter in Rc never reaches 0 because of the reference loop
• so drop is never called on the Pin instance
• yet the memory it occupies is free-ed when ArenaAllocator itself is free-ed

[RalfJung]

@asajeffrey

For contextual correctness, I was wondering if there’s a way to interpret the defn “for all safe C . C[P] has no UB” as something like “for all safe C . for all implementations I . (I satisfies appropriate contracts) implies (C[P] linked against I has no UB)”. There is lots of handwaving here, but this might be a way to recover a defn of correctness based on invariants (assuming that’s how the contracts for I are defined).

This sounds a lot like the logical relation-based approach we are using in RustBelt. However, on its own, this does not provide any wiggle room.

Btw, do you have an example of a guarantee that you'd like unsafe code to provide, but not to rely on? Some example where you think we currently still have wiggle room and should keep it?

[asajeffrey]

An example would be something where the contract hasn’t been settled yet, perhaps may_dangle would be a good example?

[RalfJung]

may_dangle seems so little understood, I don’t even know one precise definition of it – let alone two (a lower and an upper bound).

[asajeffrey]

The rely is nothing at all

But this does bring up an interesting issue, which is that the cases where wiggle room is useful are probably cases where there’s nothing sensible to say formally because the design process is still underway.

[RalfJung]

@asajeffrey

The rely is nothing at all

So Vec::drop is unsound for relying on something?

More seriously though, I do feel like there could or should also be wiggle room in the better understood parts of the type system. I mean, we have picked a concrete invariant for our research -- but the consequences of this are far-reaching: For every possible unsafe abstraction someone could come up with, it now either is or is not sound (at least if you believe in the excluded middle ), and we have no idea where this dividing line lies. I would not be surprised at all if at some point down the road, someone comes up with something that's compatible with all the unsafe code that's widely used, desirable, but is not compatible with our invariant.

[arielb1]

@atagunov

guess in the example

• the counter in Rc never reaches 0 because of the reference loop
• so drop is never called on the Pin instance
• yet the memory it occupies is free-ed when ArenaAllocator itself is free-ed

That's what I meant. An arena-allocated Rc (this is not a full "free at once" arena, but rather an "compartment arena" where data can be free-ed while the arena is being used) can't call destructors for leaked contents of the arena when the arena exits because destroying a reference cycle would be unsound, so reference cycles are still leaked. However, the memory owned by the arena could still be free-ed.

This is basically a by-design use of allocators, and therefore is unlikely to be removed.

may_dangle seems so little understood, I don’t even know one precise definition of it – let alone two (a lower and an upper bound).

From my POV (see e.g. https://github.com/rust-lang/rfcs/pull/1327#issuecomment-149366279 and the newer nll-rfc/0000-nonlexical-lifetimes.md at 30db8883d63b102bf8544e425a21f0d3ebe27ab3 · nikomatsakis/nll-rfc · GitHub), the main problem with may_dangle is that it basically makes calling functions unsafe.

The semantics are pretty clear - it removes the implicit assumption that type and lifetime parameters are active when they are in scope, and also the similar WF assumption that &'a mut T requires that T: 'a. That's a problem for safety, because any function based on that type parameter assumes that these lifetimes are in scope, which means calling it is illegal - so you basically have to prove that your destructor is safe "from first principles", as if the lifetime system did not exist.

I'll note that in a destructor impl, there's still the "data-type is destruction safe" bound - the compiler guarantees that the fields of your type are destruction-safe, which means you can safely call destructors on the types of subfields (and that ends up calling a Drop impl, then you know the lifetime obligations for that impl are met, and you're back in the "modular world" again).

There's just no compiler infrastructure for proving that sort of thing, as that would basically require duplicating the type-checker, so you're on your own when it comes to the proofs.

The "josephine invariant" (https://github.com/rust-lang/rust/issues/34761#issuecomment-362855806) was never intended to hold - in fact, as I demonstrated, planned-to-be-implemented allocator support would break it.

[RalfJung]

@arielb1

There’s just no compiler infrastructure for proving that sort of thing, as that would basically require duplicating the type-checker, so you’re on your own when it comes to the proofs.

Just to be clear, "this sort of thing" is referring to a more explicit treatment of the currently implicit bounds and having the compiler check those at every function call? I can't see any fundamental reason why this would need a second type system -- it's "just" a more flexible and expressive version of the current type system. However, I'd not be surprised if actually adapting rustc to properly do these checks would be lots of work, given how deeply well-formedness is currently (from what I gather) engraved into the compiler.

[arielb1]

@RalfJung

Just to be clear, “this sort of thing” is referring to a more explicit treatment of the currently implicit bounds and having the compiler check those at every function call?

The problem with removing the implicit lifetime bounds isn't so much technical - the compiler already handles these bounds fairly modularly - but is rather an "ecosystem split" problem: there is no way in the surface language to control the implicit lifetime bounds, and adding such a way would force "trivial" functions to make a decision: which type parameters do we force to be alive?

There's also no way to require "destructor-validity-for" except for destructors, but that's a more desirable thing which we probably want someday.

[RalfJung]

@arielb1

is rather an “ecosystem split” problem: there is no way in the surface language to control the implicit lifetime bounds, and adding such a way would force “trivial” functions to make a decision: which type parameters do we force to be alive?

Yeah, that seems pretty much necessary -- essentially this is an instance of More implicit bounds (?Sized, ?DynSized, ?Move) · Issue #2255 · rust-lang/rfcs · GitHub