finally read seL4's autobiography https://trustworthy.systems/publications/nicta_full_text/8988.pdf i think the thing that most surprised me was how disappointingly incremental it conceives itself to be. "monolithic kernel with blue hair and a mohawk"
Post
Replies:
9
Boosts:
2
i think i just totally misunderstood what people meant by "microkernel":
Microkernels minimize the functionality that is provided by the kernel:
i thought this meant like oh the actual user as in application code written by a human who is not the os developer can implement a whole stack if they want. i thought message passing was blurring the distinction entirely
The kernel provides a set of general mechanisms, while user-mode servers implement the actual operating system (OS) service
turns out "user" just means "technically in 'user' mode, with virtual memory"
if anything, the empathy between the actual user and the kernel just grows weaker. if the user is defined purely in terms of memory isolation, translation of intent becomes immediately overshadowed with "what if we did yet another permissions system".
multiple times the prospect of a process forcing a denial of service was described as further justification to scrap any consideration for expressions of cross-subsystem behavior.
maybe if you can be DOSed it's a sign your kernel mechanisms still try to infer way too much from decontextualized syscalls?
Application code obtains a system service by communicating with servers via an interprocess communication (IPC) mechanism, typically message passing.
and IPC boundaries are still basically the same kind of thing, even though we now ask the application to speak directly to the hardware interfaces???
i assumed it would just mean the interfaces between kernel duties would be more explicitly specified and queued among themselves--NOPE:
Hence, IPC is on the critical path of any service invocation, and low IPC costs are essential.
what is "low IPC cost"? surely it's not--
The typical cost for a one-way message was around 100 μs, which was too high for building performant systems.
performant systems demand low latencies!!!!!! all is sacrificed at the altar of latency!!!!! a human brain is just a really fast processor!!!!!
This resulted in a trend to move core services back into the kernel
giving up isolation on the altar of latency (the exact same thing UNIX does)
There were also arguments that high IPC costs were an (inherent?) consequence of the structure of microkernel-based system
- define every single interaction in terms of IPC that can't be planned for in advance, can't express future behavior, and can't even signal dependencies between IPC calls
- absolutely refuse to back down on IPC cost being measured by latency
that's not a "consequence", that's just refusing to innovate and calling yourself clever because others doubt you
they keep talking about fucking decades of:
- talking about i/o latency like it's the second coming of jesus christ
- using "generic" and "portable" exclusively to mean valorizing the self-defeating embrace of the absolute lowest common denominator interfaces
"portable" i typically understand to mean "does not force users to translate their program logic in terms of your hyper-specific domain assumptions". but that implies users have a program logic and that the OS is a means to express that
A common thread throughout those two decades is the minimality principle, introduced in Section 3.1, and a strong focus on the performance of the critical IPC operation
talk to your kids about IPC. before it's too late.
so an overarching principle is "minimality" (bleak!). what does that mean?
3.1. Minimality and Generality
The main drivers of Liedtke’s designs were minimality and IPC performance, with a strong conviction that the former helps the latter.
i could buy this. ok seL4 jesus, preach me your teachings:
Specifically, he formulated the
microkernel minimality principle [Liedtke 1995]:
A concept is tolerated inside the μ-kernel only if moving it outside the kernel, i.e. permitting competing implementations, would prevent the implementation of the system’s required functionality.
this is why i don't do theology. they translate His words:
This principle, which is a more pointed formulation of “only minimal mechanisms and no policy in the kernel,”
"no politics in the kernel"
the spectre of throughput begins to show its face:
In original L4, “long” messages could specify multiple buffers in a single IPC invocation to amortise the hardware mode- and context-switch costs.
but of course, long messages induce latency, so:
While long IPC provides functionality that cannot be emulated without some overhead,
literally satisfying the exact definition of minimality, but instead:
in practice it was rarely used: Shared buffers can avoid any explicit copying between address spaces and are generally preferred for bulk data transfer.
yeah, just remove memory isolation entirely. anything to reduce my IPC latency benchmarks except more structured communication
