aarch64 abstract+machine: update abstract to use semi-lazy FPU switching

This includes extending the machine interface with new ops, adding the current
owner of the FPU state to the kernel state, and adding the new
seL4_TCB_Set_Flags syscall and related functions.

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

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 a case instead of the if (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);
+     when (cur_fpu_owner \<noteq> None) $ save_fpu_state (the cur_fpu_owner);
+     if (new_owner \<noteq> None)
+     then load_fpu_state (the new_owner)
+     else do_machine_op disableFpu;
+     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/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/Schedule_A.thy

@@ -17,6 +17,7 @@ begin
 arch_requalify_consts (A)
   arch_switch_to_thread
   arch_switch_to_idle_thread
+  arch_prepare_next_domain
 
 abbreviation
   "idle st \<equiv> st = Structures_A.IdleThreadState"
@@ -34,10 +35,7 @@ where
 text \<open>Gets all schedulable threads in the system.\<close>
 definition
   allActiveTCBs :: "(obj_ref set,'z::state_ext) s_monad" where
-  "allActiveTCBs \<equiv> do
-    state \<leftarrow> get;
-    return {x. getActiveTCB x state \<noteq> None}
-   od"
+  "allActiveTCBs \<equiv> gets (\<lambda>state. {x. getActiveTCB x state \<noteq> None})"
 
 text \<open>Switches the current thread to the specified one.\<close>
 definition
@@ -100,7 +98,10 @@ definition
 definition
   "schedule_choose_new_thread \<equiv> do
      dom_time \<leftarrow> gets domain_time;
-     when (dom_time = 0) next_domain;
+     when (dom_time = 0) $ do
+       arch_prepare_next_domain;
+       next_domain
+     od;
      choose_thread;
      set_scheduler_action resume_cur_thread
    od"
@@ -166,37 +167,42 @@ end
 instantiation unit :: state_ext_sched
 begin
 
-
+\<comment> \<open>FIXME: update this comment to mention the state that might be
+  saved as part of arch_prepare_next_domain\<close>
 text \<open>
   The scheduler is heavily underspecified.
   It is allowed to pick any active thread or the idle thread.
-  If the thread the scheduler picked is the current thread, it
-  may omit the call to @{const switch_to_thread}. Likewise it
-  may omit the call to @{const switch_to_idle_thread} if the
-  idle thread is the current thread.
-\<close>
+  If the current thread is active or is already the idle thread
+  then it may omit the call to @{const switch_to_thread} or
+  @{const switch_to_idle_thread} and do nothing.\<close>
+
+definition pre_choose_thread_unit :: "(unit,unit) s_monad" where
+  "pre_choose_thread_unit \<equiv> return () \<sqinter> arch_prepare_next_domain"
+
+definition choose_thread_unit :: "(unit,unit) s_monad" where
+  "choose_thread_unit \<equiv> (do
+     threads \<leftarrow> allActiveTCBs;
+     thread \<leftarrow> select threads;
+     switch_to_thread thread
+   od) \<sqinter>
+   switch_to_idle_thread"
+
 definition schedule_unit :: "(unit,unit) s_monad" where
-"schedule_unit \<equiv> (do
-   cur \<leftarrow> gets cur_thread;
-   threads \<leftarrow> allActiveTCBs;
-   thread \<leftarrow> select threads;
-   (if thread = cur then
-     return () \<sqinter> switch_to_thread thread
-   else
-     switch_to_thread thread)
- od) \<sqinter>
- (do
-   cur \<leftarrow> gets cur_thread;
-   idl \<leftarrow> gets idle_thread;
-   if idl = cur then
-     return () \<sqinter> switch_to_idle_thread
-   else switch_to_idle_thread
-  od)"
+  "schedule \<equiv> (do
+     cur \<leftarrow> gets cur_thread;
+     cur_active \<leftarrow> gets (getActiveTCB cur);
+     idl \<leftarrow> gets idle_thread;
+     if cur_active \<noteq> None \<or> idl = cur then
+       return () \<sqinter> (do pre_choose_thread_unit; choose_thread_unit od)
+     else
+       (do pre_choose_thread_unit; choose_thread_unit od)
+   od)"
 
 instance ..
 end
 
 
 lemmas schedule_def = schedule_det_ext_ext_def schedule_unit_def
+lemmas schedule_def_all = schedule_def pre_choose_thread_unit_def choose_thread_unit_def allActiveTCBs_def
 
 end

spec/abstract/Structures_A.thy

@@ -23,6 +23,7 @@ arch_requalify_types (A)
   arch_kernel_obj
   arch_state
   arch_tcb
+  arch_tcb_flag
   aa_type
 
 arch_requalify_consts (A)
@@ -46,6 +47,7 @@ arch_requalify_consts (A)
   untyped_min_bits
   untyped_max_bits
   msg_label_bits
+  word_from_arch_tcb_flag
 
 text \<open>
   User mode can request these objects to be created by retype:
@@ -367,6 +369,19 @@ datatype thread_state
 
 type_synonym priority = word8
 
+datatype tcb_flag
+  = ArchFlag arch_tcb_flag
+
+definition word_from_tcb_flag :: "tcb_flag \<Rightarrow> machine_word" where
+  "word_from_tcb_flag flag \<equiv>
+     case flag of
+       ArchFlag arch_flag \<Rightarrow> word_from_arch_tcb_flag arch_flag"
+
+type_synonym tcb_flags = "tcb_flag set"
+
+definition word_to_tcb_flags :: "machine_word \<Rightarrow> tcb_flags" where
+  "word_to_tcb_flags w \<equiv> {flag. word_from_tcb_flag flag && w \<noteq> 0}"
+
 record tcb =
  tcb_ctable        :: cap
  tcb_vtable        :: cap
@@ -379,6 +394,7 @@ record tcb =
  tcb_fault         :: "fault option"
  tcb_bound_notification     :: "obj_ref option"
  tcb_mcpriority    :: priority
+ tcb_flags         :: tcb_flags
  tcb_arch          :: arch_tcb (* arch_tcb must have a field for user context *)
 
 
@@ -410,6 +426,7 @@ definition
       tcb_fault      = None,
       tcb_bound_notification  = None,
       tcb_mcpriority = minBound,
+      tcb_flags      = {},
       tcb_arch       = default_arch_tcb\<rparr>"
 
 text \<open>