Comment by yencabulator
2 days ago
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).