On 1 Apr 2025, at 00:50, 1plus.yijia--- via Devel <devel@sel4.systems> wrote:
One the advantages of microkernel is the extensibility of user space components; however, doesn't the static system design eliminate this advantage? Do I miss something? I wonder if it possible to only recompile a component and replace an older one; if yes, if it possible to replace it in runtime.
There are several aspects to this question. I assume you’re referring to LionsOS with its static architecture. For one, extensibility doesn’t necessarily imply “dynamic extensibility”. LionsOS is an extension of the minimal microkernel, and you can configure different systems with different architectures, i.e. extend the kernel in different ways. In fact, LionsOS very specifically aims to remain policy-free (within the limits of the static architecture). Second, no-one forces you to use LionsOS – it does restrict the design space, for reasons of making end-end verification tractable in a short-ish time period, and without limiting its use in what I have seen in the embedded-systems space to date). Other people are building different systems on seL4, eg KOS from Kry10, and we’re working on a fully-general and dynamic open-source design (but that one’s very early days): https://trustworthy.systems/projects/smos/. Gernot