ARM interrupt mapping in .system

[podhrmic]

Hello! What is the key for the interrupt numbers that are defined in .system? For example, the ethernet example for tqma8xqp1gb defines interrupts 112, 290 and 294. Looking at tqma8xqp1gb.dts, which is a device tree that seL4 presumably uses, there don't seem to be matching interrupts.

Similarly, the virt ARM example from Nick Spinale has a UART interrupt 33 but that number doesn't seem to match QEMU documentation / source code.

Does the kernel do any irq mapping, or should the numbers generally match what is in a datasheet/documentation for a particular board?

[Ivan-Velickovic]

I believe that on ARM the interrupts listed in the device tree are the hardware interrupt numbers and are not necessarily what software observes. For example, here's the UART node for the QEMU ARM virt device tree:

pl011@9000000 {
    clock-names = "uartclk\0apb_pclk";
    clocks = <0x8000 0x8000>;
    interrupts = <0x00 0x01 0x04>;
    reg = <0x00 0x9000000 0x00 0x1000>;
    compatible = "arm,pl011\0arm,primecell";
};

You'll see that the interrupt number is 0x01, whereas seL4 observes it as 33. I believe this because it is a SPI and therefore the IRQ number that software observes is offset by 32 as the GIC specifies that 32 is the lowest possible interrupt ID for SPIs. To my knowledge (which could be wrong), seL4 does not do any kind of interrupt mapping.

[podhrmic]

That was definitely it, thanks for the pointer!

It turns out that the QEMU virt arm platform doesn't have any memory mapped timer that would be accessible - I see that in your VM example you let Linux handle all that, but I am not sure how to translate it to a non-linux component/protection-domain.

The seL4 kernel uses IRQ 27 which is EL1 Virtual Timer Interrupt, so I should be able to use for example EL1 Physical Timer at IRQ30, but again - I don't seem to be able to touch the address where a timer control register would be.

Is there a way to get the kernel to periodically notify a protection domain? If not, what is the recommended way of handling periodic calls? (e.g. blinking an LED)

[abrandnewusername]

For handling periodic tasks, I have put some potential workarounds in https://github.com/au-ts/camkes_to_sel4cp_guide/issues/1.

The PPI VTimer IRQs are delivered by the seL4 kernel, There is no support for the Physical Timer for now. You might be able to access some of the Physical Timer Regs from the user space (e.g., this Ethernet example).

[Ivan-Velickovic]

Just to note that in order to access the generic timer from user-level, this kernel config option must be turned on https://github.com/seL4/seL4/blob/master/src/drivers/timer/config.cmake#L64, there's an example of using the generic timer in the seL4 util_libs repository here: https://github.com/seL4/util_libs/blob/master/libplatsupport/src/arch/arm/generic_timer.c.

[Ivan-Velickovic]

@podhrmic could I close this issue as resolved?

[podhrmic]

Yup, I believe this can be closed.