Break the spawnd kill API into kill + cleanup.
authorRazvan Damachi <razvan.damachi@gmail.com>
Tue, 27 Jun 2017 10:14:28 +0000 (12:14 +0200)
committerSimon Gerber <simon.gerber@inf.ethz.ch>
Thu, 31 Aug 2017 14:35:08 +0000 (16:35 +0200)
commit11268e99bb0c6fc4e2bddd3ba507519d0db55bec
tree21f1aed90a9dbee693fb093c32769dfca14e44c3
parent5c4c481f2ee9b7f54330220ce8aa9bccee19e797
Break the spawnd kill API into kill + cleanup.

Kill just revokes the DCB, thus removing it from the run queue. Cleanup then
revokes the victim dispatcher's root cnode.

The change is meant to fix the problem where killing the main dispatcher of a
domain or having it naturally exit main() would cause the other dispatchers to
pagefault. This used to happen because dispatchers of the same domain share
their vspace, hence when kill & cleanup were performed together the vspace
of all dispatchers would be revoked as soon as the first dispatcher exited or
was killed.

The process manager attempts to fix the issue by first sending a kill message
to each spawnd running dispatchers for a domain, in order to dequeue the DCBs.
Then, only when all DCBs have been dequeued, a cleanup message is sent to each
spawnd to further clean up the victim's cspace.

Signed-off-by: Razvan Damachi <razvan.damachi@gmail.com>
if/spawn.if
usr/proc_mgmt/domain.c
usr/proc_mgmt/domain.h
usr/proc_mgmt/service.c
usr/spawnd/ps.c
usr/spawnd/ps.h
usr/spawnd/service.c