Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Update AARCH64 Refine and CRefine for explicit FPU changes #873

Open
wants to merge 12 commits into
base: explicit_fpu
Choose a base branch
from
Open

Update AARCH64 Refine and CRefine for explicit FPU changes #873

wants to merge 12 commits into from

Conversation

corlewis
Copy link
Member

@corlewis corlewis commented Mar 21, 2025 •
edited
Loading

Test with seL4/seL4#1325

@corlewis corlewis requested review from Xaphiosis, lsf37 and ryybrr March 21, 2025 05:44
@corlewis corlewis self-assigned this Mar 21, 2025
@corlewis corlewis force-pushed the explicit_fpu_aarch64 branch 4 times, most recently from c7d17b3 to 4e1f1d0 Compare March 28, 2025 03:02
@corlewis corlewis force-pushed the explicit_fpu_aarch64 branch 2 times, most recently from 8cf9811 to c7120fd Compare March 31, 2025 07:14
corlewis added 2 commits March 31, 2025 23:09
@corlewis
lib+proof: add corres_return_eq_same_unit
17cbe7e 
This rule is instantiated for unit returns and with dc for the return
relation. It is added to the corres_term set before
corres_return_eq_same so that it matches first.

corres_machine_op_Id_dc is also moved before corres_machine_op_Id_eq for
the same reason.

Signed-off-by: Corey Lewis <[email protected]>
@corlewis
aarch64+x64 spec: fix mistakes in fpu specifications
5f4a249 
Missed control flow in lazyFpuRestore and incorrect guard in the
Haskell for switchLocalFpuOwner.

Signed-off-by: Corey Lewis <[email protected]>
@corlewis corlewis force-pushed the explicit_fpu_aarch64 branch from c7120fd to 65c4088 Compare March 31, 2025 12:14
Xaphiosis
Xaphiosis reviewed Apr 1, 2025
View reviewed changes
proof/invariant-abstract/Detype_AI.thy Outdated
@@ -1042,7 +1042,7 @@ lemma (in Detype_AI) cte_map_not_null_outside: (*FIXME: arch-split*)
apply (drule(1) valid_globals_irq_node, fastforce simp: cap_range_def)
done


\<comment> \<open>FIXME: move\<close>
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this and the next FIXME move are added as part of "aarch64 ainvs: update for spec changes" which is a bit odd.
also, nearly all our FIXME comments are in (* FIXME ... *) form, which makes grepping easier. Any reason why these ones are using the ― ‹FIXME: move› version?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Only because I have a keybind for commenting things out with ― ‹...› and because I didn't know that people used the comment format for grepping for FIXMEs.

Xaphiosis
Xaphiosis reviewed Apr 1, 2025
View reviewed changes
proof/refine/Invariants_H.thy Outdated
@@ -2695,6 +2695,14 @@ lemma obj_at'_ko_at'_prop:
"ko_at' ko t s \<Longrightarrow> obj_at' P t s = P ko"
by (drule obj_at_ko_at', clarsimp simp: obj_at'_def)

lemma ko_wp_at'_not_o:
"ko_wp_at' (\<lambda>a. \<not> P a) t s = ko_wp_at' (Not o P) t s"
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not a fan of these: <circ> is newer than o, and also it's fun_comp or comp, the suffix "not_o" is not guessable, and on top of that this is an equality lemma. If you look at some of the lemmas above, it doesn't blend in at all.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd call this one ko_wp_at'_not_comp_fold

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These were based on abstract versions for obj_at, which is I think where the name and use of o instead of comp and <circ> came from. I'll update them.

With regards to the location, I originally had them where I needed them and wanted to move them somewhere up earlier. This was the best place that I could quickly find in Invariants_H but I'm open to suggestions.

Xaphiosis
Xaphiosis reviewed Apr 1, 2025
View reviewed changes
proof/refine/AARCH64/Retype_R.thy
@@ -2397,6 +2397,10 @@ lemma other_objs_default_relation:
split: Structures_A.apiobject_type.split_asm)
done

lemma word_to_tcb_flags_0[simp]:
"word_to_tcb_flags 0 = {}"
by (clarsimp simp: word_to_tcb_flags_def)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

consider moving higher up, but up to you

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I actually originally had this marked to be moved but I couldn't find anywhere that made sense for it. It's defined in Structures_A and then there aren't any other lemmas about it.

Xaphiosis
Xaphiosis reviewed Apr 1, 2025
View reviewed changes
proof/crefine/AARCH64/Schedule_C.thy
setVMRoot tcb
od)"

lemma arch_switchToThread_rewrite:
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

does the _rewrite name fit into any kind of pattern of how we did these before? rewrite is kinda generic

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In general rewrite is a bit too vague, but since arch_switchToThread is just defined above for begin rewritten into switchToThread I would be fine with this one.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I couldn't find anything else doing quite the same thing to copy a naming pattern from and just went with rewrite, hoping that it would make sense with the comment I included. It's not a lemma that's intended to be used or found outside of this one specific use case.

Xaphiosis
Xaphiosis reviewed Apr 1, 2025
View reviewed changes
proof/crefine/AARCH64/StateRelation_C.thy
@@ -114,6 +114,12 @@ definition cur_vcpu_relation ::
Some acurvcpu \<Rightarrow> cvcpu = Ptr (fst acurvcpu) \<and> cvcpu \<noteq> NULL \<and> cactive = from_bool (snd acurvcpu)
| None \<Rightarrow> cvcpu = NULL \<and> cactive = 0"

definition cur_fpu_relation :: "machine_word option \<Rightarrow> tcb_C ptr \<Rightarrow> bool" where
"cur_fpu_relation akscurfpu cfpu \<equiv>
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

uhh... akscurfpu? it's more like afpu_opt at this point

Copy link
Member Author

@corlewis corlewis Apr 4, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is copying cur_vcpu_relation just above it. If we're being really pedantic then it should probably be something with owner in the name, since it's talking about the tcb not the fpu.

Xaphiosis
Xaphiosis reviewed Apr 1, 2025
View reviewed changes
Xaphiosis
Xaphiosis reviewed Apr 1, 2025
View reviewed changes
proof/crefine/AARCH64/ADT_C.thy
@@ -140,6 +140,12 @@ where
then None
else Some (ptr_val vcpuptr, to_bool vcpuactive)"

definition ccur_fpu_to_H :: "tcb_C ptr \<Rightarrow> machine_word option" where
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this is really any TCB pointer to a pointer option, I don't think ccur_fpu_to_H is that helpful as a name here, and cur_fpu_owner argument is misleading; don't we already have a function that does this?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

then again, this is probably copied from ccur_vcpu_to_H so I don't know anymore

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm somewhat surprised we don't have this function yet somewhere, it does seem generally useful for all C TCB pointers. +1 for giving it a more general name and argument name.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, this was just following ccur_vcpu_to_H, which is a bit more complicated being about VCPUs and needing to take into account whether the VCPU is active or not. If I make it generic should it be moved somewhere else (and if so, any suggestions?)

Xaphiosis
Xaphiosis approved these changes Apr 1, 2025
View reviewed changes
Copy link
Member

@Xaphiosis Xaphiosis left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Bunch of nipticks, but generally things look good and the proof approach seems to be working out. Nice.

Oh, commit message:
"aarch64+x64 spec: changes to ease refinement proofs": has long description with lots of commas, would prefer bullet list, also TCB vs tcb

lsf37
lsf37 reviewed Apr 2, 2025
View reviewed changes
lsf37
lsf37 reviewed Apr 2, 2025
View reviewed changes
Copy link
Member

@lsf37 lsf37 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Raf already has all the style stuff, so nothing left for me to nitpick on :-) This is turning out quite nicely, I think.

@corlewis
Copy link
Member Author

corlewis commented Apr 4, 2025

Apologies for adding new content after this had been reviewed but I want to see a green tick so this now also updates Orphanage.

corlewis added 8 commits April 4, 2025 16:17
@corlewis
aarch64+x64 spec: changes to ease refinement proofs
9e75a44 
* Reorder fpuRelease and dissociateVCPUTCB in prepareThreadDelete to
avoid needing to prove that fpuRelease preserves TCB properties.
* Move enableFpu after global accessor in switchLocalFpuOwner.
* Add fpuOwner_asrt to Haskell to cross over helpful property.

Signed-off-by: Corey Lewis <[email protected]>
@corlewis
aarch64 ainvs: update for spec changes
0d474c9 
Signed-off-by: Corey Lewis <[email protected]>
@corlewis
aarch64 refine: update proofs for explicit fpu changes
ba4b890 
Signed-off-by: Corey Lewis <[email protected]>
@corlewis
clib: add ccorres_when_strong
cbb7cb0 
Signed-off-by: Corey Lewis <[email protected]>
@corlewis
aarch64 crefine: update proofs for explicit fpu changes
2746189 
Signed-off-by: Corey Lewis <[email protected]>
@corlewis
squash refine: update Orphanage
6bd7419 
Signed-off-by: Corey Lewis <[email protected]>
@corlewis
squash spec: PR suggestions
f9915ac 
Signed-off-by: Corey Lewis <[email protected]>
@corlewis
squash ainvs: PR suggestions
9ee80e0 
Signed-off-by: Corey Lewis <[email protected]>
@corlewis corlewis force-pushed the explicit_fpu_aarch64 branch from ffe2a69 to 6f6f31b Compare April 4, 2025 05:24
@corlewis corlewis force-pushed the explicit_fpu_aarch64 branch from 6f6f31b to 3271dcc Compare April 4, 2025 06:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@lsf37 lsf37 lsf37 left review comments

@Xaphiosis Xaphiosis Xaphiosis approved these changes

@ryybrr ryybrr Awaiting requested review from ryybrr

Assignees

@corlewis corlewis

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@corlewis @Xaphiosis @lsf37