On Tue, Apr 6, 2021 at 1:56 PM Royce Mitchell III
Hi all, I've been passively following seL4 for several years. I've been reading the documentation, tutorials, watching YouTube videos.
The concepts behind capabilities and other types of kernel objects are starting to sink in but there's one piece of understanding that's eluding me.
If I just haven't stumbled across it yet in the documentation, then pointing me in the right direction would be greatly appreciated.
Given:
* An ethernet driver named "e1000" and 2 devices "eth0" and "eth1" controlled by that driver.
* A "tcp" service that would implement that network protocol.
* A higher level service named "network" that implemented some kind of networking abstraction for us.
How would:
1) the "network" service advertise its services as available via IPC?
2) an application locate this "network" service to be able to IPC with it?
I assume the mechanisms here would also apply to interactions between services as well. I picked the "network" service in this example only because it would be the boundary between application and OS services.
I'm guessing that maybe this is purely an OS design decision and not the purvue of the kernel itself. Perhaps init could launch a "service manager" process that would be responsible for starting up services and drivers for example and this "service manager" could provide an IPC endpoint back to init (or whomever) to use for IPC discovery. Then, whenever a new process is started, it is provided with the IPC discovery endpoint information that it is to inherit.
If my assumptions are correct or close, or even dead wrong, would someone be willing to share some pseudo-code on what this could/should look like in seL4?
If a central service manager is needed to glue the core OS together, does it represent a single point of failure and how would the OS recover if it crashes and loses it's database of available services without having to rebuild and restart all drivers and services? (I'm not saying that's a bad thing, just trying to wrap my head around how this particular part of seL4 works)
It is a bit difficult to introduce string -> capability lookups without introducing some form of ambient authority, where the object connectivity graph of a typical capability system is heavily reliant on application and services having direct connectivity. service managers of the sort introduce a difficult many to many applications -> service manager, service manager -> services type of object graph, which in turn loses many valuable properties... historically capability systems have typically avoided introducing such a mechanism. Instead relying on some kind of reflection mechanism or protocol. Some systems (keykos and eros) had an allegedType message that could be sent to capabilities, so if you know the allegedType of a network capability, and the messages it receives or a IDL description of the network capability associated with the allegedType, you could dynamically send it messages to which it purports to understand. This is somewhat a matter of convention, I'm not certain if there is any such thing built in to sel4 tooling e.g. to generate unique alleged types for camkes interfaces and a well-known message to dynamically query them. it sounds like there is not though. The general benefits of this is that given some enumerable set of capabilities it allows some process to filter the interesting ones, rather than introducing any new connectivity + single point of failure