From b4c3af2726dfc1a249b216c571bebefe30ba21bd Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Thu, 19 Dec 2024 11:57:33 +1100 Subject: [PATCH] aspec: change arch_prepare_set_domain to not be an extended op Now that domains are part of the extensible state, arch_prepare_set_domain does not need to be in the det_ext monad. Signed-off-by: Corey Lewis --- spec/abstract/AARCH64/ArchTcb_A.thy | 2 +- spec/abstract/ARM/ArchTcb_A.thy | 2 +- spec/abstract/ARM_HYP/ArchTcb_A.thy | 2 +- spec/abstract/RISCV64/ArchTcb_A.thy | 2 +- spec/abstract/Tcb_A.thy | 6 ++---- spec/abstract/X64/ArchTcb_A.thy | 2 +- 6 files changed, 7 insertions(+), 9 deletions(-) diff --git a/spec/abstract/AARCH64/ArchTcb_A.thy b/spec/abstract/AARCH64/ArchTcb_A.thy index 8a5d36e05d..35d1729995 100644 --- a/spec/abstract/AARCH64/ArchTcb_A.thy +++ b/spec/abstract/AARCH64/ArchTcb_A.thy @@ -31,7 +31,7 @@ definition arch_post_set_flags :: "obj_ref \ tcb_flags \ "arch_post_set_flags t flags \ when (ArchFlag FpuDisabled \ flags) (fpu_release t)" -definition arch_prepare_set_domain :: "obj_ref \ domain \ unit det_ext_monad" where +definition arch_prepare_set_domain :: "obj_ref \ domain \ (unit, 'a::state_ext) s_monad" where "arch_prepare_set_domain t new_dom \ do cur_domain \ gets cur_domain; when (cur_domain \ new_dom) $ fpu_release t diff --git a/spec/abstract/ARM/ArchTcb_A.thy b/spec/abstract/ARM/ArchTcb_A.thy index 85e70cfdb0..452ba5af9a 100644 --- a/spec/abstract/ARM/ArchTcb_A.thy +++ b/spec/abstract/ARM/ArchTcb_A.thy @@ -37,7 +37,7 @@ where definition arch_post_set_flags :: "obj_ref \ tcb_flags \ (unit, 'a::state_ext) s_monad" where "arch_post_set_flags t flags \ return ()" -definition arch_prepare_set_domain :: "obj_ref \ domain \ unit det_ext_monad" where +definition arch_prepare_set_domain :: "obj_ref \ domain \ (unit, 'a::state_ext) s_monad" where "arch_prepare_set_domain t new_dom \ return ()" end diff --git a/spec/abstract/ARM_HYP/ArchTcb_A.thy b/spec/abstract/ARM_HYP/ArchTcb_A.thy index e6bc391439..710c5ca4c5 100644 --- a/spec/abstract/ARM_HYP/ArchTcb_A.thy +++ b/spec/abstract/ARM_HYP/ArchTcb_A.thy @@ -44,7 +44,7 @@ where definition arch_post_set_flags :: "obj_ref \ tcb_flags \ (unit, 'a::state_ext) s_monad" where "arch_post_set_flags t flags \ return ()" -definition arch_prepare_set_domain :: "obj_ref \ domain \ unit det_ext_monad" where +definition arch_prepare_set_domain :: "obj_ref \ domain \ (unit, 'a::state_ext) s_monad" where "arch_prepare_set_domain t new_dom \ return ()" end diff --git a/spec/abstract/RISCV64/ArchTcb_A.thy b/spec/abstract/RISCV64/ArchTcb_A.thy index e93fcb1b27..a5b5b94d0b 100644 --- a/spec/abstract/RISCV64/ArchTcb_A.thy +++ b/spec/abstract/RISCV64/ArchTcb_A.thy @@ -27,7 +27,7 @@ definition arch_post_modify_registers :: "obj_ref \ obj_ref \ tcb_flags \ (unit, 'a::state_ext) s_monad" where "arch_post_set_flags t flags \ return ()" -definition arch_prepare_set_domain :: "obj_ref \ domain \ unit det_ext_monad" where +definition arch_prepare_set_domain :: "obj_ref \ domain \ (unit, 'a::state_ext) s_monad" where "arch_prepare_set_domain t new_dom \ return ()" end diff --git a/spec/abstract/Tcb_A.thy b/spec/abstract/Tcb_A.thy index dea613b97b..a7542e2e50 100644 --- a/spec/abstract/Tcb_A.thy +++ b/spec/abstract/Tcb_A.thy @@ -273,12 +273,10 @@ definition when (tptr = cur) reschedule_required od" - \ \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.\ -definition invoke_domain:: "obj_ref \ domain \ (data list,'z::state_ext) p_monad" where +definition invoke_domain :: "obj_ref \ domain \ (data list,'z::state_ext) p_monad" where "invoke_domain thread domain \ liftE $ do - do_extended_op (arch_prepare_set_domain thread domain); + arch_prepare_set_domain thread domain; set_domain thread domain; return [] od" diff --git a/spec/abstract/X64/ArchTcb_A.thy b/spec/abstract/X64/ArchTcb_A.thy index fb13896680..a148df67f7 100644 --- a/spec/abstract/X64/ArchTcb_A.thy +++ b/spec/abstract/X64/ArchTcb_A.thy @@ -51,7 +51,7 @@ definition arch_post_set_flags :: "obj_ref \ tcb_flags \ "arch_post_set_flags t flags \ when (ArchFlag FpuDisabled \ flags) (fpu_release t)" -definition arch_prepare_set_domain :: "obj_ref \ domain \ unit det_ext_monad" where +definition arch_prepare_set_domain :: "obj_ref \ domain \ (unit, 'a::state_ext) s_monad" where "arch_prepare_set_domain t new_dom \ do cur_domain \ gets cur_domain; when (cur_domain \ new_dom) $ fpu_release t