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