Indan Zupancic
Indan Zupancic
This is only a problem for devices which are active before seL4 user space starts. I haven't ran into this personally, as most devices only start generating interrupts after you...
> Unbinding and rebinding the IRQ handler shouldn't cause IRQs to be dropped either. That is difficult to achieve in practise, even if the kernel would maintain the IRQ state...
> If the handler exists and we want to preserve the "store and forward" behavior of the IRQ model (at least on arm) Isn't the only option for the kernel...
> > The alternative is to keep the IRQ disabled when there is no notification bound ([#1539](https://github.com/seL4/seL4/pull/1539)). Then the IRQ will trigger when it gets enabled again when a notification...
> the only difference is when the notification cap is being revoked via cap deletion (e.g. by revoking the corresponding Untyped). In that case IRQs are staying enabled, and one...
Usually x86 is fast enough to pass the test even on QEMU because it has a 1us margin.
Oops. Although it was fully intentional to get the behaviour equal, this isn't great for debug builds. Strangely enough, this doesn't happen in the simulated CI runs. I've removed all...
> Ok, but that also means that [@Indanz](https://github.com/Indanz) way of just existing the kernel is actually wrong, it would miss all that `mcsPreemptionPoint` cleanup that it needs to do because...
No idea why ZYNQ7000_debug_clang_32 [fails](https://github.com/seL4/seL4/actions/runs/17901806851/job/50896081850?pr=1513), but that needs to resolved first before merging this: ``` Enabling MMU and paging Warning: Could not infer GIC interrupt target ID, assuming 0. ERROR:...
Does that mean zync7000's `seL4_UserTop 0xe0000000` is ~wrong~ unfortunate? On 32-bit it's a bit crowded in the address space because of the limited range.