Overhaul arch-split in machine, ASpec and AInvs #805
Conversation
It was a mix of ARM_A and ARM_HYP_A previously. AInvs+Refine+CRefine needed updates. Signed-off-by: Rafal Kolanski <[email protected]>
Xaphiosis
added
enhancement
cleanup
proof engineering
(already in Arch locale) Signed-off-by: Rafal Kolanski <[email protected]>
Implicitly use L4V_ARCH for global_naming prefix. Signed-off-by: Rafal Kolanski <[email protected]>
* try get rid of `interpretation Arch .` (slow) in lieu of `(in Arch)` (faster) or proper requalifying (nearly instant) * get rid of requalifications that were already requalified, or were global (thanks to new warnings) * put arch_global_naming on same line as `context Arch begin` Signed-off-by: Rafal Kolanski <[email protected]>
Xaphiosis
force-pushed
the
arch-split_ainvs
branch
from
5cfcef5
to
561e031
Compare
* get rid of `global_naming Arch`, this is no longer needed since we can requalify directly from `arch_global_naming` with `arch_requalify` commands * add missing `arch_global_naming` for `context Arch`, for consistency * update X64 Refine `Arch.` references (other arches did not need this) Signed-off-by: Rafal Kolanski <[email protected]>
Xaphiosis
force-pushed
the
arch-split_ainvs
branch
from
561e031
to
51e53e9
Compare
Thanks for spotting those FIXMEs, I cleared them out (and some others) in a separate commit, if you want to check that. |
| by (simp add: X64.switchFpuOwner_def Arch.no_fail_machine_op_lift) | ||
| by (simp add: X64.switchFpuOwner_def X64.no_fail_machine_op_lift) |
There was a problem hiding this comment.
Out of curiosity, why is this qualified at all? It seems like it would be more consistent with other architectures (and other uses in X64) if it wasn't.
There was a problem hiding this comment.
I guess looking forward we can consider whether this will be requalified when we arch_split further, that would influence how we want to make this consistent.
There was a problem hiding this comment.
Well spotted! Probably someone getting overzealous with adding qualification, there's indeed no need for it.
There was a problem hiding this comment.
Looks like removing this qualification breaks the X64 proof. I will investigate why.
There was a problem hiding this comment.
OK, this isn't an issue with ASpec/AInvs, this is someone doing an Arch-dependent proof outside of the Arch context, because why not. Will revert this "fix" and leave it for proper arch-splitting of Refine.
| (* is this the right way? we need this fact globally but it's proven with | ||
| ARM defns. *) |
There was a problem hiding this comment.
Very minor, but it looks like you've removed this comment on most architectures but left it for this one. Was that intentional?
| arch_finalise_cap_bcorres | ||
| prepare_thread_delete_bcorres | ||
|
|
||
| lemmas aobj_ref_arch_cap_simps[simp] = aobj_ref_arch_cap | ||
|
|
||
| lemmas [wp] = arch_finalise_cap_bcorres prepare_thread_delete_bcorres |
There was a problem hiding this comment.
Out of curiosity, why were these added to LevityCatch_AI? Is it that there's nowhere better for them? I would have thought that we would like to minimise its content, with it mainly containing lemmas that could be moved elsewhere.
There was a problem hiding this comment.
Definitely a derp. Would this be acceptable instead?
apply (simp add: select_ext_fa[simplified free_asid_select_def]
free_asid_select_def o_def returnOk_liftE[symmetric]
split del: if_split)
There was a problem hiding this comment.
Just to make sure, I guess this was for the conversation just below?
There was a problem hiding this comment.
Oh, right, yes. Sorry, I missed this one as well!
There was a problem hiding this comment.
I wanted to have these in a generic theory file, but couldn't find one that was in the import hierarchy in time for these to be useful. I'll take another look while I'm fixing X64, but I don't know if I'll find anyplace better. Advice welcome.
proof/refine/ARM/Arch_R.thy
Outdated
| free_asid_select_def o_def returnOk_liftE[symmetric] | ||
| split del: if_split) | ||
| free_asid_select_def o_def returnOk_liftE[symmetric] split del: if_split) |
There was a problem hiding this comment.
Not sure about this, the previous indentation looks better.
|
Some good looking benchmarks for this |
|
@corlewis I addressed your comments, hopefully, with the latest commits (they're named after the commit I'm supposed to squash them into) |
My only guess is based on the fact that ARM seems to have the smallest spec and proof. Maybe that means its arch-specific files are smaller, and that interpreting its |
My impression was that RISCV64 is the smallest? |
* prevent duplication between arches by moving requalifications from
Arch theories to generic ones
* this strategy is not available for new constants that are introduced
in the Arch locale that need to be referenced in generic definitions
or locale instantiations
* fix up the inconsistent qualification of set_cap_valid_arch_caps_simple
Signed-off-by: Rafal Kolanski <[email protected]>
Rename the wellformed_acap version to wf_acap_rights_update_id, and the valid_arch_cap version to valid_acap_rights_update_id. Signed-off-by: Rafal Kolanski <[email protected]>
Avoid unnecessary Arch context interpretation (slow). Remove attempts at requalifying entities that are already generic (misleading). Signed-off-by: Rafal Kolanski <[email protected]>
Makes global_naming implicit (based on L4V_ARCH). Signed-off-by: Rafal Kolanski <[email protected]>
This was generic on these two architectures, not consistent with others. Signed-off-by: Rafal Kolanski <[email protected]>
MiscMachine_A already contains asid_high_bits, asid_low_bits and asid_bits. Other architectures don't duplicate them in Arch_Structs_A, so ARM and ARM_HYP shouldn't either. For ARM, this also means fixing up DRefine+DPolicy+CamkesCdlRefine to refer to the MiscMachine_A definitions when needed (CapDL duplicates them again in Types_D, but as they don't import machine theories, those can't be removed). Signed-off-by: Rafal Kolanski <[email protected]>
These proofs have been arch-split for some time now so the FIXMEs appear resolved. They are also non-specific, so it is impossible to tell at this point whether they referred to anything. Signed-off-by: Rafal Kolanski <[email protected]>
Xaphiosis
force-pushed
the
arch-split_ainvs
branch
from
2c7a062
to
a08fc9a
Compare
|
Squashed |
Sorry, by smallest I meant quickest out of the ones I had tested. I'll also test RISCV64 to see how it compares, I didn't get around to it before. |
I've added RISCV64 results to my earlier comment. Like you thought, it's the shortest/quickest AInvs. I don't know how much to read into it, but it does also show one of the smallest improvements. |
Cool, thank you! The improvement on it still beat ARM somehow, especially in ASpec. I remain puzzled. |
In #791 I went over AInvs for AARCH64 only. I've since expanded the approach to ASpec as well, and deployed it across all the architectures. The speed benefits still apply, and now ASpec is faster as well. I'll see if I can do a better benchmark, or we can pull it out of the regression tests.
🦆🦆🦆 I have put a lot of effort into splitting up the commits into being topical, because this is a rather large PR. They should not overlap much, so if you review a line in the commit view it's unlikely to be changed in another commit.
@mbrcknl @michaelmcinerney FYI in case you are interested in the new arch-splitting tech/approach.
FIXME arch_splitto PR linter to stop people reintroducing itapply_traceI accidentally left in (proof/invariant-abstract/X64/ArchCSpace_AI.thyinainvs: disambiguate acap_rights_update_id)