Update specs to use semi-lazy FPU switching

spec/abstract/AARCH64/ArchTcb_A.thy

@@ -7,7 +7,7 @@
 chapter \<open>Architecture-specific TCB functions\<close>
 
 theory ArchTcb_A
-imports KHeap_A
+imports FPU_A
 begin
 
 context Arch begin arch_global_naming (A)
@@ -26,5 +26,16 @@ definition arch_get_sanitise_register_info :: "obj_ref \<Rightarrow> (bool, 'a::
 definition arch_post_modify_registers :: "obj_ref \<Rightarrow> obj_ref \<Rightarrow> (unit, 'a::state_ext) s_monad" where
   "arch_post_modify_registers cur t \<equiv> return ()"
 
+\<comment> \<open>The corresponding C code is not arch dependent and so is inline as part of invokeSetFlags\<close>
+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>
+     when (ArchFlag FpuDisabled \<in> flags) (fpu_release t)"
+
+definition arch_prepare_set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> unit det_ext_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
+   od"
+
 end
 end

spec/abstract/AARCH64/ArchVSpace_A.thy

@@ -395,12 +395,9 @@ definition in_user_frame :: "obj_ref \<Rightarrow> 'z::state_ext state \<Rightar
   "in_user_frame p s \<equiv>
      \<exists>sz. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz))"
 
-definition fpu_thread_delete :: "obj_ref \<Rightarrow> (unit, 'z::state_ext) s_monad" where
-  "fpu_thread_delete thread_ptr \<equiv> do_machine_op (fpuThreadDeleteOp thread_ptr)"
-
 definition prepare_thread_delete :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
   "prepare_thread_delete thread_ptr \<equiv> do
-     fpu_thread_delete thread_ptr;
+     fpu_release thread_ptr;
      t_vcpu \<leftarrow> arch_thread_get tcb_vcpu thread_ptr;
      case t_vcpu of
        Some v \<Rightarrow> dissociate_vcpu_tcb v thread_ptr

spec/abstract/AARCH64/Arch_A.thy

@@ -25,7 +25,8 @@ definition arch_switch_to_thread :: "obj_ref \<Rightarrow> (unit,'z::state_ext)
   "arch_switch_to_thread t \<equiv> do
      tcb \<leftarrow> gets_the $ get_tcb t;
      vcpu_switch $ tcb_vcpu $ tcb_arch tcb;
-     set_vm_root t
+     set_vm_root t;
+     lazy_fpu_restore t
    od"
 
 definition arch_switch_to_idle_thread :: "(unit,'z::state_ext) s_monad" where
@@ -34,6 +35,9 @@ definition arch_switch_to_idle_thread :: "(unit,'z::state_ext) s_monad" where
     set_global_user_vspace
   od"
 
+definition arch_prepare_next_domain :: "(unit,'z::state_ext) s_monad" where
+  "arch_prepare_next_domain \<equiv> switch_local_fpu_owner None"
+
 definition arch_activate_idle_thread :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
   "arch_activate_idle_thread t \<equiv> return ()"
 

spec/abstract/AARCH64/Arch_Structs_A.thy

@@ -333,6 +333,7 @@ record arch_state =
   arm_us_global_vspace :: "obj_ref"
   arm_current_vcpu    :: "(obj_ref \<times> bool) option"
   arm_gicvcpu_numlistregs :: nat
+  arm_current_fpu_owner :: "obj_ref option"
 
 
 end_qualify
@@ -369,6 +370,14 @@ record arch_tcb =
   tcb_context :: user_context
   tcb_vcpu    :: "obj_ref option"
 
+datatype arch_tcb_flag
+  = FpuDisabled
+
+definition word_from_arch_tcb_flag :: "arch_tcb_flag \<Rightarrow> machine_word" where
+  "word_from_arch_tcb_flag flag \<equiv>
+     case flag of
+       FpuDisabled \<Rightarrow> bit 0"
+
 end_qualify
 
 context Arch begin arch_global_naming (A)

spec/abstract/AARCH64/FPU_A.thy

@@ -0,0 +1,59 @@
+(*
+ * Copyright 2024, Proofcraft Pty Ltd
+ *
+ * SPDX-License-Identifier: GPL-2.0-only
+ *)
+
+chapter "AARCH64 FPU Functions"
+
+theory FPU_A
+imports
+  KHeap_A
+begin
+
+context Arch begin arch_global_naming (A)
+
+definition save_fpu_state :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
+  "save_fpu_state t \<equiv> do
+     fpu_state \<leftarrow> do_machine_op readFpuState;
+     as_user t (setFPUState fpu_state)
+   od"
+
+definition load_fpu_state :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
+  "load_fpu_state t \<equiv> do
+     fpu_state \<leftarrow> as_user t getFPUState;
+     do_machine_op (writeFpuState fpu_state)
+   od"
+
+\<comment> \<open>FIXME: maybe use an if instead of the case (depends on if wpc or if\_split is easier)\<close>
+definition switch_local_fpu_owner :: "obj_ref option \<Rightarrow> (unit,'z::state_ext) s_monad" where
+  "switch_local_fpu_owner new_owner \<equiv> do
+     do_machine_op enableFpu;
+     cur_fpu_owner \<leftarrow> gets (arm_current_fpu_owner \<circ> arch_state);
+     maybeM save_fpu_state cur_fpu_owner;
+     case new_owner of
+       None \<Rightarrow> do_machine_op disableFpu
+       | Some tcb_ptr \<Rightarrow> load_fpu_state tcb_ptr;
+     modify (\<lambda>s. s \<lparr>arch_state := arch_state s\<lparr>arm_current_fpu_owner := new_owner\<rparr>\<rparr>)
+   od"
+
+definition fpu_release :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
+  "fpu_release thread_ptr \<equiv> do
+     cur_fpu_owner \<leftarrow> gets (arm_current_fpu_owner \<circ> arch_state);
+     when (cur_fpu_owner = Some thread_ptr) $ switch_local_fpu_owner None
+   od"
+
+definition lazy_fpu_restore :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
+  "lazy_fpu_restore thread_ptr \<equiv> do
+     flags \<leftarrow> thread_get tcb_flags thread_ptr;
+     if ArchFlag FpuDisabled \<in> flags
+     then do_machine_op disableFpu
+     else do
+       do_machine_op enableFpu;
+       switch_local_fpu_owner (Some thread_ptr)
+     od
+   od"
+
+end
+
+end

spec/abstract/AARCH64/Hypervisor_A.thy

@@ -14,17 +14,13 @@ context Arch begin arch_global_naming (A)
 
 fun handle_hypervisor_fault :: "machine_word \<Rightarrow> hyp_fault_type \<Rightarrow> (unit, 'z::state_ext) s_monad"
   where
-  "handle_hypervisor_fault thread (ARMVCPUFault hsr) = do
-     fpu_enabled \<leftarrow> do_machine_op isFpuEnable;
-     if \<not>fpu_enabled
-     then fail
-     else if hsr = 0x2000000 \<comment> \<open>@{text UNKNOWN_FAULT}\<close>
-          then do
-            esr \<leftarrow> do_machine_op getESR;
-            handle_fault thread (UserException (esr && mask 32) 0)
-          od
-          else handle_fault thread (ArchFault $ VCPUFault (ucast hsr))
-   od"
+  "handle_hypervisor_fault thread (ARMVCPUFault hsr) =
+     (if hsr = 0x2000000 \<comment> \<open>@{text UNKNOWN_FAULT}\<close>
+      then do
+        esr \<leftarrow> do_machine_op getESR;
+        handle_fault thread (UserException (esr && mask 32) 0)
+      od
+      else handle_fault thread (ArchFault $ VCPUFault (ucast hsr)))"
 
 end
 end

spec/abstract/AARCH64/Init_A.thy

@@ -52,7 +52,8 @@ definition init_arch_state :: arch_state where
      arm_next_vmid = 0,
      arm_us_global_vspace = arm_global_pt_ptr,
      arm_current_vcpu = None,
-     arm_gicvcpu_numlistregs = undefined
+     arm_gicvcpu_numlistregs = undefined,
+     arm_current_fpu_owner = None
    \<rparr>"
 
 
@@ -79,6 +80,7 @@ definition init_kheap :: kheap where
          tcb_fault = None,
          tcb_bound_notification = None,
          tcb_mcpriority = minBound,
+         tcb_flags = {},
          tcb_arch = init_arch_tcb
          \<rparr>,
      arm_global_pt_ptr \<mapsto> ArchObj global_pt_obj

spec/abstract/ARM/ArchTcb_A.thy

@@ -34,5 +34,11 @@ definition
 where
   "arch_post_modify_registers cur t \<equiv> return ()"
 
+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
+  "arch_prepare_set_domain t new_dom \<equiv> return ()"
+
 end
 end

spec/abstract/ARM/Arch_A.thy

@@ -45,6 +45,9 @@ definition
      set_vm_root thread
    od"
 
+definition arch_prepare_next_domain :: "(unit,'z::state_ext) s_monad" where
+  "arch_prepare_next_domain \<equiv> return ()"
+
 definition
   arch_activate_idle_thread :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
   "arch_activate_idle_thread t \<equiv> return ()"

spec/abstract/ARM/Arch_Structs_A.thy

@@ -282,6 +282,11 @@ qualify ARM_A (in Arch)
 record arch_tcb =
  tcb_context       :: user_context
 
+type_synonym arch_tcb_flag = unit
+
+definition word_from_arch_tcb_flag :: "arch_tcb_flag \<Rightarrow> machine_word" where
+  "word_from_arch_tcb_flag flag \<equiv> undefined"
+
 end_qualify
 
 context Arch begin arch_global_naming (A)

spec/abstract/ARM/Init_A.thy

@@ -74,6 +74,7 @@ definition
     tcb_fault = None,
     tcb_bound_notification = None,
     tcb_mcpriority = minBound,
+    tcb_flags = {},
     tcb_arch = init_arch_tcb
   \<rparr>,
   init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), \<comment> \<open>same reason as why we kept the definition of @{term init_globals_frame}\<close>

spec/abstract/ARM_HYP/ArchTcb_A.thy

@@ -41,5 +41,11 @@ definition
 where
   "arch_post_modify_registers cur t \<equiv> return ()"
 
+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
+  "arch_prepare_set_domain t new_dom \<equiv> return ()"
+
 end
 end

spec/abstract/ARM_HYP/Arch_A.thy

@@ -46,6 +46,9 @@ definition
      set_vm_root t
    od"
 
+definition arch_prepare_next_domain :: "(unit,'z::state_ext) s_monad" where
+  "arch_prepare_next_domain \<equiv> return ()"
+
 definition
   arch_activate_idle_thread :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
   "arch_activate_idle_thread t \<equiv> return ()"

spec/abstract/ARM_HYP/Arch_Structs_A.thy

@@ -338,6 +338,11 @@ record arch_state =
   arm_kernel_vspace :: ARM_HYP_A.arm_vspace_region_uses
   arm_us_global_pd  :: obj_ref
 
+type_synonym arch_tcb_flag = unit
+
+definition word_from_arch_tcb_flag :: "arch_tcb_flag \<Rightarrow> machine_word" where
+  "word_from_arch_tcb_flag flag \<equiv> undefined"
+
 end_qualify
 
 context Arch begin arch_global_naming (A)

spec/abstract/ARM_HYP/Init_A.thy

@@ -76,6 +76,7 @@ definition
     tcb_fault = None,
     tcb_bound_notification = None,
     tcb_mcpriority = minBound,
+    tcb_flags = {},
     tcb_arch = init_arch_tcb
   \<rparr>,
   us_global_pd_ptr \<mapsto> us_global_pd)"

spec/abstract/Decode_A.thy

@@ -380,6 +380,14 @@ where
      returnOk (SetTLSBase (obj_ref_of cap) (ucast (args ! 0)))
    odE"
 
+definition
+  decode_set_flags :: "data list \<Rightarrow> cap \<Rightarrow> (tcb_invocation,'z::state_ext) se_monad"
+where
+  "decode_set_flags args cap \<equiv> doE
+     whenE (length args < 2) $ throwError TruncatedMessage;
+     returnOk (SetFlags (obj_ref_of cap) (word_to_tcb_flags (args ! 0)) (word_to_tcb_flags (args ! 1)))
+   odE"
+
 definition
   decode_tcb_invocation ::
   "data \<Rightarrow> data list \<Rightarrow> cap \<Rightarrow> cslot_ptr \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow>
@@ -401,6 +409,7 @@ where
     | TCBBindNotification \<Rightarrow> decode_bind_notification cap excs
     | TCBUnbindNotification \<Rightarrow> decode_unbind_notification cap
     | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args cap
+    | TCBSetFlags \<Rightarrow> decode_set_flags args cap
     | _ \<Rightarrow> throwError IllegalOperation"
 
 definition

spec/abstract/Invocations_A.thy

@@ -48,6 +48,7 @@ datatype tcb_invocation =
   | Resume "obj_ref"
   | NotificationControl "obj_ref" "obj_ref option"
   | SetTLSBase obj_ref machine_word
+  | SetFlags obj_ref tcb_flags tcb_flags
 
 datatype irq_control_invocation =
     IRQControl irq cslot_ptr cslot_ptr

spec/abstract/KHeap_A.thy

@@ -132,7 +132,10 @@ definition
 
 definition
   set_mcpriority :: "obj_ref \<Rightarrow> priority \<Rightarrow> (unit, 'z::state_ext) s_monad"  where
-  "set_mcpriority ref mcp \<equiv> thread_set (\<lambda>tcb. tcb\<lparr>tcb_mcpriority:=mcp\<rparr>) ref "
+  "set_mcpriority ref mcp \<equiv> thread_set (\<lambda>tcb. tcb\<lparr>tcb_mcpriority:=mcp\<rparr>) ref"
+
+definition set_flags :: "obj_ref \<Rightarrow> tcb_flags \<Rightarrow> (unit, 'z::state_ext) s_monad" where
+  "set_flags ref flags \<equiv> thread_set (\<lambda>tcb. tcb\<lparr>tcb_flags:=flags\<rparr>) ref"
 
 
 section "simple kernel objects"

spec/abstract/RISCV64/ArchTcb_A.thy

@@ -24,5 +24,11 @@ definition arch_post_modify_registers :: "obj_ref \<Rightarrow> obj_ref \<Righta
   where
   "arch_post_modify_registers cur t \<equiv> return ()"
 
+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
+  "arch_prepare_set_domain t new_dom \<equiv> return ()"
+
 end
 end

spec/abstract/RISCV64/Arch_A.thy

@@ -36,6 +36,9 @@ definition arch_switch_to_idle_thread :: "(unit,'z::state_ext) s_monad"
     set_vm_root thread
   od"
 
+definition arch_prepare_next_domain :: "(unit,'z::state_ext) s_monad" where
+  "arch_prepare_next_domain \<equiv> return ()"
+
 definition arch_activate_idle_thread :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad"
   where
   "arch_activate_idle_thread t \<equiv> return ()"

spec/abstract/RISCV64/Arch_Structs_A.thy

@@ -274,6 +274,11 @@ text \<open> Arch-specific part of a TCB: this must have at least a field for us
 record arch_tcb =
   tcb_context :: user_context
 
+type_synonym arch_tcb_flag = unit
+
+definition word_from_arch_tcb_flag :: "arch_tcb_flag \<Rightarrow> machine_word" where
+  "word_from_arch_tcb_flag flag \<equiv> undefined"
+
 end_qualify
 
 context Arch begin arch_global_naming (A)

spec/abstract/RISCV64/Init_A.thy

@@ -111,6 +111,7 @@ definition init_kheap :: kheap
          tcb_fault = None,
          tcb_bound_notification = None,
          tcb_mcpriority = minBound,
+         tcb_flags = {},
          tcb_arch = init_arch_tcb
          \<rparr>,
       riscv_global_pt_ptr \<mapsto> init_global_pt