arch-split Schedule_R #948
Open
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
In preparation for arch-split. Create Schedule_R.thy and update import hierarchy. Signed-off-by: Rafal Kolanski <[email protected]>
For PR review: minimise diff Signed-off-by: Rafal Kolanski <[email protected]>
Signed-off-by: Rafal Kolanski <[email protected]>
With s/AARCH64/<arch>/ For PR Signed-off-by: Rafal Kolanski <[email protected]>
Weaken preconditions of setVMRoot_corres for ARM+ARM_HYP+X64: remove redundancy and use cross lemmas. Signed-off-by: Rafal Kolanski <[email protected]>
Signed-off-by: Rafal Kolanski <[email protected]>
Xaphiosis
added
the
arch-split
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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 has the same diff-reducing tech as the TcbAcc_R PR, copied instructions:
In real life, I did the usual addition of Schedule_R, hierarchy update, arch-split and then update. However, since the arch-split part first splits AARCH64, then takes the AARCH64 version of ArchSchedule_R and only fixes what broke, we ended up with a small(er) diff there (again).
Please review commit-by commit with the following notes:
[squash] PR: copy AARCH64 version into Schedule_R- same as last time: stop Schedule_R looking like a wall of green (no need to review)aarch64 refine: arch-split Schedule_R- this is the main bulk of the arch-split, dealing with AARCH64[squash] copy AARCH64 ArchSchedule_R to other arches- wipes the body (not the header!) of other arches' ArchSchedule_R with a copy of the AARCH64 version withAARCH64appropriately substituted (as @corlewis requested last time) - (mostly pointless to review)refine+crefine: update for ... arch-splitReminder: DO NOT MERGE squashed version if it still says
aarch64 refine: arch-splitStats: 30 files changed, 3108 insertions(+), 10756 deletions(-)
Total: 7648 lines removed