-
Notifications
You must be signed in to change notification settings - Fork 13.2k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Box-enclosed destructors can't safely access other boxes. #3039
Comments
No, this should not compile and it's not related to those bugs. Values with dtors should not have @ boxes in them, statically. They're supposed to be acyclic, precisely so they can run top-down. This is why resources were originally their own kind. Kind system bug. |
Sorry, that sounds yell-y, I don't mean to be unduly harsh; just want to be completely clear that "running dtors in multiple passes" is how finalizers work, not dtors, and we've made a very explicit effort to avoid that up until now. If it's not working, that's a bug, not a "let's switch to finalizers" opportunity. |
No problem. I'm trying to come up with a way that your proposal isn't quite complete, involving allocating new @-boxes inside of destructors, but I think it's solid. I came up with crashing code that respects your proposed kind restriction, but it just ended up being another demonstration of why TLS deserves to be unsafe. (note that this code follows the "tls is supposedly safe if you don't use polymorphic key functions" rule.)
|
However, if we forbid destructors in things that contain @-boxes, then the doubly-linked-list cannot possibly have its own auto-clean-up function. If a dlist goes out of scope with elements still inside, they'll stick around until the cycle collector runs (or until we add true GC to the language...). There's already a |
OK, I think your proposal is right. I was able to break it with three canonical "funny businesses" - global state (TLS, above), captured closure environments, and existentials, and all three of them can be ruled out with the "no box" kind. Crashing code with a @-closure: http://pastebin.mozilla.org/1716353 One question still: Will the "no-box" kind be equivalent to "send", or will it be able to permit region pointers too? |
these crashes still happen when the 'fail' statement is removed, which convinces me that the box annihilator is orthogonal to the problem. |
I'm not totally convinced it's no longer possible to write this program, but |
|
Oddly, if I switch the |
I looked into the mystery a bit more, and it turned into more of a mystery, enough that I'm not confident that my above code is a reproduction of the original bug here. But I note that in the other bug, the place where it segfaulted changed (here, it segfaults in |
Is this fully fixed by d4fee24? |
tests/catch_panic: make output easier to interpret
## What's Changed * Upgrade toolchain to 2024-02-14 by @zhassan-aws in model-checking/kani#3036 **Full Changelog**: model-checking/kani@kani-0.46.0...kani-0.47.0 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Ran into this issue when trying to write a destructor for the doubly-linked-list. The following code segfaults after (i believe) one of the boxes has been annihilated and the other's destructor attempts to run.
The solution, I think, is for the box annihilator to run in two phases - one phase to run destructors, and then another to actually annihilate the boxes after that. (EDIT: this is a point of contention.)
The text was updated successfully, but these errors were encountered: