←back to thread

A Higgs-Bugson in the Linux Kernel

(blog.janestreet.com)
226 points Ne02ptzero | 1 comments | 02 Jul 25 18:34 UTC | HN request time: 0.409s | source
Show context
snvzz ◴[03 Jul 25 08:35 UTC] No.44452910[source]▶
With millions of LoCs, it is no surprise there are bugs.

Worse yet, the kernel runs in supervisor mode.

This kernel design is bankrupt. There's much better available, such as seL4+Genode.

replies(4): >>44453275 #>>44453449 #>>44454879 #>>44459008 #
1. burnt-resistor ◴[03 Jul 25 20:42 UTC] No.44459008[source]▶
seL4 exhibited great advances in software engineering processes and advances in correctness, zero-copy microkernel IPC performance, and capabilities-based security, but these need explanation, adaptation, and evangelism to real-world use-cases like Linux.

Microkernels have severe limitations when it comes to transactional boundaries of calling multiple subsystems and rolling back on failure.

Linux has too much inertia to reinvent itself instantly or completely into XYZ.

What would add more value would be gradual conversion to Rust and adding formal verification to C and Rust like specifying invariants in comments/metadata like frama-c and/or flux.

PS: Religious judgement opinion wars are rarely constructive.