-
Notifications
You must be signed in to change notification settings - Fork 108
/
Ipc_SA.thy
39 lines (29 loc) · 1.15 KB
/
Ipc_SA.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: GPL-2.0-only
*)
(*
Specification of Inter-Process Communication.
*)
chapter "IPC"
theory Ipc_SA
imports "ASpec.Syscall_A"
begin
section \<open>Asynchronous Message Transfers\<close>
text \<open>
\texttt{handle_fault} in \texttt{sep-abstract} always sets the thread state to
\texttt{Inactive}. This is the same behaviour as \texttt{handle_double_fault} in the abstract
specification.
The two \texttt{handle_fault}s have the same behaviour under restricted capabilities because in
the abstract specification \texttt{handle_fault} will call \texttt{handle_double_fault} in all
cases except when the thread has an \texttt{EndpointCap}. Since \texttt{EndpointCap} is not part
of the restricted capabilities their behaviour is the same. This means, the system assumes
fully static virtual memory and no dynamic paging of any kind.
Faulting threads will be disabled by the kernel.
\<close>
definition
handle_fault :: "obj_ref \<Rightarrow> fault \<Rightarrow> (unit,'z::state_ext) s_monad"
where
"handle_fault tptr ex \<equiv> set_thread_state tptr Inactive"
end