1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6
7(*
8The TCB and thread related specifications.
9*)
10
11chapter "Threads and TCBs"
12
13theory Tcb_A
14imports TcbAcc_A Schedule_A ArchTcb_A
15begin
16
17context begin interpretation Arch .
18
19requalify_consts
20  arch_activate_idle_thread
21  sanitise_register
22  arch_get_sanitise_register_info
23  arch_post_modify_registers
24
25end
26
27section "Activating Threads"
28
29text \<open>Threads that are active always have a master Reply capability to
30themselves stored in their reply slot. This is so that a derived Reply
31capability can be generated immediately if they wish to issue one. This function
32sets up a new master Reply capability if one does not exist.\<close>
33definition
34  "setup_reply_master thread \<equiv> do
35     old_cap <- get_cap (thread, tcb_cnode_index 2);
36     when (old_cap = NullCap) $ do
37         set_original (thread, tcb_cnode_index 2) True;
38         set_cap (ReplyCap thread True {AllowGrant, AllowWrite}) (thread, tcb_cnode_index 2)
39     od
40  od"
41
42text \<open>Reactivate a thread if it is not already running.\<close>
43definition
44  restart :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
45 "restart thread \<equiv> do
46    state \<leftarrow> get_thread_state thread;
47    when (\<not> runnable state \<and> \<not> idle state) $ do
48      cancel_ipc thread;
49      setup_reply_master thread;
50      set_thread_state thread Restart;
51      do_extended_op (tcb_sched_action (tcb_sched_enqueue) thread);
52      do_extended_op (possible_switch_to thread)
53    od
54  od"
55
56text \<open>This action is performed at the end of a system call immediately before
57control is restored to a used thread. If it needs to be restarted then its
58program counter is set to the operation it was performing rather than the next
59operation. The idle thread is handled specially.\<close>
60definition
61  activate_thread :: "(unit,'z::state_ext) s_monad" where
62  "activate_thread \<equiv> do
63     thread \<leftarrow> gets cur_thread;
64     state \<leftarrow> get_thread_state thread;
65     (case state
66       of Running \<Rightarrow> return ()
67        | Restart \<Rightarrow> (do
68            pc \<leftarrow> as_user thread getRestartPC;
69            as_user thread $ setNextPC pc;
70            set_thread_state thread Running
71          od)
72        | IdleThreadState \<Rightarrow> arch_activate_idle_thread thread
73        | _ \<Rightarrow> fail)
74   od"
75
76section "Thread Message Formats"
77
78definition
79  load_word_offs :: "obj_ref \<Rightarrow> nat \<Rightarrow> (machine_word,'z::state_ext) s_monad" where
80 "load_word_offs ptr offs \<equiv>
81    do_machine_op $ loadWord (ptr + of_nat (offs * word_size))"
82definition
83  load_word_offs_word :: "obj_ref \<Rightarrow> data \<Rightarrow> (machine_word,'z::state_ext) s_monad" where
84 "load_word_offs_word ptr offs \<equiv>
85    do_machine_op $ loadWord (ptr + (offs * word_size))"
86
87text \<open>Copy message registers from one thread to another.\<close>
88definition
89  copy_mrs :: "obj_ref \<Rightarrow> obj_ref option \<Rightarrow> obj_ref \<Rightarrow>
90               obj_ref option \<Rightarrow> length_type \<Rightarrow> (length_type,'z::state_ext) s_monad" where
91  "copy_mrs sender sbuf receiver rbuf n \<equiv>
92   do
93     hardware_mrs \<leftarrow> return $ take (unat n) msg_registers;
94     mapM (\<lambda>r. do
95         v \<leftarrow> as_user sender $ getRegister r;
96         as_user receiver $ setRegister r v
97       od) hardware_mrs;
98     buf_mrs \<leftarrow> case (sbuf, rbuf) of
99       (Some sb_ptr, Some rb_ptr) \<Rightarrow> mapM (\<lambda>x. do
100                                       v \<leftarrow> load_word_offs sb_ptr x;
101                                       store_word_offs rb_ptr x v
102                                     od)
103               [length msg_registers + 1 ..< Suc (unat n)]
104     | _ \<Rightarrow> return [];
105     return $ min n $ nat_to_len $ length hardware_mrs + length buf_mrs
106   od"
107
108text \<open>The ctable and vtable slots of the TCB.\<close>
109definition
110  get_tcb_ctable_ptr :: "obj_ref \<Rightarrow> cslot_ptr" where
111  "get_tcb_ctable_ptr tcb_ref \<equiv> (tcb_ref, tcb_cnode_index 0)"
112
113definition
114  get_tcb_vtable_ptr :: "obj_ref \<Rightarrow> cslot_ptr" where
115  "get_tcb_vtable_ptr tcb_ref \<equiv> (tcb_ref, tcb_cnode_index 1)"
116
117text \<open>Optionally update the tcb at an address.\<close>
118definition
119  option_update_thread :: "obj_ref \<Rightarrow> ('a \<Rightarrow> tcb \<Rightarrow> tcb) \<Rightarrow> 'a option \<Rightarrow> (unit,'z::state_ext) s_monad" where
120 "option_update_thread thread fn \<equiv> case_option (return ()) (\<lambda>v. thread_set (fn v) thread)"
121
122text \<open>Check that a related capability is at an address. This is done before
123calling @{const cap_insert} to avoid a corner case where the would-be parent of
124the cap to be inserted has been moved or deleted.\<close>
125definition
126  check_cap_at :: "cap \<Rightarrow> cslot_ptr \<Rightarrow> (unit,'z::state_ext) s_monad \<Rightarrow> (unit,'z::state_ext) s_monad" where
127 "check_cap_at cap slot m \<equiv> do
128    cap' \<leftarrow> get_cap slot;
129    when (same_object_as cap cap') m
130  od"
131
132
133text \<open>Helper function for binding notifications\<close>
134definition
135  bind_notification :: "obj_ref \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad"
136where
137  "bind_notification tcbptr ntfnptr \<equiv> do
138     ntfn \<leftarrow> get_notification ntfnptr;
139     ntfn' \<leftarrow> return $ ntfn_set_bound_tcb ntfn (Some tcbptr);
140     set_notification ntfnptr ntfn';
141     set_bound_notification tcbptr $ Some ntfnptr
142   od"
143
144text \<open>TCB capabilities confer authority to perform seven actions. A thread can
145request to yield its timeslice to another, to suspend or resume another, to
146reconfigure another thread, or to copy register sets into, out of or between
147other threads.\<close>
148fun
149  invoke_tcb :: "tcb_invocation \<Rightarrow> (data list,'z::state_ext) p_monad"
150where
151  "invoke_tcb (Suspend thread) = liftE (do suspend thread; return [] od)"
152| "invoke_tcb (Resume thread) = liftE (do restart thread; return [] od)"
153
154| "invoke_tcb (ThreadControl target slot faultep mcp priority croot vroot buffer)
155   = doE
156    liftE $ option_update_thread target (tcb_fault_handler_update o K) faultep;
157    liftE $  case mcp of None \<Rightarrow> return()
158     | Some (newmcp, _) \<Rightarrow> set_mcpriority target newmcp;
159    (case croot of None \<Rightarrow> returnOk ()
160     | Some (new_cap, src_slot) \<Rightarrow> doE
161      cap_delete (target, tcb_cnode_index 0);
162      liftE $ check_cap_at new_cap src_slot
163            $ check_cap_at (ThreadCap target) slot
164            $ cap_insert new_cap src_slot (target, tcb_cnode_index 0)
165    odE);
166    (case vroot of None \<Rightarrow> returnOk ()
167     | Some (new_cap, src_slot) \<Rightarrow> doE
168      cap_delete (target, tcb_cnode_index 1);
169      liftE $ check_cap_at new_cap src_slot
170            $ check_cap_at (ThreadCap target) slot
171            $ cap_insert new_cap src_slot (target, tcb_cnode_index 1)
172    odE);
173    (case buffer of None \<Rightarrow> returnOk ()
174     | Some (ptr, frame) \<Rightarrow> doE
175      cap_delete (target, tcb_cnode_index 4);
176      liftE $ thread_set (\<lambda>t. t \<lparr> tcb_ipc_buffer := ptr \<rparr>) target;
177      liftE $ case frame of None \<Rightarrow> return ()
178       | Some (new_cap, src_slot) \<Rightarrow>
179            check_cap_at new_cap src_slot
180          $ check_cap_at (ThreadCap target) slot
181          $ cap_insert new_cap src_slot (target, tcb_cnode_index 4);
182      cur \<leftarrow> liftE $ gets cur_thread;
183      liftE $ when (target = cur) (do_extended_op reschedule_required)
184    odE);
185    liftE $ case priority
186              of None \<Rightarrow> return()
187               | Some (prio, _) \<Rightarrow> do_extended_op (set_priority target prio);
188    returnOk []
189  odE"
190
191| "invoke_tcb (CopyRegisters dest src suspend_source resume_target transfer_frame transfer_integer transfer_arch) =
192  (liftE $ do
193    when suspend_source $ suspend src;
194    when resume_target $ restart dest;
195    when transfer_frame $ do
196        mapM_x (\<lambda>r. do
197                v \<leftarrow> as_user src $ getRegister r;
198                as_user dest $ setRegister r v
199        od) frame_registers;
200        pc \<leftarrow> as_user dest getRestartPC;
201        as_user dest $ setNextPC pc
202    od;
203    when transfer_integer $
204        mapM_x (\<lambda>r. do
205                v \<leftarrow> as_user src $ getRegister r;
206                as_user dest $ setRegister r v
207        od) gpRegisters;
208    cur \<leftarrow> gets cur_thread;
209    arch_post_modify_registers cur dest;
210    when (dest = cur) (do_extended_op reschedule_required);
211    return []
212  od)"
213
214| "invoke_tcb (ReadRegisters src suspend_source n arch) =
215  (liftE $ do
216    when suspend_source $ suspend src;
217    self \<leftarrow> gets cur_thread;
218    regs \<leftarrow> return (take (unat n) $ frame_registers @ gp_registers);
219    as_user src $ mapM getRegister regs
220  od)"
221
222| "invoke_tcb (WriteRegisters dest resume_target values arch) =
223  (liftE $ do
224    self \<leftarrow> gets cur_thread;
225    b \<leftarrow> arch_get_sanitise_register_info dest;
226    as_user dest $ do
227        zipWithM (\<lambda>r v. setRegister r (sanitise_register b r v))
228            (frameRegisters @ gpRegisters) values;
229        pc \<leftarrow> getRestartPC;
230        setNextPC pc
231    od;
232    arch_post_modify_registers self dest;
233    when resume_target $ restart dest;
234    when (dest = self) (do_extended_op reschedule_required);
235    return []
236  od)"
237
238| "invoke_tcb (NotificationControl tcb (Some ntfnptr)) =
239  (liftE $ do
240    bind_notification tcb ntfnptr;
241    return []
242  od)"
243
244| "invoke_tcb (NotificationControl tcb None) =
245  (liftE $ do
246    unbind_notification tcb;
247    return []
248  od)"
249
250| "invoke_tcb (SetTLSBase tcb tls_base) =
251  (liftE $ do
252    as_user tcb $ setRegister tlsBaseRegister tls_base;
253    cur \<leftarrow> gets cur_thread;
254    when (tcb = cur) (do_extended_op reschedule_required);
255    return []
256  od)"
257
258definition
259  set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> unit det_ext_monad" where
260  "set_domain tptr new_dom \<equiv> do
261     cur \<leftarrow> gets cur_thread;
262     tcb_sched_action tcb_sched_dequeue tptr;
263     thread_set_domain tptr new_dom;
264     ts \<leftarrow> get_thread_state tptr;
265     when (runnable ts) (tcb_sched_action tcb_sched_enqueue tptr);
266     when (tptr = cur) reschedule_required
267   od"
268
269definition invoke_domain:: "obj_ref \<Rightarrow> domain \<Rightarrow> (data list,'z::state_ext) p_monad"
270where
271  "invoke_domain thread domain \<equiv>
272     liftE (do do_extended_op (set_domain thread domain); return [] od)"
273
274text \<open>Get all of the message registers, both from the sending thread's current
275register file and its IPC buffer.\<close>
276definition
277  get_mrs :: "obj_ref \<Rightarrow> obj_ref option \<Rightarrow> message_info \<Rightarrow>
278              (message list,'z::state_ext) s_monad" where
279  "get_mrs thread buf info \<equiv> do
280     context \<leftarrow> thread_get (arch_tcb_get_registers o tcb_arch) thread;
281     cpu_mrs \<leftarrow> return (map context msg_registers);
282     buf_mrs \<leftarrow> case buf
283       of None      \<Rightarrow> return []
284        | Some pptr \<Rightarrow> mapM (\<lambda>x. load_word_offs pptr x)
285               [length msg_registers + 1 ..< Suc msg_max_length];
286     return (take (unat (mi_length info)) $ cpu_mrs @ buf_mrs)
287   od"
288
289end
290