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

Update explicit FPU specifications for det_ext changes #843

Merged
merged 1 commit into from
Dec 19, 2024
Merged

Update explicit FPU specifications for det_ext changes #843

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion spec/abstract/AARCH64/ArchTcb_A.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ definition arch_post_set_flags :: "obj_ref \<Rightarrow> tcb_flags \<Rightarrow>
"arch_post_set_flags t flags \<equiv>
when (ArchFlag FpuDisabled \<in> flags) (fpu_release t)"

definition arch_prepare_set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> unit det_ext_monad" where
definition arch_prepare_set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> (unit, 'a::state_ext) s_monad" where
"arch_prepare_set_domain t new_dom \<equiv> do
cur_domain \<leftarrow> gets cur_domain;
when (cur_domain \<noteq> new_dom) $ fpu_release t
Expand Down
2 changes: 1 addition & 1 deletion spec/abstract/ARM/ArchTcb_A.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ where
definition arch_post_set_flags :: "obj_ref \<Rightarrow> tcb_flags \<Rightarrow> (unit, 'a::state_ext) s_monad" where
"arch_post_set_flags t flags \<equiv> return ()"

definition arch_prepare_set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> unit det_ext_monad" where
definition arch_prepare_set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> (unit, 'a::state_ext) s_monad" where
"arch_prepare_set_domain t new_dom \<equiv> return ()"

end
Expand Down
2 changes: 1 addition & 1 deletion spec/abstract/ARM_HYP/ArchTcb_A.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ where
definition arch_post_set_flags :: "obj_ref \<Rightarrow> tcb_flags \<Rightarrow> (unit, 'a::state_ext) s_monad" where
"arch_post_set_flags t flags \<equiv> return ()"

definition arch_prepare_set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> unit det_ext_monad" where
definition arch_prepare_set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> (unit, 'a::state_ext) s_monad" where
"arch_prepare_set_domain t new_dom \<equiv> return ()"

end
Expand Down
2 changes: 1 addition & 1 deletion spec/abstract/RISCV64/ArchTcb_A.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ definition arch_post_modify_registers :: "obj_ref \<Rightarrow> obj_ref \<Righta
definition arch_post_set_flags :: "obj_ref \<Rightarrow> tcb_flags \<Rightarrow> (unit, 'a::state_ext) s_monad" where
"arch_post_set_flags t flags \<equiv> return ()"

definition arch_prepare_set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> unit det_ext_monad" where
definition arch_prepare_set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> (unit, 'a::state_ext) s_monad" where
"arch_prepare_set_domain t new_dom \<equiv> return ()"

end
Expand Down
6 changes: 2 additions & 4 deletions spec/abstract/Tcb_A.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -273,12 +273,10 @@ definition
when (tptr = cur) reschedule_required
od"

\<comment> \<open>FIXME FPU: @{term arch_prepare_set_domain} shouldn't be an extended op. Fixing this will require either
adding domains to the non-det spec, or removing the non-det spec completely.\<close>
definition invoke_domain:: "obj_ref \<Rightarrow> domain \<Rightarrow> (data list,'z::state_ext) p_monad" where
definition invoke_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> (data list,'z::state_ext) p_monad" where
"invoke_domain thread domain \<equiv>
liftE $ do
do_extended_op (arch_prepare_set_domain thread domain);
arch_prepare_set_domain thread domain;
set_domain thread domain;
return []
od"
Expand Down
2 changes: 1 addition & 1 deletion spec/abstract/X64/ArchTcb_A.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ definition arch_post_set_flags :: "obj_ref \<Rightarrow> tcb_flags \<Rightarrow>
"arch_post_set_flags t flags \<equiv>
when (ArchFlag FpuDisabled \<in> flags) (fpu_release t)"

definition arch_prepare_set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> unit det_ext_monad" where
definition arch_prepare_set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> (unit, 'a::state_ext) s_monad" where
"arch_prepare_set_domain t new_dom \<equiv> do
cur_domain \<leftarrow> gets cur_domain;
when (cur_domain \<noteq> new_dom) $ fpu_release t
Expand Down
Loading