Re: [seL4] Destroying the Root Thread

Just to make sure we keep the terminology straight: seL4 only has master capabilities, no master objects. The master cap is the cap that you get when you create the object. It confers full rights to that object. You can copy the cap, i.e. create derived caps to the same object, potentially with restricted rights, so that there is still only the one object, but potentially many caps to it. If you revoke+delete this master cap, all caps derived from it are deleted, the object is deleted, and the memory can be reused (if there is still an untyped capability around that covers that memory, which allows you to create objects). If you also remove all untyped caps to that memory, the memory becomes inaccessible to the system. In general, an object is deleted and made available for reuse if the last typed cap to that object is deleted. Memory is available for reuse if there is an untyped cap that covers that memory (potentially existing children of that untyped cap might have to be revoked first as well). In case of the root thread, it may actually hold the only caps to some objects in the system. For instance, it might have created a frame and mapped it into some thread’s address space, but never given the frame cap to that thread, because it doesn’t want to give the thread any power to remap, unmap, or share the frame. If you now delete the frame cap in the root thread, that frame gets unmapped and made available for reuse. If nobody else has an untyped cap that covers this memory, it becomes inaccessible. If you keep the frame cap in an inert CNode, you force it to be static and available for the entire lifetime of the system. If you give it instead to a trusted OS server personality, it could be reused dynamically during runtime. Just depends on what you want to do and how you set things up. Cheers, Gerwin On 20 Nov 2015, at 10:06 am, Raymond Jennings <shentino(a)gmail.com> wrote: What happens to those master objects if the capabilities go poof? Do they get locked up forever, or...as I suspect...do they just escheat to the public as abandoned? On Thu, Nov 19, 2015 at 2:50 PM, Gerwin Klein <Gerwin.Klein(a)nicta.com.au> wrote: