[HN Gopher] It's time for a modern synthesis kernel (2019)
       ___________________________________________________________________
        
       It's time for a modern synthesis kernel (2019)
        
       Author : pbrowne011
       Score  : 51 points
       Date   : 2024-11-02 02:50 UTC (5 days ago)
        
 (HTM) web link (blog.regehr.org)
 (TXT) w3m dump (blog.regehr.org)
        
       | pbrowne011 wrote:
       | Previous discussion:
       | https://news.ycombinator.com/item?id=20337231
        
       | 082349872349872 wrote:
       | 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?
        
       | pfdietz wrote:
       | 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.
        
         | mgnienie wrote:
         | Is it any secret who she was back then?
         | https://dblp.org/pid/66/5507.html
        
           | pfdietz wrote:
           | I don't imagine everyone knows, so it's worth mentioning it
           | obliquely.
        
       | sph wrote:
       | 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.
        
       | magicalhippo wrote:
       | 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)
        
       | markhahn wrote:
       | 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.
        
       ___________________________________________________________________
       (page generated 2024-11-07 23:02 UTC)