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