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
11theory StartThreads_SI
12imports
13  InitTCB_SI
14begin
15
16lemma is_waiting_thread_is_tcb [simp]:
17  "\<lbrakk>cdl_objects spec obj_id = Some obj; is_waiting_thread obj\<rbrakk>
18  \<Longrightarrow> is_tcb obj"
19  by (clarsimp simp: is_waiting_thread_def)
20
21lemma is_waiting_thread_at_tcb_at [simp]:
22  "is_waiting_thread_at obj_id spec \<Longrightarrow> tcb_at obj_id spec"
23  by (clarsimp simp: object_at_def is_waiting_thread_def)
24
25lemma is_waiting_thread_at_real_object_at [simp]:
26  "\<lbrakk>well_formed spec; is_waiting_thread_at obj_id spec\<rbrakk> \<Longrightarrow> real_object_at obj_id spec"
27  by (metis is_waiting_thread_at_tcb_at real_object_not_irq_node(2))
28
29lemma is_waiting_thread_tcb_at [simp]:
30  "(tcb_at obj_id spec \<and> object_at is_waiting_thread obj_id spec) = object_at is_waiting_thread obj_id spec"
31  by fastforce
32
33lemma is_waiting_thread_opt_cap_tcb_pending_op_slot [simp]:
34  "\<lbrakk>cdl_objects spec obj_id = Some obj; is_waiting_thread obj\<rbrakk>
35  \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) spec = Some RestartCap"
36  by (clarsimp simp: is_waiting_thread_def opt_cap_def slots_of_def opt_object_def)
37
38
39lemma is_waiting_thread_opt_cap_tcb_replycap_slot [simp]:
40  "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj; is_waiting_thread obj\<rbrakk>
41  \<Longrightarrow> opt_cap (obj_id, tcb_replycap_slot) spec = Some (MasterReplyCap obj_id)"
42  apply (frule well_formed_tcb_pending_op_replycap [where obj_id=obj_id], simp add: object_at_def)
43  apply (clarsimp simp: is_waiting_thread_def opt_cap_def slots_of_def opt_object_def)
44  done
45
46lemma is_waiting_thread_opt_cap_tcb_boundntfn_slot[simp]:
47  "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj; is_waiting_thread obj\<rbrakk>
48  \<Longrightarrow> opt_cap (obj_id, tcb_boundntfn_slot) spec = Some NullCap"
49  apply (clarsimp simp: is_waiting_thread_def opt_cap_def slots_of_def opt_object_def)
50  apply (frule well_formed_tcb_boundntfn_cap [where obj_id=obj_id], simp add: object_at_def)
51  by (clarsimp simp: is_waiting_thread_def opt_cap_def slots_of_def opt_object_def)
52
53lemma cap_transform_RestartCap [simp]:
54  "cap_transform t RestartCap = RestartCap"
55  by (clarsimp simp: cap_transform_def cap_type_def update_cap_object_def)
56
57lemma cap_type_MasterReplyCap [simp]:
58  "cap_type (MasterReplyCap obj_id) = None"
59  by (simp add: cap_type_def)
60
61lemma cap_transform_MasterReplyCap:
62  "\<lbrakk>t obj_id = Some k_obj_id\<rbrakk>
63  \<Longrightarrow> cap_transform t (MasterReplyCap obj_id) = MasterReplyCap k_obj_id"
64  apply (frule cap_transform_update_cap_object [where cap="MasterReplyCap obj_id"], simp+)
65  apply (clarsimp simp: cap_transform_def cap_object_def update_cap_object_def)
66  done
67
68
69
70lemma start_thread_sep:
71  "\<lbrace>\<guillemotleft>tcb_half_initialised spec t obj_id \<and>*
72     si_cap_at t dup_caps spec False obj_id \<and>*
73     si_objects \<and>* R\<guillemotright> and
74   K(well_formed spec \<and> obj_id \<in> {obj_id. is_waiting_thread_at obj_id spec})\<rbrace>
75   start_thread spec dup_caps obj_id
76   \<lbrace>\<lambda>_.\<guillemotleft>object_initialised spec t obj_id \<and>*
77        si_cap_at t dup_caps spec False obj_id \<and>*
78        si_objects \<and>* R\<guillemotright>\<rbrace>"
79  apply (rule hoare_gen_asm)
80  apply (clarsimp simp: start_thread_def object_initialised_def tcb_half_initialised_def object_initialised_general_def
81                        si_cap_at_def si_objects_def sep_conj_exists)
82  apply (rule hoare_vcg_ex_lift | rule hoare_grab_asm | simp)+
83  apply (subst tcb_half_decomp, (simp add: object_at_def)+)+
84  apply (subst tcb_decomp, (simp add: object_at_def)+)+
85  apply (wp add: hoare_drop_imps
86         sep_wp: seL4_TCB_Resume_wp
87         [where root_tcb = root_tcb
88            and cnode_cap = si_cspace_cap
89            and root_size = si_cnode_size
90            and tcb_cap = "TcbCap (the (t obj_id))"] |
91         simp add: guard_equal_si_cspace_cap' cap_object_simps is_tcb_default_cap)+
92  apply (subst offset_slot_si_cnode_size', assumption)+
93  apply (clarsimp simp: cap_transform_MasterReplyCap)
94  by sep_solve
95
96
97lemma tcb_half_id:
98  "\<lbrakk>well_formed spec; is_tcb object; \<not> is_waiting_thread object;
99    cdl_objects spec obj_id = Some object\<rbrakk>
100  \<Longrightarrow> tcb_half spec object = object"
101  apply (frule well_formed_tcb_pending_op_cap [where obj_id=obj_id], simp add: object_at_def)
102  apply (frule well_formed_tcb_replycap_cap [where obj_id=obj_id], simp add: object_at_def)
103  apply (frule well_formed_tcb_pending_op_replycap [where obj_id=obj_id], simp add: object_at_def)
104  apply (frule well_formed_tcb_boundntfn_cap [where obj_id=obj_id], simp add: object_at_def)
105  apply (fastforce simp: tcb_half_def is_waiting_thread_def is_tcb_def
106                         opt_cap_def slots_of_def opt_object_def object_slots_def update_slots_def
107                         cdl_tcb.splits
108                  split: cdl_object.splits)
109  done
110
111lemma tcb_half_initialised_object_initialised:
112  "\<lbrakk>well_formed spec; tcb_at obj_id spec; \<not> object_at is_waiting_thread obj_id spec\<rbrakk>
113  \<Longrightarrow> tcb_half_initialised spec t obj_id = object_initialised spec t obj_id"
114  by (clarsimp simp: tcb_half_initialised_def object_initialised_def object_initialised_general_def
115                     object_at_def tcb_half_id)
116
117lemma tcb_half_initialised_object_initialised':
118  "well_formed spec
119  \<Longrightarrow> (\<And>*obj_id | tcb_at obj_id spec \<and> \<not> object_at is_waiting_thread obj_id spec.
120                   tcb_half_initialised spec t obj_id)
121    = (\<And>*obj_id | tcb_at obj_id spec \<and> \<not> object_at is_waiting_thread obj_id spec.
122                   object_initialised spec t obj_id)"
123  apply(rule sep.prod.cong, simp)
124  apply (rule tcb_half_initialised_object_initialised, simp+)
125  done
126
127lemma start_threads_sep:
128  "\<lbrace>\<guillemotleft>tcbs_half_initialised spec t {obj_id. tcb_at obj_id spec} \<and>*
129     si_caps_at t dup_caps spec False {obj_id. cnode_or_tcb_at obj_id spec} \<and>*
130     si_objects \<and>* R\<guillemotright> and
131     K(well_formed spec \<and> set obj_ids = dom (cdl_objects spec) \<and> distinct obj_ids)\<rbrace>
132   start_threads spec dup_caps obj_ids
133   \<lbrace>\<lambda>_.\<guillemotleft>objects_initialised spec t {obj_id. tcb_at obj_id spec} \<and>*
134        si_caps_at t dup_caps spec False {obj_id. cnode_or_tcb_at obj_id spec} \<and>*
135        si_objects \<and>* R\<guillemotright>\<rbrace>"
136  apply (rule hoare_gen_asm)
137  apply (clarsimp simp: start_threads_def tcbs_half_initialised_def objects_initialised_def)
138
139  (* The threads that don't need to be started can be ignored. *)
140  apply (subst sep_map_set_conj_restrict
141         [where P="tcb_half_initialised spec t"
142            and t="\<lambda>obj_id. object_at is_waiting_thread obj_id spec"], simp+)
143  apply (subst sep_map_set_conj_restrict
144         [where P="object_initialised spec t"
145            and t="\<lambda>obj_id. object_at is_waiting_thread obj_id spec"], simp+)
146  apply (subst tcb_half_initialised_object_initialised', assumption)
147
148  (* Now apply the mapM_x rule to reason about a single thread. *)
149  apply (clarsimp simp: sep_conj_ac)
150  apply (rule mapM_x_set_sep' [where
151               P="\<lambda>obj_id. tcb_half_initialised spec t obj_id" and
152               Q="\<lambda>obj_id. object_initialised spec t obj_id" and
153               I="si_caps_at t dup_caps spec False {obj_id. cnode_or_tcb_at obj_id spec} \<and>*
154                  si_objects" and
155               xs="[obj_id \<leftarrow> obj_ids. is_waiting_thread_at obj_id spec]" and
156               X="{obj_id. object_at is_waiting_thread obj_id spec}" and
157              R="R \<and>* (\<And>*obj_id | tcb_at obj_id spec \<and> \<not> object_at is_waiting_thread obj_id spec.
158                                   object_initialised spec t obj_id)"
159              , simplified sep_conj_ac], simp+)
160
161  (* Now select only a single one of the "si_cap_at t dup_caps spec" predicates. *)
162  apply (clarsimp simp: si_caps_at_def, rename_tac obj_id)
163  apply (rule hoare_chain)
164    apply (rule_tac x = obj_id
165                and xs = "{obj_id. cnode_or_tcb_at obj_id spec}"
166                and P = "tcb_half_initialised spec t obj_id \<and>* si_objects"
167                and Q = "object_initialised spec t obj_id \<and>* si_objects"
168                and I = "si_cap_at t dup_caps spec False"
169                and R=R
170                 in sep_set_conj_map_singleton_wp [simplified], simp_all add: object_at_real_object_at)
171
172  (* Then apply the start_thread_sep rule and we are done. *)
173    apply (wp sep_wp: start_thread_sep [where t=t], (simp|sep_solve)+)
174  done
175
176end
177