Thank you very much to the best of you.
Welcome to my talk.
The agenda for the talk today is for those of you who don't know NOVA.
I'll give a very brief architecture overview and explain what NOVA is and what runs on top of it.
Then I'll talk a little bit about the form of verification given update on the current status
and what NOVA is one of those microcrongals that is undergoing from the verification.
And then we get to the main topic of the talk which is scalability.
You just heard from Michael that scalability is an important topic.
And in NOVA there's a lot of work going on improving the scalability.
And today we will focus primarily on supporting thousands of devices,
this thousands of interrupts on big iron server machines and the new microchannel APIs that require that.
And hopefully we'll have some time for questions at the end.
So the architecture overview of NOVA is shown on this slide.
So you have the microchannel running at the highest privilege level.
In our case it's called the microhypervisor because it's not just the microchannel.
It is also a hypervisor.
And it's roughly 15 to 20,000 lines of code depending on how you count.
And then on top of it you have a componentized multi-server operating system running of all these colorful boxes
and every box represents a component that runs isolated in its own protection domain or its own address basin.
And NOVA is a microhypervisor because some of these components,
shown as these yellow boxes at the top, are actually used on mode virtual machine monitors.
And there's an instance of the MM for every virtual machine.
And you can run unmodified guest operating systems, unique kernels,
container run times, offices, whatever you want inside those virtual machines.
And the whole stack is undergoing formal verification.
And for those of you who are very interested in the topic of writing specifications for each of the functions
and mathematically proving those, there was a talk at the microchannel bedroom last year,
given by my colleague Hay Dang, who talked in great depths about the form of verification that we do in NOVA.
So for those of you who are interested, I suggest you check that out.
NOVA is written in C++20, so formal verification attaches a specification to every C++ function.
And then there is proofs for those functions that mathematically verify that each function conforms to its specification.
And in a NOVA case, this is actually a very complex endeavor because NOVA is a highly concurrent microchannel.
And when you have functions accessing the same state concurrently, the state space can explode.
But we are using separation logic, which makes this problem tractable.
And the approach that we are taking is actually cutting at the system called or helper call layer.
And we're very fine from there, top-stown.
So you can read this table, which I give me to provide an update on the progress that we're making.
And at the lower, at the left side, you have a list of all the helper calls in NOVA.
And which of those already have a full specification.
And then we're rolling down into the stack until at the very right side we arrive at capabilities, memory allocators, timers, coroner memory, and so forth.
It's an ongoing effort. And there's a lot of links for the NOVA specifications and the proofs.
And one of the things that happened in the last year is that we actually made those specs and proofs open source under QPRV2.
So you can go to the top link there and you find all that and you can see it.
The next steps that we're doing in form of verification is that we actually look at weak memory reasoning.
Reasoning about when one core does store, what is the point in time when all other cores have seen that store.
And also interaction with the hardware, this is the page workers in the MMU and this is TLDs that requires a lot of complex modeling.
But I don't want to go into the details here because the subject of the talk is not from the verification.
The subject of the talk is scalability.
But currently runs on the two major architectures. It runs on on the ADA called ARX64.
And it runs on the X8664 bit architecture. And it scales all the way up from the smallest embedded devices.
So in the case of ARM, I've just listed the Raspberry Pi as an example of a smaller embedded device.
All the way up to the largest servers that you can find in cloud providers.
So the largest you've currently tested is an AWS Graphitone 4 which has 192 cores, lots of memory, lots of SMMUs, lots of interrupt controllers.
And it actually has 104 PCI devices.
The same on X86, we have one binary that you can build that runs all the way from smallest X86 machines.
So we like to use internal looks in these small form factors.
All the way up to the latest granite records here on 60 views, also with 192 threads, lots of RAM.
450 is something PCI devices, 10 IOMUs, 192 CPUs, five level pitchable, so really the big iron boxes.
And when you compile a normal, it's very simple.
Assuming you have a cross compiler for the architecture that you care about or you compile it natively, you type make arc equals whatever your architecture is.
And in the ARM case, you also have to specify that you want a CPI as the board.
And then you get a binary which is roughly 100 kilobytes in size.
So really a micro kernel, not some big bloated piece of software.
And the same binary works across the entire architecture stack from small to large.
What I actually want you to take away from this slide is that the machines that we run on are now so large that we need really hundreds of devices.
And if you assume that every device just needs one interrupt which is not true, many devices nowadays need tens of interrupts, tens of messaging and interrupts.
But the number of interrupts that traditional micro kernels have provided in the past is no longer sufficient. You really need to have thousands of them.
So what do we need to do?
And you just heard from Micheal that we gained a lot of isolation and a lot of robustness from running device drivers in user mode.
And I want to take a quick look at what it takes to run a device driver in user mode.
And what infrastructure a micro kernel has to provide.
So first of all, the code and the data of the device driver, you can put that in a user mode protection domain just like an application.
But that application that device driver application needs access to the device registers.
And in modern platforms, this is memory map.io on some all the internal machines you also have sometimes pop-based.io.
And this is simple to achieve. You take the MMU, you map the memory map registers of the device into the address space of the application.
And then you can drive them with normal load install instructions.
So that functionality is trivial to implement.
But then it gets a little bit harder.
You need to make sure that this device driver can actually receive interrupts.
So you need to convert the hardware interrupts into some sort of notification mechanism.
And when the device driver is done doing the intrap handler work, the interrupt needs to be acknowledged.
So you need to have some handshake in protocol with the kernel because you cannot give it a device driver access to the intrap controller for security reasons.
That needs to be under the control of the micro kernel.
So the way no bus stops this is it transforms an occurrence of an interrupt on an app operation on a summer floor.
And when the device driver is done, it dounds the summer floor, which automatically acknowledges the interrupt.
And that's a very nice and very flexible cross-core and cheap notification mechanism.
So that's the interrupt problem.
What we also need to do is we need to control the access for device drivers which we got to the MA.
You cannot have a device driver program in arbitrary memory address.
DMA to that address and scribble all over the kernel memory.
So you need to have some access control mechanism, some hardware enforced access control,
where the use of the MA or the addressable range for the MA is restricted,
such that the device drivers can only DMA to memory or from memory that belongs to them.
And this problem has been solved in many architectures with the concept of an IOMU or system MMU,
where you can have a translation from DMA addresses to hospital addresses.
So this type of DMA remapping, but you need to design also interfaces for that and we'll talk about that.
And in another case, there's a hyper-core called assign-dev, where you can assign a device to a DMA space.
And the DMA space is effectively a page table that represents an address space that you can assign to a device to restrict
what region of memory it can DMA to or from.
And you also need to provide access to interrupts because not every device or every device driver should be able to trigger any arbitrary interrupt.
You want to say this device can trigger this particular interrupt or this particular set of interrupts,
but no more you shouldn't be able if you are the next driver, you shouldn't be able to assert an interrupt that belongs to a storage driver or the GPU.
So you need an API that transforms a global system and route that not just to a summer for an interrupt summer for,
but also to a particular CPU because not all of these thousands of interrupts should hit the same CPU core,
you actually want to send them out through many cores.
And the hyper-core that does this is a sign-in, where you can say assign this particular hardware interrupt to this device and route it to this particular CPU and configure it.
So I want to explain a little bit how the DMA translation part works because not many people know all the details in the,
and I'll use the arm SMUV3 as an example. So in arm SMUV3 is starting at the top left corner,
the DMA stream that comes from a device is identified by a stream ID.
And inside the SMMU, there's a multi-level stream table, which is set up by the normal microcom or micro hypervisor,
and every device has a stream table entry that points to a DMA pitch table, which controls what regions of memory that device can target.
And then the SMU also has a command queue, where Nova is the producer, so it puts commands into the queue,
and the SMU is the consumer, it reads commands of the queue, and there's an event queue which works in the opposite direction,
where the SMU puts commands in, and the events in and Nova reads events are also, for example, the SMU could say,
there was a DMA remapping error, where some device tried to access some region of memory that it couldn't access.
The problem with the SMUV3 is that it uses stream table entries, which are 512 bits in size.
So if you do the mass, that is 864 bit word.
You do not have a processor instruction that sets up a stream table entry automatically.
You have to write these 64 bytes in a particular order, and you're effectively racing with the SMMU against those writes.
So the spec specifically says that the SMMU may read all those 8 bytes in any arbitrary order.
The question is, how do you actually set up a stream table entry in such a way that the SMU always sees a consistent state and never some partial or corrupted state?
And you need to design a protocol for that, and the protocol works as follows.
So we start in the state, in the invalid state, where the valid bit of a stream table entry is zero, which means whatever the SMU has fetched, whatever configuration will not be considered valid,
and it won't act upon it.
And the moment that the valid bit becomes one, whatever configuration it has set will be used.
So the first thing is we need to, or it's clear, that we actually need to set the valid bit last, because that's what ultimately commits the entry.
So we are not just racing against the SMMU, we are also racing against the same call being made from other CPUs,
which may also try to configure a stream table entry. So we need to arbitrary to win this race.
So the first thing we do is we automatically set the configuration in the stream table entry to something other than zero, with an atomic store,
and whoever wins that race can proceed and everybody else will get an aborted error code.
And then once we've set up the configuration, the valid bit is clear, SMMU won't use the entry.
We have to make that configuration observable.
And that means in ARM case, that we need to make sure that the stream table walker and SMMU can see it, that if the SMMU is not coherent,
that we push those stores all the way out to memory, out of the cache hierarchy, that the SMU can actually see it.
And then, because the SMMU may have already read some of those other words, this configuration words,
we have to tell the SMMU to forget this entry.
So this means we've written the valid configuration, be tell it to forget whatever the invalid configuration was,
and then we set the stream table entry to a valid bit to one.
We make that also observable, but the SMMU may have still cached valid equal zero, so we have to invalidate the STE again.
So you see this very complicated dance, you have to do to make the SMU actually see all the changes in the right order.
And likewise, if you want to remove an entry, you have to automatically clear the valid bit,
and to ever clear the valid bit first, wins the race to unconfigure the entry.
And then you can undo all the remaining configuration, but you also have to invalidate the entry at SMMU,
and to invalidate the TLD, which means forget any translation entries from those DME page tables that were set up using this entry.
So this is just an example of the complicated synchronization you have to do in a highly concurrent microchannel,
where you're not just racing among the 192 CPUs, but you're also racing with the hardware.
The good thing is that the bad thing is that whatever locking scheme you may have in mind,
the hardware doesn't know anything about the locks in your software.
So you have to be atomic between the software and the hardware.
But the moment you get that right, you get the synchronization between the cores for free.
So let's look at the interrupts system on ARM, because I said we want to scale to thousands of interrupts
and we need to understand what types of interrupts exist and how to configure them.
And in the old ARM world, let's say before gig version 3 was introduced,
the interrupts up the system was split into several components.
Starting at the top left corner, we have a gig distributor, which has many incoming lines.
So these are wired interrupts, which ARM calls shared peripheral interrupts.
There's an extension called extended shared peripheral interrupts,
but you can think of all of these being wires that go into this global interrupt controller.
And the interrupt controller is set up to convert the assertion of any of those interrupt lines into an int ID,
and route it to one of the redistributors.
So every core, in our case, we've just two cores, because I couldn't fit more on the slide.
You have Core A and Core B. You decide whether you want to route it this way or that way.
And that gets sent as a message, so A dashed line here, denotes a message being sent.
That's no longer a signal, that's a memory right.
And then the redistributor, for what's that to the CPU cores,
takes CPU interface, where the interrupt will be delivered to software.
Another question is, how do we assert that interrupt to a user-motivized driver?
And in the ARM case, all the interrupts have a global interrupt ID, which is a number,
ranging from zero all the way up to 2 to 4 or 64.
And we have a summer for table entry. A summer for table, this up to 65,536 entries,
where you can use the hyper-core API to attach interrupt summer force.
So if you are a device driver, and you have access to say interrupt 87,
you can plug the interrupt summer for that interrupt into the summer for table.
And whenever that interrupt is asserted, no one will take a look at the summer for table
to see which interrupt summer for is attached to that and will update interrupt summer for.
So starting with gig version 3, there was a new component added, which is shown in the bottom left corner.
And that component is called the interrupt translation service.
And the purpose of that is to scale the number of interrupts much more than wires ever could.
So as I said, we can have up to 2 to about 16 interrupts here, but you couldn't possibly put that many wires on a small SOC.
So the new concept for interrupts that allow much greater scalability is called LPI, locality approval interrupts, which are message signaled.
So rather than asserting a device, an interrupt line, a device would send a message to a specific register
in the gig ITS called the translate register.
And then the gig ITS actually sees that memory right decodes it to many tables.
So there's a device table and an interrupt translation table and a collection table.
We look into those in a moment.
Figures out where this message signaled interrupt needs to go.
And then again converts it to an int ID and it ripples through the hierarchy the same way as a pin based interrupt wood.
On X86, it is a bit different.
And the goal here is for NOVA to provide the same API or as much of a uniform API to device drivers as we can.
And to abstract the differences between armament X86 as much as possible, but we have to look at how interrupts work on X86.
So we also have a via interrupt controller, which in this case is called an IOAPIC, where pin based interrupts are asserted via real electrical lines.
And then an interrupt message is sent to the CPU course.
But in order to make that secure, there is interrupt remapping in the IOM view that sits in the middle.
And in the sets, the MSI acid flows from the IOAPIC to the CPU's local APIC or X2ATIC.
And the format of messaging interrupts on the left side of the IOM view, the inbound side, is in remapable format.
So every interrupt carries a source identifier, which in the X86 case is not a stream ID or a device ID, it is a bus device function.
So it says it's this device on this PCI bus and this device number and this function number.
And it carries an interrupt number, which is this lot number of this interrupt remapping table.
And it again has two to about 16 entries.
This interrupt remapping table then translates the interrupt to a vector.
Because X86 for backward compatibility reason does not use global int IDs like on V8 does.
It actually has an IDT and interrupt script or table, this only 256 entries on every core.
And out of those 256 entries, 32 are already consumed by exceptions.
And some are consumed by Nova which leaves approximately 200 entries that you can use for device interrupts.
So the goal of the interrupt remapping unit is to translate the incoming MSI in remapable format into an outgoing MSI in compatibility format.
And the compatibility format has a destination ID, which is the APIC ID of where the interrupt is supposed to go to which CPU and a vector, which will then be used to index into the interrupt vector table on that particular CPU.
So the difference between X86 and ARM is that on ARM you have a global table, whereas on X86 you have a pure core local table and we somehow need to deal with this.
Otherwise, it's the same as soon as an interrupt arrives, it will be translated through the sum of four tables of that core and will be signaled on the corresponding interrupt sum of four.
So to sum up what the key differences are, is in both architectures you have global pin-based interrupts.
You have some per CPU local interrupts that are not exposed to device drivers.
They are used by Nova internally like timer interrupts, performance counter interrupts and so forth.
And you have messaging interrupts, which in the case of ARM are translated through tables in the gig IDS in the interrupt translation service.
And they assert a global interrupt ID, and on the X86 case you have messaging interrupts that are translated through one interrupt table in the IOMU and they assert a per CPU vector.
So the table on ARM is indexed by the int ID, and Nova checks that the incoming int ID actually is within the range of the table.
And that you can only plug an interrupt sum of four into the slot belonging to that interrupt sum of four.
So the interrupt number must match the slot number.
And the scalability limit is two to the power of 16 GSI, because that's the capacity that you can have in the remapping table.
The practical limit is actually how many bits of LPI int ID the system implements.
In the X86 case, you only have these CPU local tables with about 200 entries.
So Nova checks if the vector fits with the range of this IDT vector table.
But you have a free choice to say I want to map this global interrupt on this particular CPU to this vector or that vector.
So the scalability limit is two to the power of 16 GSI, but per segment group.
If you have multiple pieces as segment buses, you get twice or three times or four times two to the power of 16 GSI.
The practical limit though is 200 interrupts per CPU.
So if you have just four CPUs, you're practically limit to 800 interrupts.
But if you have 1952 CPUs, the limit is much higher.
So that's just an artifact of X86.
I want to talk a little bit about the gig interrupt translation service and what pain and operating system person has to go through,
because hardware manufacturers try to be very flexible and then decide not to be.
So in the ARM case, a device sends an interrupt with two identifiers.
It has a device ID, which is usually communicated through some sideband signals,
the ITS or this particular device or that particular device allows the ITS to tell different devices apart.
And it has an event ID, which is a local interrupt number that can get translated to this global entity.
And the device table, the interrupt and the collection table are both pointed to by what ARM calls base registers.
And inside an ITS, you have base registers from zero to seven.
But it's not architecturally specified which base register maps what type of table.
So software has to figure that out and remember it.
And they only define this in version gig version four.
But since Nova is backward compatible to gig B3 as well.
We have to discover this and remember this.
So this is just unnecessary inflexibility.
So in interrupt arrives, the ITS uses the device ID to look up an entry in the device table.
And the device table points to an interrupt translation table.
The event ID is used as an index into the interrupt translation table.
And inside there, the ITS finds the final int ID.
And the interrupt translation table entry also carries a collection ID, which says which interrupt collection.
So you can group interrupts into collections.
That's this belong to and we don't use this in Nova too much.
We effectively say every CPU has a collection.
So the number of CPUs defines how many collections you have.
And this allows us for, for example, to set up the collection table only once at boot and to never touch it again.
So now comes a really interesting part.
It's when you want to program these base registers.
Depending on how many bits of device ID you want to support, this device table can be one level or two level.
And there's an indirect bit which you can set in the device table entry to say I want the one level table or two level table.
Sounds very flexible.
Until you read the fine print in the manual that says this bit is read as zero right ignored for gig implementation that only support flat tables.
So in the reverse case you decide a software that you want the two level table and the hardware says, nope.
I only support flat tables.
And then there's other bits which say what is the shareability of this table can this actually participate in coherency or not.
And you may say I want the table to be shared with all the processes in the in our shareable domain.
And then the fine print in the manual says it is implementation defined whether this field has a fixed value.
Or can be programmed so again you have to deal with all the possible cases of oh it's actually not shareable and you have to do manual coherency management.
And the worst part of it all is there's a page that's actually two page size bits where you can say a table in this hierarchy is 4k 16k or 64k in size.
And again there's some fine print that says the gig implementation may only support one fixed page size and the field might be read only.
So what software actually has to do is it has to make a guess and say I wanted to level table with 4k try to program that and then you read back the configuration the hardware says nope.
Okay, then I'll use 16k tables and then the hardware says nope.
And in the worst case you end up with oh you can only have 164k table and you can only have one level so a flat table.
And then you may end up having to concatenate 256 64k pages in one flat table which means you have to allocate a giant 16 megabyte table and your memory allocator needs to support that.
So we have this algorithm in over and it works but this amount of pain is interesting.
So let's talk about the number API because when you want to configure an interrupt or a device you have to name it and we make interrupt and devices available as capabilities because capabilities provide for very nice authorization model where you can say if I have a capability I can name some resource and it also conveys my access to it.
So multiple of these hypercalls need to name devices or interrupts but as you've seen the naming between x86 and arm is not the same on arm an interrupt has an end ID on x86 an interrupt has a global system interrupt number.
So the idea is that when we create a device or when we create an interrupt number 4 we provide the name once and this is the part of the API which is architecture specific.
So for when you create an interrupt sum of 4 you either provide the name in an arm specific manner on an x86 specific manner and then you get a capability to an interrupt sum of 4 which is uniform across all architectures and likewise when you create device context you provide the name for the device either in the x86 or in the arm format depending on which architecture you're on.
And then you have a device capability which is again generic across architectures so it keeps the rest of the hypercalls API clean and you no longer have to worry about those differences.
So device context is what we introduced for devices to encapsulate all this architecture specific state into a new object you don't really create a device because the device is there but you create a management context for device which you call device context.
And it encodes the topology so the device ID the stream ID on an arm case and the PCI topology in the x86 case but it also encodes information about which SMMU or get asked is managing the DMA and interrupt translation for the device.
And then you get a capability which you can use with the assign dev or assign hint called to associate that device with the ms base or to route an interrupt from that device.
So in inches of time I'm going to skip this slide which talks about the novel releases and which features appeared in which novel release suffice it to say that we do a release a new release every two months for this six releases per year.
And all the things that are listed in both on the slide we've briefly covered in this talk there's one thing that I want to mention at the end and that is when we implemented all this stuff we could get no running quite nicely on.
Grab it on server machines which require all these features for scaling.
But then we tried to put an over on a new machine that we've got which was an Nvidia digit spark which is one of those Nvidia AI machines.
And unfortunately this machine doesn't have any URLs or know you are connected so you can't really capture the output.
And what we had to do is we actually had to implement the framework for console in Nova.
This is something that I've tried to avoid for a long time because I didn't want to do any front rendering and scrolling and blitting.
But I had to do it to actually get some output on this box.
And I had to implement a lot of performance tricks but none of this code uses any architectural specific assembler code it's all portable C++.
But it's very heavily optimized and we can actually get very high frame rates for scrolling.
So on the Intel platform we can actually get 4,500 frames per second.
And even on some Vimpi Raspberry Pi we still get 245 frames per second.
And you can actually see the boot output from just Nova is nothing running on top of it on the digit spark.
So if you're interested in what we needed to do to make this happen, it's just 350 lines of code of which 250 lines are front loops.
So what's next, Nova has been open source for 15 years.
And as I mentioned, the open source from the specs and proofs last year.
This year, later this year we are going to make significant portions of the Nova user and stack available publicly on an open source license.
And we are currently figuring out how we can reduce the barrier of entry such that it becomes easy for all of you to use this.
So what we decided we will do, but it's open for discussion.
So if you have ideas, talk to us.
We want to make everything configurable with K config so that you have a global config for the entire software stack.
When you do this and you type make you get one giant image which contains all the components.
And you can just boot this image from your favorite bootloader and there's three different ways of booting supported.
You can either boot this as a booty boot image or you can boot this like a Linux kernel in the form you would boot it busy image or you can boot this as you if I executable from your UEFI shell.
So the same image works in all these three different ways.
So with that, my time is up.
I don't know, maybe you have room for one or two questions.
I have one question.
I have a question.
Thank you.
For questions, regarding data.
So did you have the chance to introduce user interrupt insights and shows on the latest Intel CPUs?
I read about it in the manual, but it's becoming available only on the latest processes of generations.
and since we go all the way back to the first 64-bit capable processors,
it's not clear if you want to support that.
Yeah.
The question was, what are the firmware requirements?
On X86, it's all UFI.
On ARM, we actually prefer UFI.
If we can, but we can also launch from UBoot or on ARM,
we ask the firmware not to close boot services.
So, you boot into Nova with UFI boot services enabled
and then Nova actually closes the boot services
after obtaining a memory map and taking some information from UFI.
So, for example, we use the UFI graphics output protocol
to determine whether we have a framework for and what the resolution is.
Which means, we actually switch to the highest possible resolution in UFI.
So, UFI sets up the framework for and the resolution for us.
And we do not have to worry about EDID, display resolution,
mode switching.
We effectively get a linear framework for and we can just write it.
We still have to do all the manuals crawling and glyphorandering and whatnot.
Thank you.