Comment by vacuity
2 days ago
Barrelfish! My dream project is developing a multikernel with seL4's focus on assurance. I want to go even further than seL4's minimalism, particularly with regards to the scheduler. I thiiiiink it doesn't have to be bad for performance. But I've not materialized anything and so I am just delusional. And yes, I am thinking of doing it in Rust. For all of Rust's shortcomings, especially for kernel development, I think it has a lot of promise. I also have the already-loves-Rust cognitive bias. Not trying to somehow achieve seL4's massive verification effort. (Will gasp AI faciliate it? Not likely.) I am sad that Barrelfish hasn't gotten more attention. We need more OS research.
You didn't mention capabilities, otherwise very much yes. Though I have to say I think I'd vote EROS or Theseus harder than Barrelfish; Barrelfish is "just" a multikernel. All I've materialized is a bunch of notes and bookmarks.
Kani et al are very interesting, but can't handle large codebases yet. I'm trying to write Rust in very compartmentalized, sans-IO etc, way to have small libraries that are fuzzable and more amenable to Kani verification.
Capabilities are implied; seL4 did it (everyone cool does it) and Barrelfish designed their capability system off of seL4's. When I say multikernel, that is the main innovation of Barrelfish to take; the kernel design otherwise is more like seL4 or perhaps EROS. Barrelfish also has some interesting takes on other OS services that I want to use, but that's not kernel design. I assume Theseus is [0]. It requires the whole system to buy in to one language and model, so I consider it untenable for a general-purpose OS. I think they're planning to use WASM to increase flexibility, but eh.
> I'm trying to write Rust in very compartmentalized, sans-IO etc, way to have small libraries that are fuzzable and more amenable to Kani verification.
Good design even if Kani isn't used in the end.
[0] https://www.usenix.org/conference/osdi20/presentation/boos
Yeah, also https://github.com/theseus-os/Theseus
One could also run virtual machines for end user workloads under a Theseus design. (The other meaning, not bytecode interpreter.) That sounds like a nice way to real world applicability, to me. History has shown reimplementing Linux syscalls is not realistic (gVisor, WSL1).