I understand the minimality principle but one should not be afraid to violate layers of abstraction when justified. The whole point of the minimality principle is to improve modularity and remove the need to worry about the correctness of various OS components.

What would you be able to do in a userspace scheduler that couldn't be done safely in an in-kernel scheduler? Why couldn't it be configured or given a safe API to interact with userspace at runtime? But I guess your shared memory bit is an API to a userspace scheduler?

Well, one thing about adapting seL4 is that we shouldn't assume derivatives will be formally verified to the same degree. Ideally we would, but I don't expect this to happen in practice. And having a kernelspace scheduler that is minimal and requires a userspace scheduler to achieve full control of scheduling, where a userspace scheduler would do, is redundant overhead. If the kernelspace scheduler wasn't minimal, it would both be hard to verify and extend. This is all in line with seL4's design. So you're concerned about power where the question was always about performance. Hydra had userspace schedulers way back when, and it wasn't followed because it was prohibitive then. The minimality principle might be given various explanations, but I think the end result of what a system following it achieves speaks for itself.

> I understand the minimality principle but one should not be afraid to violate layers of abstraction when justified.

Rather, in a well-designed system, the justification necessarily is performance. Abstractions exist for the ease of the developer to write code that is correct. Performance (runtime, memory usage, etc.) is the concrete impact of code. For concerns like debugging or flexibility, those arise if the abstractions are lacking. Performance concerns arise because even good abstractions impose overhead. Note that conventional layered architectures are usually poor abstractions for implementation. Good for design but not coding.

> But I guess your shared memory bit is an API to a userspace scheduler?

Indeed. I would rather not, but shared memory probably is necessary to some degree for a userspace scheduler.