1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(NICTA_GPL) 9 *) 10 11(* 12 * System calls 13 *) 14 15theory Syscall_D 16imports 17 Schedule_D 18 Decode_D 19 "ExecSpec.Event_H" 20begin 21 22(* 23 * Perform system calls. 24 * 25 * Each system call is broken into three stages: 26 * 27 * (1) Cap validation, where we ensure that all caps passed 28 * into the system call are valid; 29 * 30 * (2) Argument validation, where we ensure that the requested 31 * operation is valid and permitted; and 32 * 33 * (3) Syscall execution, where we carry out the actual 34 * operation. 35 * 36 * For this function, the user passes us in 5 functions: 37 * 38 * (1, 2) A cap validation function, and an error handler; 39 * (3, 4) A argument validation function, and an error handler; 40 * (5) A syscall execution function. 41 * 42 * This function returns an item of type "'c", and may also 43 * return an exception if operation (3) above was preempted 44 * by an interrupt. 45 *) 46 47definition 48syscall :: " 49 ('a fault_monad) \<Rightarrow> (unit k_monad) \<Rightarrow> 50 ('a \<Rightarrow> 'b except_monad) \<Rightarrow> (unit k_monad) \<Rightarrow> 51 ('b \<Rightarrow> unit preempt_monad) \<Rightarrow> unit preempt_monad" 52where 53 "syscall 54 cap_decoder_fn decode_error_handler_fn 55 arg_decode_fn arg_error_handler_fn 56 perform_syscall_fn \<equiv> 57 cap_decoder_fn 58 <handle> 59 (\<lambda> _. liftE $ decode_error_handler_fn) 60 <else> 61 (\<lambda> a. ((arg_decode_fn a) 62 <handle> 63 (\<lambda> _. liftE $ arg_error_handler_fn) 64 <else> 65 perform_syscall_fn)) 66 " 67 68fun 69 perform_invocation :: "bool \<Rightarrow> bool \<Rightarrow> cdl_invocation \<Rightarrow> unit preempt_monad" 70where 71 "perform_invocation is_call can_block (InvokeUntyped untyped_params) = (invoke_untyped untyped_params)" 72 | "perform_invocation is_call can_block (InvokeEndpoint endpoint_params) = liftE (invoke_endpoint is_call can_block endpoint_params)" 73 | "perform_invocation is_call can_block (InvokeNotification ntfn_params) = liftE (invoke_notification ntfn_params)" 74 | "perform_invocation is_call can_block (InvokeReply reply_params) = liftE (invoke_reply reply_params)" 75 | "perform_invocation is_call can_block (InvokeTcb tcb_params) = (invoke_tcb tcb_params)" 76 | "perform_invocation is_call can_block (InvokeDomain domain_params) = (invoke_domain domain_params)" 77 | "perform_invocation is_call can_block (InvokeCNode cnode_params) = invoke_cnode cnode_params" 78 | "perform_invocation is_call can_block (InvokeIrqControl irq_params) = liftE (invoke_irq_control irq_params)" 79 | "perform_invocation is_call can_block (InvokeIrqHandler handler_params) = liftE (invoke_irq_handler handler_params)" 80 | "perform_invocation is_call can_block (InvokePageTable page_table_params) = liftE (invoke_page_table page_table_params)" 81 | "perform_invocation is_call can_block (InvokePage page_params) = liftE (invoke_page page_params)" 82 | "perform_invocation is_call can_block (InvokeAsidControl asid_control_params) = liftE (invoke_asid_control asid_control_params)" 83 | "perform_invocation is_call can_block (InvokeAsidPool asid_pool_params) = liftE (invoke_asid_pool asid_pool_params)" 84 | "perform_invocation is_call can_block (InvokePageDirectory page_dir_params) = liftE (invoke_page_directory page_dir_params) " 85 86definition ep_related_cap :: "cdl_cap \<Rightarrow> bool" 87where "ep_related_cap cap \<equiv> case cap of 88 cdl_cap.EndpointCap o_id badge rights \<Rightarrow> True 89| cdl_cap.NotificationCap o_id badge rights \<Rightarrow> True 90| cdl_cap.ReplyCap o_id \<Rightarrow> True 91| _ \<Rightarrow> False" 92 93definition "has_restart_cap \<equiv> \<lambda>tcb_id. do 94 t \<leftarrow> get_thread tcb_id; 95 return ((cdl_tcb_caps t) tcb_pending_op_slot = Some cdl_cap.RestartCap) 96 od" 97 98definition 99 handle_invocation :: "bool \<Rightarrow> bool \<Rightarrow> unit preempt_monad" 100where 101 "handle_invocation is_call can_block \<equiv> 102 doE 103 thread_ptr \<leftarrow> liftE $ gets_the cdl_current_thread; 104 thread \<leftarrow> liftE $ get_thread thread_ptr; 105 full_intent \<leftarrow> returnOk $ cdl_tcb_intent thread; 106 107 intent \<leftarrow> returnOk $ cdl_intent_op full_intent; 108 invoked_cptr \<leftarrow> returnOk $ cdl_intent_cap full_intent; 109 extra_cap_cptrs \<leftarrow> returnOk $ cdl_intent_extras full_intent; 110 111 syscall 112 (* Lookup all caps presented. *) 113 (doE 114 (cap, cap_ref) \<leftarrow> lookup_cap_and_slot thread_ptr invoked_cptr; 115 extra_caps \<leftarrow> lookup_extra_caps thread_ptr extra_cap_cptrs; 116 returnOk (cap, cap_ref, extra_caps) 117 odE) 118 (* If that failed, send off a fault IPC (if we did a blocking operation). *) 119 (when can_block $ handle_fault) 120 121 (* Decode the user's intent. *) 122 (\<lambda> (cap, cap_ref, extra_caps). 123 case intent of 124 None \<Rightarrow> (if ep_related_cap cap then 125 decode_invocation cap cap_ref extra_caps undefined 126 else throw) 127 | Some intent' \<Rightarrow> 128 decode_invocation cap cap_ref extra_caps intent') 129 130 (* If that stuffed up, we do nothing more than corrupt the frames. *) 131 (do corrupt_ipc_buffer thread_ptr True; 132 when is_call (mark_tcb_intent_error thread_ptr True) 133 od) 134 135 (* Invoke the system call. *) 136 (\<lambda> inv. doE 137 liftE $ set_cap (thread_ptr,tcb_pending_op_slot) RestartCap; 138 perform_invocation is_call can_block inv; 139 restart \<leftarrow> liftE $ has_restart_cap thread_ptr; 140 whenE restart $ liftE (do 141 corrupt_ipc_buffer thread_ptr True; 142 when (is_call) (mark_tcb_intent_error thread_ptr False); 143 set_cap (thread_ptr,tcb_pending_op_slot) RunningCap 144 od) 145 odE) 146 odE 147 " 148 149definition 150 handle_recv :: "unit k_monad" 151where 152 "handle_recv \<equiv> 153 do 154 (* Get the current thread. *) 155 tcb_id \<leftarrow> gets_the cdl_current_thread; 156 tcb \<leftarrow> get_thread tcb_id; 157 (* Get the endpoint it is trying to receive from. *) 158 (doE 159 ep_cptr \<leftarrow> returnOk $ cdl_intent_cap (cdl_tcb_intent tcb); 160 ep_cap \<leftarrow> lookup_cap tcb_id ep_cptr; 161 (case ep_cap of 162 EndpointCap o_id badge rights \<Rightarrow> 163 if Read \<in> rights then 164 (liftE $ do 165 delete_cap_simple (tcb_id, tcb_caller_slot); 166 receive_ipc tcb_id (cap_object ep_cap) 167 od) \<sqinter> throw 168 else 169 throw 170 | NotificationCap o_id badge rights \<Rightarrow> 171 if Read \<in> rights then 172 (liftE $ recv_signal tcb_id ep_cap) \<sqinter> throw 173 else 174 throw 175 | _ \<Rightarrow> 176 throw) 177 odE) 178 <catch> 179 (\<lambda> _. handle_fault) 180 od 181 " 182 183definition 184 handle_reply :: "unit k_monad" 185where 186 "handle_reply \<equiv> 187 do 188 tcb_id \<leftarrow> gets_the cdl_current_thread; 189 caller_cap \<leftarrow> get_cap (tcb_id, tcb_caller_slot); 190 191 case caller_cap of 192 ReplyCap target \<Rightarrow> do_reply_transfer tcb_id target (tcb_id, tcb_caller_slot) 193 | NullCap \<Rightarrow> return () 194 | _ \<Rightarrow> fail 195 od 196 " 197 198definition handle_hypervisor_fault :: "unit k_monad" 199where "handle_hypervisor_fault \<equiv> return ()" 200 201definition 202 handle_syscall :: "syscall \<Rightarrow> unit preempt_monad" 203where 204 "handle_syscall sys \<equiv> 205 case sys of 206 SysSend \<Rightarrow> handle_invocation False True 207 | SysNBSend \<Rightarrow> handle_invocation False False 208 | SysCall \<Rightarrow> handle_invocation True True 209 | SysRecv \<Rightarrow> liftE $ handle_recv 210 | SysYield \<Rightarrow> returnOk () 211 | SysReply \<Rightarrow> liftE $ handle_reply 212 | SysReplyRecv \<Rightarrow> liftE $ do 213 handle_reply; 214 handle_recv 215 od 216 | SysNBRecv \<Rightarrow> liftE $ handle_recv" 217 218definition 219 handle_event :: "event \<Rightarrow> unit preempt_monad" 220where 221 "handle_event ev \<equiv> case ev of 222 SyscallEvent sys \<Rightarrow> handle_syscall sys 223 | UnknownSyscall n \<Rightarrow> liftE $ handle_fault 224 | UserLevelFault a b \<Rightarrow> liftE $ handle_fault 225 | VMFaultEvent c \<Rightarrow> liftE $ handle_fault 226 | Interrupt \<Rightarrow> liftE $ handle_pending_interrupts 227 | HypervisorEvent w \<Rightarrow> liftE $ handle_hypervisor_fault 228 " 229 230definition 231 call_kernel :: "event \<Rightarrow> unit k_monad" 232where 233 "call_kernel ev \<equiv> 234 do 235 (* Deal with the event. *) 236 handle_event ev 237 <handle> (\<lambda> _. liftE handle_pending_interrupts); 238 schedule; 239 t \<leftarrow> gets cdl_current_thread; 240 case t of Some thread \<Rightarrow> do 241 restart \<leftarrow> has_restart_cap thread; 242 when restart $ set_cap (thread, tcb_pending_op_slot) RunningCap 243 od | None \<Rightarrow> return () 244 od" 245 246end 247