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(* 12Specification of Inter-Process Communication. 13*) 14 15chapter "IPC" 16 17theory Ipc_SA 18imports "ASpec.Syscall_A" 19begin 20 21 22section {* Asynchronous Message Transfers *} 23 24text {* 25 26 \texttt{handle_fault} in \texttt{sep-abstract} always sets the thread state to 27 \texttt{Inactive}. This is the same behaviour as \texttt{handle_double_fault} in the abstract 28 specification. 29 30 The two \texttt{handle_fault}s have the same behaviour under restricted capabilities because in 31 the abstract specification \texttt{handle_fault} will call \texttt{handle_double_fault} in all 32 cases except when the thread has an \texttt{EndpointCap}. Since \texttt{EndpointCap} is not part 33 of the restricted capabilities their behaviour is the same. This means, the system assumes 34 fully static virtual memory and no dynamic paging of any kind. 35 Faulting threads will be disabled by the kernel. 36*} 37 38definition 39 handle_fault :: "obj_ref \<Rightarrow> fault \<Rightarrow> (unit,'z::state_ext) s_monad" 40where 41 "handle_fault tptr ex \<equiv> set_thread_state tptr Inactive" 42 43end 44