The patch here removes a terminated facet from its parent's
`facet-children` set only in a script, and only after all other
scripts enqueued as part of facet termination have executed without an
uncaught exception.
This means that, if (say) a stop script raises an uncaught exception,
it might have happened after some *but not all* scripts resulting from
calls to `retract-facet-assertions-and-subscriptions!` have already
executed. So some endpoints' assertions and subscriptions will have
been removed.
When the uncaught exception is caught by the handler in
`with-current-facet`, a call to `abandon-queued-work!` is made, which
discards queued scripts, including the remaining assertion-cleanup
scripts as well as the scripts for removing dead facets from their
parents' `facet-children` sets. It also (crucially) discards queued
patch actions, including those resulting from already-executed
assertion-cleanup scripts.
At this point, we have a facet tree with some dead facets still in it,
and no queued outbound patches. The assertions for the still-present
dead facets are still logically asserted.
Then, a call to `terminate-actor!` happens, which traverses the whole
tree enqueueing assertion-cleanup scripts. No user code is enqueued,
so (in principle) no exceptions can be signalled.
Once these `terminate-actor!`-enqueued scripts execute, a pending
patch exists that will remove all remaining endpoint assertions.
The remaining sticky point is the calls to `dataspace-unsubscribe!`.
Happily, these are idempotent because of the implementation in
`skeleton.rkt`.
Prior to this patch, terminating facets were removed early from their
parents' `facet-children` sets, meaning there was no way to find them
again to clean up if a failure occurred during a stop script.
Ideally, it'd be easy to see that the code is correct in this respect.
We're not there yet.
Tony Garnock-Jones