It's time for a modern synthesis kernel (2019)

I remember meeting Alexia briefly decades ago. I was working in western Connecticut and went down to NYC (Columbia, I think) to hear presentations at a meeting where the Synthesis kernel was discussed. It was clever and memorable. She was known by her deadname at the time; the literature from then still has that name, so be aware if searching.

Interesting idea but I'm not sure I see the practical benefit. Also, this seems to be implemented as a partial evaluator/compiler for C, and I am not really sure C is the best suited language for this kind of isomorphic transformations.

Lately I have been doing some reading on term-rewriting systems, and designing a simple string->sexp rewriter, which could form the basis of a compiler or partial evaluator: a compiler is nothing more than parsing into an AST and rewriting AST all the way down to another string (of machine code bytes). A partial evaluator for C would be much easier to write if you first turn it into parsed AST, which would look a lot like S-expressions from Lisp.

Anyway, I smile and cringe at the idea of embedding LLVM into the kernel.

Reminded me of Singularity[1], Microsofts research OS where the kernel and drivers were all written in managed code like C#.

[1]: https://en.wikipedia.org/wiki/Singularity_(operating_system)

Previous discussion: https://news.ycombinator.com/item?id=20337231

Rpython's JIT is pretty good at removing administrative work from loop interiors and oo layers; one might be able to play with it to see how much practical specialisation may help? Depending upon how much of the OS ABI its generated C uses, that could be done at least in a microkernel setup, and maybe even on nearly-bare metal?

eBPF

I think the question becomes: how do you all creation of safe kernel code when that code becomes more functional. historically, BPF was just performing some filtering (near reception -> efficient). eBPF originally added more metrics and aggregation. But it's also been extended to change, drop, direct packets, and hook into all sorts of parts of the kernel. All based on the premise of compiling to safe code (which mainly means that you prove it does only what you intend).

So the Synthesis question is really: suppose a kernel only comes with eBPF, and you synthesize all the other interfaces you need?

I think this leads to some metaphysical navel-gazing - what is an kernel+OS, really? Practically, it's about providing stable interfaces (both upwards to user-space and downwards to hardware) so you can run things. Philosophically it's really just resource management, isolation.