On Mon, 24 Jun 2024 at 23:31, Gernot Heiser via Devel <devel@sel4.systems> wrote: > > 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. > 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 _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
