This Year in Robigalia

Today marks the first anniversary since Robigalia made its public debut. This was much to my dismay at the time. It’s hard to express how much anxiety having something posted to a large forum like HN can cause when the work isn’t yet ready for public consumption. Not a great way to spend your birthday! With that in mind, the project has been relatively quiet until recently. I largely suspended code work on Robigalia while I was interning at Data61 on the seL4 verification team. That didn’t stop me thinking about it, though. A lot of the conceptual design is basically done.

I’ve been working on a "book", "Robigalia: An Operating System for the Modern Era" which documents the design and theory behind Robigalia. This has been really helpful for teasing out design issues before spending a lot of time implementing things. We’ve also been (idly) looking at modeling various portions of the system formally, for use with model checking tools to show that at least the model is sound. As time goes on, portions of the book will be serialized and posted on the blog. The book will become the core of my undergraduate thesis. One such post on timekeeping will be coming out shortly, pending expert review.

Implementation progress hasn’t completely stalled either. I’ve been chipping away at ACPI handling and device drivers. This is slowed massively by me teaching and training other undergraduates at my university how operating systems work, with the hope of getting them to be productive contributors to Robigalia. While I was at Data61, a student there implemented NetBSD’s rump hypercall interface. This will allow us to use NetBSD’s drivers in the short run. This is a huge help, given the wide variety of hardware that a modern OS needs to support!

In terms of inspiration, I’ve been hugely inspired by the Houyhnhnm computing essays, as well as KeyKOS, EROS, and Coyotos. As more of our design is made public, their influence will become very apparent. Our goal of a POSIX userspace hasn’t been forgotten. It’s still there. But making native application support as good as it can be is our top priority. Midori has also been a huge inspiration here.

seL4 has changed in the meantime too. The realtime kernel has been released, as has multicore support and an x64 port. A RISC-V port is also soon to come. We now target what will be known as the "stage" branch of seL4, which contains features destined to be verified, but which haven’t been yet.

The future is bright for Robigalia. While we work on the core, if you’re interested in helping the project, a good way to do that is to give feedback in the IRC channel when we’re brainstorming or analyzing designs. The absolute best way, however, is to contribute to rips, libpnet, tokio, rust-crypto, rustls, rayon, or even Rust itself. Bettering the Rust ecosystem is the best way to better Robigalia, in the short run. If you’re interested in devices, you might take a look at starting a pure-Rust USB stack or Vulkan drivers for some openly documented platform like AMD or Intel. This can largely be done in userspace on Linux, for the first phases.

Our plan is to have an initial release of the book and a working Robigalia system on April 25, 2017. See you then!