diff --git a/spec/abstract/AARCH64/ArchTcb_A.thy b/spec/abstract/AARCH64/ArchTcb_A.thy index ad486ad50f..8a5d36e05d 100644 --- a/spec/abstract/AARCH64/ArchTcb_A.thy +++ b/spec/abstract/AARCH64/ArchTcb_A.thy @@ -7,7 +7,7 @@ chapter \Architecture-specific TCB functions\ 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 \ (bool, 'a:: definition arch_post_modify_registers :: "obj_ref \ obj_ref \ (unit, 'a::state_ext) s_monad" where "arch_post_modify_registers cur t \ return ()" +\ \The corresponding C code is not arch dependent and so is inline as part of invokeSetFlags\ +definition arch_post_set_flags :: "obj_ref \ tcb_flags \ (unit, 'a::state_ext) s_monad" where + "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 + "arch_prepare_set_domain t new_dom \ do + cur_domain \ gets cur_domain; + when (cur_domain \ new_dom) $ fpu_release t + od" + end end diff --git a/spec/abstract/AARCH64/ArchVSpace_A.thy b/spec/abstract/AARCH64/ArchVSpace_A.thy index 962540c8ec..ff31e855cb 100644 --- a/spec/abstract/AARCH64/ArchVSpace_A.thy +++ b/spec/abstract/AARCH64/ArchVSpace_A.thy @@ -395,12 +395,9 @@ definition in_user_frame :: "obj_ref \ 'z::state_ext state \ \sz. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz))" -definition fpu_thread_delete :: "obj_ref \ (unit, 'z::state_ext) s_monad" where - "fpu_thread_delete thread_ptr \ do_machine_op (fpuThreadDeleteOp thread_ptr)" - definition prepare_thread_delete :: "obj_ref \ (unit,'z::state_ext) s_monad" where "prepare_thread_delete thread_ptr \ do - fpu_thread_delete thread_ptr; + fpu_release thread_ptr; t_vcpu \ arch_thread_get tcb_vcpu thread_ptr; case t_vcpu of Some v \ dissociate_vcpu_tcb v thread_ptr diff --git a/spec/abstract/AARCH64/Arch_A.thy b/spec/abstract/AARCH64/Arch_A.thy index 462642c0a4..b807ba1358 100644 --- a/spec/abstract/AARCH64/Arch_A.thy +++ b/spec/abstract/AARCH64/Arch_A.thy @@ -25,7 +25,8 @@ definition arch_switch_to_thread :: "obj_ref \ (unit,'z::state_ext) "arch_switch_to_thread t \ do tcb \ 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 \ switch_local_fpu_owner None" + definition arch_activate_idle_thread :: "obj_ref \ (unit,'z::state_ext) s_monad" where "arch_activate_idle_thread t \ return ()" diff --git a/spec/abstract/AARCH64/Arch_Structs_A.thy b/spec/abstract/AARCH64/Arch_Structs_A.thy index 753e95142e..2098fc1cf0 100644 --- a/spec/abstract/AARCH64/Arch_Structs_A.thy +++ b/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 \ 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 \ machine_word" where + "word_from_arch_tcb_flag flag \ + case flag of + FpuDisabled \ bit 0" + end_qualify context Arch begin arch_global_naming (A) diff --git a/spec/abstract/AARCH64/FPU_A.thy b/spec/abstract/AARCH64/FPU_A.thy new file mode 100644 index 0000000000..9d6fd6cffc --- /dev/null +++ b/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 \ (unit,'z::state_ext) s_monad" where + "save_fpu_state t \ do + fpu_state \ do_machine_op readFpuState; + as_user t (setFPUState fpu_state) + od" + +definition load_fpu_state :: "obj_ref \ (unit,'z::state_ext) s_monad" where + "load_fpu_state t \ do + fpu_state \ as_user t getFPUState; + do_machine_op (writeFpuState fpu_state) + od" + +\ \FIXME: maybe use an if instead of the case (depends on if wpc or if\_split is easier)\ +definition switch_local_fpu_owner :: "obj_ref option \ (unit,'z::state_ext) s_monad" where + "switch_local_fpu_owner new_owner \ do + do_machine_op enableFpu; + cur_fpu_owner \ gets (arm_current_fpu_owner \ arch_state); + maybeM save_fpu_state cur_fpu_owner; + case new_owner of + None \ do_machine_op disableFpu + | Some tcb_ptr \ load_fpu_state tcb_ptr; + modify (\s. s \arch_state := arch_state s\arm_current_fpu_owner := new_owner\\) + od" + +definition fpu_release :: "obj_ref \ (unit,'z::state_ext) s_monad" where + "fpu_release thread_ptr \ do + cur_fpu_owner \ gets (arm_current_fpu_owner \ arch_state); + when (cur_fpu_owner = Some thread_ptr) $ switch_local_fpu_owner None + od" + +definition lazy_fpu_restore :: "obj_ref \ (unit,'z::state_ext) s_monad" where + "lazy_fpu_restore thread_ptr \ do + flags \ thread_get tcb_flags thread_ptr; + if ArchFlag FpuDisabled \ flags + then do_machine_op disableFpu + else do + do_machine_op enableFpu; + switch_local_fpu_owner (Some thread_ptr) + od + od" + +end + +end \ No newline at end of file diff --git a/spec/abstract/AARCH64/Hypervisor_A.thy b/spec/abstract/AARCH64/Hypervisor_A.thy index b396cf8d64..46d5aa207b 100644 --- a/spec/abstract/AARCH64/Hypervisor_A.thy +++ b/spec/abstract/AARCH64/Hypervisor_A.thy @@ -14,17 +14,13 @@ context Arch begin arch_global_naming (A) fun handle_hypervisor_fault :: "machine_word \ hyp_fault_type \ (unit, 'z::state_ext) s_monad" where - "handle_hypervisor_fault thread (ARMVCPUFault hsr) = do - fpu_enabled \ do_machine_op isFpuEnable; - if \fpu_enabled - then fail - else if hsr = 0x2000000 \ \@{text UNKNOWN_FAULT}\ - then do - esr \ 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 \ \@{text UNKNOWN_FAULT}\ + then do + esr \ do_machine_op getESR; + handle_fault thread (UserException (esr && mask 32) 0) + od + else handle_fault thread (ArchFault $ VCPUFault (ucast hsr)))" end end diff --git a/spec/abstract/AARCH64/Init_A.thy b/spec/abstract/AARCH64/Init_A.thy index 9182f606e2..5cb9c5ea4e 100644 --- a/spec/abstract/AARCH64/Init_A.thy +++ b/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 \" @@ -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 \, arm_global_pt_ptr \ ArchObj global_pt_obj diff --git a/spec/abstract/ARM/ArchTcb_A.thy b/spec/abstract/ARM/ArchTcb_A.thy index 27c9bc67a1..85e70cfdb0 100644 --- a/spec/abstract/ARM/ArchTcb_A.thy +++ b/spec/abstract/ARM/ArchTcb_A.thy @@ -34,5 +34,11 @@ definition where "arch_post_modify_registers cur t \ return ()" +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 + "arch_prepare_set_domain t new_dom \ return ()" + end end diff --git a/spec/abstract/ARM/Arch_A.thy b/spec/abstract/ARM/Arch_A.thy index 4f55fb3795..8ea29c5ed5 100644 --- a/spec/abstract/ARM/Arch_A.thy +++ b/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 \ return ()" + definition arch_activate_idle_thread :: "obj_ref \ (unit,'z::state_ext) s_monad" where "arch_activate_idle_thread t \ return ()" diff --git a/spec/abstract/ARM/Arch_Structs_A.thy b/spec/abstract/ARM/Arch_Structs_A.thy index 5c2a766816..9f466cf52e 100644 --- a/spec/abstract/ARM/Arch_Structs_A.thy +++ b/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 \ machine_word" where + "word_from_arch_tcb_flag flag \ undefined" + end_qualify context Arch begin arch_global_naming (A) diff --git a/spec/abstract/ARM/Init_A.thy b/spec/abstract/ARM/Init_A.thy index 2872ed1276..89836bc135 100644 --- a/spec/abstract/ARM/Init_A.thy +++ b/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 \, init_globals_frame \ ArchObj (DataPage False ARMSmallPage), \ \same reason as why we kept the definition of @{term init_globals_frame}\ diff --git a/spec/abstract/ARM_HYP/ArchTcb_A.thy b/spec/abstract/ARM_HYP/ArchTcb_A.thy index e5da56d323..e6bc391439 100644 --- a/spec/abstract/ARM_HYP/ArchTcb_A.thy +++ b/spec/abstract/ARM_HYP/ArchTcb_A.thy @@ -41,5 +41,11 @@ definition where "arch_post_modify_registers cur t \ return ()" +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 + "arch_prepare_set_domain t new_dom \ return ()" + end end diff --git a/spec/abstract/ARM_HYP/Arch_A.thy b/spec/abstract/ARM_HYP/Arch_A.thy index 15beb775a1..cc87d0bc0e 100644 --- a/spec/abstract/ARM_HYP/Arch_A.thy +++ b/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 \ return ()" + definition arch_activate_idle_thread :: "obj_ref \ (unit,'z::state_ext) s_monad" where "arch_activate_idle_thread t \ return ()" diff --git a/spec/abstract/ARM_HYP/Arch_Structs_A.thy b/spec/abstract/ARM_HYP/Arch_Structs_A.thy index ba98106cc1..9db213ab9c 100644 --- a/spec/abstract/ARM_HYP/Arch_Structs_A.thy +++ b/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 \ machine_word" where + "word_from_arch_tcb_flag flag \ undefined" + end_qualify context Arch begin arch_global_naming (A) diff --git a/spec/abstract/ARM_HYP/Init_A.thy b/spec/abstract/ARM_HYP/Init_A.thy index e87c2dd6cd..a7746a7e23 100644 --- a/spec/abstract/ARM_HYP/Init_A.thy +++ b/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 \, us_global_pd_ptr \ us_global_pd)" diff --git a/spec/abstract/Decode_A.thy b/spec/abstract/Decode_A.thy index abe85ced52..69846bfc56 100644 --- a/spec/abstract/Decode_A.thy +++ b/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 \ cap \ (tcb_invocation,'z::state_ext) se_monad" +where + "decode_set_flags args cap \ 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 \ data list \ cap \ cslot_ptr \ (cap \ cslot_ptr) list \ @@ -401,6 +409,7 @@ where | TCBBindNotification \ decode_bind_notification cap excs | TCBUnbindNotification \ decode_unbind_notification cap | TCBSetTLSBase \ decode_set_tls_base args cap + | TCBSetFlags \ decode_set_flags args cap | _ \ throwError IllegalOperation" definition diff --git a/spec/abstract/Invocations_A.thy b/spec/abstract/Invocations_A.thy index c8026c6755..4bb34913f4 100644 --- a/spec/abstract/Invocations_A.thy +++ b/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 diff --git a/spec/abstract/KHeap_A.thy b/spec/abstract/KHeap_A.thy index 3d9a4542e1..c5ca951609 100644 --- a/spec/abstract/KHeap_A.thy +++ b/spec/abstract/KHeap_A.thy @@ -132,7 +132,10 @@ definition definition set_mcpriority :: "obj_ref \ priority \ (unit, 'z::state_ext) s_monad" where - "set_mcpriority ref mcp \ thread_set (\tcb. tcb\tcb_mcpriority:=mcp\) ref " + "set_mcpriority ref mcp \ thread_set (\tcb. tcb\tcb_mcpriority:=mcp\) ref" + +definition set_flags :: "obj_ref \ tcb_flags \ (unit, 'z::state_ext) s_monad" where + "set_flags ref flags \ thread_set (\tcb. tcb\tcb_flags:=flags\) ref" section "simple kernel objects" diff --git a/spec/abstract/RISCV64/ArchTcb_A.thy b/spec/abstract/RISCV64/ArchTcb_A.thy index 4e071341a9..e93fcb1b27 100644 --- a/spec/abstract/RISCV64/ArchTcb_A.thy +++ b/spec/abstract/RISCV64/ArchTcb_A.thy @@ -24,5 +24,11 @@ definition arch_post_modify_registers :: "obj_ref \ obj_ref \ return ()" +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 + "arch_prepare_set_domain t new_dom \ return ()" + end end diff --git a/spec/abstract/RISCV64/Arch_A.thy b/spec/abstract/RISCV64/Arch_A.thy index 818e3a7cf9..29168b7931 100644 --- a/spec/abstract/RISCV64/Arch_A.thy +++ b/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 \ return ()" + definition arch_activate_idle_thread :: "obj_ref \ (unit,'z::state_ext) s_monad" where "arch_activate_idle_thread t \ return ()" diff --git a/spec/abstract/RISCV64/Arch_Structs_A.thy b/spec/abstract/RISCV64/Arch_Structs_A.thy index 8844ee0576..161777bd8e 100644 --- a/spec/abstract/RISCV64/Arch_Structs_A.thy +++ b/spec/abstract/RISCV64/Arch_Structs_A.thy @@ -274,6 +274,11 @@ text \ 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 \ machine_word" where + "word_from_arch_tcb_flag flag \ undefined" + end_qualify context Arch begin arch_global_naming (A) diff --git a/spec/abstract/RISCV64/Init_A.thy b/spec/abstract/RISCV64/Init_A.thy index 42bb63a180..03eb6d0196 100644 --- a/spec/abstract/RISCV64/Init_A.thy +++ b/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 \, riscv_global_pt_ptr \ init_global_pt diff --git a/spec/abstract/Schedule_A.thy b/spec/abstract/Schedule_A.thy index a541a1dc88..699733490d 100644 --- a/spec/abstract/Schedule_A.thy +++ b/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 \ st = Structures_A.IdleThreadState" @@ -34,10 +35,7 @@ where text \Gets all schedulable threads in the system.\ definition allActiveTCBs :: "(obj_ref set,'z::state_ext) s_monad" where - "allActiveTCBs \ do - state \ get; - return {x. getActiveTCB x state \ None} - od" + "allActiveTCBs \ gets (\state. {x. getActiveTCB x state \ None})" text \Switches the current thread to the specified one.\ definition @@ -100,7 +98,10 @@ definition definition "schedule_choose_new_thread \ do dom_time \ 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 - +\ \FIXME: update this comment to mention the state that might be + saved as part of @{term arch_prepare_next_domain}\ text \ 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. -\ + 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.\ + +definition pre_choose_thread_unit :: "(unit,unit) s_monad" where + "pre_choose_thread_unit \ return () \ arch_prepare_next_domain" + +definition choose_thread_unit :: "(unit,unit) s_monad" where + "choose_thread_unit \ (do + threads \ allActiveTCBs; + thread \ select threads; + switch_to_thread thread + od) \ + switch_to_idle_thread" + definition schedule_unit :: "(unit,unit) s_monad" where -"schedule_unit \ (do - cur \ gets cur_thread; - threads \ allActiveTCBs; - thread \ select threads; - (if thread = cur then - return () \ switch_to_thread thread - else - switch_to_thread thread) - od) \ - (do - cur \ gets cur_thread; - idl \ gets idle_thread; - if idl = cur then - return () \ switch_to_idle_thread - else switch_to_idle_thread - od)" + "schedule \ (do + cur \ gets cur_thread; + cur_active \ gets (getActiveTCB cur); + idl \ gets idle_thread; + if cur_active \ None \ idl = cur then + return () \ 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 diff --git a/spec/abstract/Structures_A.thy b/spec/abstract/Structures_A.thy index b8c7a568ca..fdacc9ce84 100644 --- a/spec/abstract/Structures_A.thy +++ b/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 \ 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 \ machine_word" where + "word_from_tcb_flag flag \ + case flag of + ArchFlag arch_flag \ word_from_arch_tcb_flag arch_flag" + +type_synonym tcb_flags = "tcb_flag set" + +definition word_to_tcb_flags :: "machine_word \ tcb_flags" where + "word_to_tcb_flags w \ {flag. word_from_tcb_flag flag && w \ 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\" text \ diff --git a/spec/abstract/Tcb_A.thy b/spec/abstract/Tcb_A.thy index 89fe35d96a..645277fab0 100644 --- a/spec/abstract/Tcb_A.thy +++ b/spec/abstract/Tcb_A.thy @@ -19,6 +19,8 @@ arch_requalify_consts (A) sanitise_register arch_get_sanitise_register_info arch_post_modify_registers + arch_post_set_flags + arch_prepare_set_domain section "Activating Threads" @@ -251,6 +253,15 @@ where return [] od)" +| "invoke_tcb (SetFlags tcb clearFlags setFlags) = + (liftE $ do + flags \ thread_get tcb_flags tcb; + new_flags \ return $ flags - clearFlags \ setFlags; + set_flags tcb new_flags; + arch_post_set_flags tcb new_flags; + return [] + od)" + definition set_domain :: "obj_ref \ domain \ unit det_ext_monad" where "set_domain tptr new_dom \ do @@ -262,10 +273,15 @@ definition when (tptr = cur) reschedule_required od" -definition invoke_domain:: "obj_ref \ domain \ (data list,'z::state_ext) p_monad" -where + \ \FIXME: @{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 "invoke_domain thread domain \ - liftE (do do_extended_op (set_domain thread domain); return [] od)" + liftE $ do + do_extended_op (arch_prepare_set_domain thread domain); + do_extended_op (set_domain thread domain); + return [] + od" text \Get all of the message registers, both from the sending thread's current register file and its IPC buffer.\ diff --git a/spec/abstract/X64/ArchTcb_A.thy b/spec/abstract/X64/ArchTcb_A.thy index 56d8c16a8b..fb13896680 100644 --- a/spec/abstract/X64/ArchTcb_A.thy +++ b/spec/abstract/X64/ArchTcb_A.thy @@ -11,7 +11,7 @@ Arch-specific functions for the abstract model of CSpace. chapter "Architecture-specific TCB functions" theory ArchTcb_A -imports KHeap_A +imports FPU_A begin context Arch begin arch_global_naming (A) @@ -46,5 +46,16 @@ definition where "arch_post_modify_registers cur t \ when (t \ cur) $ as_user t $ setRegister ErrorRegister 0" +\ \The corresponding C code is not arch dependent and so is inline as part of invokeSetFlags\ +definition arch_post_set_flags :: "obj_ref \ tcb_flags \ (unit, 'a::state_ext) s_monad" where + "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 + "arch_prepare_set_domain t new_dom \ do + cur_domain \ gets cur_domain; + when (cur_domain \ new_dom) $ fpu_release t + od" + end end diff --git a/spec/abstract/X64/ArchVSpace_A.thy b/spec/abstract/X64/ArchVSpace_A.thy index 78c3df1fd0..464d707236 100644 --- a/spec/abstract/X64/ArchVSpace_A.thy +++ b/spec/abstract/X64/ArchVSpace_A.thy @@ -11,7 +11,9 @@ Higher level functions for manipulating virtual address spaces chapter "x64 VSpace Functions" theory ArchVSpace_A -imports Retype_A +imports + Retype_A + FPU_A begin context Arch begin arch_global_naming (A) @@ -474,18 +476,10 @@ definition \sz. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz))" -definition - fpu_thread_delete :: "obj_ref \ (unit, 'z::state_ext) s_monad" -where - "fpu_thread_delete thread_ptr \ do - using_fpu \ do_machine_op (nativeThreadUsingFPU thread_ptr); - when using_fpu $ do_machine_op (switchFpuOwner 0 0) - od" - definition prepare_thread_delete :: "obj_ref \ (unit,'z::state_ext) s_monad" where - "prepare_thread_delete thread_ptr \ fpu_thread_delete thread_ptr" + "prepare_thread_delete thread_ptr \ fpu_release thread_ptr" text \Make numeric value of @{const msg_align_bits} visible.\ lemmas msg_align_bits = msg_align_bits'[unfolded word_size_bits_def, simplified] diff --git a/spec/abstract/X64/Arch_A.thy b/spec/abstract/X64/Arch_A.thy index a835552d65..afc7f75170 100644 --- a/spec/abstract/X64/Arch_A.thy +++ b/spec/abstract/X64/Arch_A.thy @@ -47,7 +47,10 @@ text \Switch to a thread's virtual address space context.\ definition arch_switch_to_thread :: "obj_ref \ (unit,'z::state_ext) s_monad" where - "arch_switch_to_thread t \ set_vm_root t" + "arch_switch_to_thread t \ do + set_vm_root t; + lazy_fpu_restore t + od" definition arch_switch_to_idle_thread :: "(unit,'z::state_ext) s_monad" where @@ -56,6 +59,9 @@ definition set_vm_root thread od" +definition arch_prepare_next_domain :: "(unit,'z::state_ext) s_monad" where + "arch_prepare_next_domain \ switch_local_fpu_owner None" + definition arch_activate_idle_thread :: "obj_ref \ (unit,'z::state_ext) s_monad" where "arch_activate_idle_thread t \ return ()" diff --git a/spec/abstract/X64/Arch_Structs_A.thy b/spec/abstract/X64/Arch_Structs_A.thy index 2cb066cbf0..ff306c5554 100644 --- a/spec/abstract/X64/Arch_Structs_A.thy +++ b/spec/abstract/X64/Arch_Structs_A.thy @@ -312,6 +312,7 @@ record arch_state = x64_num_ioapics :: "64 word" x64_ioapic_nirqs :: "machine_word \ 8 word" x64_irq_state :: "8 word \ X64_A.X64IRQState" + x64_current_fpu_owner :: "obj_ref option" (* FIXME x64-vtd: x64_num_io_domain_bits :: "16 word" @@ -409,6 +410,14 @@ text \ Arch-specific part of a TCB: this must have at least a field for us record arch_tcb = tcb_context :: user_context +datatype arch_tcb_flag + = FpuDisabled + +definition word_from_arch_tcb_flag :: "arch_tcb_flag \ machine_word" where + "word_from_arch_tcb_flag flag \ + case flag of + FpuDisabled \ bit 0" + end_qualify context Arch begin arch_global_naming (A) diff --git a/spec/abstract/X64/FPU_A.thy b/spec/abstract/X64/FPU_A.thy new file mode 100644 index 0000000000..0890c68f8a --- /dev/null +++ b/spec/abstract/X64/FPU_A.thy @@ -0,0 +1,59 @@ +(* + * Copyright 2024, Proofcraft Pty Ltd + * + * SPDX-License-Identifier: GPL-2.0-only + *) + +chapter "X64 FPU Functions" + +theory FPU_A +imports + KHeap_A +begin + +context Arch begin arch_global_naming (A) + +definition save_fpu_state :: "obj_ref \ (unit,'z::state_ext) s_monad" where + "save_fpu_state t \ do + fpu_state \ do_machine_op readFpuState; + as_user t (setFPUState fpu_state) + od" + +definition load_fpu_state :: "obj_ref \ (unit,'z::state_ext) s_monad" where + "load_fpu_state t \ do + fpu_state \ as_user t getFPUState; + do_machine_op (writeFpuState fpu_state) + od" + +\ \FIXME: maybe use an if instead of the case (depends on if wpc or if\_split is easier)\ +definition switch_local_fpu_owner :: "obj_ref option \ (unit,'z::state_ext) s_monad" where + "switch_local_fpu_owner new_owner \ do + do_machine_op enableFpu; + cur_fpu_owner \ gets (x64_current_fpu_owner \ arch_state); + maybeM save_fpu_state cur_fpu_owner; + case new_owner of + None \ do_machine_op disableFpu + | Some tcb_ptr \ load_fpu_state tcb_ptr; + modify (\s. s \arch_state := arch_state s\x64_current_fpu_owner := new_owner\\) + od" + +definition fpu_release :: "obj_ref \ (unit,'z::state_ext) s_monad" where + "fpu_release thread_ptr \ do + cur_fpu_owner \ gets (x64_current_fpu_owner \ arch_state); + when (cur_fpu_owner = Some thread_ptr) $ switch_local_fpu_owner None + od" + +definition lazy_fpu_restore :: "obj_ref \ (unit,'z::state_ext) s_monad" where + "lazy_fpu_restore thread_ptr \ do + flags \ thread_get tcb_flags thread_ptr; + if ArchFlag FpuDisabled \ flags + then do_machine_op disableFpu + else do + do_machine_op enableFpu; + switch_local_fpu_owner (Some thread_ptr) + od + od" + +end + +end \ No newline at end of file diff --git a/spec/abstract/X64/Init_A.thy b/spec/abstract/X64/Init_A.thy index c0dd40f3a4..bb1dc38f97 100644 --- a/spec/abstract/X64/Init_A.thy +++ b/spec/abstract/X64/Init_A.thy @@ -57,7 +57,8 @@ definition x64_allocated_io_ports = \_. False, x64_num_ioapics = 1, x64_ioapic_nirqs = \_. ucast ioapicIRQLines, - x64_irq_state = K IRQFree + x64_irq_state = K IRQFree, + x64_current_fpu_owner = None \" definition [simp]: @@ -92,6 +93,7 @@ definition tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, + tcb_flags = {}, tcb_arch = init_arch_tcb \, init_global_pml4 \ ArchObj (PageMapL4 global_pml4), diff --git a/spec/design/m-skel/AARCH64/MachineTypes.thy b/spec/design/m-skel/AARCH64/MachineTypes.thy index 01858f1636..de45f5201c 100644 --- a/spec/design/m-skel/AARCH64/MachineTypes.thy +++ b/spec/design/m-skel/AARCH64/MachineTypes.thy @@ -26,7 +26,7 @@ text \ section "Types" -#INCLUDE_HASKELL SEL4/Machine/RegisterSet/AARCH64.hs CONTEXT AARCH64 decls_only NOT UserContext UserMonad Word getRegister setRegister newContext FPUState newFPUState +#INCLUDE_HASKELL SEL4/Machine/RegisterSet/AARCH64.hs CONTEXT AARCH64 decls_only NOT UserContext UserMonad Word getRegister setRegister getFPUState setFPUState newContext FPUState newFPUState #INCLUDE_HASKELL SEL4/Object/Structures/AARCH64.hs CONTEXT AARCH64 ONLY VPPIEventIRQ VirtTimer (*<*) @@ -40,7 +40,7 @@ context Arch begin arch_global_naming #INCLUDE_HASKELL SEL4/Machine/RegisterSet/AARCH64.hs CONTEXT AARCH64 instanceproofs #INCLUDE_HASKELL SEL4/Object/Structures/AARCH64.hs CONTEXT AARCH64 instanceproofs ONLY VPPIEventIRQ VirtTimer (*>*) -#INCLUDE_HASKELL SEL4/Machine/RegisterSet/AARCH64.hs CONTEXT AARCH64 bodies_only NOT getRegister setRegister newContext newFPUState +#INCLUDE_HASKELL SEL4/Machine/RegisterSet/AARCH64.hs CONTEXT AARCH64 bodies_only NOT getRegister setRegister getFPUState setFPUState newContext newFPUState section "Machine State" @@ -62,6 +62,7 @@ record irq_state :: nat underlying_memory :: "machine_word \ word8" device_state :: "machine_word \ word8 option" + fpu_enabled :: bool machine_state_rest :: AARCH64.machine_state_rest axiomatization @@ -109,6 +110,7 @@ definition irq_state = 0, underlying_memory = init_underlying_memory, device_state = Map.empty, + fpu_enabled = False, machine_state_rest = undefined \" #INCLUDE_HASKELL SEL4/Machine/Hardware/AARCH64.hs CONTEXT AARCH64 ONLY \ diff --git a/spec/design/m-skel/X64/MachineTypes.thy b/spec/design/m-skel/X64/MachineTypes.thy index 229318ad57..1f240b8067 100644 --- a/spec/design/m-skel/X64/MachineTypes.thy +++ b/spec/design/m-skel/X64/MachineTypes.thy @@ -24,7 +24,7 @@ text \ section "Types" -#INCLUDE_HASKELL SEL4/Machine/RegisterSet/X64.lhs CONTEXT X64 decls_only NOT UserContext UserMonad Word getRegister setRegister newContext +#INCLUDE_HASKELL SEL4/Machine/RegisterSet/X64.lhs CONTEXT X64 decls_only NOT UserContext UserMonad Word getRegister setRegister getFPUState setFPUState newContext (*<*) end @@ -35,7 +35,7 @@ context Arch begin arch_global_naming #INCLUDE_HASKELL SEL4/Machine/RegisterSet/X64.lhs CONTEXT X64 instanceproofs (*>*) -#INCLUDE_HASKELL SEL4/Machine/RegisterSet/X64.lhs CONTEXT X64 bodies_only NOT getRegister setRegister newContext +#INCLUDE_HASKELL SEL4/Machine/RegisterSet/X64.lhs CONTEXT X64 bodies_only NOT getRegister setRegister getFPUState setFPUState newContext section "Machine State" @@ -57,6 +57,7 @@ record irq_state :: nat underlying_memory :: "word64 \ word8" device_state :: "word64 \ word8 option" + fpu_enabled :: bool machine_state_rest :: X64.machine_state_rest consts irq_oracle :: "nat \ word8" @@ -101,6 +102,7 @@ definition irq_state = 0, underlying_memory = init_underlying_memory, device_state = Map.empty, + fpu_enabled = False, machine_state_rest = undefined \" #INCLUDE_HASKELL SEL4/Machine/Hardware/X64.lhs CONTEXT X64 ONLY VMFaultType HypFaultType VMPageSize VMMapType pageBits ptTranslationBits pageBitsForSize diff --git a/spec/design/skel/AARCH64/ArchTCB_H.thy b/spec/design/skel/AARCH64/ArchTCB_H.thy index 39085e3663..b18ea5c2c6 100644 --- a/spec/design/skel/AARCH64/ArchTCB_H.thy +++ b/spec/design/skel/AARCH64/ArchTCB_H.thy @@ -5,7 +5,9 @@ *) theory ArchTCB_H -imports TCBDecls_H +imports + TCBDecls_H + FPU_H begin context Arch begin arch_global_naming (H) diff --git a/spec/design/skel/AARCH64/ArchThread_H.thy b/spec/design/skel/AARCH64/ArchThread_H.thy index 3cb95f63f9..0450df8db6 100644 --- a/spec/design/skel/AARCH64/ArchThread_H.thy +++ b/spec/design/skel/AARCH64/ArchThread_H.thy @@ -13,6 +13,7 @@ imports TCBDecls_H ArchVSpaceDecls_H ArchHypervisor_H + FPU_H begin context Arch begin arch_global_naming (H) diff --git a/spec/design/skel/AARCH64/FPU_H.thy b/spec/design/skel/AARCH64/FPU_H.thy new file mode 100644 index 0000000000..a5fb57f6c5 --- /dev/null +++ b/spec/design/skel/AARCH64/FPU_H.thy @@ -0,0 +1,19 @@ +(* + * Copyright 2024, Proofcraft Pty Ltd + * + * SPDX-License-Identifier: GPL-2.0-only + *) + +chapter "FPU" + +theory FPU_H +imports + Hardware_H + TCBDecls_H +begin +context Arch begin arch_global_naming (H) + +#INCLUDE_HASKELL SEL4/Object/FPU/AARCH64.hs CONTEXT AARCH64_H ArchInv=Arch + +end +end diff --git a/spec/design/skel/AARCH64/Hardware_H.thy b/spec/design/skel/AARCH64/Hardware_H.thy index 9c1e2074f1..366f8ba550 100644 --- a/spec/design/skel/AARCH64/Hardware_H.thy +++ b/spec/design/skel/AARCH64/Hardware_H.thy @@ -23,7 +23,7 @@ context Arch begin arch_global_naming (H) pptrUserTop kernelELFBase kernelELFBaseOffset kernelELFPAddrBase \ addrFromKPPtr ptTranslationBits vmFaultTypeFSR setVSpaceRoot \ setIRQTrigger \ - config_ARM_PA_SIZE_BITS_40 fpuThreadDeleteOp isFpuEnable \ + config_ARM_PA_SIZE_BITS_40 readFpuState writeFpuState enableFpu disableFpu isFpuEnable \ hcrVCPU hcrNative sctlrDefault vgicHCREN gicVCPUMaxNumLR sctlrEL1VM \ get_gic_vcpu_ctrl_hcr set_gic_vcpu_ctrl_hcr get_gic_vcpu_ctrl_vmcr \ set_gic_vcpu_ctrl_vmcr get_gic_vcpu_ctrl_apr set_gic_vcpu_ctrl_apr \ diff --git a/spec/design/skel/Retype_H.thy b/spec/design/skel/Retype_H.thy index 6d325434e8..6ed9c02303 100644 --- a/spec/design/skel/Retype_H.thy +++ b/spec/design/skel/Retype_H.thy @@ -26,7 +26,7 @@ requalify_consts (aliasing) hasCancelSendRights sameRegionAs isPhysicalCap sameObjectAs updateCapData maskCapRights createObject capUntypedPtr capUntypedSize - performInvocation decodeInvocation prepareThreadDelete + performInvocation decodeInvocation prepareThreadDelete prepareSetDomain context begin global_naming global diff --git a/spec/design/skel/Structures_H.thy b/spec/design/skel/Structures_H.thy index 833ba5f48c..87a164b281 100644 --- a/spec/design/skel/Structures_H.thy +++ b/spec/design/skel/Structures_H.thy @@ -24,11 +24,13 @@ arch_requalify_types (H) arch_kernel_object asid arch_tcb + arch_tcb_flag arch_requalify_consts (H) archObjSize nullPointer newArchTCB + archTcbFlagToWord fromPPtr PPtr atcbContextGet diff --git a/spec/design/skel/TCB_H.thy b/spec/design/skel/TCB_H.thy index 5c9b070e1c..cb1473f135 100644 --- a/spec/design/skel/TCB_H.thy +++ b/spec/design/skel/TCB_H.thy @@ -22,6 +22,7 @@ arch_requalify_consts (H) msgRegisters fromVPtr postModifyRegisters + postSetFlags sanitiseRegister getSanitiseRegisterInfo diff --git a/spec/design/skel/Thread_H.thy b/spec/design/skel/Thread_H.thy index 7464c3c6aa..e78cda95c8 100644 --- a/spec/design/skel/Thread_H.thy +++ b/spec/design/skel/Thread_H.thy @@ -31,6 +31,7 @@ requalify_consts (aliasing) configureIdleThread switchToIdleThread switchToThread + prepareNextDomain context begin global_naming global diff --git a/spec/design/skel/X64/ArchRetype_H.thy b/spec/design/skel/X64/ArchRetype_H.thy index 87a0bbeca9..d4a7986757 100644 --- a/spec/design/skel/X64/ArchRetype_H.thy +++ b/spec/design/skel/X64/ArchRetype_H.thy @@ -12,6 +12,7 @@ imports ArchVSpaceDecls_H Hardware_H KI_Decls_H + FPU_H begin context Arch begin arch_global_naming (H) diff --git a/spec/design/skel/X64/ArchTCB_H.thy b/spec/design/skel/X64/ArchTCB_H.thy index c67b323a3e..30b460130b 100644 --- a/spec/design/skel/X64/ArchTCB_H.thy +++ b/spec/design/skel/X64/ArchTCB_H.thy @@ -5,7 +5,9 @@ *) theory ArchTCB_H -imports TCBDecls_H +imports + TCBDecls_H + FPU_H begin context Arch begin arch_global_naming (H) diff --git a/spec/design/skel/X64/ArchThread_H.thy b/spec/design/skel/X64/ArchThread_H.thy index abb68b88e8..ecd5b7dcc7 100644 --- a/spec/design/skel/X64/ArchThread_H.thy +++ b/spec/design/skel/X64/ArchThread_H.thy @@ -11,6 +11,7 @@ imports ArchThreadDecls_H TCBDecls_H ArchVSpaceDecls_H + FPU_H begin diff --git a/spec/design/skel/X64/FPU_H.thy b/spec/design/skel/X64/FPU_H.thy new file mode 100644 index 0000000000..8fb52027a5 --- /dev/null +++ b/spec/design/skel/X64/FPU_H.thy @@ -0,0 +1,19 @@ +(* + * Copyright 2024, Proofcraft Pty Ltd + * + * SPDX-License-Identifier: GPL-2.0-only + *) + +chapter "FPU" + +theory FPU_H +imports + Hardware_H + TCBDecls_H +begin +context Arch begin arch_global_naming (H) + +#INCLUDE_HASKELL SEL4/Object/FPU/X64.hs CONTEXT X64_H ArchInv=Arch + +end +end diff --git a/spec/design/skel/X64/Hardware_H.thy b/spec/design/skel/X64/Hardware_H.thy index 085eabdc3e..7c0d0001f9 100644 --- a/spec/design/skel/X64/Hardware_H.thy +++ b/spec/design/skel/X64/Hardware_H.thy @@ -12,7 +12,7 @@ begin context Arch begin arch_global_naming (H) -#INCLUDE_HASKELL SEL4/Machine/Hardware/X64.lhs Platform=Platform.X64 CONTEXT X64_H NOT getMemoryRegions getDeviceRegions getKernelDevices loadWord storeWord storeWordVM getActiveIRQ ackInterrupt maskInterrupt configureTimer resetTimer debugPrint getRestartPC setNextPC clearMemory clearMemoryVM initMemory freeMemory wordFromPDE wordFromPTE VMFaultType HypFaultType VMMapType VMPageSize pageBits pageBitsForSize paddrBase pptrBase pptrTop pptrBaseOffset kernelELFBaseOffset kernelELFPAddrBase kernelELFBase toPAddr addrFromPPtr ptrFromPAddr addrFromKPPtr setCurrentUserCR3 getCurrentUserCR3 invalidateTLB invalidateTLBEntry mfence wordFromPML4E wordFromPDPTE firstValidIODomain numIODomainIDBits hwASIDInvalidate getFaultAddress irqIntOffset maxPCIBus maxPCIDev maxPCIFunc ioapicIRQLines ioapicMapPinToVector irqStateIRQIOAPICNew irqStateIRQMSINew updateIRQState in8 out8 in16 out16 in32 out32 invalidatePageStructureCache writeCR3 invalidateASID invalidateTranslationSingleASID invalidateLocalPageStructureCacheASID ptTranslationBits nativeThreadUsingFPU switchFpuOwner +#INCLUDE_HASKELL SEL4/Machine/Hardware/X64.lhs Platform=Platform.X64 CONTEXT X64_H NOT getMemoryRegions getDeviceRegions getKernelDevices loadWord storeWord storeWordVM getActiveIRQ ackInterrupt maskInterrupt configureTimer resetTimer debugPrint getRestartPC setNextPC clearMemory clearMemoryVM initMemory freeMemory wordFromPDE wordFromPTE VMFaultType HypFaultType VMMapType VMPageSize pageBits pageBitsForSize paddrBase pptrBase pptrTop pptrBaseOffset kernelELFBaseOffset kernelELFPAddrBase kernelELFBase toPAddr addrFromPPtr ptrFromPAddr addrFromKPPtr setCurrentUserCR3 getCurrentUserCR3 invalidateTLB invalidateTLBEntry mfence wordFromPML4E wordFromPDPTE firstValidIODomain numIODomainIDBits hwASIDInvalidate getFaultAddress irqIntOffset maxPCIBus maxPCIDev maxPCIFunc ioapicIRQLines ioapicMapPinToVector irqStateIRQIOAPICNew irqStateIRQMSINew updateIRQState in8 out8 in16 out16 in32 out32 invalidatePageStructureCache writeCR3 invalidateASID invalidateTranslationSingleASID invalidateLocalPageStructureCacheASID ptTranslationBits readFpuState writeFpuState enableFpu disableFpu end diff --git a/spec/haskell/SEL4.cabal b/spec/haskell/SEL4.cabal index a23531ee62..cf62af8573 100644 --- a/spec/haskell/SEL4.cabal +++ b/spec/haskell/SEL4.cabal @@ -169,6 +169,7 @@ Library SEL4.Object.Instances.X64 SEL4.Object.IOPort.X64 SEL4.Object.TCB.X64 + SEL4.Object.FPU.X64 SEL4.Model.StateData.X64 SEL4.Model.PSpace.X64 SEL4.Machine.RegisterSet.X64 @@ -214,6 +215,7 @@ Library SEL4.Object.Instances.AARCH64 SEL4.Object.VCPU.AARCH64 SEL4.Object.TCB.AARCH64 + SEL4.Object.FPU.AARCH64 SEL4.Model.StateData.AARCH64 SEL4.Model.PSpace.AARCH64 SEL4.Machine.RegisterSet.AARCH64 diff --git a/spec/haskell/src/SEL4/API/Invocation.lhs b/spec/haskell/src/SEL4/API/Invocation.lhs index 6997554773..de4819c427 100644 --- a/spec/haskell/src/SEL4/API/Invocation.lhs +++ b/spec/haskell/src/SEL4/API/Invocation.lhs @@ -83,6 +83,10 @@ The following data type defines the set of possible TCB invocation operations. T > | SetTLSBase { > setTLSBaseTCB :: PPtr TCB, > setTLSBaseNewBase :: Word } +> | SetFlags { +> setFlagsTCB :: PPtr TCB, +> setFlagsClear :: Word, +> setFlagsSet :: Word } > deriving Show \subsubsection{CNode Invocations} diff --git a/spec/haskell/src/SEL4/API/InvocationLabels.lhs b/spec/haskell/src/SEL4/API/InvocationLabels.lhs index 9258f70047..3ad6a263b5 100644 --- a/spec/haskell/src/SEL4/API/InvocationLabels.lhs +++ b/spec/haskell/src/SEL4/API/InvocationLabels.lhs @@ -45,6 +45,7 @@ The following type enumerates all the kinds of invocations that clients can requ > | TCBBindNotification > | TCBUnbindNotification > | TCBSetTLSBase +> | TCBSetFlags > | CNodeRevoke > | CNodeDelete > | CNodeCancelBadgedSends diff --git a/spec/haskell/src/SEL4/Kernel/Hypervisor/AARCH64.hs b/spec/haskell/src/SEL4/Kernel/Hypervisor/AARCH64.hs index cd9e2790d7..82242c4f9b 100644 --- a/spec/haskell/src/SEL4/Kernel/Hypervisor/AARCH64.hs +++ b/spec/haskell/src/SEL4/Kernel/Hypervisor/AARCH64.hs @@ -13,19 +13,13 @@ import SEL4.Object.Structures import SEL4.API.Failures import SEL4.Kernel.FaultHandler import SEL4.API.Failures.AARCH64 -import SEL4.Machine.Hardware.AARCH64 (HypFaultType(..),isFpuEnable,getESR) +import SEL4.Machine.Hardware.AARCH64 (HypFaultType(..),getESR) import Data.Bits handleHypervisorFault :: PPtr TCB -> HypFaultType -> Kernel () handleHypervisorFault thread (ARMVCPUFault hsr) = do - fpu_enabled <- doMachineOp isFpuEnable - -- the C code makes extra checks on hsr to get to this branch, but the - -- handling of lazy FPU switching is out of scope of verification at this - -- time, so we omit the entire branch where an FPU fault could occur - if not fpu_enabled - then error "Lazy FPU switch is outside of current verification scope" - else if hsr == 0x2000000 -- UNKNOWN_FAULT - then do - esr <- doMachineOp getESR - handleFault thread (UserException (esr .&. mask 32) 0) - else handleFault thread (ArchFault $ VCPUFault $ fromIntegral hsr) + if hsr == 0x2000000 -- UNKNOWN_FAULT + then do + esr <- doMachineOp getESR + handleFault thread (UserException (esr .&. mask 32) 0) + else handleFault thread (ArchFault $ VCPUFault $ fromIntegral hsr) diff --git a/spec/haskell/src/SEL4/Kernel/Thread.lhs b/spec/haskell/src/SEL4/Kernel/Thread.lhs index e3215bd567..68e0292c5a 100644 --- a/spec/haskell/src/SEL4/Kernel/Thread.lhs +++ b/spec/haskell/src/SEL4/Kernel/Thread.lhs @@ -19,7 +19,7 @@ We use the C preprocessor to select a target architecture. \begin{impdetails} % {-# BOOT-IMPORTS: SEL4.Model SEL4.Machine SEL4.Object.Structures SEL4.Object.Instances() SEL4.API.Types #-} -% {-# BOOT-EXPORTS: setDomain setMCPriority setPriority getThreadState setThreadState setBoundNotification getBoundNotification doIPCTransfer isRunnable restart suspend doReplyTransfer tcbSchedEnqueue tcbSchedDequeue rescheduleRequired timerTick possibleSwitchTo tcbQueueEmpty tcbQueuePrepend tcbQueueAppend tcbQueueInsert tcbQueueRemove #-} +% {-# BOOT-EXPORTS: setDomain setMCPriority setPriority setFlags getThreadState setThreadState setBoundNotification getBoundNotification doIPCTransfer isRunnable restart suspend doReplyTransfer tcbSchedEnqueue tcbSchedDequeue rescheduleRequired timerTick possibleSwitchTo tcbQueueEmpty tcbQueuePrepend tcbQueueAppend tcbQueueInsert tcbQueueRemove #-} > import Prelude hiding (Word) > import SEL4.Config @@ -308,7 +308,9 @@ has the highest runnable priority in the system on kernel entry (unless idle). > scheduleChooseNewThread :: Kernel () > scheduleChooseNewThread = do > domainTime <- getDomainTime -> when (domainTime == 0) $ nextDomain +> when (domainTime == 0) $ do +> Arch.prepareNextDomain +> nextDomain > chooseThread > setSchedulerAction ResumeCurrentThread @@ -457,6 +459,12 @@ The following function is used to alter a thread's domain. > when runnable $ tcbSchedEnqueue tptr > when (tptr == curThread) $ rescheduleRequired +\subsubsection{Changing a thread's flags} + +> setFlags :: PPtr TCB -> TcbFlags -> Kernel () +> setFlags tptr flags = do +> threadSet (\t -> t { tcbFlags = flags }) tptr + \subsubsection{Changing a thread's MCP} > setMCPriority :: PPtr TCB -> Priority -> Kernel () diff --git a/spec/haskell/src/SEL4/Kernel/Thread/AARCH64.hs b/spec/haskell/src/SEL4/Kernel/Thread/AARCH64.hs index 9329e5a30d..1b6ce2996d 100644 --- a/spec/haskell/src/SEL4/Kernel/Thread/AARCH64.hs +++ b/spec/haskell/src/SEL4/Kernel/Thread/AARCH64.hs @@ -19,12 +19,14 @@ import {-# SOURCE #-} SEL4.Kernel.Init import {-# SOURCE #-} SEL4.Object.TCB (asUser, threadGet) import SEL4.Machine.RegisterSet.AARCH64(Register(..)) import SEL4.Object.VCPU.AARCH64 +import SEL4.Object.FPU.AARCH64 switchToThread :: PPtr TCB -> Kernel () switchToThread tcb = do tcbobj <- getObject tcb vcpuSwitch (atcbVCPUPtr $ tcbArch tcbobj) setVMRoot tcb + lazyFpuRestore tcb configureIdleThread :: PPtr TCB -> KernelInit () configureIdleThread _ = error "Unimplemented init code" @@ -36,3 +38,6 @@ switchToIdleThread = do activateIdleThread :: PPtr TCB -> Kernel () activateIdleThread _ = return () + +prepareNextDomain :: Kernel () +prepareNextDomain = switchLocalFpuOwner Nothing diff --git a/spec/haskell/src/SEL4/Kernel/Thread/ARM.lhs b/spec/haskell/src/SEL4/Kernel/Thread/ARM.lhs index c844d80aa5..060b185072 100644 --- a/spec/haskell/src/SEL4/Kernel/Thread/ARM.lhs +++ b/spec/haskell/src/SEL4/Kernel/Thread/ARM.lhs @@ -65,3 +65,7 @@ There is nothing special about idle thread activation on ARM. > activateIdleThread :: PPtr TCB -> Kernel () > activateIdleThread _ = return () +There is nothing special that needs to be done before calling nextDomain on ARM. + +> prepareNextDomain :: Kernel () +> prepareNextDomain = return () diff --git a/spec/haskell/src/SEL4/Kernel/Thread/RISCV64.hs b/spec/haskell/src/SEL4/Kernel/Thread/RISCV64.hs index ea92b524c7..34ed57c7e5 100644 --- a/spec/haskell/src/SEL4/Kernel/Thread/RISCV64.hs +++ b/spec/haskell/src/SEL4/Kernel/Thread/RISCV64.hs @@ -30,3 +30,6 @@ switchToIdleThread = do activateIdleThread :: PPtr TCB -> Kernel () activateIdleThread _ = return () + +prepareNextDomain :: Kernel () +prepareNextDomain = return () diff --git a/spec/haskell/src/SEL4/Kernel/Thread/X64.lhs b/spec/haskell/src/SEL4/Kernel/Thread/X64.lhs index f3df8dd867..c31fbce0ae 100644 --- a/spec/haskell/src/SEL4/Kernel/Thread/X64.lhs +++ b/spec/haskell/src/SEL4/Kernel/Thread/X64.lhs @@ -16,11 +16,14 @@ This module contains the architecture-specific thread switch code for X86-64bit. > import SEL4.Object.Structures > import SEL4.Kernel.VSpace.X64 > import {-# SOURCE #-} SEL4.Kernel.Init +> import SEL4.Object.FPU.X64 \end{impdetails} > switchToThread :: PPtr TCB -> Kernel () -> switchToThread tcb = setVMRoot tcb +> switchToThread tcb = do +> setVMRoot tcb +> lazyFpuRestore tcb > configureIdleThread :: PPtr TCB -> KernelInit () > configureIdleThread _ = error "Unimplemented. init code" @@ -33,3 +36,5 @@ This module contains the architecture-specific thread switch code for X86-64bit. > activateIdleThread :: PPtr TCB -> Kernel () > activateIdleThread _ = return () +> prepareNextDomain :: Kernel () +> prepareNextDomain = switchLocalFpuOwner Nothing diff --git a/spec/haskell/src/SEL4/Machine/Hardware/AARCH64.hs b/spec/haskell/src/SEL4/Machine/Hardware/AARCH64.hs index 887cd90aa7..ca4c6884e4 100644 --- a/spec/haskell/src/SEL4/Machine/Hardware/AARCH64.hs +++ b/spec/haskell/src/SEL4/Machine/Hardware/AARCH64.hs @@ -387,11 +387,20 @@ debugPrint str = liftIO $ putStrLn str {- FPU Operations -} -fpuThreadDeleteOp :: Word -> MachineMonad () -fpuThreadDeleteOp tcbPtr = error "Unimplemented callback" +readFpuState :: MachineMonad AARCH64.FPUState +readFpuState = error "Unimplemented - machine op" + +writeFpuState :: AARCH64.FPUState -> MachineMonad () +writeFpuState _ = error "Unimplemented - machine op" + +enableFpu :: MachineMonad () +enableFpu = error "Unimplemented - machine op" + +disableFpu :: MachineMonad () +disableFpu = error "Unimplemented - machine op" isFpuEnable :: MachineMonad Bool -isFpuEnable = error "Unimplemented - lazy FPU switch abstracted as machine op" +isFpuEnable = error "Unimplemented - machine op" {- GIC VCPU interface -} diff --git a/spec/haskell/src/SEL4/Machine/Hardware/X64.lhs b/spec/haskell/src/SEL4/Machine/Hardware/X64.lhs index aef01f9b9f..f74109666f 100644 --- a/spec/haskell/src/SEL4/Machine/Hardware/X64.lhs +++ b/spec/haskell/src/SEL4/Machine/Hardware/X64.lhs @@ -639,13 +639,17 @@ IRQ parameters FPU operations -> nativeThreadUsingFPU :: Word -> MachineMonad Bool -> nativeThreadUsingFPU threadPtr = do -> cbptr <- ask -> liftIO $ Platform.nativeThreadUsingFPU threadPtr +> readFpuState :: MachineMonad X64.FPUState +> readFpuState = error "Unimplemented - machine op" -> switchFpuOwner :: Word -> Word -> MachineMonad () -> switchFpuOwner newOwner cpu = do -> cbptr <- ask -> liftIO $ Platform.switchFpuOwner newOwner cpu +> writeFpuState :: X64.FPUState -> MachineMonad () +> writeFpuState _ = error "Unimplemented - machine op" + +> enableFpu :: MachineMonad () +> enableFpu = error "Unimplemented - machine op" + +> disableFpu :: MachineMonad () +> disableFpu = error "Unimplemented - machine op" +> isFpuEnable :: MachineMonad Bool +> isFpuEnable = error "Unimplemented - machine op" diff --git a/spec/haskell/src/SEL4/Machine/RegisterSet/AARCH64.hs b/spec/haskell/src/SEL4/Machine/RegisterSet/AARCH64.hs index 7bf4414118..03c684deb5 100644 --- a/spec/haskell/src/SEL4/Machine/RegisterSet/AARCH64.hs +++ b/spec/haskell/src/SEL4/Machine/RegisterSet/AARCH64.hs @@ -118,8 +118,7 @@ data FPUState = FPUState { fpuRegs :: Array Int Data.Word.Word64 -- The representation of the user-level context of a thread is an array of -- machine words, indexed by register name for the user registers, plus the --- state of the FPU. There are no operations on the FPU state apart from save --- and restore at kernel entry and exit. +-- state of the FPU. data UserContext = UC { fromUC :: Array Register Word, fpuState :: FPUState } deriving Show @@ -134,8 +133,13 @@ newFPUState = FPUState (funPartialArray (const 0) (0,63)) 0 0 newContext :: UserContext newContext = UC ((funArray $ const 0)//initContext) newFPUState --- Functions are provided to get and set a single register. +-- Functions are provided to get and set a single register, or to get and set the FPU state. getRegister r = gets $ (! r) . fromUC setRegister r v = modify (\ uc -> UC (fromUC uc //[(r, v)]) (fpuState uc)) + +getFPUState :: State UserContext FPUState +getFPUState = gets fpuState + +setFPUState fc = modify (\ uc -> UC (fromUC uc) fc) diff --git a/spec/haskell/src/SEL4/Machine/RegisterSet/X64.lhs b/spec/haskell/src/SEL4/Machine/RegisterSet/X64.lhs index ad639b4a47..4c9cf7e64e 100644 --- a/spec/haskell/src/SEL4/Machine/RegisterSet/X64.lhs +++ b/spec/haskell/src/SEL4/Machine/RegisterSet/X64.lhs @@ -82,11 +82,12 @@ This module defines the x86 64-bit register set. On X64 the representation of the user-level context of a thread is an array of machine words, indexed by register name for the user registers, plus the state of the FPU, which we represent as a function from machine word to bytes -with the convention that all unused entries map to 0. There are no operations -on the FPU state apart from save and restore at kernel entry and exit. +with the convention that all unused entries map to 0. + +> type FPUState = Array Word Data.Word.Word8 > data UserContext = UC { fromUC :: Array Register Word, -> fpuState :: Array Word Data.Word.Word8 } +> fpuState :: FPUState } > deriving Show @@ -98,9 +99,13 @@ initialised to 0. > newContext :: UserContext > newContext = UC ((funArray $ const 0)//initContext) (funPartialArray (const 0) (0,575)) -Functions are provided to get and set a single register. +Functions are provided to get and set a single register, or to get and set the FPU state. > getRegister r = gets $ (! r) . fromUC > setRegister r v = modify (\ uc -> UC (fromUC uc //[(r, v)]) (fpuState uc)) +> getFPUState :: State UserContext FPUState +> getFPUState = gets fpuState + +> setFPUState fc = modify (\ uc -> UC (fromUC uc) fc) diff --git a/spec/haskell/src/SEL4/Model/StateData/AARCH64.hs b/spec/haskell/src/SEL4/Model/StateData/AARCH64.hs index 037fd06e5b..6fdaea0fe6 100644 --- a/spec/haskell/src/SEL4/Model/StateData/AARCH64.hs +++ b/spec/haskell/src/SEL4/Model/StateData/AARCH64.hs @@ -13,6 +13,7 @@ module SEL4.Model.StateData.AARCH64 where import Prelude hiding (Word) import SEL4.Machine import SEL4.Machine.Hardware.AARCH64 (PTE(..), PT_Type, config_ARM_PA_SIZE_BITS_40) +import SEL4.Object.Structures import SEL4.Object.Structures.AARCH64 import Data.Array @@ -41,7 +42,8 @@ data KernelState = ARMKernelState { armKSGlobalUserVSpace :: PPtr PTE, armHSCurVCPU :: Maybe (PPtr VCPU, Bool), armKSGICVCPUNumListRegs :: Int, - gsPTTypes :: Word -> Maybe PT_Type + gsPTTypes :: Word -> Maybe PT_Type, + armKSCurFPUOwner :: Maybe (PPtr TCB) } -- counting from 0 at bottom, i.e. number of levels = maxPTLevel + 1; diff --git a/spec/haskell/src/SEL4/Model/StateData/X64.lhs b/spec/haskell/src/SEL4/Model/StateData/X64.lhs index 7e99bd1d79..cfa3bfc091 100644 --- a/spec/haskell/src/SEL4/Model/StateData/X64.lhs +++ b/spec/haskell/src/SEL4/Model/StateData/X64.lhs @@ -13,6 +13,7 @@ This module contains the architecture-specific kernel global data for the X86-64 > import Prelude hiding (Word) > import SEL4.Machine > import SEL4.Machine.Hardware.X64 (PML4E(..),PDPTE(..),PDE(..),PTE(..),IOPort) +> import SEL4.Object.Structures > import SEL4.Object.Structures.X64 > import Data.Array @@ -43,7 +44,8 @@ This module contains the architecture-specific kernel global data for the X86-64 > x64KSAllocatedIOPorts :: Array IOPort Bool, > x64KSNumIOAPICs :: Word, > x64KSIOAPICnIRQs :: Word -> Word8, -> x64KSIRQState :: Array IRQ X64IRQState} +> x64KSIRQState :: Array IRQ X64IRQState, +> x64KSCurFPUOwner :: Maybe (PPtr TCB)} > newKernelState :: PAddr -> (KernelState, [PAddr]) > newKernelState _ = error "No initial state defined for x64" diff --git a/spec/haskell/src/SEL4/Object/FPU/AARCH64.hs b/spec/haskell/src/SEL4/Object/FPU/AARCH64.hs new file mode 100644 index 0000000000..ac4a4266f1 --- /dev/null +++ b/spec/haskell/src/SEL4/Object/FPU/AARCH64.hs @@ -0,0 +1,54 @@ +-- +-- Copyright 2024, Proofcraft Pty Ltd +-- +-- SPDX-License-Identifier: GPL-2.0-only +-- + +{-# LANGUAGE CPP #-} + +module SEL4.Object.FPU.AARCH64 where + +import SEL4.Machine +import SEL4.Model +import SEL4.Object.Structures +import SEL4.Machine.Hardware.AARCH64 +import SEL4.Machine.RegisterSet.AARCH64 +import SEL4.Model.StateData.AARCH64 +import {-# SOURCE #-} SEL4.Object.TCB(asUser, threadGet) + +import Data.Bits +import Data.Maybe + +saveFpuState :: PPtr TCB -> Kernel () +saveFpuState tcbPtr = do + fpuState <- doMachineOp readFpuState + asUser tcbPtr (setFPUState fpuState) + +loadFpuState :: PPtr TCB -> Kernel () +loadFpuState tcbPtr = do + fpuState <- asUser tcbPtr getFPUState + doMachineOp (writeFpuState fpuState) + +switchLocalFpuOwner :: Maybe (PPtr TCB) -> Kernel () +switchLocalFpuOwner newOwner = do + doMachineOp enableFpu + curFpuOwner <- gets (armKSCurFPUOwner . ksArchState) + maybe (return ()) saveFpuState curFpuOwner + case newOwner of + Nothing -> doMachineOp disableFpu + Just tcbPtr -> loadFpuState tcbPtr + modifyArchState (\s -> s { armKSCurFPUOwner = newOwner }) + +fpuRelease :: PPtr TCB -> Kernel () +fpuRelease tcbPtr = do + curFpuOwner <- gets (armKSCurFPUOwner . ksArchState) + when (curFpuOwner /= Just tcbPtr) (switchLocalFpuOwner Nothing) + +lazyFpuRestore :: PPtr TCB -> Kernel () +lazyFpuRestore tcbPtr = do + flags <- threadGet tcbFlags tcbPtr + if (tcbFlagToWord (ArchFlag FpuDisabled) .&. flags /= 0) + then doMachineOp disableFpu + else do + doMachineOp enableFpu + switchLocalFpuOwner (Just tcbPtr) diff --git a/spec/haskell/src/SEL4/Object/FPU/X64.hs b/spec/haskell/src/SEL4/Object/FPU/X64.hs new file mode 100644 index 0000000000..10368c1051 --- /dev/null +++ b/spec/haskell/src/SEL4/Object/FPU/X64.hs @@ -0,0 +1,54 @@ +-- +-- Copyright 2024, Proofcraft Pty Ltd +-- +-- SPDX-License-Identifier: GPL-2.0-only +-- + +{-# LANGUAGE CPP #-} + +module SEL4.Object.FPU.X64 where + +import SEL4.Machine +import SEL4.Model +import SEL4.Object.Structures +import SEL4.Machine.Hardware.X64 +import SEL4.Machine.RegisterSet.X64 +import SEL4.Model.StateData.X64 +import {-# SOURCE #-} SEL4.Object.TCB(asUser, threadGet) + +import Data.Bits +import Data.Maybe + +saveFpuState :: PPtr TCB -> Kernel () +saveFpuState tcbPtr = do + fpuState <- doMachineOp readFpuState + asUser tcbPtr (setFPUState fpuState) + +loadFpuState :: PPtr TCB -> Kernel () +loadFpuState tcbPtr = do + fpuState <- asUser tcbPtr getFPUState + doMachineOp (writeFpuState fpuState) + +switchLocalFpuOwner :: Maybe (PPtr TCB) -> Kernel () +switchLocalFpuOwner newOwner = do + doMachineOp enableFpu + curFpuOwner <- gets (x64KSCurFPUOwner . ksArchState) + maybe (return ()) saveFpuState curFpuOwner + case newOwner of + Nothing -> doMachineOp disableFpu + Just tcbPtr -> loadFpuState tcbPtr + modifyArchState (\s -> s { x64KSCurFPUOwner = newOwner }) + +fpuRelease :: PPtr TCB -> Kernel () +fpuRelease tcbPtr = do + curFpuOwner <- gets (x64KSCurFPUOwner . ksArchState) + when (curFpuOwner /= Just tcbPtr) (switchLocalFpuOwner Nothing) + +lazyFpuRestore :: PPtr TCB -> Kernel () +lazyFpuRestore tcbPtr = do + flags <- threadGet tcbFlags tcbPtr + if (tcbFlagToWord (ArchFlag FpuDisabled) .&. flags /= 0) + then doMachineOp disableFpu + else do + doMachineOp enableFpu + switchLocalFpuOwner (Just tcbPtr) diff --git a/spec/haskell/src/SEL4/Object/Instances.lhs b/spec/haskell/src/SEL4/Object/Instances.lhs index eb20a91117..e06b7c74dc 100644 --- a/spec/haskell/src/SEL4/Object/Instances.lhs +++ b/spec/haskell/src/SEL4/Object/Instances.lhs @@ -140,6 +140,7 @@ By default, new threads are unable to change the security domains of other threa > tcbBoundNotification = Nothing, > tcbSchedPrev = Nothing, > tcbSchedNext = Nothing, +> tcbFlags = 0, > tcbArch = newArchTCB } > injectKO = KOTCB > projectKO o = case o of diff --git a/spec/haskell/src/SEL4/Object/ObjectType.lhs b/spec/haskell/src/SEL4/Object/ObjectType.lhs index 8fc24967ab..6a8ffb8e0d 100644 --- a/spec/haskell/src/SEL4/Object/ObjectType.lhs +++ b/spec/haskell/src/SEL4/Object/ObjectType.lhs @@ -45,6 +45,7 @@ We use the C preprocessor to select a target architecture. The architecture-specific definitions are imported qualified with the "Arch" prefix. > import qualified SEL4.Object.ObjectType.TARGET as Arch +> import qualified SEL4.Object.TCB.TARGET as Arch(prepareSetDomain) \subsection{Creating Capabilities} @@ -461,6 +462,7 @@ This function just dispatches invocations to the type-specific invocation functi > performInvocation _ _ (InvokeTCB invok) = invokeTCB invok > > performInvocation _ _ (InvokeDomain thread domain) = withoutPreemption $ do +> Arch.prepareSetDomain thread domain > setDomain thread domain > return $ [] > diff --git a/spec/haskell/src/SEL4/Object/ObjectType/AARCH64.hs b/spec/haskell/src/SEL4/Object/ObjectType/AARCH64.hs index b71e018100..b55a5ce762 100644 --- a/spec/haskell/src/SEL4/Object/ObjectType/AARCH64.hs +++ b/spec/haskell/src/SEL4/Object/ObjectType/AARCH64.hs @@ -23,6 +23,7 @@ import SEL4.Object.Structures import SEL4.Kernel.VSpace.AARCH64 import SEL4.Object.VCPU.AARCH64 import {-# SOURCE #-} SEL4.Object.TCB +import SEL4.Object.FPU.AARCH64 import Data.Bits import Data.Word(Word16) @@ -246,13 +247,9 @@ capUntypedSize (VCPUCap {}) = bit vcpuBits -- Thread deletion requires associated FPU cleanup -fpuThreadDelete :: PPtr TCB -> Kernel () -fpuThreadDelete threadPtr = - doMachineOp $ fpuThreadDeleteOp (fromPPtr threadPtr) - prepareThreadDelete :: PPtr TCB -> Kernel () prepareThreadDelete thread = do - fpuThreadDelete thread + fpuRelease thread tcbVCPU <- archThreadGet atcbVCPUPtr thread case tcbVCPU of Just ptr -> dissociateVCPUTCB ptr thread diff --git a/spec/haskell/src/SEL4/Object/ObjectType/X64.lhs b/spec/haskell/src/SEL4/Object/ObjectType/X64.lhs index b2b8ec3d29..6eb6b3143b 100644 --- a/spec/haskell/src/SEL4/Object/ObjectType/X64.lhs +++ b/spec/haskell/src/SEL4/Object/ObjectType/X64.lhs @@ -21,6 +21,7 @@ This module contains operations on machine-specific object types for x64. > import SEL4.Object.Structures > import SEL4.Kernel.VSpace.X64 > import {-# SOURCE #-} SEL4.Object.IOPort.X64 +> import SEL4.Object.FPU.X64 > import Data.Bits > import Data.Word(Word16) @@ -387,10 +388,5 @@ Create an architecture-specific object. Notify the FPU when deleting a thread, in case that thread is using the FPU > prepareThreadDelete :: PPtr TCB -> Kernel () -> prepareThreadDelete threadPtr = fpuThreadDelete threadPtr - -> fpuThreadDelete :: PPtr TCB -> Kernel () -> fpuThreadDelete threadPtr = do -> usingFpu <- doMachineOp $ nativeThreadUsingFPU (fromPPtr threadPtr) -> when usingFpu $ doMachineOp (switchFpuOwner 0 0) +> prepareThreadDelete threadPtr = fpuRelease threadPtr diff --git a/spec/haskell/src/SEL4/Object/Structures.lhs b/spec/haskell/src/SEL4/Object/Structures.lhs index d3d1263e40..5cd0c0eefe 100644 --- a/spec/haskell/src/SEL4/Object/Structures.lhs +++ b/spec/haskell/src/SEL4/Object/Structures.lhs @@ -283,6 +283,10 @@ The TCB is used to store various data about the thread's current state: > tcbSchedPrev :: Maybe (PPtr TCB), > tcbSchedNext :: Maybe (PPtr TCB), +\item the thread's feature flags, currently only used for fpuDisabled + +> tcbFlags :: TcbFlags, + \item and any arch-specific TCB contents > tcbArch :: ArchTCB } @@ -492,3 +496,15 @@ Various operations on the free index of an Untyped cap. > data TcbQueue = TcbQueue { > tcbQueueHead :: Maybe (PPtr TCB), > tcbQueueEnd :: Maybe (PPtr TCB) } + +\subsubsection{TCB Flags} + +> type TcbFlags = Word + +> data TcbFlag +> = NoFlag +> | ArchFlag ArchTcbFlag + +> tcbFlagToWord :: TcbFlag -> Word +> tcbFlagToWord NoFlag = 0x0 +> tcbFlagToWord (ArchFlag archFlag) = archTcbFlagToWord archFlag diff --git a/spec/haskell/src/SEL4/Object/Structures/AARCH64.hs b/spec/haskell/src/SEL4/Object/Structures/AARCH64.hs index aa1d6ec3ac..2bbe4dc10b 100644 --- a/spec/haskell/src/SEL4/Object/Structures/AARCH64.hs +++ b/spec/haskell/src/SEL4/Object/Structures/AARCH64.hs @@ -70,6 +70,11 @@ atcbContextSet uc atcb = atcb { atcbContext = uc } atcbContextGet :: ArchTCB -> UserContext atcbContextGet = atcbContext +data ArchTcbFlag = FpuDisabled + +archTcbFlagToWord :: ArchTcbFlag -> Word +archTcbFlagToWord (FpuDisabled) = 0x1 + {- ASID Pools -} diff --git a/spec/haskell/src/SEL4/Object/Structures/ARM.lhs b/spec/haskell/src/SEL4/Object/Structures/ARM.lhs index c660aaeb12..692f8f2c19 100644 --- a/spec/haskell/src/SEL4/Object/Structures/ARM.lhs +++ b/spec/haskell/src/SEL4/Object/Structures/ARM.lhs @@ -136,6 +136,11 @@ present on all platforms is stored here. > atcbContextGet :: ArchTCB -> UserContext > atcbContextGet = atcbContext +> type ArchTcbFlag = () + +> archTcbFlagToWord :: ArchTcbFlag -> Word +> archTcbFlagToWord _ = error "ARM does not have any arch specific flags" + \subsection{ASID Pools} An ASID pool is an array of pointers to page directories. This is used to implement virtual ASIDs on ARM; it is not accessed by the hardware. diff --git a/spec/haskell/src/SEL4/Object/Structures/RISCV64.hs b/spec/haskell/src/SEL4/Object/Structures/RISCV64.hs index 49974204fd..bdcd44ae7c 100644 --- a/spec/haskell/src/SEL4/Object/Structures/RISCV64.hs +++ b/spec/haskell/src/SEL4/Object/Structures/RISCV64.hs @@ -73,6 +73,10 @@ atcbContextSet uc atcb = atcb { atcbContext = uc } atcbContextGet :: ArchTCB -> UserContext atcbContextGet = atcbContext +type ArchTcbFlag = () + +archTcbFlagToWord :: ArchTcbFlag -> Word +archTcbFlagToWord _ = error "ARM does not have any arch specific flags" {- ASID Pools -} diff --git a/spec/haskell/src/SEL4/Object/Structures/X64.lhs b/spec/haskell/src/SEL4/Object/Structures/X64.lhs index dde3c813d7..1b028a88f0 100644 --- a/spec/haskell/src/SEL4/Object/Structures/X64.lhs +++ b/spec/haskell/src/SEL4/Object/Structures/X64.lhs @@ -121,6 +121,11 @@ present on all platforms is stored here. > atcbContextGet :: ArchTCB -> UserContext > atcbContextGet = atcbContext +> data ArchTcbFlag = FpuDisabled + +> archTcbFlagToWord :: ArchTcbFlag -> Word +> archTcbFlagToWord (FpuDisabled) = 0x1 + \subsection{ASID Pools} An ASID pool is an array of pointers to page directories. This is used to implement virtual ASIDs on x64; it is not accessed by the hardware. diff --git a/spec/haskell/src/SEL4/Object/TCB.lhs b/spec/haskell/src/SEL4/Object/TCB.lhs index 20b8195638..7e142cd3c9 100644 --- a/spec/haskell/src/SEL4/Object/TCB.lhs +++ b/spec/haskell/src/SEL4/Object/TCB.lhs @@ -85,6 +85,7 @@ There are eleven types of invocation for a thread control block. All require wri > TCBBindNotification -> decodeBindNotification cap extraCaps > TCBUnbindNotification -> decodeUnbindNotification cap > TCBSetTLSBase -> decodeSetTLSBase args cap +> TCBSetFlags -> decodeSetFlags args cap > _ -> throw IllegalOperation \subsubsection{Reading, Writing and Copying Registers} @@ -377,6 +378,14 @@ This is to ensure that the source capability is not made invalid by the deletion > setTLSBaseNewBase = tls_base } > decodeSetTLSBase _ _ = throw TruncatedMessage +> decodeSetFlags :: [Word] -> Capability -> +> KernelF SyscallError TCBInvocation +> decodeSetFlags (flagsClear:flagsSet:_) cap = do +> return $ SetFlags { +> setFlagsTCB = capTCBPtr cap, +> setFlagsClear = flagsClear, +> setFlagsSet = flagsSet } +> decodeSetFlags _ _ = throw TruncatedMessage \subsection[invoke]{Performing TCB Invocations} @@ -545,6 +554,14 @@ Modifying the current thread may require rescheduling because modified registers > when (tcb == cur) rescheduleRequired > return [] +> invokeTCB (SetFlags tcb flagsClear flagsSet) = +> withoutPreemption $ do +> flags <- threadGet tcbFlags tcb +> let newFlags = (flags .&. complement flagsClear) .|. flagsSet +> setFlags tcb newFlags +> Arch.postSetFlags tcb newFlags +> return [] + \subsection{Decoding Domain Invocations} The domain cap is invoked to set the domain of a given TCB object to a given value. diff --git a/spec/haskell/src/SEL4/Object/TCB/AARCH64.hs b/spec/haskell/src/SEL4/Object/TCB/AARCH64.hs index f96ed14f96..805ab06d3d 100644 --- a/spec/haskell/src/SEL4/Object/TCB/AARCH64.hs +++ b/spec/haskell/src/SEL4/Object/TCB/AARCH64.hs @@ -20,11 +20,13 @@ import SEL4.Machine(PPtr) import SEL4.Model import SEL4.Object.Structures import SEL4.Object.Instances() +import SEL4.API.Types import SEL4.API.Failures import SEL4.API.Invocation.AARCH64 import SEL4.Machine.RegisterSet(setRegister, UserMonad, VPtr(..)) import qualified SEL4.Machine.RegisterSet as RegisterSet(Register(..)) import SEL4.Machine.RegisterSet.AARCH64(Register(..), Word) +import SEL4.Object.FPU.AARCH64 import Data.Bits import Data.Maybe import Data.Word(Word8) @@ -51,3 +53,14 @@ getSanitiseRegisterInfo t = do postModifyRegisters :: PPtr TCB -> PPtr TCB -> UserMonad () postModifyRegisters _ _ = return () + +postSetFlags :: PPtr TCB -> TcbFlags -> Kernel () +postSetFlags t flags = + when (tcbFlagToWord (ArchFlag FpuDisabled) .&. flags /= 0) (fpuRelease t) + +-- Save and clear FPU state before setting the domain of a TCB, to ensure that +-- we do not later write to cross-domain state. +prepareSetDomain :: PPtr TCB -> Domain -> Kernel () +prepareSetDomain t newDom = do + curDom <- curDomain + when (curDom /= newDom) (fpuRelease t) diff --git a/spec/haskell/src/SEL4/Object/TCB/ARM.lhs b/spec/haskell/src/SEL4/Object/TCB/ARM.lhs index b40d822d62..337e760f99 100644 --- a/spec/haskell/src/SEL4/Object/TCB/ARM.lhs +++ b/spec/haskell/src/SEL4/Object/TCB/ARM.lhs @@ -23,6 +23,7 @@ There are presently no ARM-specific register subsets defined, but in future this > import SEL4.Model > import SEL4.Object.Structures > import SEL4.Object.Instances() +> import SEL4.API.Types > import SEL4.API.Failures > import SEL4.API.Invocation.ARM > import SEL4.Machine.RegisterSet(setRegister, UserMonad, VPtr(..)) @@ -66,3 +67,8 @@ There are presently no ARM-specific register subsets defined, but in future this > postModifyRegisters :: PPtr TCB -> PPtr TCB -> UserMonad () > postModifyRegisters cur ptr = return () +> postSetFlags :: PPtr TCB -> TcbFlags -> Kernel () +> postSetFlags t flags = return () + +> prepareSetDomain :: PPtr TCB -> Domain -> Kernel () +> prepareSetDomain t newDom = return () diff --git a/spec/haskell/src/SEL4/Object/TCB/RISCV64.hs b/spec/haskell/src/SEL4/Object/TCB/RISCV64.hs index 32fc54cf90..a0bbb595b8 100644 --- a/spec/haskell/src/SEL4/Object/TCB/RISCV64.hs +++ b/spec/haskell/src/SEL4/Object/TCB/RISCV64.hs @@ -18,6 +18,7 @@ import Prelude hiding (Word) import SEL4.Machine(PPtr) import SEL4.Model import SEL4.Object.Structures +import SEL4.API.Types import SEL4.API.Failures import SEL4.API.Invocation.RISCV64 import SEL4.Machine.RegisterSet(setRegister, UserMonad, VPtr(..)) @@ -41,3 +42,9 @@ getSanitiseRegisterInfo _ = return False postModifyRegisters :: PPtr TCB -> PPtr TCB -> UserMonad () postModifyRegisters _ _ = return () + +postSetFlags :: PPtr TCB -> TcbFlags -> Kernel () +postSetFlags t flags = return () + +prepareSetDomain :: PPtr TCB -> Domain -> Kernel () +prepareSetDomain t newDom = return () diff --git a/spec/haskell/src/SEL4/Object/TCB/X64.lhs b/spec/haskell/src/SEL4/Object/TCB/X64.lhs index c971b424ae..3528f9b810 100644 --- a/spec/haskell/src/SEL4/Object/TCB/X64.lhs +++ b/spec/haskell/src/SEL4/Object/TCB/X64.lhs @@ -18,11 +18,13 @@ There are presently no x64-specific register subsets defined, but in future this > import SEL4.Machine(PPtr) > import SEL4.Model > import SEL4.Object.Structures +> import SEL4.API.Types > import SEL4.API.Failures > import SEL4.API.Invocation.X64 > import SEL4.Machine.RegisterSet(setRegister, UserMonad, VPtr(..)) > import qualified SEL4.Machine.RegisterSet as RegisterSet(Register(..)) > import SEL4.Machine.RegisterSet.X64(Register(..), Word) +> import SEL4.Object.FPU.X64 > import Data.Bits > import Data.Word(Word8) @@ -60,3 +62,14 @@ Here, cur = ksCurThread > postModifyRegisters cur dest = > when (dest /= cur) $ setRegister (RegisterSet.Register ErrorRegister) 0 +> postSetFlags :: PPtr TCB -> TcbFlags -> Kernel () +> postSetFlags t flags = +> when (tcbFlagToWord (ArchFlag FpuDisabled) .&. flags /= 0) (fpuRelease t) + +Save and clear FPU state before setting the domain of a TCB, to ensure that +we do not later write to cross-domain state. + +> prepareSetDomain :: PPtr TCB -> Domain -> Kernel () +> prepareSetDomain t newDom = do +> curDom <- curDomain +> when (curDom /= newDom) (fpuRelease t) diff --git a/spec/machine/AARCH64/MachineOps.thy b/spec/machine/AARCH64/MachineOps.thy index e5a5dde703..f5791f8f55 100644 --- a/spec/machine/AARCH64/MachineOps.thy +++ b/spec/machine/AARCH64/MachineOps.thy @@ -168,6 +168,7 @@ definition setNextPC :: "machine_word \ unit user_monad" where subsection "FPU-related" +\ \FIXME: Should this modify @{term fpu_enabled}? The C doesn't update isFPUEnabledCached when this is called directly.\ consts' enableFpuEL01_impl :: "unit machine_rest_monad" definition enableFpuEL01 :: "unit machine_monad" where "enableFpuEL01 \ machine_op_lift enableFpuEL01_impl" @@ -178,31 +179,28 @@ definition getFPUState :: "fpu_state user_monad" where definition setFPUState :: "fpu_state \ unit user_monad" where "setFPUState fc \ modify (\s. UserContext fc (user_regs s))" -consts' nativeThreadUsingFPU_impl :: "machine_word \ unit machine_rest_monad" -consts' nativeThreadUsingFPU_val :: "machine_state \ bool" -definition nativeThreadUsingFPU :: "machine_word \ bool machine_monad" where - "nativeThreadUsingFPU thread_ptr \ do - machine_op_lift (nativeThreadUsingFPU_impl thread_ptr); - gets nativeThreadUsingFPU_val - od" +consts' readFpuState_val :: "machine_state_rest \ fpu_state" +definition readFpuState :: "fpu_state machine_monad" where + "readFpuState \ do + state_assert fpu_enabled; + machine_rest_lift $ gets readFpuState_val + od" + +consts' writeFpuState_impl :: "fpu_state \ unit machine_rest_monad" +definition writeFpuState :: "fpu_state \ unit machine_monad" where + "writeFpuState val \ do + state_assert fpu_enabled; + machine_op_lift $ writeFpuState_impl val + od" + +definition enableFpu :: "unit machine_monad" where + "enableFpu \ modify (\s. s\fpu_enabled := True \)" + +definition disableFpu :: "unit machine_monad" where + "disableFpu \ modify (\s. s\fpu_enabled := False \)" -consts' switchFpuOwner_impl :: "machine_word \ machine_word \ unit machine_rest_monad" -definition switchFpuOwner :: "machine_word \ machine_word \ unit machine_monad" where - "switchFpuOwner new_owner cpu \ machine_op_lift (switchFpuOwner_impl new_owner cpu)" - -(* FIXME this is a very high-level FPU abstraction *) -consts' fpuThreadDeleteOp_impl :: "machine_word \ unit machine_rest_monad" -definition fpuThreadDeleteOp :: "machine_word \ unit machine_monad" where - "fpuThreadDeleteOp thread_ptr \ machine_op_lift (fpuThreadDeleteOp_impl thread_ptr)" - -(* FIXME this machine op is used to abstract the entire lazy FPU switch interrupt mechanism, - which can only trigger when the current thread's FPU is disabled and it performs an FPU - operation. We have no model for this mechanism or the state that it caches, so for - verification purposes we act as if the FPU is always enabled. - Future lazy FPU switch overhaul will involve the state that this operation reads, at which - point it should become a normal function. *) definition isFpuEnable :: "bool machine_monad" where - "isFpuEnable \ return True" + "isFpuEnable \ gets fpu_enabled" subsection "Fault Registers" diff --git a/spec/machine/X64/MachineOps.thy b/spec/machine/X64/MachineOps.thy index 6ec113cc06..8a649f724d 100644 --- a/spec/machine/X64/MachineOps.thy +++ b/spec/machine/X64/MachineOps.thy @@ -264,23 +264,28 @@ where consts' FPUNullState :: fpu_state -consts' - nativeThreadUsingFPU_impl :: "machine_word \ unit machine_rest_monad" - nativeThreadUsingFPU_val :: "machine_state \ bool" -definition - nativeThreadUsingFPU :: "machine_word \ bool machine_monad" -where - "nativeThreadUsingFPU thread_ptr \ do - machine_op_lift (nativeThreadUsingFPU_impl thread_ptr); - gets nativeThreadUsingFPU_val - od" - -consts' - switchFpuOwner_impl :: "machine_word \ machine_word \ unit machine_rest_monad" -definition - switchFpuOwner :: "machine_word \ machine_word \ unit machine_monad" -where - "switchFpuOwner new_owner cpu \ machine_op_lift (switchFpuOwner_impl new_owner cpu)" +consts' readFpuState_val :: "machine_state_rest \ fpu_state" +definition readFpuState :: "fpu_state machine_monad" where + "readFpuState \ do + state_assert fpu_enabled; + machine_rest_lift $ gets readFpuState_val + od" + +consts' writeFpuState_impl :: "fpu_state \ unit machine_rest_monad" +definition writeFpuState :: "fpu_state \ unit machine_monad" where + "writeFpuState val \ do + state_assert fpu_enabled; + machine_op_lift $ writeFpuState_impl val + od" + +definition enableFpu :: "unit machine_monad" where + "enableFpu \ modify (\s. s\fpu_enabled := True \)" + +definition disableFpu :: "unit machine_monad" where + "disableFpu \ modify (\s. s\fpu_enabled := False \)" + +definition isFpuEnable :: "bool machine_monad" where + "isFpuEnable \ gets fpu_enabled" consts' initL2Cache_impl :: "unit machine_rest_monad" diff --git a/tools/haskell-translator/lhs_pars.py b/tools/haskell-translator/lhs_pars.py index ecdd94604d..e51537e98e 100644 --- a/tools/haskell-translator/lhs_pars.py +++ b/tools/haskell-translator/lhs_pars.py @@ -706,6 +706,8 @@ def typename_transform(line, header, d): # take off the prefix, leave Word32 or Word64 etc oldtype = oldtype[10:] oldtype = type_conv(oldtype) + # get rid of (), insert unit + oldtype = 'unit'.join(oldtype.split('()')) bits = oldtype.split() for bit in bits: d.typedeps.add(bit)