Re: [seL4] How to (and how not to) use seL4 IPC

On 3/7/19, Gernot.Heiser(a)data61.csiro.au <Gernot.Heiser(a)data61.csiro.au> wrote: The IPC transport layer for UX/RT will follow these rules for the most part AFAICT (although there is one possible caveat). It will use an unstructured call-return model in which every IPC transport layer call is either a read that requests a specified number of bytes with a specified offset and expects either data or an error code, or a write that sends a specified number of bytes with a specified offset and expects a status code (unlike most IPC transport layers for microkernel OSes there will be no support for arbitrary typed messages or marshalling, with both of those left to higher-level libraries). There will be a short message API using abstract message registers (which may or may not be directly mapped onto seL4 message registers depending onto the situation), a long message API using a shared buffer, and a traditional Unix-style read()/write() API that may use either, with all three being interchangeable (messages will be automatically copied when necessary by the transport layer). All IPC endpoints will be presented as named files much as in Plan 9 (UX/RT will go even further in its file orientation in that all process memory will be presented as files as well). The raw seL4 IPC API won't be exposed to user processes, since the transport layer API will map onto it pretty closely, and I want UX/RT to have only one IPC transport layer that is compatible even between processes using different APIs (and reads and writes will not be required to go through an intermediary server so there will be no performance reason to bypass the transport layer). The caveat is that seL4 may have SMP scalability issues with a general-purpose OS running a wide variety of applications on a wide variety of hardware like UX/RT will be. In a general-purpose OS, processes shouldn't have to be statically assigned to run on specific cores (although of course that should be an option), and they shouldn't have to care about which core a server is running on. Passive servers don't completely solve the problem since I want UX/RT to be compatible with code from other OSes that don't have such a concept, and it should be possible for arbitrary processes (even something like a shell script) to serve filesystems as in QNX and Plan 9. Linux in a VM is not a substitute for native Unix compatibility since my goal is to make an advanced Unix-like OS in which all processes benefit from safer code and extensible multi-server architecture, rather than forcing anything not specifically ported to run in a "penalty box" where it still suffers from most of the problems with conventional OSes. If I can't make seL4 scale well for UX/RT I may end up having to fork it. Of all the existing open source microkernels it is still the closest to what I consider ideal in terms of architecture, despite the possible SMP scalability issues.