ManyThreads
resolve recursive deletion of capability maps
Capability maps can contain the original capability to a slice of kernel memory. From this kernel memory, another capability map can be allocated and then mapped into the capability space. Then another slice of kernel memory can be allocated in that map in order to repeat. This results in a long chain of length linear to the size of available memory.
Deleting such chain is non-obvious: In order to delete the first kernel memory, it is necessary to delete the conainted capability map. In order to delete it, all contained capability entries need to be deleted. This triggers the recursive deletion of the next slice of kernel memory, which requires to delete it's contained capability map and so on.
Our current implementation probably runs out of stack space. The code in seL4 might run of processing time before the next timer interrupt. One possible fix is, to transform the recursion into an iteration by using a single-linked list to stack up the "to-be-deleted" kernel memory and capability map objects. The needed pointer/handle is already in the kernel object for the chain of "ready-to-delete" objects.
Will probably need more discussion.
