ioapic: set IOAPIC_IRQ_LINES to max allowed #1263
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Correctly mask the IOAPICVER register to the Maximum Redirection Entry field to potential avoid spurious higher bits on e.g. AMD processors. Set IOAPIC_IRQ_LINES to the maximum value this field is allowed to return (239+1). While our haswell machines report 24 IRQ lines as expected, the skylake machines report 120. The only impact should be the size of the ioredtbl_state array. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
d68a5ce to
6d97856
Compare
wom-bat
approved these changes
Jun 13, 2024
|
The proofs are failing because this repo still points to Isabelle2023 and l4v has moved to Isabelle2024 already. Added #1264 to get automatic updates in the future. |
|
Have checked the proofs separately, and they pass. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Correctly mask the IOAPICVER register to the Maximum Redirection Entry field to potential avoid spurious higher bits on e.g. AMD processors.
Set IOAPIC_IRQ_LINES to the maximum value this field is allowed to return (239+1). While our
haswellmachines report 24 IRQ lines as expected, theskylakemachines report 120.The only impact should be the size of the ioredtbl_state array.
Sources: it was extremely hard to find actual docs for the IOAPIC. The Intel manual was not helpful. This ancient PDF had information on the register format, max value, and masking requirements, which I followed here. This seems to be consistent with what FreeBSD does in e.g. apicreg.h.