On 25 Jun 2024, at 06:30, Isaac Beckett
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. 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