Hi Alex, The reason edge triggered interrupts are masked is because, due to the current design of seL4, they represent a potential denial of service vector. Devices, such as the PIT, that do not need to be directly acknowledged before they will generate an additional interrupt, could be setup to rapidly generate interrupts causing the kernel interrupt handler to continuously run and no user level progress to be made. One option is to just say 'we will trust the drivers for any devices that can behave in this manner'. Clearly this should be an option of last resort though. You should be able to work around this at user level if you check if you missed an interrupt after calling seL4_IRQHandler_Ack, and perform any necessary fixups. Another option is to change how interrupts are handled in the kernel and delay acknowledging the local interrupt controller until the user calls seL4_IRQHandler_Ack. This would remove the need mask and unmask the I/O APIC. Although it still doesn't change the fact that if additional interrupts come in before the user handler can run they will still get dropped. All in all I cannot provide a simple solution off the top of my head. This is something that may take a bit of serious thinking. Adrian On Tue 23-Aug-2016 6:57 PM, Alexander Boettcher wrote:

Hi,

we are using as user level timer driver the PIT on Genode/seL4 and experience situations that the driver does not get IRQs after a while. It happens on Qemu as also on native x86 hardware.

We tracked down the problem to the masking of edge-triggered IRQs on the I/O APIC in the seL4 kernel. According to Intel, [0] chapter 3.2.4 "Interrupt Mask R/W", edge interrupts on a masked interrupt pin gets ignored and are not held pending. On [2] there are also some discussion about this topic too.

We solved/workaround the issue by this patch [1]. I looked additionally into two other microkernels using the I/O APIC and they don't mask edge level triggered I/O APIC interrupts. I wonder if anybody already stumbled about the issue on seL4/x86? If not, please take the patch or give advices to adapt the patch so that it may get upstream.

Thanks,

Alexander Boettcher.

[0] http://www.intel.com/design/chipsets/datashts/29056601.pdf [1] https://github.com/genodelabs/genode/blob/master/repos/base-sel4/patches/ioa... [2] http://yarchive.net/comp/linux/edge_triggered_interrupts.html

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel