1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7(* 8Top-level system call interface. 9*) 10 11chapter "System Calls" 12 13theory Syscall_A 14imports 15 "ExecSpec.Event_H" 16 Decode_A 17 Init_A 18 Hypervisor_A 19begin 20 21context begin interpretation Arch . 22 23requalify_consts 24 arch_perform_invocation 25 handle_vm_fault 26 handle_hypervisor_fault 27end 28 29 30text\<open> 31\label{c:syscall} 32 33This theory defines the entry point to the kernel, @{term 34call_kernel}, which is called by the assembly stubs after 35switching into kernel mode and saving registers. 36There are five kinds of events that end up in a switch to 37kernel mode. These events are described by the enumerated type @{term 38event}, defined in \autoref{sec:Event_H}. One of the five events is an 39actual system call by the user, the other four are related to faults 40and interrupts. There are seven different kinds of user system calls, 41described by the enumerated type @{term syscall}, also defined in 42\autoref{sec:Event_H}. 43 44The @{text call_kernel} function delegates the event-specific behaviour 45to @{text handle_event} which in turn further dispatches to system-call 46specific handler functions. 47 48In particular, two of the system calls, namely @{term SysSend} and 49@{term SysCall}, correspond to a method invocation on capabilities. 50They are handled in the @{term handle_invocation} operation, which is 51made up of 52three phases: first checking if the caller has the capabilities to 53perform the operation, then decoding the arguments received from the 54user (using the @{term decode_invocation} operation), and finally 55actually performing the invocation (using the @{term 56perform_invocation}). These three phases are wrapped into a more 57generic @{term syscall} framework function described below. 58\<close> 59 60 61section \<open>Generic system call structure\label{s:spec_syscall}\<close> 62 63 64text\<open>The @{term syscall} operation generically describes the usual 65execution of system calls in three phases, where the first phase may 66result in a fault, the second phase may result in an error and the third 67phase may be interrupted. The first two phases are used for argument decoding 68and checking. The last phase commits and executes the system call. 69 70The @{term syscall} operation has five arguments: 71\begin{itemize} 72\item the first operation @{text m_fault} to execute, that may 73result in a fault; 74\item the fault handler @{text h_fault} to execute if the first 75operation resulted in a fault; 76\item the second operation @{text m_error} to execute (if no fault 77occurred in the first operation); this second operation may result in 78an error; 79\item the error handler @{text h_error} to execute if the second 80operation resulted in an error; 81\item the third and last operation @{text m_finalise} to execute (if 82no error occurred in the second operation); this operation may be 83interrupted. 84\end{itemize} 85\<close> 86 87definition 88 syscall :: "('a,'z::state_ext) f_monad 89 \<Rightarrow> (fault \<Rightarrow> ('c,'z::state_ext) s_monad) 90 \<Rightarrow> ('a \<Rightarrow> ('b,'z::state_ext) se_monad) 91 \<Rightarrow> (syscall_error \<Rightarrow> ('c,'z::state_ext) s_monad) 92 \<Rightarrow> ('b \<Rightarrow> ('c,'z::state_ext) p_monad) \<Rightarrow> ('c,'z::state_ext) p_monad" 93where 94"syscall m_fault h_fault m_error h_error m_finalise \<equiv> doE 95 r_fault \<leftarrow> without_preemption $ m_fault; 96 case r_fault of 97 Inl f \<Rightarrow> without_preemption $ h_fault f 98 | Inr a \<Rightarrow> doE 99 r_error \<leftarrow> without_preemption $ m_error a; 100 case r_error of 101 Inl e \<Rightarrow> without_preemption $ h_error e 102 | Inr b \<Rightarrow> m_finalise b 103 odE 104odE" 105 106 107section \<open>System call entry point\<close> 108 109text\<open>The kernel user can perform seven kinds of system calls, 110described by the enumerated type @{term syscall}, defined in \autoref{s:spec_syscall}. 111These seven system calls can be categorised into two broad 112families: sending messages and receiving messages, the two main 113services provided by the kernel. 114 115The usual case for sending messages (@{text Send} event) consists of the user 116sending a message to an object, without expecting any answer. The sender is 117blocked until the receiver is waiting to receive. In case the 118receiver is not trusted, an explicit non-blocking send operation can 119be used (@{text NBSend} event). If a reply is requested from the 120receiver, the Call operation can be used (@{text Call} event). The Call operation 121will automatically provide a @{text Reply} capability to the receiver. 122 123All three sending operations are handled by the @{text 124handle_invocation} operation, which takes two boolean arguments, one 125to indicate if a reply is requested and the other to indicate if the 126send is blocking or not. 127 128The other direction is the reception of messages. This is done by 129performing a Recv operation on an endpoint kernel object. The receiver 130is then blocked until a sender performs a Send operation on the 131endpoint object, resulting in a message transfer between the sender 132and the receiver. The receiver may also perform a Reply operation 133(@{text Reply} event) in response to a @{text Call}, which is always 134non-blocking. When the receiver is a user-level server, it generally 135runs a loop waiting for messages. On handling a received message, the 136server will send a reply and then return to waiting. To avoid 137excessive switching between user and kernel mode, the kernel provides 138a ReplyRecv operation, which is simply a Reply followed by Recv. 139 140Finally, the last event, @{text Yield}, enables the user to donate its 141remaining timeslice.\<close> 142 143text\<open>The invocation is made up of three phases. The first phase 144corresponds to a lookup of capabilities to check that the invocation 145is valid. This phase can result in a fault if a given CSpace address 146is invalid (see the function @{text "resolve_address_bits"}). The 147second phase is the decoding of the arguments given by the user. This 148is handled by the @{text decode_invocation} operation. This operation 149can result in an error if, for example, the number of arguments is 150less than required by the operation, or if some argument capability 151has the wrong type. Finally, the actual invocation is performed, using 152the @{text perform_invocation} function. Note that this last phase is 153preemptable. 154\<close> 155 156fun 157 perform_invocation :: "bool \<Rightarrow> bool \<Rightarrow> invocation \<Rightarrow> (data list,'z::state_ext) p_monad" 158where 159 "perform_invocation block call (InvokeUntyped i) = 160 doE 161 invoke_untyped i; 162 returnOk [] 163 odE" 164 165| "perform_invocation block call (InvokeEndpoint ep badge canGrant canGrantReply) = 166 (without_preemption $ do 167 thread \<leftarrow> gets cur_thread; 168 send_ipc block call badge canGrant canGrantReply thread ep; 169 return [] 170 od)" 171 172| "perform_invocation block call (InvokeNotification ep badge) = 173 doE 174 without_preemption $ send_signal ep badge; 175 returnOk [] 176 odE" 177 178| "perform_invocation block call (InvokeTCB i) = invoke_tcb i" 179 180| "perform_invocation block call (InvokeDomain tptr d) = invoke_domain tptr d" 181 182| "perform_invocation block call (InvokeReply thread slot grant) = 183 liftE (do 184 sender \<leftarrow> gets cur_thread; 185 do_reply_transfer sender thread slot grant; 186 return [] 187 od)" 188 189| "perform_invocation block call (InvokeCNode i) = 190 doE 191 invoke_cnode i; 192 returnOk [] 193 odE" 194 195| "perform_invocation block call (InvokeIRQControl i) = 196 doE 197 invoke_irq_control i; 198 returnOk [] 199 odE" 200 201| "perform_invocation block call (InvokeIRQHandler i) = 202 doE 203 liftE $ invoke_irq_handler i; 204 returnOk [] 205 odE" 206 207| "perform_invocation block call (InvokeArchObject i) = 208 arch_perform_invocation i" 209 210 211definition 212 handle_invocation :: "bool \<Rightarrow> bool \<Rightarrow> (unit,'z::state_ext) p_monad" 213where 214 "handle_invocation calling blocking \<equiv> doE 215 thread \<leftarrow> liftE $ gets cur_thread; 216 info \<leftarrow> without_preemption $ get_message_info thread; 217 ptr \<leftarrow> without_preemption $ liftM data_to_cptr $ 218 as_user thread $ getRegister cap_register; 219 syscall 220 (doE 221 (cap, slot) \<leftarrow> cap_fault_on_failure (of_bl ptr) False $ 222 lookup_cap_and_slot thread ptr; 223 buffer \<leftarrow> liftE $ lookup_ipc_buffer False thread; 224 extracaps \<leftarrow> lookup_extra_caps thread buffer info; 225 returnOk (slot, cap, extracaps, buffer) 226 odE) 227 (\<lambda>fault. when blocking $ handle_fault thread fault) 228 (\<lambda>(slot,cap,extracaps,buffer). doE 229 args \<leftarrow> liftE $ get_mrs thread buffer info; 230 decode_invocation (mi_label info) args ptr slot cap extracaps 231 odE) 232 (\<lambda>err. when calling $ 233 reply_from_kernel thread $ msg_from_syscall_error err) 234 (\<lambda>oper. doE 235 without_preemption $ set_thread_state thread Restart; 236 reply \<leftarrow> perform_invocation blocking calling oper; 237 without_preemption $ do 238 state \<leftarrow> get_thread_state thread; 239 case state of 240 Restart \<Rightarrow> do 241 when calling $ 242 reply_from_kernel thread (0, reply); 243 set_thread_state thread Running 244 od 245 | _ \<Rightarrow> return () 246 od 247 odE) 248 odE" 249 250 251definition 252 handle_yield :: "(unit,'z::state_ext) s_monad" where 253 "handle_yield \<equiv> do 254 thread \<leftarrow> gets cur_thread; 255 do_extended_op (tcb_sched_action (tcb_sched_dequeue) thread); 256 do_extended_op (tcb_sched_action (tcb_sched_append) thread); 257 do_extended_op (reschedule_required) 258 od" 259 260definition 261 handle_send :: "bool \<Rightarrow> (unit,'z::state_ext) p_monad" where 262 "handle_send bl \<equiv> handle_invocation False bl" 263 264definition 265 handle_call :: "(unit,'z::state_ext) p_monad" where 266 "handle_call \<equiv> handle_invocation True True" 267 268definition 269 delete_caller_cap :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where 270 "delete_caller_cap t \<equiv> cap_delete_one (t, tcb_cnode_index 3)" 271 272definition 273 handle_recv :: "bool \<Rightarrow> (unit,'z::state_ext) s_monad" where 274 "handle_recv is_blocking \<equiv> do 275 thread \<leftarrow> gets cur_thread; 276 277 ep_cptr \<leftarrow> liftM data_to_cptr $ as_user thread $ 278 getRegister cap_register; 279 280 (cap_fault_on_failure (of_bl ep_cptr) True $ doE 281 ep_cap \<leftarrow> lookup_cap thread ep_cptr; 282 283 let flt = (throwError $ MissingCapability 0) 284 in 285 case ep_cap 286 of EndpointCap ref badge rights \<Rightarrow> 287 (if AllowRecv \<in> rights 288 then liftE $ do 289 delete_caller_cap thread; 290 receive_ipc thread ep_cap is_blocking 291 od 292 else flt) 293 | NotificationCap ref badge rights \<Rightarrow> 294 (if AllowRecv \<in> rights 295 then doE 296 ntfn \<leftarrow> liftE $ get_notification ref; 297 boundTCB \<leftarrow> returnOk $ ntfn_bound_tcb ntfn; 298 if boundTCB = Some thread \<or> boundTCB = None 299 then liftE $ receive_signal thread ep_cap is_blocking 300 else flt 301 odE 302 else flt) 303 | _ \<Rightarrow> flt 304 odE) 305 <catch> handle_fault thread 306 od" 307 308definition 309 handle_reply :: "(unit,'z::state_ext) s_monad" where 310 "handle_reply \<equiv> do 311 thread \<leftarrow> gets cur_thread; 312 caller_cap \<leftarrow> get_cap (thread, tcb_cnode_index 3); 313 case caller_cap of 314 ReplyCap caller False R \<Rightarrow> 315 do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) 316 | NullCap \<Rightarrow> return () 317 | _ \<Rightarrow> fail 318 od" 319 320 321section \<open>Top-level event handling\<close> 322 323fun 324 handle_event :: "event \<Rightarrow> (unit,'z::state_ext) p_monad" 325where 326 "handle_event (SyscallEvent call) = 327 (case call of 328 SysSend \<Rightarrow> handle_send True 329 | SysNBSend \<Rightarrow> handle_send False 330 | SysCall \<Rightarrow> handle_call 331 | SysRecv \<Rightarrow> without_preemption $ handle_recv True 332 | SysYield \<Rightarrow> without_preemption handle_yield 333 | SysReply \<Rightarrow> without_preemption handle_reply 334 | SysReplyRecv \<Rightarrow> without_preemption $ do 335 handle_reply; 336 handle_recv True 337 od 338 | SysNBRecv \<Rightarrow> without_preemption $ handle_recv False)" 339 340| "handle_event (UnknownSyscall n) = (without_preemption $ do 341 thread \<leftarrow> gets cur_thread; 342 handle_fault thread $ UnknownSyscallException $ of_nat n; 343 return () 344 od)" 345 346| "handle_event (UserLevelFault w1 w2) = (without_preemption $ do 347 thread \<leftarrow> gets cur_thread; 348 handle_fault thread $ UserException (w1 && mask 32) (w2 && mask 28); 349 return () 350 od)" 351 352| "handle_event Interrupt = (without_preemption $ do 353 active \<leftarrow> do_machine_op $ getActiveIRQ False; 354 case active of 355 Some irq \<Rightarrow> handle_interrupt irq 356 | None \<Rightarrow> return () 357 od)" 358 359| "handle_event (VMFaultEvent fault_type) = (without_preemption $ do 360 thread \<leftarrow> gets cur_thread; 361 handle_vm_fault thread fault_type <catch> handle_fault thread; 362 return () 363 od)" 364 365| "handle_event (HypervisorEvent hypfault_type) = (without_preemption $ do 366 thread \<leftarrow> gets cur_thread; 367 handle_hypervisor_fault thread hypfault_type 368 od)" 369 370 371section \<open>Kernel entry point\<close> 372 373text \<open> 374 This function is the main kernel entry point. The main event loop of the 375 kernel handles events, handles a potential preemption interrupt, schedules 376 and switches back to the active thread. 377\<close> 378 379definition 380 call_kernel :: "event \<Rightarrow> (unit,'z::state_ext_sched) s_monad" where 381 "call_kernel ev \<equiv> do 382 handle_event ev <handle> 383 (\<lambda>_. without_preemption $ do 384 irq \<leftarrow> do_machine_op $ getActiveIRQ True; 385 when (irq \<noteq> None) $ handle_interrupt (the irq) 386 od); 387 schedule; 388 activate_thread 389 od" 390 391end 392