Indan Zupancic

> Kernel is loaded to `0x_e000_0000`, but this also happens to be the UART address: > > https://github.com/seL4/seL4/blob/09e6c3f5e27607cd6f7854bdc5e87d829c48d500/tools/dts/zynq7000.dts#L260-L269 Good find. > Somehow I've become mistaken, I thought the kernel booted...

> What about having the uart mapped to a defined virtual address as part of the boot contract with the elfloader. The elfloader always has uart working when it switches...

> > Assuming 8 byte aligned watchpoints are not an Aarch64-only thing, all seems fine to me. If it isn't, then you need to align to either 4 or 8...

> My comments were based on the ARM architecture reference manual (https://developer.arm.com/documentation/ddi0487/latest/). I know that. When I ask for a reference, I mean document version + chapter/section/page number, as searching...

Is no one using x86 seL4 that this hasn't bothered people more in the last decade?

Seems very straightforward and overall a simplification which is more user friendly in a backward compatible way. Except if I'm missing something, the only downside is that it causes some...

> Oh, that's nice. It also seems to have removed some complexity with the delete/deletingIRQHandler too, which is great. I love it when this sort of improvement makes the code...

New push with the old cleanup code left intact, but only enabling IRQs when setting a notification and disabling IRQs when clearing the IRQHandler.

With this change the new invariant could be something like: "IRQs are disabled if no corresponding IRQ handler cap exists and enabled when there is a notification registered". And deliberately...

Thanks for the update. > For acknowledging an interrupt, we currently require that `interrupt_states s irq != IRQInactive`. With the new invariant we no longer know this, and it can...