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
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