4 ms·

If it took a huge development effort for SEL4 to get to the state it is currently in, doesn't that make it unlikely anyone can easier go in and change thinks or

by Hypx 12y ago

If it took a huge development effort for SEL4 to get to the state it is currently in, doesn't that make it unlikely anyone can easier go in and change thinks or add features? Not knowing too much about SEL4, but it just seems like a very limited kernel, meant primary for embedded devices, and that's about it. It doesn't seem to have the feature you expect from kernels these days. A Rust based kernel could be a *nix, and do everything from desktops to server. It would be developer friendly in the same way Linux or Windows is. Plus, the baseline safety would be much higher with a Rust based kernel, without having to formally proven everything.

nanofortnight 12y ago
It's a microkernel: it is intentionally minimal. Microkernel operating system design is from the 1980s is different from the monolithic, bulky and older operating systems designs you are used to (famously including Linux, see the Tanenbaum-Torvalds debate). It has all the features that it would likely ever need already. Instead of having all the services required for an operating system in the kernel, the kernel just implements the bare minimum including fast IPC. Things that traditionally are implemented in the kernel (filesystems, device drivers, other modules, etc) are all implemented as services living in userland and are assigned the minimum necessary additional permissions for them to perform their task. You can build a *nix like system on top of seL4. You can even run Linux itself on top of seL4, with L4 acting as a hypervisor. An operating system doesn't consist of just the kernel.
imanaccount247 12y ago
>If it took a huge development effort for SEL4 to get to the state it is currently in, doesn't that make it unlikely anyone can easier go in and change thinks or add features? No. Most of the huge development was in developing proofs for C. The developers now find that development is easier than just using C directly. The process is to write it in a high level specification language, then when you're done messing around and know you have it how you want it, translate it to C by hand and the proofs will tell you that you did it right (or wrong). >It doesn't seem to have the feature you expect from kernels these days. It has exactly the features we expect from kernels these days. The features we do not expect from kernels these days but did expect from them 30 years ago are available in a library where they belong. >A Rust based kernel could be a *nix So can any L4. Why would "start from absolutely nothing" be easier than "start from an existing microkernel"?

by Hypx 12y ago

nanofortnight 12y ago

It's a microkernel: it is intentionally minimal. Microkernel operating system design is from the 1980s is different from the monolithic, bulky and older operating systems designs you are used to (famously including Linux, see the Tanenbaum-Torvalds debate). It has all the features that it would likely ever need already. Instead of having all the services required for an operating system in the kernel, the kernel just implements the bare minimum including fast IPC. Things that traditionally are implemented in the kernel (filesystems, device drivers, other modules, etc) are all implemented as services living in userland and are assigned the minimum necessary additional permissions for them to perform their task. You can build a *nix like system on top of seL4. You can even run Linux itself on top of seL4, with L4 acting as a hypervisor. An operating system doesn't consist of just the kernel.

imanaccount247 12y ago

>If it took a huge development effort for SEL4 to get to the state it is currently in, doesn't that make it unlikely anyone can easier go in and change thinks or add features? No. Most of the huge development was in developing proofs for C. The developers now find that development is easier than just using C directly. The process is to write it in a high level specification language, then when you're done messing around and know you have it how you want it, translate it to C by hand and the proofs will tell you that you did it right (or wrong). >It doesn't seem to have the feature you expect from kernels these days. It has exactly the features we expect from kernels these days. The features we do not expect from kernels these days but did expect from them 30 years ago are available in a library where they belong. >A Rust based kernel could be a *nix So can any L4. Why would "start from absolutely nothing" be easier than "start from an existing microkernel"?