Dynamic resource management with seL4

seL4 kernel
#1

When building dynamic systems, frequently you will have resources that need to be managed that may be passed between processes within the system (such as sockets, files, memory regions, or even higher level resources).

With these resources, the server managing the resources should not rely on the consumers of a resource for the resource to be handled correctly, but consumers of the resource should be able to use it as they please, including duplicating references to the resource and passing the resource to other processes.

What would be the most robust way of managing such resources on seL4? Also, what would be the best way to ensure that when processes end, their shared resources are cleaned up?

My current thoughts on this tend to involve having standard protocols for all such resources to advertise when a reference has been duplicated (such that the server can increase the reference count) and when they are removed as well as having a trusted memory manager to clean up processor memory and cspace when it is exited. Would this be a reasonable way to construct such a system?

#2

Using a reference counter is always frowned upon. The problem is that not all resource users are the same. Consider a server A which obtain resources and distribute it among its client. The guarantee that you are looking for (…consumers of the resource should be able to use it as they please…) depends on the guarantee of resource availability for server A. This forms a hierarchy of resource consumption.

The most appropriate solution is to put the burden of resource management on clients. Referring to the example, rather than relying on A to obtain and refcount resources, it needs clients to use their quota to delegate the required resources. This design while reducing the complexity of server design (e.g. no complex resource negotiation, covert channel and DoS attacks) have some drawbacks (e.g. asynchronous resources disappearance; server could not use these resources to implement linked-lists).

This was originally implemented in Coyotos; you can also take alook at “space bank” in EROS.

#3

Thanks, this is a really interesting way of looking at the problem and should be some good reading material.

The solution your suggesting seems to be to assume (from the server side) that there is only a single user of a particular resource and if the client wants to share that resource it is there responsibility to virtualise that resource across a number of resources it shares with its own clients.

That does seem like an appropriate solution and would likely lead to more library-OS style features being used.