Just the operating system, but I like Barrelfish's idea of having a separate kernel on every core and doing message passing. Each "CPU driver" is single-threade

Just the operating system, but I like Barrelfish's idea of having a separate kernel on every core and doing message passing. Each "CPU driver" is single-threaded, non-preemptible (no interrupts), shares no state, bounded-time, and runs to completion. Userspace programs can access shared memory, but the low-level stuff doesn't do that. Bounded-time run to completion kinda makes me think of seL4, if it was designed to be natively multicore. https://en.wikipedia.org/wiki/Barrelfish_(operating_system) https://en.wikipedia.org/wiki/Barrelfish_(operating_system) https://barrelfish.org/publications/TN-000-Overview.pdf https://barrelfish.org/publications/TN-000-Overview.pdf