Even if the kernel allowed it, you still can't tell which PD the interrupt is for, you need device knowledge for that, which requires either broadcast or some driver-level knowledge: so to replicate it on seL4 you need an intermediary PD.
(Possibly we should document this pattern somewhere?)
Originally posted by @midnightveil in #600 (comment)
Even if the kernel allowed it, you still can't tell which PD the interrupt is for, you need device knowledge for that, which requires either broadcast or some driver-level knowledge: so to replicate it on seL4 you need an intermediary PD.
(Possibly we should document this pattern somewhere?)
Originally posted by @midnightveil in #600 (comment)