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 <[email protected]>
seL4 · Dec 19, 2024 · a068f41 · a068f41
1 parent 8b01191
commit a068f41
Show file tree

Hide file tree

Showing 6 changed files with 7 additions and 9 deletions.
diff --git 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 \<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

diff --git 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 \<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

diff --git 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 \<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

diff --git 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 \<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

diff --git a/spec/abstract/Tcb_A.thy b/spec/abstract/Tcb_A.thy
@@ -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"

diff --git 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 \<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