Thank you, so hi, my name is Drew and I'd like to talk to you today about a new microkernel
I've been working on called Helios.
For context, I work at a place called Source Set and I'm the project lead for a new programming
language called Hair and I've done many other projects but that's what's relevant for today.
This is a new microkernel.
It's inspired a lot by SEL4 but it differs in many ways.
It's written in this hair programming language that I mentioned and one of the main motivations
for it is to find out if we can use the hair programming language to write microkernels
in or any kind of kernel really.
Presently it runs on X8664 and ARM64 and we're thinking about risk 5 in the foreseeable future.
In terms of the footprint of this kernel, it's pretty small.
The portable code is about 8,500 lines of code.
Each architecture adds about another 3,000 lines of code, all hair code and then add
on top of that the boot loaders which are also written in hair and it's a pretty small
footprint.
We've been working on it for about nine months now and we use the GPL3 license.
So again, about nine months of progress so far.
Where do we stand in terms of functionality is about here.
We have capability-based security and the capabilities do work similar to what SEL4
does and also similar to SEL4 we have inter-process communication working using endpoints and
notifications, very similar to SEL4 with some notable differences.
We have scheduler work, we're in user space and we have multi-processing but we don't
have symmetric multi-processing, we have only one core at the moment but we'll do SMP fairly
soon.
We also have all of the necessary rigging in place for drivers in user space so we have
access to ports on X86 and we have memory and map.io support as well as IRQs are rigged
up.
And for booting up the kernel, we currently support EFI on ARM and multi-boot on X86.
We'll be doing EFI on X86 as well in the future and our plan is to also do EFI on risk 5.
So we'll use EFI as the default approach for booting Helios in the future.
But why should we be thinking about writing a new macro kernel or a new kernel of any
sort?
I imagine that for this particular dev room I don't need to give too many reasons but
for the sake of anybody who's maybe watching online, the first point is pretty obvious.
It's really fun to write kernels and that's kind of reason enough so I'm having a great
time working on it and that's enough for me.
But also, importantly, we've been working on this programming language here for about
three years now and it's a systems programming language and one of our goals is to be able
to write things like kernels and so in order to prove that we have achieved this goal,
we have to write a kernel with it and so Helios is that kernel.
I also am a big fan of SCL4's design but I also have some criticisms of it and I'm curious
if we do a kernel which is inspired by SCL4, can we make some improvements on its design?
And if we were to be particularly ambitious, could we perhaps do better than Linux?
We'll see.
I should also point out that this slide deck is going to cover a lot of details which maybe
will seem redundant to people who are already familiar with the design of SCL4 and that
could be a problem with this audience but please bear with me while I explain things
that you already understand at some point in the future.
So the hair programming language, this is the pitch from the website.
I won't read it out to you but essentially it's a very simple language which is very
close to C in terms of design but with a lot of benefit of 50 years of hindsight of what
could be made better about C but compared to other C alternatives that are floating around
today like Rust and Zig and Nim and so on, I would say hair is much, much closer to C's
original ideas than any of these other attempts but it improves in many respects like dealing
with modules and error handling and bound checked things and some safety features.
So it improves in a number of respects.
It's also very, very simple.
So here we have some more line counts for people who like the line counts.
The hair compiler is 18,000 lines of code in C11.
The back end that we use, it's not L of the M, we use cube as our back end, is another
12,000 lines of C99 and then we use binutils for the linker and assembler and that's it.
We support three targets, XA664, AR64 and RISC-564 which it's no coincidence that those
are the targets I'm working on for the macro kernel.
We intend to add more but this is where the language is at.
I started, again, I started here specifically to work on this kind of project and this project
exists to validate the language design for this use case and also because it's fun and
maybe it could be useful.
For those of us who have never seen any hair code before, I just have a little snippet
here so you can get a vague idea of what it looks like.
Again, not going to explain this in too much detail but if you're familiar with C, a lot
of things will seem familiar to you and you can probably guess the double colon does namespaces.
You can guess what the no return tag does.
It's fairly straightforward programming language and this is what it looks like.
The code sample we're looking at here is the portable kernel entry point so it starts with
the boot letter entry point and then the arch specific entry point.
This is the first line of portable code that runs when you boot the kernel.
With the context out of the way, let's talk about Helios itself.
We're going to go over a number of things here with respect to the design of Helios
and the implementation of Helios.
I'm going to talk about our approach to capabilities and on memory management and some other things
specific with how various capabilities actually work like processes and threads and talk about
inter-process communication and then also talk a little bit about the implementation
as well, not just the design.
Here's the big picture in terms of the implementation.
Again, those who are familiar with SEL4 will find no surprises on this slide but essentially
access to all system resources including kernel objects is semantically governed by user space
and we use the MMU to isolate user space processes from each other and to enforce this capability
model.
On system boot up, the kernel enumerates all of the resources on the system, all of the
memory and all of the IO ports and all of the IRQs and it prepares capabilities that
entitle the bearer to access these resources and then it hands all of these off to the
first process, the init process which can then subject to its own user space policy
decisions, choose how to allocate those resources to various processes in such a way that it
can provide a secure system.
Here's a look at our capabilities.
There's an example here on the left of a fake physical address space and on the right shows
the kind of state that we'd be storing in this.
Here we have a number of physical pages, one for a capability space, one for a virtual
address space for a task, a bunch of memory pages, some free memory and so on.
In this physical memory, we store the state you see on the right, so the C space here
stores a list of capability slots, very similar to SEL4, and in those capability slots is
a very small amount of state.
Each of them leave 64 bytes so there's not a whole lot to store there.
In this case, a task, which is like a thread or a process, stores a pointer to another
physical memory page where the bulk of its state really lives.
In this case, we have an example of some registers for XDD664.
And the access to this state is gated behind the MMU, so only the kernel itself can directly
read from this kind of physical memory.
But then, user space, who, you know, maybe this process that we're looking at has semantic
ownership over the C space and this V space.
They can invoke the kernel to do operations against those things, but they can't actually
directly access the memory.
Instead, the virtual memory can only contain certain kinds of capabilities or certain kinds
of physical memory pages, so that could be, you know, arbitrary general purpose memory
or it could be a memory map diode, it could end up in their address space.
But while they have semantic ownership over these other capabilities, the actual state
behind them is not accessible to user space.
So in order to work with these capabilities that the user space has semantic ownership
over, it uses, of course, the syscall API.
And Helios has a very, very small syscall API, it is a microkernel after all.
We have 14 syscalls, which I have enumerated here, 12 of these are for working with capabilities.
And again, if you're familiar with SEL4 here, there's probably no surprises here, except
maybe for syspol, which I'll talk about later.
So here is a little example of how you might invoke a capability on x86 to make use of the
microkernels API.
Again, you're going to be making a syscall here at the end, and here we're going to
be filling up registers and memory buffers with the information we want to use.
So this code is going to invoke the vspace map operation, which accepts a page capability,
a virtual address, and a list of mapping flags, like writer or execute.
And its goal is to map a page of physical memory into a slot in a virtual address space.
And in order to invoke this operation, the caller needs to have access to a vspace capability,
which they're going to modify, and a page capability, which they're going to map.
And these capabilities are provided here in two different ways.
The object being invoked is the vspace, and it gets its own register, RDI, which is the
first API register.
The page which is being used, again similarly to SEL4, is going to be placed into that process's
IPC buffer, which is done here with a fake capability address for the page.
And then we have additional arguments like the message tag, which contains the operation
name, the number of capabilities, and a number of parameters.
And then any additional arguments to the function.
You run syscall, and the operation happens.
I also want to talk a little bit about the specifics of interprocess communication.
So we have two approaches, and I'll first look at endpoints, which they are kind of
a generalized form of IPC.
And the way you use them is very similar to how you use chronologics.
In fact, the interface is uniform, but it can send a set of registers or a set of capabilities
between tasks.
So one task can transfer a capability to another task.
There is synchronous, so calling send on an endpoint or calling receive on an endpoint
will block until the two tasks run debut.
And if there are many senders or many receivers, then the one who has been blocked the longest
will wake up, so you can have many processes, maybe doing some kind of load balancing operation
against IPC operations.
And also, SEL4 style call and reply is supported, so if one task does a call rather than a send,
then it immediately blocks waiting for the reply, which is guaranteed to go back to the
same thread.
I have here a more detailed example of exactly how that kind of IPC interaction looks on
Helios.
So I have here on the left one task, and on the right two tasks that want to communicate
with each other, and the text which is in black is taking place in user space, and the
text in red is taking place in kernel space.
So let's say task two is a daemon or a service of some kind which wants to provide a service,
and so it's going to essentially have its main IO loop call sys receive and then block
until somebody has work for it to do.
And task one wants to be a consumer of that interface, so it will invoke sys call, and
the kernel will notice that task two is blocked waiting for somebody to call it.
And so the kernel will perform the copy of registers, move any capabilities as necessary,
unblock task two, and then block task one while they wait for task two to process the
message and prepare a reply, which is what happens next over here.
The sys call returns from task two, they process the IPC request according to however
they implement their services, and they call the reply sys call, which copies the reply
registers back to task one, very similar to this fourth step, and then unblocks task
one, and then both of them can proceed onwards with whatever CPU time they're given.
Another interesting feature we have in terms of endpoints, which is one of the things that
distinguishes Helios from SEL4, is support for a pull-like interface.
Similar to Unix's pull on file descriptors, Helios lets you pull on capabilities.
So this is an example from the serial driver that I implemented for the standard X86 comports
service.
It has two capabilities it mainly cares about.
It has an endpoint capability that it uses to implement its API for consumers of the
serial port.
So if you want to request a read or a write from serial, you'll send a message to this
endpoint, and then it has an IRQ handler for when the serial port says it's ready to receive
or transmit more data.
And you can prepare a list of capabilities you're interested in, and a list of events
you're interested in, and block on pull, and then when one of those is ready to be done,
you can call it, and it's guaranteed not to block, very similar to the Unix pull syscall.
And again, I think this is, for me, one of the more notable improvements and derivations
from the SEL4 model.
And I mentioned this earlier, but this interface for doing endpoints and for invoking kernel
objects like virtual outer spaces is uniform between user space endpoints and kernel objects.
So it is, for example, possible for a user space process to create a set of endpoints
and then use them to implement an API which is identical to the kernel API.
And if that process is the parent of some other process which thinks it's talking directly
to kernel, it can be sandboxed according to whatever kind of policy you want.
So the kernel is using this API which is uniform with the way that user space communicates
with itself, and thus user space can fill the role of the kernel in sometimes.
This can, for example, allow you to very easily run several different Helio systems on the
same computer at once without going to virtualization, which is kind of interesting.
So here I have a little bit more detail on capabilities in particular, and then the implementation
that some of our capability objects use.
Here we have a capability space on the left, which is, again, a little bit distinct from
SEL4.
We don't use guarded page tables.
It's more like a file descriptor table.
It's just zero to however many slots are allocated in that capability space, and the process
invokes a capability by its number, not by its address.
Here we have an example of slots where we have a number of things which are preallocated,
but then notably we also have some empty capability slots.
And another derivation from the SEL4 model is that we support capability allocation in
the kernel.
We do this by maintaining inside of empty capabilities a free list.
And so when you invoke an endpoint or you want to allocate a capability, you can set
the capability address to the maximum possible address, and the kernel will allocate one
for you using the free list.
You don't have to worry about that state in user space, which is, I think, a very nice
convenience to have and very easy to implement as well.
This is a list of the capabilities that we have implemented.
On the left here is a list of all the capabilities which are available on every architecture.
We have things like memory, device memory, IPC capabilities, threads, and so on.
And then on the right, we have a number of additional capabilities which are specific
to each port.
In this case, I've listed the capabilities which are used on x8664.
I'm going to look at just a few of these.
First I want to talk about memory management, again, very similar to how we use capability
allocation with the C space in the kernel using a free list.
We also derivate from SCL4 in that general purpose memory uses a free list as well so
you can allocate pages without trying to keep track of a watermark, without trying to reset
your watermark, or divide it into smaller objects.
We have a free list of pages, so you can just allocate pages, which is quite nice.
But the only reason the slide is here is to tell you how it differs from SCL4.
We also have address space capabilities, vspaces, which is, again, similar to SCL4.
In fact, it's so similar that we've cargo-cultured this constraint that you can't share page
tables.
I don't really know why SCL4 does that, but once we understand, then we will probably
either commit to this or change our mind.
But we have virtual address space capabilities which can be used to manage processes.
And then we have tasks, which can be either a thread or a process or something else if
you come up with something creative.
But essentially, a task just has a capability space, which is optional, so that I can do
IO and invoke capabilities as an address space, and it receives some CPU time when it is configured
appropriately.
And again, we don't have SMP support yet.
We would like to do that soon.
And for now, the scheduler is very simple.
We just have a round-robin scheduler, but we would like to expand that in the future.
It should be at least easy enough to add priorities or niceness, and we can probably look into
some more sophisticated exclusions a little bit later.
Oh, and I missed one on my notes here.
A quick note to add on the topic of address spaces is that I think it's implemented a
little bit more elegantly than SCL4, but I did not write down why in my notes, so you'll
have to take my word for it.
OK, so that's enough about the design.
I'd like to talk a little bit about the implementation.
The goal is to keep the kernel very straightforward when it comes to booting.
I don't really care for the never-ending nightmare, which is different ways of booting
up computers.
And so the kernel is an Elf executable, and the bootloader's job is to do whatever
crazy bullshit is required on whatever platform it's running on to just load a goddamn Elf
executable into memory.
So that's what we've done.
And these bootloaders are also implemented in here, by the way.
We support, again, multi-boot in X86, and EFI and AR64, and we'll do EFI everywhere
soon.
But the bootloader comes up, and it's responsible for a few things.
It has to, of course, read the memory map.
It also has to load from the file system any boot modules, like similar to an initRAMFS
on Linux, where it's going to pull out the init binary or the init executable for the
first user space process to run, as well as maybe a tarball that init binary wants to
use to read some early drivers from.
It's also going to provide to the kernel that memory map, those boot modules, and details
about the loader kernel, like where it was placed in physical memory and so on.
If we're booting with EFI, we're going to pass along some stuff about the EFI runtime
services.
And if we have a frame buffer at this stage, thanks to GOP or multi-boot, we'll pass that
along as well, and that will eventually make its way to user space.
During boot, we have system initialization.
You saw a little bit of this in the earlier slide, which showed the code sample of the
kernel's portable entry point.
That's where the system initialization begins.
So of the three phases of the kernel runtime, we have the boot phase, the system initialization
phase, and the runtime phase.
So during sysinit, the purpose is to do something I hinted at earlier, which is to enumerate
all of the system resources, create capabilities for them, and then assign them to the inner
process, which is, just again, an alpha executable.
So we pull that alpha executable in from the boot modules.
The kernel has a simple loader, which pulls it into memory.
Enumerate system resources creates enough capabilities to host a task and a v-space
and so on for that initial executable and hand it off.
The basic problem at this stage is not messing up memory.
Everybody who has written a kernel from scratch, maybe as opposed to approaching a project
later, knows that the hardest thing about memory management is you need memory to manage
memory.
So there's a lot of stuff in this stage to deal with that.
We also tried to enumerate resources on the system at this stage, but this is actually
going to change soon.
The kernel, at the time of speaking, has a PCI driver for x86 or a device tree scanner
for ARM, and we kind of tried to enumerate the physical address of everything, but this
is not a good idea, so we're just going to take all physical memory and give it to user
space and let it use policy decisions to figure out who gets what, rather than trying to enumerate
everything in the kernel, just to keep the kernel smaller.
And we definitely don't want to do ACPI, so please, please.
If anybody here is on the risk-fire board or something, I'm begging you.
No ACPI, device trees.
And then finally, we jump to user space, and that concludes the sysinit.
Speaking of user space, I want to talk a little bit about our future plans.
So here we have kind of the onion of Aries, is what it's called.
The Helios is the kernel at the core of this dream of a larger operating system called
the Aries operating system.
And we want to wrap the kernel with various layers to add more functionality.
So we have Helios as the kernel.
We've also started working on Mercury, which is a framework for writing drivers.
It's basically a user space interface to the kernel API, which you can use for drivers
plus some useful functionality like utilities to make it easier to map memory and so on.
And then this Mercury system is applied by Venus, which is a collection of drivers, real-world
drivers for actual hardware.
At the time of this talk, Helios exists, Mercury mostly exists, and Venus was just started
last week.
Gaia is going to be the next thing that we're going to do on top of this.
So through Mercury and Venus, we'll get this kind of abstract view of the devices on the
system as presented through IPC, our capabilities.
And then this will be consumed by Gaia and formed into a cohesive user space, which is
going to essentially be Unix, but everything is not a file.
Everything is a capability.
So you open slash def slash fb and you get a frame buffer capability rather than an IO
object that you might see on Unix.
And furthermore, the design of Gaia is going to be mostly a combination of inspirations
from Unix and Plan 9.
And on top of this, we'll add a POSIX compatibility layer because Gaia is a chance to leave behind
the legacy of POSIX, but the legacy of POSIX is strong, so we'll have to accommodate it
somehow.
And we'll tie all of this up into an operating system called Aries.
So we're going to use your space and we're going to build this stuff there.
One other thing I want to show off is something which is part of the Mercury system, which
is our DSL for defining IPC interfaces.
We were thinking about not doing a DSL, but DSLs are kind of good for this use case,
so we made one.
This is an example of a serial device.
It has support for configuring the BOD rate and stop bits and parity and so on.
And it implements the IO device because it supports read and write as well.
We have a tool called IPCGen, which reads this DSL and generates hair code for it.
And this is now mostly working, but we're going to start actually writing more real
drivers with it soon, so it'll be, remains to be seen if we'll like it after we use
it for a while.
So does Helios work?
And the answer is self-evidently yes, because this slide deck is being presented from this
Raspberry Pi, which is running Helios right now.
Thank you.
So I have no C code written on this device beyond the point of EDK2.
It has EDK2 to run UA5, but once EDK2 hands over to our EFI boot loader.
From that point forward, 100% hair and assembly, just a little bit of assembly.
This port to ARM64 was accomplished over the past eight weeks.
Actually it took exactly 42 days to port the kernel from X86 to AR64.
This system has a simple driver for the Raspberry Pi GPU running in user space to drive the
projector.
And it has a serial port driver, which I'm connected to on my laptop here, to switch
between slides because I could not write a USB driver in eight weeks.
The slide deck itself is encoded as quite okay images, which are packed into a tarball
and dropped in like an NFS would be.
And there really are very few hacks.
I would say that this is a pretty complete port of the kernel with very little shortcuts
or problems.
The reason why I chose to port the kernel to ARM in 42 days is because I was originally
going to give this talk from a laptop running Helios for X8664, where I was going to drive
the projector through Intel HD graphics, and then I read the Intel HD graphics manuals
and it decided it would be much easier to port the entire kernel to ARM and write an
ARM GPU driver.
So that's what I did.
After about two days of reading the HD graphics manuals, I was like, I've had enough.
And then I pulled down the ARM manual and tried to find a PDF reader which could handle
it.
In terms of those hacks and shortcuts, there's no SOC specific builds, so the same kernel
that I wrote will boot from any ARM device with the standard EFI configuration and a
device tree.
It's not Raspberry Pi specific.
The user space is Raspberry Pi specific.
It's actually Raspberry Pi 4 specific, because that's the one I have, just because I didn't
feel like doing device tree parsing in user space for the sake of a silly demo.
But all of the silly demo code aside, the stuff that's necessary to make this talk
work is maybe a little bit hacky and Raspberry Pi specific, but the kernel port is a genuine
port which has basically feature complete.
I think the only hack that's in place is that I said earlier that the kernel tries to enumerate
the device tree to find physical memory for devices to provide to user space through device
memory capabilities, and that was a bad idea.
I was right that it was a bad idea, but there is a little bit of a hack in the kernel in
that I just gave all physical memory to the Raspberry Pi to user space without really
much critical thought.
That's really the only hack.
The full complete, it's done port will correct that oversight by using the EFI memory map
to find memory, which is less stupid to just blithely give to user space.
Additionally, I will confess that I don't have support for IRQs in user space, so if
I put my finger on the heat sink here, it kind of hurts, because it's just busy looping
in user space while I wait for the next slide.
I did get that working before FOSSTEM.
I just didn't incorporate it into the loadout for running the slide deck, so yeah.
It's a good thing that it's not that hot in here or this would crash.
In total, Helios has been developed in nine months.
The ARM port was done in eight weeks, and it's sophisticated enough to run this slide
deck, which is pretty cool, but what's left to do?
The kernel is mostly done, and by done, I mean feature complete, but not necessarily
where we want it to be.
So, by feature complete, I mean the kernel API is complete, and you can write programs
against it, which do everything we want them to do, and then other improvements won't maybe
not necessarily affect that API.
Still needs to be polished in a number of places, like that device tree issue that I mentioned
is one case.
If you get grep through the code base, you'll find about a hundred do comments which we need
to address.
One of the more challenging things that we're going to have to do is SMP support, but again,
the kernel is a total of like 15,000 lines of code, so despite the boogeyman the SMP often
appears to be to most kernel hackers, I imagine that it won't be that difficult for us to
do, which could be famous last words, but we'll see.
I also want to put it to risk five.
I have gotten some hair code running on risk five at the supervisor level, thanks to the
efforts of one of the hair contributors.
We did do some basic OSDA research, but we haven't actually ported Helios itself to risk
five.
We'll do that soon.
I also mentioned that we're going to work on more options for the boot loaders, so we're
going to try to get EFI going everywhere.
The main blocker for EFI on x8664, for example, is that our programming language, which again
is hair, which is developed almost alongside this project.
X86 doesn't have for PIC, and so it would kind of be a little bit of a nightmare to
like do runtime relocations of the boot loader and assembly or something of that nature,
so we're going to do PIC first before we try to do any EFI boot loader for x86, but we
do have PIC for ARM, so that's already working.
Then I also want to improve the docs.
I spent the past few weeks in between hacking on the ARM kernel, improving the documentation
on the website aries-os.org, which there will be a link to in a later slide, which is probably
now about 60% complete, so if you're curious about the project and maybe you want to try
your hand at a little driver in user space, feel free to check that out, and wherever
you find a page, which is a stub, and you need to know what it should say, you can come
to IRC and ask about it, and we'll fill it in.
After the kernel is polished, actually alongside the kernel polish, is going to user space
where I explained a lot of the things that we were looking at.
Mercury again mostly exists, and Venus is just getting started.
Prior to the introduction of Venus, we did have a number of drivers that were built.
For the purpose of testing the kernel and testing Mercury and so on, we obviously have
a serial driver for X86, we have a PL011 serial driver for ARM, but we've also done things
like E1000 networking, we did send pings with that, we did the Rodeo block devices and a
couple of other simple drivers, just as we were working to prove the design of the support
code for drivers.
But the support code is mostly done, so now we're going to start writing drivers for real.
I need to provide some acknowledgments here to people who helped make Helios work.
Finally I mentioned earlier that there's a RISC-5 kernel by Alexi Yuren, Ember Sovati
also did some work on X86 for early kernel attempts.
This was really useful stuff, none of this code, very little of this code that came from
these efforts, they did it to Helios, and these projects never really developed into
full systems, I don't think either of them made it to user space.
But they were still very useful for proving out some ideas about how to actually do basic
kernel hacking in here, how do we boot up the system, how do we work from ring zero,
how do we configure the MMU, how do we do yada-yada-yada, deal with interrupts and so
on, how do we link it properly, all questions that had not been answered previously within
the context of the hair programming language, and so this work was definitely instrumental
in setting the field upon which Helios could be built, so big thanks to these guys.
Also thanks to the hair community, there's almost 80 people now, actually I think it's
more than 80 now, but there's around 80 people who have been working on the programming
language itself, again we've been working on it for about three years now, and the project
Helios of course would not be possible without the programming language that's written in,
so a huge shout out to the hair community for everything they've done, very proud of
that community.
I also want to thank the OSDev community on the Baruchat, hands up if any of you are
in this channel, yeah, so OSDev on the Baruchat is the single best place to learn about kernel
hacking on the entire internet, those guys are so smart and helpful and they're very
knowledgeable, they know everything about kernel hacking and drivers and anything you
want to know, if you want to mess with kernels, go talk to these people.
And also of course to SCL4, as I'm sure you noticed we took a whole bunch of ideas from
SCL4, I think SCL4 has got a really cool kernel design and I was really happy to learn about
it and apply a lot of its ideas to my own kernel.
So kernel hacking is fun, hair is fun, that's all I have fun, that's it.
Thank you so much Drew.
Any questions from the audience?
Martin.
I'm going to give you guys my soap, best thanks to Martin first and then we're going to give
you.
Hi, thanks for the talk, very interesting work.
I was unable to map the standard SCL4 capability derivation tree, like starting with anti-memory
and then converting that to your slides, so do you have it as well or are you?
Yeah, we do track capability derivations in a manner very similar to SCL4 and it really
would have been smart for me to put in a slide about that.
So thanks for the clarification and the second, well I have a hard time formulating it as
a question, so maybe just take it as an unsolicited advice.
Many of the design decisions of SCL4 were strictly motivated by the formal verification
target.
So maybe when you have spoken for example about not sharing the pages, etc., just give
it a thought that the reason for that might be that they did not want to make their life
harder regarding the formal verification and that might be the only reason.
Yeah, I think I've noticed that for a few other implementation details from SCL4 when
we were studying the kernel to learn what we could do for ours and with examples like
sharing page tables, I had bigger fish to fry so I left a comment which says SCL4 doesn't
support copying these and I would rather not run into a Heisenberg because we did it without
thinking about it, you know, and then we can really address it at some point in the future.
Thanks.
Hi, yeah, thanks for the talk, very interesting, quite impressive.
Yesterday we were talking about hair and thinking about it in retrospective, it seemed to me,
my personal opinion, that the great mechanisms of language design are mostly discovered like
we have garbage collection and tech unions and that, assuming you agree with that statement
now that you've written that operating system kernel, would you also say that the great
mechanisms how to write a kernel are established and well-known, things like paging, was there
still areas to experiment in new ways to do memory management, things like that?
Interesting question, I would say that there's a lot of concepts and ideas which can be applied
in the field of OS development which are understood and you can see examples of kernels and systems
which apply these ideas and various different designs that you can learn from and study
and maybe apply to your own kernel if they're the right choice and you can make a complete
kernel which is interesting basically only using proven ideas which is for the most part
describes Helios but at the same time there's certainly all kinds of research which is being
done into more novel approaches, there's been talks in this room throughout the day which
address some of those novel approaches and ideas so I would say that there is certainly
room to build a kernel out of understood ideas and still make it interesting but there's
also definitely an active frontier of research ongoing as well.
Thank you.
Thank you so much.
Any other questions?
Yeah, please.
Yeah, thank you for the talk.
You mentioned that you need position independent code, right?
Yeah.
But I don't understand if you use every driver and it's just like a user space process so
can't you just remap that in MMU so that all the processes like a normal Linux process
just have the same memory map?
Yeah, actually the kernel and user space processes both use a fixed memory map.
The thing where we would maybe want to look at position independent code is specifically
for the case of loading our EFI bootloader as a P32 plus executable.
After that stage it's all fixed memory addresses.
Yeah, then I understand.
Cool.
Hello, thank you for the talk.
Can I ask a non-technical element?
You've GPL-3'd it.
How are you making decisions around the kernel?
Like is it inevitable?
Tata, are you making decisions or are you having massive conversations about things?
How's that looking at the moment?
The vast majority of the work is just done by me personally at the moment.
The project is still pretty early on but we do have a number of other contributors.
I would say that the group of people who ought to be consulted on changes is probably in the
ballpark of five people in total.
So we just have a fairly informal community based on trust.
We try to be transparent, like I am transparent in all of my free software, so we have a public
IRC channel where we have these discussions and anybody can jump in at any time and there's
a patch review process which just goes through me at the moment.
In the hair community, for example, which is a lot bigger at this stage, we have something
more of a governance model where there's less of a BDFL and more of multiple maintainers
who all can do code reviews and improve patches and things like this.
As the Helios project grows, I imagine it will adopt a model similar to hair and perhaps
as hair grows, we'll have to improve upon the model even further.
But we'll see.
Thank you.
Nice shirt, by the way.
Thank you.
Can you pass it on?
Yeah.
Thanks.
You mentioned that you don't want to deal with ACPI but at the same time you want to
make UFI standard, so what's the plan there?
Is there any way to sort of port ACPI in your system because I imagine that it will become
mandatory, right?
Yeah.
I'm going to wail and gnash my teeth and hope it doesn't happen in practice because
at the moment, you know, something like EDK2, to be clear, by the way, I don't give a fuck
about non-free firmwares, so I'm thinking about EDK2 and things like that or Uboot and
so on where there's already an EFI standard UUID for passing a device tree along and
they can be configured to do that instead of ACPI, which is what I'm doing on this Raspberry
Pi, for example, and what I hope to continue to do on risk five and so on.
Our proof of concept on risk five took the same approach.
But there's very little in the kernel that actually needs to be concerned with ACPI
versus device trees that, again, it is a microkernel, so in the long term, we might just pass along
the... at least a little bit in X86, you know, because there's no device trees.
But you know, I'm fingers in my ears not thinking about the fact that ACPI is upon us, but we'll
probably have to deal with it at some point.
Thank you for the presentation.
Which software is running the presentation itself and how is it compiled?
This is just a custom piece of software I wrote myself.
It's a single binary which is loaded by the bootloader as the inner process and then
the kernel loads it into an address space and boots it up as PID1.
And there's additionally a tarball as a second boot module which is, again, loaded into memory
and then passed along to PID1 which is a tarball full of slides.
And then there's just one statically linked executable which contains a serial driver
and a GPU driver and the code to glue everything together.
The code, by the way, is available on source set if you're curious.
As you mentioned, Elios is heavily inspired by SCL4, so is there any plan on format verification
for Elios or that's not something you're interested in?
No, I'm not particularly interested in that.
In the back, there's someone.
Thanks for the presentation.
I have a question, is it on the road map that something like Weston or a other GUI server
or other service like that could potentially be reported to Elios?
I'm actually also the original author of WROTS and have a lot of experience in Wayland
and so there is a 100% chance that Wayland will be running on Elios at some point.
Any other questions?
As you said, for Gaia, you are inspired by Plan 9 and Unix.
What do you plan for Gaia?
What's the best of those both worlds?
It's a little bit hard to say.
At this point, there's less plans and more vision in that respect because we have at
least probably a year of work before we can really start serious work on Gaia.
But I will say that there is a lot of stuff I admire about Plan 9.
There's per process namespaces is one great idea.
I'm also going to go further with the idea of there not being any kind of global file
system at all.
We're also going to take a look at things like using text-based protocols where possible
and we're going to use different from Plan 9.
We're going to use this IPC generation thing for places where text protocols maybe don't
make sense.
I also have a lot of admiration for things like MBD on Plan 9 and so I would like to
organize networks perhaps in a similar fashion.
Also, I would say that the bigger vision for the whole area system is you can almost say
it's correcting a mistake that Plan 9 made, which is that Plan 9 was correct, that distributed
computing is the future, but it was incorrect that they would be distributed across a main
frame and a bunch of thin clients in office building, which is how Plan 9 was designed.
In fact, the group of devices which should be running a uniform operating system is all
of your personal devices, my laptop, my workstation at home, my phones, they should all present
as a single system.
It's very vague and lofty and long-term vision, but I would like to try and achieve that with
the design of Gaia and Aries.
Thank you.
Any other questions?
Okay, then thank you so much, Drew.
Thanks a lot.
So, 10 minutes break until the next talk.