Tutorial feedback :)

[midnightveil]

• Part 0 Setup — The Fedora aarch64-linux-gnu compiler mentioned as part of the linux setup appears to be incompatible with the code in this tutorial in some way. Don't remember the error; was informed to use the ARM gcc toolchain as mentioned in the repo https://github.com/sel4/microkit, though this required modifying the Makefile to use the correct compiler name.

• Part 1 — The section on interrupt handling describes the IRQ as the 'hardware IRQ number', but is actually 32 + hardware IRQ number. Supposedly this is because 0-32 are reserved for software IRQ (?), but I can't find any other documentation about this (or whether it's microkit, or seL4). This got me later on.

• Part 2 — admittedly somewhat of a nitpick, but exactly what had been done already and what was needed to be implemented was unclear; the fact that the table & moving around being done already wasn't immediately obvious and I spent more time confused about what the tutorial was wanting to do.

[Indanz]

The section on interrupt handling describes the IRQ as the 'hardware IRQ number', but is actually 32 + hardware IRQ number. Supposedly this is because 0-32 are reserved for software IRQ (?), but I can't find any other documentation about this (or whether it's microkit, or seL4). This got me later on.

This is ARM specific, but other platforms probably have a similar setup:

• 0-15 are PPI, Per processor interrupts.
• 16-31 are SGI, Software generated interrupts.
• 32-1020 are SPI, Shared processor interrupts.

See The Generic Interrupt Controller.

Depending on your platform's datasheet, it may list the peripheral IRQ numbers starting from either 0 or 32. The ambiguity is whether "HW" refers to peripherals or the CPU.

seL4 always uses the IRQ numbers as seen by the CPU, so including the 32, even though usually you don't have access to those lower IRQs from user space.

[Ivan-Velickovic]

Thank you for the feedback, appreciate it.

Part 0 Setup — The Fedora aarch64-linux-gnu compiler mentioned as part of the linux setup appears to be incompatible with the code in this tutorial in some way. Don't remember the error; was informed to use the ARM gcc toolchain as mentioned in the repo https://github.com/sel4/microkit, though this required modifying the Makefile to use the correct compiler name.

If you could post what the error was that would be really helpful. I tested the solutions on a Fedora 39 virtual machine and it all worked using the instructions from the tutorial.

The section on interrupt handling describes the IRQ as the 'hardware IRQ number', but is actually 32 + hardware IRQ number. Supposedly this is because 0-32 are reserved for software IRQ (?), but I can't find any other documentation about this (or whether it's microkit, or seL4). This got me later on.

Like Indan says I guess it depends on your meaning of 'hardware'. I'll just say 'IRQ' instead to avoid confusion.

Part 2 — admittedly somewhat of a nitpick, but exactly what had been done already and what was needed to be implemented was unclear; the fact that the table & moving around being done already wasn't immediately obvious and I spent more time confused about what the tutorial was wanting to do.

There is a list of bullet points at the end listing what you should do but I agree it might be a bit vague. I'll have a look and see if it could be improved (it doesn't say what already exists so maybe I can include that).

[midnightveil]

Huh, weird. I just did a clean build following all the steps and everything worked just fine. Rather not sure then, iirc it was something about not being able to find symbols, but I can't remember anymore. On Fedora 40 fwiw.

Re: IRQ numbers, fair, I definitely don't have too much experience with this. Didn't help at all that the Linux DTS files don't reference them in that format; which confused me for a while.

[Ivan-Velickovic]

Re: IRQ numbers, fair, I definitely don't have too much experience with this. Didn't help at all that the Linux DTS files don't reference them in that format; which confused me for a while.

It is something that trips up every new student that comes into Trustworthy Systems. It is something that's hard to figure out yourself. I'm not sure whether the best place for it is, I might be able to add something into the Microkit manual mentioning that the IRQ number is what the CPU observes.

I'll add a footnote to the tutorial explaining how the IRQ number is figured out in the first place.

Huh, weird. I just did a clean build following all the steps and everything worked just fine. Rather not sure then, iirc it was something about not being able to find symbols, but I can't remember anymore. On Fedora 40 fwiw.

Ok cool. Let me know if you run into anything else weird on Fedora, it's not a system I'm familiar with and is largely untested with all of our other tooling/projects.