Is it immediate UB to cancel a thread and deallocate it's stack

[chorman0773]

System APIs pthread_exit and pthread_cancel are able to terminate a thread and deallocate it's stack without running destructors.

Because of APIs like Pin, this cannot be sound for Rust code. Is there any reason that this should be considered undefined behaviour immediately (if any rust frame is on its stack), or just unsound in the face of stack-pinning. Additionally, is there anything else beyond Pin that would cause this to be unsound (if it is defined).

[CAD97]

Generally, Rust code is allowed to assume that stack locals' destructors run, so deallocating stack without running destructors is isomorphic to a forced unwind (longjmp) without running destructors, and is presumably UB since this is a guarantee from the language to the developers.

Before pinning, we had scoped threads and take_mut; various APIs that rely on the running of destructors (sometimes just of unwind-to-abort shims) for soundness in the face of other threads seeing the mess left behind if we don't get a chance to clean up.

Carving an open middle in language semantics is hard; you can't really have both that stack destructors are guaranteed to run before deallocation (i.e. stack pinning is sound) and that it's not UB if destructors aren't run; failure to prevent NonBehavior is exactly as meaningless as the execution of UB; you've exited the domain of the well-defined language and now all bets are off.

[digama0]

Carving an open middle in language semantics is hard; you can't really have both that stack destructors are guaranteed to run before deallocation (i.e. stack pinning is sound) and that it's not UB if destructors aren't run; failure to prevent NonBehavior is exactly as meaningless as the execution of UB; you've exited the domain of the well-defined language and now all bets are off.

I don't agree with this. Skipping destructors violates the safety condition on the affected types, hence longjmp or equivalents must be unsafe, but it does not mean that it has to be immediate UB unless the compiler also takes advantage of the running of destructors in some way (which may well exist but does not seem to be indicated by this line of investigation). The UB would happen when one of those types with a violated safety condition goes on to assume that its invariants still hold and does a UB later.

In practice, this still means that you (the user) can't meaningfully use longjmp safely unless you know you are not jumping over destructors, or you control all the code being jumped and know that it is safe to mem::forget those types, since if you jump over code out of your control then you have no idea if doing this will cause UB in any later operation.

[RalfJung]

In the context of the Rust AM, asking whether thread canceling / setjmp-longjmp are UB doesn't even make sense since these operations literally cannot be expressed in the language. Calling such operations is akin to using inline assembly to modify state that is private to the abstract machine implementation: it is your responsibility to ensure that all invariants are preserved. If you fail to do that, you have UB -- but a somewhat different kind of UB than what Miri raises, since this UB is not triggered by the AM, it arises from violating the assumptions of the "AM to ASM" lowering proof.

We don't currently have a great way to write down these invariants; I guess the best we can do is tell programmers some things they can do and not let them do anything else. (Yes, this is axiomatic.)

Having said all this I guess it doesn't really help to answer the question... except for one observation: axiomatically speaking, the default is that things are UB, and we have to explicitly write down each guarantee ("you can mess with the ASM state in the following ways and it's okay"). We should probably be careful not to guarantee too much here until we have a better understanding of which obligations this imposes on the compiler.

[RalfJung]

Why is this thread separate from #404? Both are basically the same question: removing Rust stack frames from the stack without giving the AM implementation a chance to do anything. We should answer these questions in a consistent way and also discuss them together, IMO.

[chorman0773]

The T-opsem meeting separated the questions, somewhat. And there is a bit of a difference in that longjmp is partial and cancelation is total. There was also a third question of terminating a thread and leaking it's stack, which was wrapped into an issue on progress.

…

On Wed, May 24, 2023 at 08:58 Ralf Jung ***@***.***> wrote: Why is this thread separate from #404 <#404>? Both are basically the same question: removing Rust stack frames from the stack without giving the AM implementation a chance to do anything. We should answer these questions in a consistent way and also discuss them together, IMO. — Reply to this email directly, view it on GitHub <#405 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABGLD2ZZJ7ZR7PZAZYBBRLTXHYAWPANCNFSM6AAAAAAYMPIQQM> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[nbdd0121]

In glibc pthread_exit is implemented as forced unwind, and, if that failed, a longjmp. So they are exactly the same.

For implementations that just discard the stack completely, we can still conceptually model it as a longjmp to the point before the first Rust frame.

If we solve the partial frame deallocation problem then it essentially solves the total frame deallocation problem.

[RalfJung]

Yeah, I don't see a benefit from focusing on the "total" case, it should entirely fall out of the longjmp case.

[JakobDegen]

Ah, the point about this actually being the same question as longjmp is a good one, I hadn't realized. I'm ok to close this issue then if we want

[RalfJung]

Closing as duplicate of #404 then.