seL4
Only access IOAPIC registers that are actually present
IOAPICS can have varying numbers of lines attached. The actual number can be accessed in the top 16 bits of the version register.
Rather than assuming fixed 24 lines per IRQ, read the actual number and use that.
Signed-off-by: Peter Chubb [email protected]
Maybe a comment should be added to ioredtbl_high to explain that IOAPIC_IRQ_LINES is used as an upper bound of how much memory to reserve for book keeping.
Fixed.
Problem I'm trying to solve is machine hang when attempting to access non-existent registers.
Spec and proof, yes.
@lsf37, are proof updates scheduled or in progres?
Problem I'm trying to solve is machine hang when attempting to access non-existent registers.
@wom-bat, is this urgent? I don't think we can merge it until proofs are ready. If proof updates aren't scheduled and the changes are urgent, we could put it behind a temporary compile-time config? Otherwise the PR is blocked until proofs are done AFAIK.
Spec and proof, yes.
@lsf37, are proof updates scheduled or in progres?
Unless someone has funding for it it'll have to wait until I have spare time (with a bit of luck in the week after next) or someone else picks it up.