Proofs for SGI API #733
Draft
Proofs for SGI API #733
Conversation
This file contains 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
lsf37
force-pushed
the
sgi
branch
5 times, most recently
from
6176090
to
5b40e6f
Compare
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
In preparation for adding an API for software-generated interrupts, make config_ARM_GIC_V3 visible to the proofs, so values of constants can be defined conditionally on GICv2/v3 use. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This affects all architectures, because generic interfaces are changing, but the SGISignalCap API is only added to ARM, ARM_HYP, and AARCH64. For X64 and RISCV64, we trivially implement the new interfaces, and in generic code we call those interfaces. These new interfaces are isArchMDBParentOf and isIRQControlCapDescendant, for checking in generic code if there are architecture specific cases in isMDBParentOf and isCapRevocable respectively. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Define the new constants numSGIs and gicSGITargetMaskBits, plus a new machine operation ipiSendTarget. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- add SGISignalCap API for ARM, ARM_HYP, AARCH64 - add generic interface for should_be_arch_parent_of and is_irq_control_descendant in the cdt implementation - add default interface implementations new interfaces for RISCV64, X64 Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This contains a slight tweak to generic CSpace_AI and proof adjustments for the architectures that do not implement the SGISignalCap API. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
For now exclude SGISignalCap from wellformed specs. To be relaxed later. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Fix + modernise style and proofs. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add separation logic specification lemmas for the new SGISignalCap API for later use in sys-init. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
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.
This PR adds verification for the SGISignalCap API of RFC-17 (seL4/seL4#1222).
Specs and proofs are updated for all architectures (affects mostly ARM, ARM_HYP, and AARCH64), including all affected parts of the proof stack (access control, infoflow, capDL, system initialiser etc). In the system initialiser, SGISignalCaps are currently still excluded via the definition of wellformed specifications.
Test with: seL4/seL4#1222
This is currently still in draft mode until the RFC recommendations have been implemented.