On Mon, 24 Jun 2024 at 23:31, Gernot Heiser via Devel wrote:

On 25 Jun 2024, at 06:30, Isaac Beckett wrote:

...

I recall reading about old CPUs/ISAs made for Lisp machines, with features and optimized for specifically running Lisp. And I’ve heard people discuss how current CPUs are optimized for C code and similar programming paradigms, and vice versa: C and others are optimized for those CPUs.

Lisp machines were stack machines with tagged memory words for HW-enforced type enforcement.

...

This got me wondering, what might a CPU or instruction set designed more specifically to run seL4 look like? I’m guessing it might involve capability hardware like CHERI to accelerate seL4’s software implementation of capabilities, but what else might be relevant?

CHERI caps don’t do much for seL4, they are good for intra-address-space isolation (and thus single-address-space OSes). seL4 is about AS isolation.

True, not for the seL4 kernel itself as a kernel, but it could greatly help with securing C-based seL4 userspace by enforcing memory/pointer safety. So it could complement seL4's inter-address-space isolation by also providing intra-address-space isolation. This is useful for the seL4 ecosystem itself (and not just single address space OSes) when, for example, it runs single-address-space servers/applications (e.g., rump kernels) or VMs (e.g., Linux). This is comparable to re-writing Rust-based user-level or formally verifying userspace to not have buffer overflows at all. But it doesn't have to incur the overhead or time of re-writing everything in Rust and/or formally verifying large, existing, C-based projects such as seL4 libraries, rump kernels, etc.

The best thing the architecture can do for seL4 is make context-switching cheap.

Funnily, these days all major ISAs are similar, with x86 becoming faster and Arm slower than they used to be, and RISC-V with ASIDs is similar.

Gernot _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems