arch-split Ipc_R#993
Conversation
Allows copyMRs_corres and getMRs_corres to become generic. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
In preparation for arch-split. Create Ipc_R.thy and update import hierarchy. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Decreases diff during PR review. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
To reduce diff during PR review. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Xaphiosis
added
the
arch-split
| (* FIXME arch-split: move up *) | ||
| arch_requalify_consts pageBitsForSize | ||
|
|
||
| arch_requalify_facts mab_pb (* FIXME arch-split: from ArchTcbAcc_AI *) |
There was a problem hiding this comment.
Are these FIXMEs that you want to resolve as part of this round or leave for later?
There was a problem hiding this comment.
I want to leave these for a second pass, as it involves diving into AInvs, including figuring out where the Machine_AI exports are, and having a clearer head to maybe improve something over there.
There's a FIXME a bit below this that says "review for sanity", which I'd appreciate an opinion on. I'm not sure if I captured the right idea.
| shows | ||
| "corres (=) (tcb_at t and pspace_aligned and pspace_distinct and case_option \<top> in_user_frame buf) | ||
| (case_option \<top> valid_ipc_buffer_ptr' buf) | ||
| (set_mrs t buf mrs) (setMRs t buf mrs')" |
There was a problem hiding this comment.
Out of curiosity, why is setMRs_corres the only one out of the MRs family that had to stay in the arch file? The definition of setMRs doesn't seem to do anything more arch-specific than getMRs.
There was a problem hiding this comment.
Oh, is it because its proof refers to user_fpu_state on architectures that have it? Fair enough then, probably not worth trying to abstract that.
There was a problem hiding this comment.
Yeah, that kept popping up, but even ignoring that it kept throwing up an update to the TCB arch state for which I was unable produce a nice interface.
| (* FIXME: poor name, eliminate as wp argument *) | ||
| lemma lookup_cap_valid'[wp]: |
There was a problem hiding this comment.
It took me a moment to work out what you meant with the second part of this FIXME, and I'm not sure I would have without the context of this being added to wp. Possible reword?
(* FIXME: change name, eliminate existing uses as argument to wp method *)
There was a problem hiding this comment.
Oh yes, much better, I'll take your version.
| (* FIXME arch-split: move, review for sanity *) | ||
| lemma no_fail_zipWithM_x: | ||
| assumes P: "\<And>x y. no_fail P (f x y)" | ||
| assumes inv: "\<And>x y. f x y \<lbrace>P\<rbrace>" | ||
| shows "no_fail P (zipWithM_x f xs ys)" |
There was a problem hiding this comment.
This looks reasonable to me. If you really want to though, you could strengthen it to be more like no_fail_mapM_wp.
2 participants
🦆🦆🦆 In the process of doing Ipc_R, I discovered that TcbAcc_R could be improved, so there is an extra commit with that improvement in this PR before the Ipc_R arch-splitting starts. Again, please review commit-by-commit.
Instructions:
In real life, I did the usual addition of Ipc_R, hierarchy update, arch-split and then update. However, since the arch-split part first splits AARCH64, then takes the AARCH64 version of Ipc_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 (some inconsistency with squash/wip/fake comments on the PR-only commits):
[squash] PR: copy AARCH64 version into ..._R- same as last time: stop..._Rlooking like a wall of green (no need to review)refine: arch-split..._R (AARCH64 ONLY)` - this is the main bulk of the arch-split, dealing with AARCH64, as well as updates[squash] copy AARCH64 Arch..._R to other arches- wipes the body (not the header!) of other arches' Arch..._R with a copy of the AARCH64 version withAARCH64appropriately substituted - (mostly pointless to review)Reminder: DO NOT MERGE squashed version if it still says
aarch64 refine: arch-splitorAARCH64Stats: 76 files changed, 3313 insertions(+), 20017 deletions(-)
Total: 16704 lines removed