1(* 2 * Copyright 2014, General Dynamics C4 Systems 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(GD_GPL) 9 *) 10 11theory IpcCancel_C 12imports SyscallArgs_C 13begin 14 15context kernel_m 16begin 17 18lemma cready_queues_index_to_C_in_range': 19 assumes prems: "qdom \<le> ucast maxDom" "prio \<le> ucast maxPrio" 20 shows "cready_queues_index_to_C qdom prio < numDomains * numPriorities" 21proof - 22 have P: "unat prio < numPriorities" 23 using prems 24 by (simp add: numPriorities_def seL4_MaxPrio_def Suc_le_lessD unat_le_helper) 25 have Q: "unat qdom < numDomains" 26 using prems 27 by (simp add: numDomains_def maxDom_def Suc_le_lessD unat_le_helper) 28 show ?thesis 29 using mod_lemma[OF _ P, where q="unat qdom" and c=numDomains] Q 30 by (clarsimp simp: cready_queues_index_to_C_def field_simps numDomains_def) 31qed 32 33lemmas cready_queues_index_to_C_in_range 34 = cready_queues_index_to_C_in_range'[unfolded numPriorities_def numDomains_def, simplified] 35 36lemma cready_queues_index_to_C_inj: 37 "\<lbrakk> cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio'; 38 prio \<le> ucast maxPrio; prio' \<le> ucast maxPrio \<rbrakk> \<Longrightarrow> prio = prio' \<and> qdom = qdom'" 39 apply (rule context_conjI) 40 apply (auto simp: cready_queues_index_to_C_def numPriorities_def 41 seL4_MaxPrio_def word_le_nat_alt dest: arg_cong[where f="\<lambda>x. x mod 256"]) 42 done 43 44lemma cready_queues_index_to_C_distinct: 45 "\<lbrakk> qdom = qdom' \<longrightarrow> prio \<noteq> prio'; prio \<le> ucast maxPrio; prio' \<le> ucast maxPrio \<rbrakk> 46 \<Longrightarrow> cready_queues_index_to_C qdom prio \<noteq> cready_queues_index_to_C qdom' prio'" 47 apply (auto simp: cready_queues_index_to_C_inj) 48 done 49 50lemma cstate_relation_ksReadyQueues_update: 51 "\<lbrakk> cstate_relation hs cs; arr = ksReadyQueues_' cs; 52 sched_queue_relation' (clift (t_hrs_' cs)) v (head_C v') (end_C v'); 53 qdom \<le> ucast maxDom; prio \<le> ucast maxPrio \<rbrakk> 54 \<Longrightarrow> cstate_relation (ksReadyQueues_update (\<lambda>qs. qs ((qdom, prio) := v)) hs) 55 (ksReadyQueues_'_update (\<lambda>_. Arrays.update arr 56 (cready_queues_index_to_C qdom prio) v') cs)" 57 apply (clarsimp simp: cstate_relation_def Let_def 58 cmachine_state_relation_def 59 carch_state_relation_def carch_globals_def 60 cready_queues_relation_def seL4_MinPrio_def minDom_def) 61 apply (frule cready_queues_index_to_C_in_range, assumption) 62 apply clarsimp 63 apply (frule_tac qdom=qdoma and prio=prioa in cready_queues_index_to_C_in_range, assumption) 64 apply (frule cready_queues_index_to_C_distinct, assumption+) 65 apply clarsimp 66 done 67 68lemma cmap_relation_drop_fun_upd: 69 "\<lbrakk> cm x = Some v; \<And>v''. rel v'' v = rel v'' v' \<rbrakk> 70 \<Longrightarrow> cmap_relation am (cm (x \<mapsto> v')) f rel 71 = cmap_relation am cm f rel" 72 apply (simp add: cmap_relation_def) 73 apply (rule conj_cong[OF refl]) 74 apply (rule ball_cong[OF refl]) 75 apply (auto split: if_split) 76 done 77 78lemma valid_queuesD': 79 "\<lbrakk> obj_at' (inQ d p) t s; valid_queues' s \<rbrakk> 80 \<Longrightarrow> t \<in> set (ksReadyQueues s (d, p))" 81 by (simp add: valid_queues'_def) 82 83lemma invs_valid_queues'[elim!]: 84 "invs' s \<Longrightarrow> valid_queues' s" 85 by (simp add: invs'_def valid_state'_def) 86 87 88lemma ntfn_ptr_get_queue_spec: 89 "\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> \<sigma> \<Turnstile>\<^sub>c \<^bsup>\<sigma>\<^esup>ntfnPtr} \<acute>ret__struct_tcb_queue_C :== PROC ntfn_ptr_get_queue(\<acute>ntfnPtr) 90 \<lbrace>head_C \<acute>ret__struct_tcb_queue_C = Ptr (ntfnQueue_head_CL (notification_lift (the (cslift s \<^bsup>s\<^esup>ntfnPtr)))) \<and> 91 end_C \<acute>ret__struct_tcb_queue_C = Ptr (ntfnQueue_tail_CL (notification_lift (the (cslift s \<^bsup>s\<^esup>ntfnPtr))))\<rbrace>" 92 apply vcg 93 apply clarsimp 94 done 95 96(* Although tcb_C contains an user_fpu_state_C field, 97 none of the uses of this abbreviation involve modifying 98 any user_fpu_state_C within a tcb_C. 99 It is therefore convenient to include user_fpu_state_C here 100 to cover preservation of the global FPU null state. *) 101abbreviation 102 "cslift_all_but_tcb_C s t \<equiv> (cslift s :: cte_C typ_heap) = cslift t 103 \<and> (cslift s :: endpoint_C typ_heap) = cslift t 104 \<and> (cslift s :: notification_C typ_heap) = cslift t 105 \<and> (cslift s :: asid_pool_C typ_heap) = cslift t 106 \<and> (cslift s :: pte_C typ_heap) = cslift t 107 \<and> (cslift s :: pde_C typ_heap) = cslift t 108 \<and> (cslift s :: pdpte_C typ_heap) = cslift t 109 \<and> (cslift s :: pml4e_C typ_heap) = cslift t 110 \<and> (cslift s :: user_data_C typ_heap) = cslift t 111 \<and> (cslift s :: user_data_device_C typ_heap) = cslift t 112 \<and> (cslift s :: ioport_table_C typ_heap) = cslift t 113 \<and> (cslift s :: user_fpu_state_C typ_heap) = cslift t" 114 115lemma tcbEPDequeue_spec: 116 "\<forall>s queue. \<Gamma> \<turnstile> \<lbrace>s. \<exists>t. (t, s) \<in> rf_sr 117 \<and> (\<forall>tcb\<in>set queue. tcb_at' tcb t) \<and> distinct queue 118 \<and> (ctcb_ptr_to_tcb_ptr \<acute>tcb \<in> set queue) 119 \<and> ep_queue_relation' (cslift s) queue (head_C \<acute>queue) (end_C \<acute>queue) \<rbrace> 120 Call tcbEPDequeue_'proc 121 {t. (head_C (ret__struct_tcb_queue_C_' t) = 122 (if (tcbEPPrev_C (the (cslift s (\<^bsup>s\<^esup>tcb)))) = NULL then 123 (tcbEPNext_C (the (cslift s (\<^bsup>s\<^esup>tcb)))) 124 else 125 (head_C \<^bsup>s\<^esup>queue))) 126 \<and> (end_C (ret__struct_tcb_queue_C_' t) = 127 (if (tcbEPNext_C (the (cslift s (\<^bsup>s\<^esup>tcb)))) = NULL then 128 (tcbEPPrev_C (the (cslift s (\<^bsup>s\<^esup>tcb)))) 129 else 130 (end_C \<^bsup>s\<^esup>queue))) 131 \<and> (ep_queue_relation' (cslift t) 132 (Lib.delete (ctcb_ptr_to_tcb_ptr \<^bsup>s\<^esup>tcb) queue) 133 (head_C (ret__struct_tcb_queue_C_' t)) 134 (end_C (ret__struct_tcb_queue_C_' t)) 135 \<and> (cslift t |` (- tcb_ptr_to_ctcb_ptr ` set queue)) = 136 (cslift s |` (- tcb_ptr_to_ctcb_ptr ` set queue)) 137 \<and> option_map tcb_null_ep_ptrs \<circ> (cslift t) = 138 option_map tcb_null_ep_ptrs \<circ> (cslift s)) 139 \<and> cslift_all_but_tcb_C t s 140 \<and> (\<forall>rs. zero_ranges_are_zero rs (\<^bsup>t\<^esup>t_hrs) 141 = zero_ranges_are_zero rs (\<^bsup>s\<^esup>t_hrs)) 142 \<and> (hrs_htd \<^bsup>t\<^esup>t_hrs) = (hrs_htd \<^bsup>s\<^esup>t_hrs)}" 143 apply (intro allI) 144 apply (rule conseqPre) 145 apply vcg 146 apply (clarsimp split del: if_split) 147 apply (frule (4) tcb_queue_valid_ptrsD [OF _ _ _ _ tcb_queue_relation'_queue_rel]) 148 apply (elim conjE exE) 149 apply (frule (3) tcbEPDequeue_update) 150 apply simp 151 apply (unfold upd_unless_null_def) 152 apply (frule (2) tcb_queue_relation_ptr_rel' [OF tcb_queue_relation'_queue_rel]) 153 prefer 2 154 apply assumption 155 apply simp 156 apply (frule c_guard_clift) 157 apply (simp add: typ_heap_simps') 158 apply (intro allI conjI impI) 159 apply (clarsimp simp add: typ_heap_simps h_t_valid_clift_Some_iff) 160 apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff 161 cong: if_weak_cong) 162 apply (rule ext) 163 apply (clarsimp simp add: typ_heap_simps h_t_valid_clift_Some_iff tcb_null_ep_ptrs_def) 164 apply (clarsimp simp add: typ_heap_simps h_t_valid_clift_Some_iff c_guard_clift) 165 apply (clarsimp simp add: typ_heap_simps h_t_valid_clift_Some_iff) 166 apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff tcb_null_ep_ptrs_def 167 cong: if_weak_cong) 168 apply (rule ext) 169 apply (clarsimp simp add: typ_heap_simps h_t_valid_clift_Some_iff tcb_null_ep_ptrs_def) 170 apply (clarsimp simp add: typ_heap_simps h_t_valid_clift_Some_iff c_guard_clift) 171 apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff 172 cong: if_weak_cong) 173 apply (rule ext) 174 apply (clarsimp simp add: typ_heap_simps h_t_valid_clift_Some_iff tcb_null_ep_ptrs_def) 175 apply (clarsimp simp add: typ_heap_simps h_t_valid_clift_Some_iff c_guard_clift) 176 done 177 178lemma ntfn_ptr_set_queue_spec: 179 "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>ntfnPtr\<rbrace> Call ntfn_ptr_set_queue_'proc 180 {t. (\<exists>ntfn'. notification_lift ntfn' = 181 (notification_lift (the (cslift s (\<^bsup>s\<^esup>ntfnPtr))))\<lparr> 182 ntfnQueue_head_CL := sign_extend 47 (ptr_val (head_C \<^bsup>s\<^esup>ntfn_queue)), 183 ntfnQueue_tail_CL := sign_extend 47 (ptr_val (end_C \<^bsup>s\<^esup>ntfn_queue)) \<rparr> 184 \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (\<^bsup>s\<^esup>ntfnPtr) ntfn') 185 (t_hrs_' (globals s)))}" 186 apply (rule allI, rule conseqPre, vcg) 187 apply (clarsimp simp: packed_heap_update_collapse_hrs typ_heap_simps') 188 done 189 190 191lemma cancelSignal_ccorres_helper: 192 "ccorres dc xfdc (invs' and st_tcb_at' ((=) (BlockedOnNotification ntfn)) thread and ko_at' ntfn' ntfn) 193 UNIV 194 [] 195 (setNotification ntfn (ntfnObj_update 196 (\<lambda>_. if remove1 thread (ntfnQueue (ntfnObj ntfn')) = [] 197 then ntfn.IdleNtfn 198 else ntfnQueue_update (\<lambda>_. remove1 thread (ntfnQueue (ntfnObj ntfn'))) (ntfnObj ntfn')) ntfn')) 199 (\<acute>ntfn_queue :== CALL ntfn_ptr_get_queue(Ptr ntfn);; 200 \<acute>ntfn_queue :== CALL tcbEPDequeue(tcb_ptr_to_ctcb_ptr thread,\<acute>ntfn_queue);; 201 CALL ntfn_ptr_set_queue(Ptr ntfn,\<acute>ntfn_queue);; 202 IF head_C \<acute>ntfn_queue = NULL THEN 203 CALL notification_ptr_set_state(Ptr ntfn, 204 scast NtfnState_Idle) 205 FI)" 206 apply (rule ccorres_from_vcg) 207 apply (rule allI, rule conseqPre, vcg) 208 apply (clarsimp split del: if_split) 209 apply (frule (2) ntfn_blocked_in_queueD) 210 apply (frule (1) ko_at_valid_ntfn' [OF _ invs_valid_objs']) 211 apply (elim conjE) 212 apply (frule (1) valid_ntfn_isWaitingNtfnD) 213 apply (elim conjE) 214 apply (frule cmap_relation_ntfn) 215 apply (erule (1) cmap_relation_ko_atE) 216 apply (rule conjI) 217 apply (erule h_t_valid_clift) 218 apply (rule impI) 219 apply (rule exI) 220 apply (rule conjI) 221 apply (rule_tac x = \<sigma> in exI) 222 apply (intro conjI, assumption+) 223 apply (drule (2) ntfn_to_ep_queue) 224 apply (simp add: tcb_queue_relation'_def) 225 apply (clarsimp simp: typ_heap_simps cong: imp_cong split del: if_split) 226 apply (frule null_ep_queue [simplified Fun.comp_def]) 227 apply (intro impI conjI allI) 228 \<comment> \<open>empty case\<close> 229 apply clarsimp 230 apply (frule iffD1 [OF tcb_queue_head_empty_iff [OF tcb_queue_relation'_queue_rel]]) 231 apply (rule ballI, erule bspec) 232 apply (erule subsetD [rotated]) 233 apply clarsimp 234 apply simp 235 apply (simp add: setNotification_def split_def) 236 apply (rule bexI [OF _ setObject_eq]) 237 apply (simp add: remove1_empty rf_sr_def cstate_relation_def Let_def 238 cpspace_relation_def update_ntfn_map_tos 239 typ_heap_simps') 240 apply (elim conjE) 241 apply (intro conjI) 242 \<comment> \<open>tcb relation\<close> 243 apply (erule ctcb_relation_null_queue_ptrs) 244 apply (clarsimp simp: comp_def) 245 \<comment> \<open>ep relation\<close> 246 apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) 247 apply simp 248 apply (rule cendpoint_relation_ntfn_queue [OF invs_sym'], assumption+) 249 apply simp 250 apply (erule (1) map_to_ko_atI') 251 \<comment> \<open>ntfn relation\<close> 252 apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) 253 apply (simp add: cnotification_relation_def Let_def NtfnState_Idle_def) 254 apply (simp add: carch_state_relation_def carch_globals_def) 255 \<comment> \<open>queue relation\<close> 256 apply (rule cready_queues_relation_null_queue_ptrs, assumption+) 257 apply (clarsimp simp: comp_def) 258 apply (clarsimp simp: carch_state_relation_def carch_globals_def 259 typ_heap_simps' packed_heap_update_collapse_hrs 260 fpu_null_state_heap_update_tag_disj_simps 261 elim!: fpu_null_state_typ_heap_preservation) 262 apply (simp add: cmachine_state_relation_def) 263 apply (simp add: h_t_valid_clift_Some_iff) 264 apply (simp add: objBits_simps') 265 apply (simp add: objBits_simps) 266 apply assumption 267 \<comment> \<open>non empty case\<close> 268 apply (frule tcb_queue_head_empty_iff [OF tcb_queue_relation'_queue_rel]) 269 apply (rule ballI, erule bspec) 270 apply (erule subsetD [rotated]) 271 apply clarsimp 272 apply (simp add: setNotification_def split_def) 273 apply (rule bexI [OF _ setObject_eq]) 274 apply (frule (1) st_tcb_at_h_t_valid) 275 apply (simp add: remove1_empty rf_sr_def cstate_relation_def Let_def 276 cpspace_relation_def update_ntfn_map_tos 277 typ_heap_simps') 278 apply (elim conjE) 279 apply (intro conjI) 280 \<comment> \<open>tcb relation\<close> 281 apply (erule ctcb_relation_null_queue_ptrs) 282 apply (clarsimp simp: comp_def) 283 \<comment> \<open>ep relation\<close> 284 apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) 285 apply simp 286 apply (rule cendpoint_relation_ntfn_queue) 287 apply fastforce 288 apply assumption+ 289 apply simp 290 apply (erule (1) map_to_ko_atI') 291 \<comment> \<open>ntfn relation\<close> 292 apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) 293 apply (simp add: cnotification_relation_def Let_def isWaitingNtfn_def 294 split: ntfn.splits split del: if_split) 295 apply (erule iffD1 [OF tcb_queue_relation'_cong [OF refl _ _ refl], rotated -1]) 296 apply (clarsimp simp add: h_t_valid_clift_Some_iff) 297 apply (subst tcb_queue_relation'_next_sign; assumption?) 298 apply fastforce 299 apply (simp add: notification_lift_def sign_extend_sign_extend_eq) 300 apply (clarsimp simp: h_t_valid_clift_Some_iff notification_lift_def sign_extend_sign_extend_eq) 301 apply (subst tcb_queue_relation'_prev_sign; assumption?) 302 apply fastforce 303 apply simp 304 apply simp 305 \<comment> \<open>queue relation\<close> 306 apply (rule cready_queues_relation_null_queue_ptrs, assumption+) 307 apply (clarsimp simp: comp_def) 308 subgoal by (clarsimp simp: carch_state_relation_def carch_globals_def 309 fpu_null_state_heap_update_tag_disj_simps 310 global_ioport_bitmap_heap_update_tag_disj_simps 311 elim!: fpu_null_state_typ_heap_preservation) 312 subgoal by (simp add: cmachine_state_relation_def) 313 subgoal by (simp add: h_t_valid_clift_Some_iff) 314 subgoal by (simp add: objBits_simps') 315 subgoal by (simp add: objBits_simps) 316 by assumption 317 318lemmas rf_sr_tcb_update_no_queue_gen 319 = rf_sr_tcb_update_no_queue[where t="t''\<lparr> globals := gs \<lparr> t_hrs_' := th \<rparr>\<rparr>" for th, simplified] 320 321lemma threadSet_tcbState_simple_corres: 322 "ccorres dc xfdc (tcb_at' thread) 323 {s. (\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := v64_' s && mask 4\<rparr>, fl)) \<and> 324 thread_state_ptr_' s = Ptr &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])} [] 325 (threadSet (tcbState_update (\<lambda>_. st)) thread) (Call thread_state_ptr_set_tsType_'proc)" 326 apply (rule threadSet_corres_lemma) 327 apply (rule thread_state_ptr_set_tsType_spec) 328 apply (rule thread_state_ptr_set_tsType_modifies) 329 apply clarsimp 330 apply (frule (1) obj_at_cslift_tcb) 331 apply (clarsimp simp: typ_heap_simps') 332 apply (rule rf_sr_tcb_update_no_queue_gen, assumption+, simp, simp_all) 333 apply (rule ball_tcb_cte_casesI, simp_all) 334 apply (frule cmap_relation_tcb) 335 apply (frule (1) cmap_relation_ko_atD) 336 apply clarsimp 337 apply (simp add: ctcb_relation_def cthread_state_relation_def) 338 apply (frule (1) obj_at_cslift_tcb) 339 apply (clarsimp simp: typ_heap_simps) 340 done 341 342lemma ko_at_obj_congD': 343 "\<lbrakk>ko_at' k p s; ko_at' k' p s\<rbrakk> \<Longrightarrow> k = k'" 344 apply (erule obj_atE')+ 345 apply simp 346 done 347 348lemma threadGet_vcg_corres_P: 349 assumes c: "\<And>x. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr 350 \<and> tcb_at' thread \<sigma> \<and> P \<sigma> 351 \<and> (\<forall>tcb. ko_at' tcb thread \<sigma> \<longrightarrow> (\<exists>tcb'. 352 x = f tcb \<and> cslift s (tcb_ptr_to_ctcb_ptr thread) = Some tcb' 353 \<and> ctcb_relation tcb tcb'))} c {s. (\<sigma>, s) \<in> rf_sr \<and> r x (xf s)}" 354 shows "ccorres r xf P UNIV hs (threadGet f thread) c" 355 apply (rule ccorres_add_return2) 356 apply (rule ccorres_guard_imp2) 357 apply (rule ccorres_pre_threadGet) 358 apply (rule_tac P = "\<lambda>\<sigma>. \<exists>tcb. ko_at' tcb thread \<sigma> \<and> x = f tcb \<and> P \<sigma>" 359 and P' = UNIV in ccorres_from_vcg) 360 apply (simp add: return_def) 361 apply (rule allI, rule conseqPre) 362 apply (rule spec [OF c]) 363 apply clarsimp 364 apply (frule cmap_relation_tcb) 365 apply (frule (1) cmap_relation_ko_atD) 366 apply clarsimp 367 apply (rule conjI) 368 apply (erule obj_at'_weakenE) 369 apply simp 370 apply clarsimp 371 apply (drule (1) ko_at_obj_congD') 372 apply simp 373 apply fastforce 374 done 375 376lemmas threadGet_vcg_corres = threadGet_vcg_corres_P[where P=\<top>] 377 378lemma threadGet_specs_corres: 379 assumes spec: "\<forall>s. \<Gamma> \<turnstile> {s} Call g {t. xf t = f' s}" 380 and mod: "modifies_spec g" 381 and xf: "\<And>f s. xf (globals_update f s) = xf s" 382 shows "ccorres r xf (ko_at' ko thread) {s'. r (f ko) (f' s')} hs (threadGet f thread) (Call g)" 383 apply (rule ccorres_Call_call_for_vcg) 384 apply (rule ccorres_guard_imp2) 385 apply (rule ccorres_add_return2) 386 apply (rule ccorres_pre_threadGet) 387 apply (rule_tac P = "\<lambda>s. ko_at' ko thread s \<and> x = f ko" in ccorres_from_vcg [where P' = "{s'. r (f ko) (f' s')}"]) 388 apply (rule allI) 389 apply (rule HoarePartial.ProcModifyReturnNoAbr [where return' = "\<lambda>s t. t\<lparr> globals := globals s \<rparr>"]) 390 apply (rule HoarePartial.ProcSpecNoAbrupt [OF _ _ spec]) 391 defer 392 apply vcg 393 prefer 2 394 apply (rule mod) 395 apply (clarsimp simp: mex_def meq_def) 396 apply (frule obj_at'_weakenE [OF _ TrueI]) 397 apply clarsimp 398 apply (drule (1) ko_at_obj_congD') 399 apply simp 400 apply (clarsimp simp: return_def) 401 apply (rule conjI) 402 apply (erule iffD1 [OF rf_sr_upd, rotated -1], simp_all)[1] 403 apply (simp add: xf) 404 done 405 406lemma ccorres_exI1: 407 assumes rl: "\<And>x. ccorres r xf (Q x) (P' x) hs a c" 408 shows "ccorres r xf (\<lambda>s. (\<exists>x. P x s) \<and> (\<forall>x. P x s \<longrightarrow> Q x s)) 409 {s'. \<forall>x s. (s, s') \<in> rf_sr \<and> P x s \<longrightarrow> s' \<in> P' x} hs a c" 410 apply (rule ccorresI') 411 apply clarsimp 412 apply (drule spec, drule (1) mp) 413 apply (rule ccorresE [OF rl], assumption+) 414 apply fastforce 415 apply assumption 416 apply assumption 417 apply fastforce 418 done 419 420lemma isBlocked_ccorres [corres]: 421 "ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_' 422 (tcb_at' thread) (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr thread}) [] 423 (isBlocked thread) (Call isBlocked_'proc)" 424 apply (cinit lift: thread_' simp: getThreadState_def) 425 apply (rule ccorres_pre_threadGet) 426 apply (rule ccorres_move_c_guard_tcb) 427 apply (rule ccorres_symb_exec_r) 428 apply (rule ccorres_cond_weak) 429 apply (rule ccorres_return_C) 430 apply simp 431 apply simp 432 apply simp 433 apply (simp add: ccorres_cond_iffs) 434 apply (rule ccorres_return_C) 435 apply simp 436 apply simp 437 apply simp 438 apply vcg 439 apply (rule conseqPre) 440 apply vcg 441 apply clarsimp 442 apply clarsimp 443 apply (clarsimp simp: to_bool_def true_def false_def typ_heap_simps 444 ctcb_relation_thread_state_to_tsType split: thread_state.splits) 445 apply (simp add: "StrictC'_thread_state_defs")+ 446 done 447 448lemma isRunnable_ccorres [corres]: 449 "ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_' 450 (tcb_at' thread) (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr thread}) [] 451 (isRunnable thread) (Call isRunnable_'proc)" 452 apply (cinit lift: thread_' simp: getThreadState_def) 453 apply (rule ccorres_move_c_guard_tcb) 454 apply (rule ccorres_pre_threadGet) 455 apply (rule ccorres_symb_exec_r) 456 apply (rule ccorres_cond_weak) 457 apply (rule ccorres_return_C) 458 apply (simp) 459 apply (simp) 460 apply (simp) 461 apply (simp add: ccorres_cond_iffs) 462 apply (rule ccorres_return_C) 463 apply (simp) 464 apply (simp) 465 apply (simp) 466 apply (vcg) 467 apply (rule conseqPre) 468 apply (vcg) 469 apply (clarsimp) 470 apply (clarsimp) 471 apply (clarsimp simp: to_bool_def true_def false_def typ_heap_simps 472 ctcb_relation_thread_state_to_tsType split: thread_state.splits) 473 apply (simp add: "StrictC'_thread_state_defs")+ 474done 475 476 477 478lemma tcb_queue_relation_update_head: 479 fixes getNext_update :: "(tcb_C ptr \<Rightarrow> tcb_C ptr) \<Rightarrow> tcb_C \<Rightarrow> tcb_C" and 480 getPrev_update :: "(tcb_C ptr \<Rightarrow> tcb_C ptr) \<Rightarrow> tcb_C \<Rightarrow> tcb_C" 481 assumes qr: "tcb_queue_relation getNext getPrev mp queue NULL qhead" 482 and qh': "qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue" 483 and cs_tcb: "mp qhead' = Some tcb" 484 and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 485 and qhN: "qhead' \<noteq> NULL" 486 and fgN: "fg_cons getNext (getNext_update \<circ> (\<lambda>x _. x))" 487 and fgP: "fg_cons getPrev (getPrev_update \<circ> (\<lambda>x _. x))" 488 and npu: "\<And>f t. getNext (getPrev_update f t) = getNext t" 489 and pnu: "\<And>f t. getPrev (getNext_update f t) = getPrev t" 490 shows "tcb_queue_relation getNext getPrev 491 (upd_unless_null qhead (getPrev_update (\<lambda>_. qhead') (the (mp qhead))) 492 (mp(qhead' := Some (getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. qhead) tcb))))) 493 (ctcb_ptr_to_tcb_ptr qhead' # queue) NULL qhead'" 494 using qr qh' cs_tcb valid_ep qhN 495 apply (subgoal_tac "qhead \<noteq> qhead'") 496 apply (clarsimp simp: pnu upd_unless_null_def fg_consD1 [OF fgN] fg_consD1 [OF fgP] npu) 497 apply (cases queue) 498 apply simp 499 apply (frule (2) tcb_queue_relation_next_not_NULL) 500 apply simp 501 apply (clarsimp simp: fg_consD1 [OF fgN] fg_consD1 [OF fgP] pnu npu) 502 apply (subst tcb_queue_relation_cong [OF refl refl refl, where mp' = mp]) 503 apply (clarsimp simp: inj_eq) 504 apply (intro impI conjI) 505 apply (frule_tac x = x in imageI [where f = tcb_ptr_to_ctcb_ptr]) 506 apply simp 507 apply simp 508 apply simp 509 apply clarsimp 510 apply (cases queue) 511 apply simp 512 apply simp 513 done 514 515lemma tcbSchedEnqueue_update: 516 assumes sr: "sched_queue_relation' mp queue qhead qend" 517 and qh': "qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue" 518 and cs_tcb: "mp qhead' = Some tcb" 519 and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 520 and qhN: "qhead' \<noteq> NULL" 521 shows 522 "sched_queue_relation' 523 (upd_unless_null qhead (tcbSchedPrev_C_update (\<lambda>_. qhead') (the (mp qhead))) 524 (mp(qhead' \<mapsto> tcb\<lparr>tcbSchedNext_C := qhead, tcbSchedPrev_C := NULL\<rparr>))) 525 (ctcb_ptr_to_tcb_ptr qhead' # queue) qhead' (if qend = NULL then qhead' else qend)" 526 using sr qh' cs_tcb valid_ep qhN 527 apply - 528 apply (erule tcb_queue_relationE') 529 apply (rule tcb_queue_relationI') 530 apply (erule (5) tcb_queue_relation_update_head 531 [where getNext_update = tcbSchedNext_C_update and getPrev_update = tcbSchedPrev_C_update], simp_all)[1] 532 apply simp 533 apply (intro impI) 534 apply (erule (1) tcb_queue_relation_not_NULL') 535 apply simp 536 done 537 538lemma tcb_ptr_to_ctcb_ptr_imageD: 539 "x \<in> tcb_ptr_to_ctcb_ptr ` S \<Longrightarrow> ctcb_ptr_to_tcb_ptr x \<in> S" 540 apply (erule imageE) 541 apply simp 542 done 543 544lemma ctcb_ptr_to_tcb_ptr_imageI: 545 "ctcb_ptr_to_tcb_ptr x \<in> S \<Longrightarrow> x \<in> tcb_ptr_to_ctcb_ptr ` S" 546 apply (drule imageI [where f = tcb_ptr_to_ctcb_ptr]) 547 apply simp 548 done 549 550lemma tcb_queue'_head_end_NULL: 551 assumes qr: "tcb_queue_relation' getNext getPrev mp queue qhead qend" 552 and tat: "\<forall>t\<in>set queue. tcb_at' t s" 553 shows "(qend = NULL) = (qhead = NULL)" 554 using qr tat 555 apply - 556 apply (erule tcb_queue_relationE') 557 apply (simp add: tcb_queue_head_empty_iff) 558 apply (rule impI) 559 apply (rule tcb_at_not_NULL) 560 apply (erule bspec) 561 apply simp 562 done 563 564lemma tcb_queue_relation_qhead_mem: 565 "\<lbrakk> tcb_queue_relation getNext getPrev mp queue NULL qhead; 566 (\<forall>tcb\<in>set queue. tcb_at' tcb t) \<rbrakk> 567 \<Longrightarrow> qhead \<noteq> NULL \<longrightarrow> ctcb_ptr_to_tcb_ptr qhead \<in> set queue" 568 by (clarsimp simp: tcb_queue_head_empty_iff tcb_queue_relation_head_hd) 569 570lemma tcb_queue_relation_qhead_valid: 571 "\<lbrakk> tcb_queue_relation getNext getPrev (cslift s') queue NULL qhead; 572 (s, s') \<in> rf_sr; (\<forall>tcb\<in>set queue. tcb_at' tcb s) \<rbrakk> 573 \<Longrightarrow> qhead \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c qhead" 574 apply (frule (1) tcb_queue_relation_qhead_mem) 575 apply clarsimp 576 apply(drule (3) tcb_queue_memberD) 577 apply (simp add: h_t_valid_clift_Some_iff) 578 done 579 580lemmas tcb_queue_relation_qhead_mem' = tcb_queue_relation_qhead_mem [OF tcb_queue_relation'_queue_rel] 581lemmas tcb_queue_relation_qhead_valid' = tcb_queue_relation_qhead_valid [OF tcb_queue_relation'_queue_rel] 582 583 584lemma valid_queues_valid_q: 585 "valid_queues s \<Longrightarrow> (\<forall>tcb\<in>set (ksReadyQueues s (qdom, prio)). tcb_at' tcb s) \<and> distinct (ksReadyQueues s (qdom, prio))" 586 apply (clarsimp simp: valid_queues_def valid_queues_no_bitmap_def) 587 apply (drule spec [where x = qdom]) 588 apply (drule spec [where x = prio]) 589 apply clarsimp 590 apply (drule (1) bspec, erule obj_at'_weakenE) 591 apply simp 592 done 593 594lemma invs_valid_q: 595 "invs' s \<Longrightarrow> (\<forall>tcb\<in>set (ksReadyQueues s (qdom, prio)). tcb_at' tcb s) \<and> distinct (ksReadyQueues s (qdom, prio))" 596 apply (rule valid_queues_valid_q) 597 apply (clarsimp simp: invs'_def valid_state'_def) 598 done 599 600lemma tcbQueued_not_in_queues: 601 assumes vq: "valid_queues s" 602 and objat: "obj_at' (Not \<circ> tcbQueued) thread s" 603 shows "thread \<notin> set (ksReadyQueues s (d, p))" 604 using vq objat 605 apply - 606 apply clarsimp 607 apply (drule (1) valid_queues_obj_at'D) 608 apply (erule obj_atE')+ 609 apply (clarsimp simp: inQ_def) 610 done 611 612declare unat_ucast_8_64[simp] 613 614lemma rf_sr_sched_queue_relation: 615 "\<lbrakk> (s, s') \<in> rf_sr; d \<le> ucast maxDom; p \<le> ucast maxPrio \<rbrakk> 616 \<Longrightarrow> sched_queue_relation' (cslift s') (ksReadyQueues s (d, p)) 617 (head_C (index (ksReadyQueues_' (globals s')) 618 (cready_queues_index_to_C d p))) 619 (end_C (index (ksReadyQueues_' (globals s')) 620 (cready_queues_index_to_C d p)))" 621 unfolding rf_sr_def cstate_relation_def cready_queues_relation_def 622 apply (clarsimp simp: Let_def seL4_MinPrio_def minDom_def) 623 done 624 625lemma ready_queue_not_in: 626 assumes vq: "valid_queues s" 627 and inq: "t \<in> set (ksReadyQueues s (d, p))" 628 and neq: "d \<noteq> d' \<or> p \<noteq> p'" 629 shows "t \<notin> set (ksReadyQueues s (d', p'))" 630proof 631 assume "t \<in> set (ksReadyQueues s (d', p'))" 632 hence "obj_at' (inQ d' p') t s" using vq by (rule valid_queues_obj_at'D) 633 moreover have "obj_at' (inQ d p) t s" using inq vq by (rule valid_queues_obj_at'D) 634 ultimately show False using neq 635 by (clarsimp elim!: obj_atE' simp: inQ_def) 636qed 637 638lemma ctcb_relation_unat_prio_eq: 639 "ctcb_relation tcb tcb' \<Longrightarrow> unat (tcbPriority tcb) = unat (tcbPriority_C tcb')" 640 apply (clarsimp simp: ctcb_relation_def) 641 apply (erule_tac t = "tcbPriority_C tcb'" in subst) 642 apply simp 643 done 644 645lemma ctcb_relation_unat_dom_eq: 646 "ctcb_relation tcb tcb' \<Longrightarrow> unat (tcbDomain tcb) = unat (tcbDomain_C tcb')" 647 apply (clarsimp simp: ctcb_relation_def) 648 apply (erule_tac t = "tcbDomain_C tcb'" in subst) 649 apply simp 650 done 651 652lemma threadSet_queued_ccorres [corres]: 653 shows "ccorres dc xfdc (tcb_at' thread) 654 {s. v64_' s = from_bool v \<and> thread_state_ptr_' s = Ptr &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])} [] 655 (threadSet (tcbQueued_update (\<lambda>_. v)) thread) 656 (Call thread_state_ptr_set_tcbQueued_'proc)" 657 apply (rule threadSet_corres_lemma) 658 apply (rule thread_state_ptr_set_tcbQueued_spec) 659 apply (rule thread_state_ptr_set_tcbQueued_modifies) 660 apply clarsimp 661 apply (frule (1) obj_at_cslift_tcb) 662 apply clarsimp 663 apply (rule rf_sr_tcb_update_no_queue_gen, assumption+, simp, simp_all) 664 apply (rule ball_tcb_cte_casesI, simp_all) 665 apply (simp add: ctcb_relation_def cthread_state_relation_def) 666 apply (case_tac "tcbState ko", simp_all add: Word_Lemmas.from_bool_mask_simp)[1] 667 apply (frule (1) obj_at_cslift_tcb) 668 apply (clarsimp simp: typ_heap_simps) 669 done 670 671lemma ccorres_pre_getQueue: 672 assumes cc: "\<And>queue. ccorres r xf (P queue) (P' queue) hs (f queue) c" 673 shows "ccorres r xf (\<lambda>s. P (ksReadyQueues s (d, p)) s \<and> d \<le> maxDomain \<and> p \<le> maxPriority) 674 {s'. \<forall>queue. (let cqueue = index (ksReadyQueues_' (globals s')) 675 (cready_queues_index_to_C d p) in 676 sched_queue_relation' (cslift s') queue (head_C cqueue) (end_C cqueue)) \<longrightarrow> s' \<in> P' queue} 677 hs (getQueue d p >>= (\<lambda>queue. f queue)) c" 678 apply (rule ccorres_guard_imp2) 679 apply (rule ccorres_symb_exec_l2) 680 defer 681 defer 682 apply (rule gq_sp) 683 defer 684 apply (rule ccorres_guard_imp) 685 apply (rule cc) 686 apply clarsimp 687 apply assumption 688 apply assumption 689 apply (clarsimp simp: getQueue_def gets_exs_valid) 690 apply clarsimp 691 apply (drule spec, erule mp) 692 apply (simp add: Let_def) 693 apply (erule rf_sr_sched_queue_relation) 694 apply (simp add: maxDom_to_H maxPrio_to_H)+ 695 done 696 697(* FIXME: move *) 698lemma threadGet_wp: 699 "\<lbrace>\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> P (f tcb) s\<rbrace> threadGet f thread \<lbrace>P\<rbrace>" 700 apply (rule hoare_post_imp [OF _ tg_sp']) 701 apply clarsimp 702 apply (frule obj_at_ko_at') 703 apply (clarsimp elim: obj_atE') 704 done 705 706lemma state_relation_queue_update_helper': 707 "\<lbrakk> (s, s') \<in> rf_sr; 708 (\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) 709 \<and> distinct (ksReadyQueues s (d, p))); 710 globals t = ksReadyQueues_'_update 711 (\<lambda>_. Arrays.update (ksReadyQueues_' (globals s')) prio' q') 712 (t_hrs_'_update f (globals s')); 713 sched_queue_relation' (cslift t) q (head_C q') (end_C q'); 714 cslift t |` ( - tcb_ptr_to_ctcb_ptr ` S ) 715 = cslift s' |` ( - tcb_ptr_to_ctcb_ptr ` S ); 716 option_map tcb_null_sched_ptrs \<circ> cslift t 717 = option_map tcb_null_sched_ptrs \<circ> cslift s'; 718 cslift_all_but_tcb_C t s'; 719 zero_ranges_are_zero (gsUntypedZeroRanges s) (f (t_hrs_' (globals s'))) 720 = zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); 721 hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s')); 722 prio' = cready_queues_index_to_C qdom prio; 723 \<forall>x \<in> S. obj_at' (inQ qdom prio) x s 724 \<or> (obj_at' (\<lambda>tcb. tcbPriority tcb = prio) x s 725 \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = qdom) x s) 726 \<or> (tcb_at' x s \<and> (\<forall>d' p'. (d' \<noteq> qdom \<or> p' \<noteq> prio) 727 \<longrightarrow> x \<notin> set (ksReadyQueues s (d', p')))); 728 S \<noteq> {}; qdom \<le> ucast maxDom; prio \<le> ucast maxPrio \<rbrakk> 729 \<Longrightarrow> (s \<lparr>ksReadyQueues := (ksReadyQueues s)((qdom, prio) := q)\<rparr>, t) \<in> rf_sr" 730 apply (subst(asm) disj_imp_rhs) 731 apply (subst obj_at'_and[symmetric]) 732 apply (rule disjI1, erule obj_at'_weakenE, simp add: inQ_def) 733 apply (subst(asm) disj_imp_rhs) 734 apply (subst(asm) obj_at'_and[symmetric]) 735 apply (rule conjI, erule obj_at'_weakenE, simp) 736 apply (rule allI, rule allI) 737 apply (drule_tac x=d' in spec) 738 apply (drule_tac x=p' in spec) 739 apply clarsimp 740 apply (drule(1) bspec) 741 apply (clarsimp simp: inQ_def obj_at'_def) 742 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 743 apply (intro conjI) 744 \<comment> \<open>cpspace_relation\<close> 745 apply (erule nonemptyE, drule(1) bspec) 746 apply (clarsimp simp: cpspace_relation_def) 747 apply (drule obj_at_ko_at', clarsimp) 748 apply (rule cmap_relationE1, assumption, 749 erule ko_at_projectKO_opt) 750 apply (frule null_sched_queue) 751 apply (frule null_sched_epD) 752 apply (intro conjI) 753 \<comment> \<open>tcb relation\<close> 754 apply (drule ctcb_relation_null_queue_ptrs, 755 simp_all)[1] 756 \<comment> \<open>endpoint relation\<close> 757 apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) 758 apply simp 759 apply (erule cendpoint_relation_upd_tcb_no_queues, simp+) 760 \<comment> \<open>ntfn relation\<close> 761 apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) 762 apply simp 763 apply (erule cnotification_relation_upd_tcb_no_queues, simp+) 764 \<comment> \<open>ready queues\<close> 765 apply (simp add: cready_queues_relation_def Let_def 766 cready_queues_index_to_C_in_range 767 seL4_MinPrio_def minDom_def) 768 apply clarsimp 769 apply (frule cready_queues_index_to_C_distinct, assumption+) 770 apply (clarsimp simp: cready_queues_index_to_C_in_range all_conj_distrib) 771 apply (rule iffD1 [OF tcb_queue_relation'_cong[OF refl], rotated -1], 772 drule spec, drule spec, erule mp, simp+) 773 apply clarsimp 774 apply (drule_tac x="tcb_ptr_to_ctcb_ptr x" in fun_cong)+ 775 apply (clarsimp simp: restrict_map_def 776 split: if_split_asm) 777 by (auto simp: carch_state_relation_def cmachine_state_relation_def 778 elim!: fpu_null_state_typ_heap_preservation) 779 780lemma state_relation_queue_update_helper: 781 "\<lbrakk> (s, s') \<in> rf_sr; valid_queues s; 782 globals t = ksReadyQueues_'_update 783 (\<lambda>_. Arrays.update (ksReadyQueues_' (globals s')) prio' q') 784 (t_hrs_'_update f (globals s')); 785 sched_queue_relation' (cslift t) q (head_C q') (end_C q'); 786 cslift t |` ( - tcb_ptr_to_ctcb_ptr ` S ) 787 = cslift s' |` ( - tcb_ptr_to_ctcb_ptr ` S ); 788 option_map tcb_null_sched_ptrs \<circ> cslift t 789 = option_map tcb_null_sched_ptrs \<circ> cslift s'; 790 cslift_all_but_tcb_C t s'; 791 zero_ranges_are_zero (gsUntypedZeroRanges s) (f (t_hrs_' (globals s'))) 792 = zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); 793 hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s')); 794 prio' = cready_queues_index_to_C qdom prio; 795 \<forall>x \<in> S. obj_at' (inQ qdom prio) x s 796 \<or> (obj_at' (\<lambda>tcb. tcbPriority tcb = prio) x s 797 \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = qdom) x s) 798 \<or> (tcb_at' x s \<and> (\<forall>d' p'. (d' \<noteq> qdom \<or> p' \<noteq> prio) 799 \<longrightarrow> x \<notin> set (ksReadyQueues s (d', p')))); 800 S \<noteq> {}; qdom \<le> ucast maxDom; prio \<le> ucast maxPrio \<rbrakk> 801 \<Longrightarrow> (s \<lparr>ksReadyQueues := (ksReadyQueues s)((qdom, prio) := q)\<rparr>, t) \<in> rf_sr" 802 apply (subgoal_tac "\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) 803 \<and> distinct(ksReadyQueues s (d, p))") 804 apply (erule(5) state_relation_queue_update_helper', simp_all) 805 apply (clarsimp simp: valid_queues_def valid_queues_no_bitmap_def) 806 apply (drule_tac x=d in spec) 807 apply (drule_tac x=p in spec) 808 apply (clarsimp) 809 apply (drule(1) bspec) 810 apply (erule obj_at'_weakenE, clarsimp) 811 done 812 813(* FIXME: move *) 814lemma from_bool_vals [simp]: 815 "from_bool True = scast true" 816 "from_bool False = scast false" 817 "scast true \<noteq> scast false" 818 by (auto simp add: from_bool_def true_def false_def) 819 820(* FIXME: move *) 821lemma cmap_relation_no_upd: 822 "\<lbrakk> cmap_relation a c f rel; a p = Some ko; rel ko v; inj f \<rbrakk> \<Longrightarrow> cmap_relation a (c(f p \<mapsto> v)) f rel" 823 apply (clarsimp simp: cmap_relation_def) 824 apply (subgoal_tac "f p \<in> dom c") 825 prefer 2 826 apply (drule_tac t="dom c" in sym) 827 apply fastforce 828 apply clarsimp 829 apply (drule (1) injD) 830 apply simp 831 done 832 833(* FIXME: move *) 834lemma cmap_relation_rel_upd: 835 "\<lbrakk> cmap_relation a c f rel; \<And>v v'. rel v v' \<Longrightarrow> rel' v v' \<rbrakk> \<Longrightarrow> cmap_relation a c f rel'" 836 by (simp add: cmap_relation_def) 837 838declare fun_upd_restrict_conv[simp del] 839 840lemmas queue_in_range = of_nat_mono_maybe[OF _ cready_queues_index_to_C_in_range, 841 where 'a=32, unfolded cready_queues_index_to_C_def numPriorities_def, 842 simplified, unfolded ucast_nat_def] 843 of_nat_mono_maybe[OF _ cready_queues_index_to_C_in_range, 844 where 'a="32 signed", unfolded cready_queues_index_to_C_def numPriorities_def, 845 simplified, unfolded ucast_nat_def] 846 of_nat_mono_maybe[OF _ cready_queues_index_to_C_in_range, 847 where 'a=64, unfolded cready_queues_index_to_C_def numPriorities_def, 848 simplified, unfolded ucast_nat_def] 849 850lemma cready_queues_index_to_C_def2': 851 "\<lbrakk> qdom \<le> ucast maxDom; prio \<le> ucast maxPrio \<rbrakk> 852 \<Longrightarrow> cready_queues_index_to_C qdom prio 853 = unat (ucast qdom * of_nat numPriorities + ucast prio :: machine_word)" 854 apply (simp add: cready_queues_index_to_C_def numPriorities_def) 855 apply (subst unat_add_lem[THEN iffD1]) 856 apply (frule cready_queues_index_to_C_in_range, simp) 857 apply (simp add: cready_queues_index_to_C_def numPriorities_def) 858 apply (subst unat_mult_simple) 859 apply (simp add: word_bits_def maxDom_def) 860 apply simp 861 apply (subst unat_mult_simple) 862 apply (simp add: word_bits_def maxDom_def) 863 apply (subst (asm) word_le_nat_alt) 864 apply simp 865 apply simp 866 done 867 868lemmas cready_queues_index_to_C_def2 869 = cready_queues_index_to_C_def2'[simplified maxDom_to_H maxPrio_to_H] 870 871lemma ready_queues_index_spec: 872 "\<forall>s. \<Gamma> \<turnstile> {s} Call ready_queues_index_'proc 873 \<lbrace>\<acute>ret__unsigned_long = (dom_' s) * 0x100 + (prio_' s)\<rbrace>" 874 by vcg (simp add: word_sless_alt) 875 876lemma prio_to_l1index_spec: 877 "\<forall>s. \<Gamma> \<turnstile> {s} Call prio_to_l1index_'proc 878 \<lbrace>\<acute>ret__unsigned_long = prio_' s >> wordRadix \<rbrace>" 879 by vcg (simp add: word_sle_def wordRadix_def') 880 881lemma invert_l1index_spec: 882 "\<forall>s. \<Gamma> \<turnstile> {s} Call invert_l1index_'proc 883 \<lbrace>\<acute>ret__unsigned_long = of_nat l2BitmapSize - 1 - l1index_' s \<rbrace>" 884 unfolding l2BitmapSize_def' 885 by vcg 886 (simp add: word_sle_def sdiv_int_def sdiv_word_def smod_word_def smod_int_def) 887 888lemma cbitmap_L1_relation_update: 889 "\<lbrakk> (\<sigma>, s) \<in> rf_sr ; cbitmap_L1_relation cupd aupd \<rbrakk> 890 \<Longrightarrow> (\<sigma>\<lparr>ksReadyQueuesL1Bitmap := aupd \<rparr>, 891 globals_update (ksReadyQueuesL1Bitmap_'_update (\<lambda>_. cupd)) s) 892 \<in> rf_sr" 893 by (simp add: rf_sr_def cstate_relation_def Let_def carch_state_relation_def 894 cmachine_state_relation_def) 895 896lemma cbitmap_L2_relation_update: 897 "\<lbrakk> (\<sigma>, s) \<in> rf_sr ; cbitmap_L2_relation cupd aupd \<rbrakk> 898 \<Longrightarrow> (\<sigma>\<lparr>ksReadyQueuesL2Bitmap := aupd \<rparr>, 899 globals_update (ksReadyQueuesL2Bitmap_'_update (\<lambda>_. cupd)) s) 900 \<in> rf_sr" 901 by (simp add: rf_sr_def cstate_relation_def Let_def carch_state_relation_def 902 cmachine_state_relation_def) 903 904lemma unat_ucast_prio_shiftr_simp[simp]: 905 "unat (ucast (p::priority) >> n :: machine_word) = unat (p >> n)" 906 by (simp add: shiftr_div_2n')+ 907 908lemma unat_ucast_prio_mask_simp[simp]: 909 "unat (ucast (p::priority) && mask m :: machine_word) = unat (p && mask m)" 910 by (metis ucast_and_mask unat_ucast_8_64) 911 912lemma unat_ucast_prio_L1_cmask_simp: 913 "unat (ucast (p::priority) && 0x3F :: machine_word) = unat (p && 0x3F)" 914 using unat_ucast_prio_mask_simp[where m=6] 915 by (simp add: mask_def) 916 917lemma machine_word_and_3F_less_40: 918 "(w :: machine_word) && 0x3F < 0x40" 919 by (rule word_and_less', simp) 920 921lemma prio_ucast_shiftr_wordRadix_helper: (* FIXME generalise *) 922 "(ucast (p::priority) >> wordRadix :: machine_word) < 4" 923 unfolding maxPriority_def numPriorities_def wordRadix_def 924 using unat_lt2p[where x=p] 925 apply (clarsimp simp add: word_less_nat_alt shiftr_div_2n' unat_ucast_upcast is_up word_le_nat_alt) 926 apply arith 927 done 928 929lemma prio_ucast_shiftr_wordRadix_helper': (* FIXME generalise *) 930 "(ucast (p::priority) >> wordRadix :: machine_word) \<le> 3" 931 unfolding maxPriority_def numPriorities_def wordRadix_def 932 using unat_lt2p[where x=p] 933 apply (clarsimp simp add: word_less_nat_alt shiftr_div_2n' unat_ucast_upcast is_up word_le_nat_alt) 934 apply arith 935 done 936 937lemma prio_unat_shiftr_wordRadix_helper': (* FIXME generalise *) 938 "unat ((p::priority) >> wordRadix) \<le> 3" 939 unfolding maxPriority_def numPriorities_def wordRadix_def 940 using unat_lt2p[where x=p] 941 apply (clarsimp simp add: word_less_nat_alt shiftr_div_2n' unat_ucast_upcast is_up word_le_nat_alt) 942 apply arith 943 done 944 945lemma prio_ucast_shiftr_wordRadix_helper2: (* FIXME possibly unused *) 946 "(ucast (p::priority) >> wordRadix :: machine_word) < 0x20" 947 by (rule order_less_trans[OF prio_ucast_shiftr_wordRadix_helper]; simp) 948 949lemma prio_ucast_shiftr_wordRadix_helper3: 950 "(ucast (p::priority) >> wordRadix :: machine_word) < 0x40" 951 by (rule order_less_trans[OF prio_ucast_shiftr_wordRadix_helper]; simp) 952 953lemma dom_less_0x10_helper: 954 "d \<le> maxDomain \<Longrightarrow> (ucast d :: machine_word) < 0x10" 955 unfolding maxDomain_def numDomains_def 956 by (clarsimp simp add: word_less_nat_alt unat_ucast_upcast is_up word_le_nat_alt) 957 958lemma cready_queues_index_to_C_ucast_helper: 959 fixes p :: priority 960 fixes d :: domain 961 shows "unat (ucast d * 0x100 + ucast p :: machine_word) = unat d * 256 + unat p" 962 unfolding tcb_queue_relation'_def maxPriority_def maxDomain_def numDomains_def numPriorities_def 963 using unat_lt2p[where x=p] unat_lt2p[where x=d] 964 by (clarsimp simp: cready_queues_index_to_C_def word_le_nat_alt unat_word_ariths) 965 966lemmas prio_and_dom_limit_helpers = 967 prio_ucast_shiftr_wordRadix_helper 968 prio_ucast_shiftr_wordRadix_helper' 969 prio_ucast_shiftr_wordRadix_helper2 970 prio_ucast_shiftr_wordRadix_helper3 971 prio_unat_shiftr_wordRadix_helper' 972 dom_less_0x10_helper 973 cready_queues_index_to_C_ucast_helper 974 unat_ucast_prio_L1_cmask_simp 975 machine_word_and_3F_less_40 976 977(* FIXME MOVE *) 978lemma rf_sr_cbitmap_L1_relation[intro]: 979 "(\<sigma>, x) \<in> rf_sr \<Longrightarrow> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>)" 980 by (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 981 982(* FIXME MOVE *) 983lemma rf_sr_cbitmap_L2_relation[intro]: 984 "(\<sigma>, x) \<in> rf_sr \<Longrightarrow> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>)" 985 by (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 986 987lemma cbitmap_L1_relation_bit_set: 988 fixes p :: priority 989 shows 990 "\<lbrakk> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>) ; 991 d \<le> maxDomain \<rbrakk> \<Longrightarrow> 992 cbitmap_L1_relation 993 (Arrays.update (ksReadyQueuesL1Bitmap_' (globals x)) (unat d) 994 (ksReadyQueuesL1Bitmap_' (globals x).[unat d] || 2 ^ unat (p >> wordRadix))) 995 ((ksReadyQueuesL1Bitmap \<sigma>)(d := ksReadyQueuesL1Bitmap \<sigma> d || 2 ^ prioToL1Index p))" 996 apply (unfold cbitmap_L1_relation_def) 997 apply (clarsimp simp: prioToL1Index_def wordRadix_def' maxDomain_def numDomains_def word_le_nat_alt) 998 done 999 1000lemma cbitmap_L2_relation_bit_set: 1001 fixes p :: priority 1002 fixes d :: domain 1003 shows "\<lbrakk> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals \<sigma>')) (ksReadyQueuesL2Bitmap \<sigma>) ; 1004 d \<le> maxDomain ; b = b' \<rbrakk> 1005 \<Longrightarrow> 1006 cbitmap_L2_relation 1007 (Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>')) (unat d) 1008 (Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d]) 1009 (invertL1Index (prioToL1Index p)) 1010 (ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d].[invertL1Index (prioToL1Index p)] || 1011 2 ^ unat (p && b)))) 1012 ((ksReadyQueuesL2Bitmap \<sigma>) 1013 ((d, invertL1Index (prioToL1Index p)) := 1014 ksReadyQueuesL2Bitmap \<sigma> (d, invertL1Index (prioToL1Index p)) || 1015 2 ^ unat (p && b')))" 1016 unfolding cbitmap_L2_relation_def numPriorities_def wordBits_def word_size l2BitmapSize_def' 1017 apply (clarsimp simp: word_size prioToL1Index_def wordRadix_def mask_def 1018 invertL1Index_def l2BitmapSize_def' 1019 maxDomain_def numDomains_def word_le_nat_alt) 1020 apply (case_tac "da = d" ; clarsimp) 1021 done 1022 1023lemma carch_state_relation_enqueue_simp: 1024 "carch_state_relation (ksArchState \<sigma>) 1025 (t_hrs_'_update f 1026 (globals \<sigma>' \<lparr>ksReadyQueuesL1Bitmap_' := l1upd, ksReadyQueuesL2Bitmap_' := l2upd \<rparr>) 1027 \<lparr>ksReadyQueues_' := rqupd \<rparr>) = 1028 carch_state_relation (ksArchState \<sigma>) (t_hrs_'_update f (globals \<sigma>'))" 1029 unfolding carch_state_relation_def 1030 by clarsimp 1031 1032(* FIXME move to lib/Eisbach_Methods *) 1033(* FIXME consider printing error on solve goal apply *) 1034context 1035begin 1036 1037private definition "bool_protect (b::bool) \<equiv> b" 1038 1039lemma bool_protectD: 1040 "bool_protect P \<Longrightarrow> P" 1041 unfolding bool_protect_def by simp 1042 1043lemma bool_protectI: 1044 "P \<Longrightarrow> bool_protect P" 1045 unfolding bool_protect_def by simp 1046 1047(* 1048 When you want to apply a rule/tactic to transform a potentially complex goal into another 1049 one manually, but want to indicate that any fresh emerging goals are solved by a more 1050 brutal method. 1051 E.g. apply (solves_emerging \<open>frule x=... in my_rule\<close>\<open>fastforce simp: ... intro!: ... \<close> *) 1052method solves_emerging methods m1 m2 = (rule bool_protectD, (m1 ; (rule bool_protectI | (m2; fail)))) 1053 1054end 1055 1056lemma t_hrs_ksReadyQueues_upd_absorb: 1057 "t_hrs_'_update f (g s) \<lparr>ksReadyQueues_' := rqupd \<rparr> = 1058 t_hrs_'_update f (g s \<lparr>ksReadyQueues_' := rqupd\<rparr>)" 1059 by simp 1060 1061lemma rf_sr_drop_bitmaps_enqueue_helper: 1062 "\<lbrakk> (\<sigma>,\<sigma>') \<in> rf_sr ; 1063 cbitmap_L1_relation ksqL1upd' ksqL1upd ; cbitmap_L2_relation ksqL2upd' ksqL2upd \<rbrakk> 1064 \<Longrightarrow> 1065 ((\<sigma>\<lparr>ksReadyQueues := ksqupd, ksReadyQueuesL1Bitmap := ksqL1upd, ksReadyQueuesL2Bitmap := ksqL2upd\<rparr>, 1066 \<sigma>'\<lparr>idx_' := i', queue_' := queue_upd', 1067 globals := t_hrs_'_update f 1068 (globals \<sigma>' 1069 \<lparr>ksReadyQueuesL1Bitmap_' := ksqL1upd', 1070 ksReadyQueuesL2Bitmap_' := ksqL2upd', 1071 ksReadyQueues_' := ksqupd'\<rparr>)\<rparr>) \<in> rf_sr) = 1072 ((\<sigma>\<lparr>ksReadyQueues := ksqupd\<rparr>, 1073 \<sigma>'\<lparr>idx_' := i', queue_' := queue_upd', 1074 globals := t_hrs_'_update f 1075 (globals \<sigma>' \<lparr>ksReadyQueues_' := ksqupd'\<rparr>)\<rparr>) \<in> rf_sr)" 1076 unfolding rf_sr_def cstate_relation_def Let_def 1077 carch_state_relation_def cmachine_state_relation_def 1078 by (clarsimp simp: rf_sr_cbitmap_L1_relation rf_sr_cbitmap_L2_relation) 1079 1080lemma cmachine_state_relation_enqueue_simp: 1081 "cmachine_state_relation (ksMachineState \<sigma>) 1082 (t_hrs_'_update f 1083 (globals \<sigma>' \<lparr>ksReadyQueuesL1Bitmap_' := l1upd, ksReadyQueuesL2Bitmap_' := l2upd \<rparr>) 1084 \<lparr>ksReadyQueues_' := rqupd \<rparr>) = 1085 cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update f (globals \<sigma>'))" 1086 unfolding cmachine_state_relation_def 1087 by clarsimp 1088 1089lemma tcb_queue_relation'_empty_ksReadyQueues: 1090 "\<lbrakk> sched_queue_relation' (cslift x) (q s) NULL NULL ; \<forall>t\<in> set (q s). tcb_at' t s \<rbrakk> \<Longrightarrow> q s = []" 1091 apply (clarsimp simp add: tcb_queue_relation'_def) 1092 apply (subst (asm) eq_commute) 1093 apply (cases "q s" rule: rev_cases, simp) 1094 apply (clarsimp simp: tcb_at_not_NULL) 1095 done 1096 1097lemma invert_prioToL1Index_c_simp: 1098 "p \<le> maxPriority 1099 \<Longrightarrow> 1100 unat ((of_nat l2BitmapSize :: machine_word) - 1 - (ucast p >> wordRadix)) 1101 = invertL1Index (prioToL1Index p)" 1102 unfolding maxPriority_def l2BitmapSize_def' invertL1Index_def prioToL1Index_def 1103 numPriorities_def 1104 by (simp add: unat_sub prio_and_dom_limit_helpers) 1105 1106lemma c_invert_assist: "3 - (ucast (p :: priority) >> 6 :: machine_word) < 4" 1107 using prio_ucast_shiftr_wordRadix_helper'[simplified wordRadix_def] 1108 by - (rule word_less_imp_diff_less, simp_all) 1109 1110lemma tcbSchedEnqueue_ccorres: 1111 "ccorres dc xfdc 1112 (valid_queues and tcb_at' t and valid_objs') 1113 (UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>) 1114 hs 1115 (tcbSchedEnqueue t) 1116 (Call tcbSchedEnqueue_'proc)" 1117proof - 1118 note prio_and_dom_limit_helpers[simp] word_sle_def[simp] maxDom_to_H[simp] maxPrio_to_H[simp] 1119 note invert_prioToL1Index_c_simp[simp] 1120 1121 show ?thesis 1122 apply (cinit lift: tcb_') 1123 apply (rule_tac r'="\<lambda>rv rv'. rv = to_bool rv'" and xf'="ret__unsigned_longlong_'" 1124 in ccorres_split_nothrow) 1125 apply (rule threadGet_vcg_corres) 1126 apply (rule allI, rule conseqPre, vcg) 1127 apply clarsimp 1128 apply (drule obj_at_ko_at', clarsimp) 1129 apply (drule spec, drule(1) mp, clarsimp) 1130 apply (clarsimp simp: typ_heap_simps ctcb_relation_def) 1131 apply ceqv 1132 apply (simp add: when_def unless_def del: Collect_const split del: if_split) 1133 apply (rule ccorres_cond[where R=\<top>]) 1134 apply (simp add: to_bool_def) 1135 apply (rule ccorres_rhs_assoc)+ 1136 apply csymbr 1137 apply csymbr 1138 apply csymbr 1139 apply csymbr 1140 apply (rule_tac r'="\<lambda>rv rv'. rv' = ucast rv" and xf'="dom_'" in ccorres_split_nothrow) 1141 apply (rule threadGet_vcg_corres) 1142 apply (rule allI, rule conseqPre, vcg) 1143 apply clarsimp 1144 apply (drule obj_at_ko_at', clarsimp) 1145 apply (drule spec, drule(1) mp, clarsimp) 1146 apply (clarsimp simp: typ_heap_simps ctcb_relation_def) 1147 apply ceqv 1148 apply (rule_tac r'="\<lambda>rv rv'. rv' = ucast rv" and xf'="prio_'" in ccorres_split_nothrow) 1149 apply (rule threadGet_vcg_corres) 1150 apply (rule allI, rule conseqPre, vcg) 1151 apply clarsimp 1152 apply (drule obj_at_ko_at', clarsimp) 1153 apply (drule spec, drule(1) mp, clarsimp) 1154 apply (clarsimp simp: typ_heap_simps ctcb_relation_def) 1155 apply ceqv 1156 apply (rule ccorres_rhs_assoc2)+ 1157 apply (simp only: bind_assoc[symmetric]) 1158 apply (rule ccorres_split_nothrow_novcg_dc) 1159 prefer 2 1160 apply (rule ccorres_move_c_guard_tcb) 1161 apply (simp only: dc_def[symmetric]) 1162 apply ctac 1163 prefer 2 1164 apply (wp, clarsimp, wp+) 1165 apply (rule_tac P="\<lambda>s. valid_queues s \<and> (\<forall>p. t \<notin> set (ksReadyQueues s p)) 1166 \<and> (\<exists>tcb. ko_at' tcb t s \<and> tcbDomain tcb =rva 1167 \<and> tcbPriority tcb = rvb \<and> valid_tcb' tcb s)" 1168 and P'=UNIV in ccorres_from_vcg) 1169 apply (rule allI, rule conseqPre, vcg) 1170 apply (clarsimp simp: getQueue_def gets_def get_def setQueue_def modify_def 1171 put_def bind_def return_def bitmap_fun_defs null_def) 1172 apply (clarsimp simp: queue_in_range valid_tcb'_def) 1173 apply (rule conjI; clarsimp simp: queue_in_range) 1174 (* queue is empty, set t to be new queue *) 1175 apply (drule (1) obj_at_cslift_tcb) 1176 apply clarsimp 1177 apply (frule_tac d="tcbDomain tcb" and p="tcbPriority tcb" 1178 in rf_sr_sched_queue_relation) 1179 apply clarsimp 1180 apply clarsimp 1181 apply (frule_tac s=\<sigma> in tcb_queue'_head_end_NULL) 1182 apply (simp add: valid_queues_valid_q) 1183 apply (subgoal_tac 1184 "head_C (ksReadyQueues_' (globals x) 1185 .[cready_queues_index_to_C (tcbDomain tcb) (tcbPriority tcb)]) = NULL") 1186 prefer 2 1187 apply (frule_tac s=\<sigma> in tcb_queue'_head_end_NULL; simp add: valid_queues_valid_q) 1188 apply (subgoal_tac 1189 "end_C (ksReadyQueues_' (globals x) 1190 .[cready_queues_index_to_C (tcbDomain tcb) (tcbPriority tcb)]) = NULL") 1191 prefer 2 1192 apply (frule_tac s=\<sigma> in tcb_queue'_head_end_NULL[symmetric]; simp add: valid_queues_valid_q) 1193 apply (clarsimp simp: cready_queues_index_to_C_def numPriorities_def) 1194 apply (clarsimp simp: h_val_field_clift' h_t_valid_clift) 1195 apply (simp add: t_hrs_ksReadyQueues_upd_absorb) 1196 1197 apply (rule conjI) 1198 apply (clarsimp simp: l2BitmapSize_def' wordRadix_def c_invert_assist) 1199 apply (subst rf_sr_drop_bitmaps_enqueue_helper, assumption) 1200 apply (fastforce intro: cbitmap_L1_relation_bit_set) 1201 apply (fastforce intro: cbitmap_L2_relation_bit_set simp: wordRadix_def mask_def) 1202 1203 apply (frule_tac d="tcbDomain tcb" and p="tcbPriority tcb" in rf_sr_sched_queue_relation) 1204 apply clarsimp 1205 apply clarsimp 1206 apply (drule_tac qhead'="tcb_ptr_to_ctcb_ptr t" and s=\<sigma> in tcbSchedEnqueue_update, 1207 simp_all add: valid_queues_valid_q)[1] 1208 apply (rule tcb_at_not_NULL, erule obj_at'_weakenE, simp) 1209 apply (erule(1) state_relation_queue_update_helper[where S="{t}"], 1210 (simp | rule globals.equality)+, 1211 simp_all add: cready_queues_index_to_C_def2 numPriorities_def 1212 t_hrs_ksReadyQueues_upd_absorb upd_unless_null_def 1213 typ_heap_simps)[1] 1214 apply (fastforce simp: tcb_null_sched_ptrs_def typ_heap_simps c_guard_clift 1215 elim: obj_at'_weaken)+ 1216 1217 apply (rule conjI; clarsimp simp: queue_in_range) 1218 (* invalid, disagreement between C and Haskell on emptiness of queue *) 1219 apply (drule (1) obj_at_cslift_tcb) 1220 apply (clarsimp simp: h_val_field_clift' h_t_valid_clift) 1221 apply (frule_tac d="tcbDomain tcb" and p="tcbPriority tcb" in rf_sr_sched_queue_relation) 1222 apply clarsimp 1223 apply clarsimp 1224 apply (clarsimp simp: cready_queues_index_to_C_def numPriorities_def) 1225 apply (frule_tac s=\<sigma> in tcb_queue'_head_end_NULL) 1226 apply (simp add: valid_queues_valid_q) 1227 apply clarsimp 1228 apply (drule tcb_queue_relation'_empty_ksReadyQueues; simp add: valid_queues_valid_q) 1229 (* queue was not empty, add t to queue and leave bitmaps alone *) 1230 apply (drule (1) obj_at_cslift_tcb) 1231 apply (clarsimp simp: h_val_field_clift' h_t_valid_clift) 1232 apply (frule_tac d="tcbDomain tcb" and p="tcbPriority tcb" in rf_sr_sched_queue_relation) 1233 apply clarsimp 1234 apply clarsimp 1235 apply (clarsimp simp: cready_queues_index_to_C_def numPriorities_def) 1236 apply (frule_tac s=\<sigma> in tcb_queue'_head_end_NULL) 1237 apply (simp add: valid_queues_valid_q) 1238 apply clarsimp 1239 apply (frule_tac t=\<sigma> in tcb_queue_relation_qhead_mem') 1240 apply (simp add: valid_queues_valid_q) 1241 apply (frule(1) tcb_queue_relation_qhead_valid') 1242 apply (simp add: valid_queues_valid_q) 1243 apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff numPriorities_def 1244 cready_queues_index_to_C_def2) 1245 apply (drule_tac qhead'="tcb_ptr_to_ctcb_ptr t" and s=\<sigma> in tcbSchedEnqueue_update, 1246 simp_all add: valid_queues_valid_q)[1] 1247 apply clarsimp 1248 1249 apply (rule tcb_at_not_NULL, erule obj_at'_weakenE, simp) 1250 apply (frule(2) obj_at_cslift_tcb[OF valid_queues_obj_at'D]) 1251 apply (clarsimp simp: h_val_field_clift' h_t_valid_clift) 1252 apply (erule_tac S="{t, v}" for v in state_relation_queue_update_helper, 1253 (simp | rule globals.equality)+, 1254 simp_all add: typ_heap_simps if_Some_helper numPriorities_def 1255 cready_queues_index_to_C_def2 upd_unless_null_def 1256 del: fun_upd_restrict_conv 1257 cong: if_cong 1258 split del: if_split)[1] 1259 apply simp 1260 apply (rule conjI) 1261 apply clarsimp 1262 apply (drule_tac s="tcb_ptr_to_ctcb_ptr t" in sym, simp) 1263 apply (clarsimp simp add: fun_upd_twist) 1264 prefer 4 1265 apply (simp add: obj_at'_weakenE[OF _ TrueI]) 1266 apply (rule disjI1, erule (1) valid_queues_obj_at'D) 1267 apply clarsimp 1268 apply (fastforce simp: tcb_null_sched_ptrs_def) 1269 apply (simp add: fpu_state_preservation[OF _ h_t_valid_clift] typ_heap_simps') 1270 apply (simp add: typ_heap_simps c_guard_clift) 1271 apply (simp add: guard_is_UNIV_def) 1272 apply simp 1273 apply (wp threadGet_wp) 1274 apply vcg 1275 apply simp 1276 apply (wp threadGet_wp) 1277 apply vcg 1278 apply (rule ccorres_return_Skip[unfolded dc_def]) 1279 apply simp 1280 apply (wp threadGet_wp) 1281 apply vcg 1282 apply (fastforce simp: valid_objs'_def obj_at'_def ran_def projectKOs typ_at'_def 1283 valid_obj'_def inQ_def 1284 dest!: valid_queues_obj_at'D) 1285 done 1286qed 1287 1288lemmas tcbSchedDequeue_update 1289 = tcbDequeue_update[where tn=tcbSchedNext_C and tn_update=tcbSchedNext_C_update 1290 and tp=tcbSchedPrev_C and tp_update=tcbSchedPrev_C_update, 1291 simplified] 1292 1293lemma tcb_queue_relation_prev_next: 1294 "\<lbrakk> tcb_queue_relation tn tp mp queue qprev qhead; 1295 tcbp \<in> set queue; distinct (ctcb_ptr_to_tcb_ptr qprev # queue); 1296 \<forall>t \<in> set queue. tcb_at' t s; qprev \<noteq> tcb_Ptr 0 \<longrightarrow> mp qprev \<noteq> None; 1297 mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb \<rbrakk> 1298 \<Longrightarrow> (tn tcb \<noteq> tcb_Ptr 0 \<longrightarrow> tn tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue 1299 \<and> mp (tn tcb) \<noteq> None \<and> tn tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp) 1300 \<and> (tp tcb \<noteq> tcb_Ptr 0 \<longrightarrow> (tp tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue 1301 \<or> tp tcb = qprev) 1302 \<and> mp (tp tcb) \<noteq> None \<and> tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp) 1303 \<and> (tn tcb \<noteq> tcb_Ptr 0 \<longrightarrow> tn tcb \<noteq> tp tcb)" 1304 apply (induct queue arbitrary: qprev qhead) 1305 apply simp 1306 apply simp 1307 apply (erule disjE) 1308 apply clarsimp 1309 apply (case_tac "queue") 1310 apply clarsimp 1311 apply clarsimp 1312 apply (rule conjI) 1313 apply clarsimp 1314 apply clarsimp 1315 apply (drule_tac f=ctcb_ptr_to_tcb_ptr in arg_cong[where y="tp tcb"], simp) 1316 apply clarsimp 1317 apply fastforce 1318 done 1319 1320lemma tcb_queue_relation_prev_next': 1321 "\<lbrakk> tcb_queue_relation' tn tp mp queue qhead qend; tcbp \<in> set queue; distinct queue; 1322 \<forall>t \<in> set queue. tcb_at' t s; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb \<rbrakk> 1323 \<Longrightarrow> (tn tcb \<noteq> tcb_Ptr 0 \<longrightarrow> tn tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue 1324 \<and> mp (tn tcb) \<noteq> None \<and> tn tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp) 1325 \<and> (tp tcb \<noteq> tcb_Ptr 0 \<longrightarrow> tp tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue 1326 \<and> mp (tp tcb) \<noteq> None \<and> tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp) 1327 \<and> (tn tcb \<noteq> tcb_Ptr 0 \<longrightarrow> tn tcb \<noteq> tp tcb)" 1328 apply (clarsimp simp: tcb_queue_relation'_def split: if_split_asm) 1329 apply (drule(1) tcb_queue_relation_prev_next, simp_all) 1330 apply (fastforce dest: tcb_at_not_NULL) 1331 apply clarsimp 1332 done 1333 1334(* L1 bitmap only updated if L2 entry bits end up all zero *) 1335lemma rf_sr_drop_bitmaps_dequeue_helper_L2: 1336 "\<lbrakk> (\<sigma>,\<sigma>') \<in> rf_sr ; 1337 cbitmap_L2_relation ksqL2upd' ksqL2upd \<rbrakk> 1338 \<Longrightarrow> 1339((\<sigma>\<lparr>ksReadyQueues := ksqupd, 1340 ksReadyQueuesL2Bitmap := ksqL2upd\<rparr>, 1341 \<sigma>'\<lparr>idx_' := i', 1342 queue_' := queue_upd', 1343 globals := globals \<sigma>' 1344 \<lparr>ksReadyQueuesL2Bitmap_' := ksqL2upd', 1345 ksReadyQueues_' := ksqupd'\<rparr>\<rparr>) 1346 \<in> rf_sr) 1347 = 1348((\<sigma>\<lparr>ksReadyQueues := ksqupd\<rparr>, 1349 \<sigma>'\<lparr>idx_' := i', 1350 queue_' := queue_upd', 1351 globals := globals \<sigma>' 1352 \<lparr>ksReadyQueues_' := ksqupd'\<rparr>\<rparr>) \<in> rf_sr) 1353" 1354 unfolding rf_sr_def cstate_relation_def Let_def 1355 carch_state_relation_def cmachine_state_relation_def 1356 by (clarsimp simp: rf_sr_cbitmap_L1_relation rf_sr_cbitmap_L2_relation) 1357 1358lemma rf_sr_drop_bitmaps_dequeue_helper: 1359 "\<lbrakk> (\<sigma>,\<sigma>') \<in> rf_sr ; 1360 cbitmap_L1_relation ksqL1upd' ksqL1upd ; cbitmap_L2_relation ksqL2upd' ksqL2upd \<rbrakk> 1361 \<Longrightarrow> 1362((\<sigma>\<lparr>ksReadyQueues := ksqupd, 1363 ksReadyQueuesL2Bitmap := ksqL2upd, 1364 ksReadyQueuesL1Bitmap := ksqL1upd\<rparr>, 1365 \<sigma>'\<lparr>idx_' := i', 1366 queue_' := queue_upd', 1367 globals := globals \<sigma>' 1368 \<lparr>ksReadyQueuesL2Bitmap_' := ksqL2upd', 1369 ksReadyQueuesL1Bitmap_' := ksqL1upd', 1370 ksReadyQueues_' := ksqupd'\<rparr>\<rparr>) 1371 \<in> rf_sr) 1372 = 1373((\<sigma>\<lparr>ksReadyQueues := ksqupd\<rparr>, 1374 \<sigma>'\<lparr>idx_' := i', 1375 queue_' := queue_upd', 1376 globals := globals \<sigma>' 1377 \<lparr>ksReadyQueues_' := ksqupd'\<rparr>\<rparr>) \<in> rf_sr) 1378" 1379 unfolding rf_sr_def cstate_relation_def Let_def 1380 carch_state_relation_def cmachine_state_relation_def 1381 by (clarsimp simp: rf_sr_cbitmap_L1_relation rf_sr_cbitmap_L2_relation) 1382 1383lemma filter_empty_unfiltered_contr: 1384 "\<lbrakk> [x\<leftarrow>xs . x \<noteq> y] = [] ; x' \<in> set xs ; x' \<noteq> y \<rbrakk> \<Longrightarrow> False" 1385 by (induct xs, auto split: if_split_asm) 1386 1387(* FIXME same proofs as bit_set, maybe can generalise? *) 1388lemma cbitmap_L1_relation_bit_clear: 1389 fixes p :: priority 1390 shows 1391 "\<lbrakk> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>) ; 1392 d \<le> maxDomain \<rbrakk> \<Longrightarrow> 1393 cbitmap_L1_relation 1394 (Arrays.update (ksReadyQueuesL1Bitmap_' (globals x)) (unat d) 1395 (ksReadyQueuesL1Bitmap_' (globals x).[unat d] && ~~ 2 ^ unat (p >> wordRadix))) 1396 ((ksReadyQueuesL1Bitmap \<sigma>)(d := ksReadyQueuesL1Bitmap \<sigma> d && ~~ 2 ^ prioToL1Index p))" 1397 apply (unfold cbitmap_L1_relation_def) 1398 apply (clarsimp simp: prioToL1Index_def wordRadix_def' maxDomain_def numDomains_def word_le_nat_alt) 1399 done 1400 1401lemma cready_queues_relation_empty_queue_helper: 1402 "\<lbrakk> tcbDomain ko \<le> maxDomain ; tcbPriority ko \<le> maxPriority ; 1403 cready_queues_relation (cslift \<sigma>') (ksReadyQueues_' (globals \<sigma>')) (ksReadyQueues \<sigma>)\<rbrakk> 1404 \<Longrightarrow> 1405 cready_queues_relation (cslift \<sigma>') 1406 (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (unat (tcbDomain ko) * 256 + unat (tcbPriority ko)) 1407 (tcb_queue_C.end_C_update (\<lambda>_. NULL) 1408 (head_C_update (\<lambda>_. NULL) 1409 (ksReadyQueues_' (globals \<sigma>').[unat (tcbDomain ko) * 256 + unat (tcbPriority ko)])))) 1410 ((ksReadyQueues \<sigma>)((tcbDomain ko, tcbPriority ko) := []))" 1411 unfolding cready_queues_relation_def Let_def 1412 using maxPrio_to_H[simp] maxDom_to_H[simp] 1413 apply clarsimp 1414 apply (frule (1) cready_queues_index_to_C_in_range[simplified maxDom_to_H maxPrio_to_H]) 1415 apply (fold cready_queues_index_to_C_def[simplified numPriorities_def]) 1416 apply (case_tac "qdom = tcbDomain ko", 1417 simp_all add: prio_and_dom_limit_helpers seL4_MinPrio_def 1418 minDom_def) 1419 apply (fastforce simp: cready_queues_index_to_C_in_range simp: cready_queues_index_to_C_distinct)+ 1420 done 1421 1422lemma cbitmap_L2_relationD: 1423 "\<lbrakk> cbitmap_L2_relation cbitmap2 abitmap2 ; d \<le> maxDomain ; i < l2BitmapSize \<rbrakk> \<Longrightarrow> 1424 cbitmap2.[unat d].[i] = abitmap2 (d, i)" 1425 unfolding cbitmap_L2_relation_def l2BitmapSize_def' 1426 by clarsimp 1427 1428(* FIXME move *) 1429lemma filter_noteq_op: 1430 "[x \<leftarrow> xs . x \<noteq> y] = filter ((\<noteq>) y) xs" 1431 by (induct xs) auto 1432 1433(* FIXME move *) 1434lemma all_filter_propI: 1435 "\<forall>x\<in>set lst. P x \<Longrightarrow> \<forall>x\<in>set (filter Q lst). P x" 1436 by (induct lst, auto) 1437 1438lemma cbitmap_L2_relation_bit_clear: 1439 fixes p :: priority 1440 fixes d :: domain 1441 shows "\<lbrakk> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals \<sigma>')) (ksReadyQueuesL2Bitmap \<sigma>) ; 1442 d \<le> maxDomain \<rbrakk> 1443 \<Longrightarrow> 1444 cbitmap_L2_relation 1445 (Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>')) (unat d) 1446 (Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d]) 1447 (invertL1Index (prioToL1Index p)) 1448 (ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d].[invertL1Index (prioToL1Index p)] && 1449 ~~ 2 ^ unat (p && 0x3F)))) 1450 ((ksReadyQueuesL2Bitmap \<sigma>) 1451 ((d, invertL1Index (prioToL1Index p)) := 1452 ksReadyQueuesL2Bitmap \<sigma> (d, invertL1Index (prioToL1Index p)) && 1453 ~~ 2 ^ unat (p && mask wordRadix)))" 1454 unfolding cbitmap_L2_relation_def numPriorities_def wordBits_def word_size l2BitmapSize_def' 1455 apply (clarsimp simp: word_size prioToL1Index_def wordRadix_def mask_def 1456 invertL1Index_def l2BitmapSize_def' 1457 maxDomain_def numDomains_def word_le_nat_alt) 1458 apply (case_tac "da = d" ; clarsimp) 1459 done 1460 1461lemma tcbSchedDequeue_ccorres': 1462 "ccorres dc xfdc 1463 ((\<lambda>s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) 1464 \<and> distinct (ksReadyQueues s (d, p))) 1465 and valid_queues' and tcb_at' t and valid_objs') 1466 (UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>) 1467 [] 1468 (tcbSchedDequeue t) 1469 (Call tcbSchedDequeue_'proc)" 1470proof - 1471 1472 note prio_and_dom_limit_helpers[simp] word_sle_def[simp] 1473 1474 have ksQ_tcb_at': "\<And>s ko d p. 1475 \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) 1476 \<and> distinct (ksReadyQueues s (d, p)) \<Longrightarrow> 1477 \<forall>t\<in>set (ksReadyQueues s (d, p)). tcb_at' t s" 1478 by (fastforce dest: spec elim: obj_at'_weakenE) 1479 1480 have invert_l1_index_limit: "\<And>p. invertL1Index (prioToL1Index p) < 4" 1481 unfolding invertL1Index_def l2BitmapSize_def' prioToL1Index_def 1482 by simp 1483 1484 show ?thesis 1485 apply (cinit lift: tcb_') 1486 apply (rule_tac r'="\<lambda>rv rv'. rv = to_bool rv'" and xf'="ret__unsigned_longlong_'" 1487 in ccorres_split_nothrow) 1488 apply (rule threadGet_vcg_corres) 1489 apply (rule allI, rule conseqPre, vcg) 1490 apply clarsimp 1491 apply (drule obj_at_ko_at', clarsimp) 1492 apply (drule spec, drule(1) mp, clarsimp) 1493 apply (clarsimp simp: typ_heap_simps ctcb_relation_def) 1494 apply ceqv 1495 apply (simp add: when_def del: Collect_const split del: if_split) 1496 apply (rule ccorres_cond[where R=\<top>]) 1497 apply (simp add: to_bool_def) 1498 apply (rule ccorres_rhs_assoc)+ 1499 apply csymbr 1500 apply csymbr 1501 apply csymbr 1502 apply csymbr 1503 apply (rule_tac r'="\<lambda>rv rv'. rv' = ucast rv" and xf'="dom_'" in ccorres_split_nothrow) 1504 apply (rule threadGet_vcg_corres) 1505 apply (rule allI, rule conseqPre, vcg) 1506 apply clarsimp 1507 apply (drule obj_at_ko_at', clarsimp) 1508 apply (drule spec, drule(1) mp, clarsimp) 1509 apply (clarsimp simp: typ_heap_simps ctcb_relation_def) 1510 apply ceqv 1511 apply (rule_tac r'="\<lambda>rv rv'. rv' = ucast rv" and xf'="prio_'" in ccorres_split_nothrow) 1512 apply (rule threadGet_vcg_corres) 1513 apply (rule allI, rule conseqPre, vcg) 1514 apply clarsimp 1515 apply (drule obj_at_ko_at', clarsimp) 1516 apply (drule spec, drule(1) mp, clarsimp) 1517 apply (clarsimp simp: typ_heap_simps ctcb_relation_def) 1518 apply ceqv 1519 apply (rule ccorres_rhs_assoc2)+ 1520 apply (simp only: bind_assoc[symmetric]) 1521 apply (rule ccorres_split_nothrow_novcg_dc) 1522 prefer 2 1523 apply (rule ccorres_move_c_guard_tcb) 1524 apply (simp only: dc_def[symmetric]) 1525 apply ctac 1526 prefer 2 1527 apply (wp, clarsimp, wp+) 1528 apply (rule_tac P="(\<lambda>s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) 1529 \<and> distinct(ksReadyQueues s (d, p))) 1530 and valid_queues' and obj_at' (inQ rva rvb) t 1531 and (\<lambda>s. rva \<le> maxDomain \<and> rvb \<le> maxPriority)" 1532 and P'=UNIV in ccorres_from_vcg) 1533 apply (rule allI, rule conseqPre, vcg) 1534 apply (clarsimp simp: getQueue_def gets_def get_def setQueue_def modify_def 1535 put_def bind_def return_def bitmap_fun_defs when_def 1536 null_def) 1537 1538 apply (rule conjI; clarsimp simp: queue_in_range[simplified maxDom_to_H maxPrio_to_H]) 1539 apply (rule conjI; clarsimp simp: queue_in_range[simplified maxDom_to_H maxPrio_to_H]) 1540 apply (frule(1) valid_queuesD') 1541 apply (drule (1) obj_at_cslift_tcb, clarsimp simp: inQ_def) 1542 apply (frule_tac d="tcbDomain ko" and p="tcbPriority ko" in rf_sr_sched_queue_relation) 1543 apply (fastforce simp: maxDom_to_H maxPrio_to_H)+ 1544 apply (frule_tac s=\<sigma> in tcb_queue_relation_prev_next'; (fastforce simp: ksQ_tcb_at')?) 1545 apply (drule_tac s=\<sigma> in tcbSchedDequeue_update, assumption, 1546 simp_all add: remove1_filter ksQ_tcb_at')[1] 1547 apply (intro conjI; 1548 clarsimp simp: h_val_field_clift' 1549 h_t_valid_clift[THEN h_t_valid_field] h_t_valid_clift)+ 1550 apply (drule(2) filter_empty_unfiltered_contr, simp)+ 1551 apply (rule conjI; clarsimp) 1552 apply (rule conjI) 1553 apply (fastforce simp: c_invert_assist l2BitmapSize_def' wordRadix_def) 1554 apply (rule conjI; clarsimp) 1555 apply (subst rf_sr_drop_bitmaps_dequeue_helper, assumption) 1556 apply (fastforce intro: cbitmap_L1_relation_bit_clear) 1557 apply (simp add: invert_prioToL1Index_c_simp) 1558 apply (frule rf_sr_cbitmap_L2_relation) 1559 apply (clarsimp simp: cbitmap_L2_relation_def 1560 word_size prioToL1Index_def wordRadix_def mask_def 1561 maxDomain_def numDomains_def word_le_nat_alt 1562 numPriorities_def wordBits_def l2BitmapSize_def' 1563 invertL1Index_def) 1564 apply (case_tac "d = tcbDomain ko" ; fastforce) 1565 1566 apply (drule (1) obj_at_cslift_tcb, clarsimp simp: inQ_def) 1567 apply (frule_tac d="tcbDomain ko" and p="tcbPriority ko" 1568 in rf_sr_sched_queue_relation) 1569 apply (fold_subgoals (prefix))[2] 1570 subgoal premises prems using prems by (fastforce simp: maxDom_to_H maxPrio_to_H)+ 1571 1572 apply (frule_tac s=\<sigma> in tcb_queue_relation_prev_next', assumption) 1573 prefer 3 1574 apply fastforce 1575 apply (fold_subgoals (prefix))[2] 1576 subgoal premises prems using prems by ((fastforce simp: ksQ_tcb_at')+) 1577 apply (drule_tac s=\<sigma> in tcbSchedDequeue_update, assumption, 1578 simp_all add: remove1_filter ksQ_tcb_at')[1] 1579 (* trivial case, setting queue to empty *) 1580 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def 1581 cmachine_state_relation_def) 1582 apply (erule (2) cready_queues_relation_empty_queue_helper) 1583 (* impossible case, C L2 update disagrees with Haskell update *) 1584 apply (simp add: invert_prioToL1Index_c_simp) 1585 apply (subst (asm) Arrays.index_update) 1586 subgoal by (simp add: maxDomain_def numDomains_def word_le_nat_alt) 1587 apply (subst (asm) Arrays.index_update) 1588 apply (simp add: invert_l1_index_limit) 1589 1590 apply (frule rf_sr_cbitmap_L2_relation) 1591 apply (drule_tac i="invertL1Index (prioToL1Index (tcbPriority ko))" 1592 in cbitmap_L2_relationD, assumption) 1593 apply (fastforce simp: l2BitmapSize_def' invert_l1_index_limit) 1594 apply (fastforce simp: prioToL1Index_def invertL1Index_def mask_def wordRadix_def) 1595 (* impossible case *) 1596 apply (clarsimp simp: h_val_field_clift' h_t_valid_clift) 1597 apply (drule(2) filter_empty_unfiltered_contr, fastforce) 1598 1599 apply (frule (1) valid_queuesD') 1600 apply (drule (1) obj_at_cslift_tcb, clarsimp simp: inQ_def) 1601 apply (frule_tac d="tcbDomain ko" and p="tcbPriority ko" 1602 in rf_sr_sched_queue_relation) 1603 apply fold_subgoals[2] 1604 apply (fastforce simp: maxDom_to_H maxPrio_to_H)+ 1605 apply (clarsimp simp: h_val_field_clift' 1606 h_t_valid_clift[THEN h_t_valid_field] h_t_valid_clift) 1607 apply (frule_tac s=\<sigma> in tcb_queue_relation_prev_next', assumption) 1608 prefer 3 1609 apply fastforce 1610 apply (fold_subgoals (prefix))[2] 1611 subgoal premises prems using prems by (fastforce simp: ksQ_tcb_at')+ 1612 apply (drule_tac s=\<sigma> in tcbSchedDequeue_update, assumption, 1613 simp_all add: remove1_filter ksQ_tcb_at')[1] 1614 apply (clarsimp simp: filter_noteq_op upd_unless_null_def) 1615 apply (rule conjI, clarsimp) 1616 apply (clarsimp simp: h_val_field_clift' 1617 h_t_valid_clift[THEN h_t_valid_field] h_t_valid_clift) 1618 apply (rule conjI; clarsimp) 1619 apply (simp add: typ_heap_simps) 1620 apply (clarsimp simp: h_t_valid_c_guard [OF h_t_valid_field, OF h_t_valid_clift] 1621 h_t_valid_field[OF h_t_valid_clift] h_t_valid_clift) 1622 apply (erule_tac S="set (ksReadyQueues \<sigma> (tcbDomain ko, tcbPriority ko))" 1623 in state_relation_queue_update_helper', 1624 (simp | rule globals.equality)+, 1625 simp_all add: clift_field_update if_Some_helper numPriorities_def 1626 cready_queues_index_to_C_def2 typ_heap_simps 1627 maxDom_to_H maxPrio_to_H 1628 cong: if_cong split del: if_split)[1] 1629 1630 apply (fastforce simp: tcb_null_sched_ptrs_def typ_heap_simps c_guard_clift 1631 elim: obj_at'_weaken)+ 1632 apply (erule_tac S="set (ksReadyQueues \<sigma> (tcbDomain ko, tcbPriority ko))" 1633 in state_relation_queue_update_helper', 1634 (simp | rule globals.equality)+, 1635 simp_all add: clift_field_update if_Some_helper numPriorities_def 1636 cready_queues_index_to_C_def2 1637 maxDom_to_H maxPrio_to_H 1638 cong: if_cong split del: if_split, 1639 simp_all add: typ_heap_simps')[1] 1640 subgoal by (fastforce simp: tcb_null_sched_ptrs_def) 1641 subgoal by (simp add: fpu_state_preservation[OF _ h_t_valid_clift] typ_heap_simps') 1642 subgoal by fastforce 1643 apply clarsimp 1644 apply (rule conjI; clarsimp) 1645 apply (rule conjI) 1646 apply (fastforce simp: c_invert_assist l2BitmapSize_def' wordRadix_def) 1647 apply (rule conjI; clarsimp) 1648 (* invalid, missing bitmap updates on haskell side *) 1649 apply (fold_subgoals (prefix))[2] 1650 subgoal premises prems using prems 1651 by (fastforce dest!: tcb_queue_relation'_empty_ksReadyQueues 1652 elim: obj_at'_weaken)+ 1653 apply (clarsimp simp: h_val_field_clift' h_t_valid_clift) 1654 apply (erule_tac S="set (ksReadyQueues \<sigma> (tcbDomain ko, tcbPriority ko))" 1655 in state_relation_queue_update_helper', 1656 (simp | rule globals.equality)+, 1657 simp_all add: clift_field_update if_Some_helper numPriorities_def 1658 cready_queues_index_to_C_def2 1659 maxDom_to_H maxPrio_to_H 1660 cong: if_cong split del: if_split)[1] 1661 apply (fold_subgoals (prefix))[4] 1662 subgoal premises prems using prems 1663 by - (fastforce simp: typ_heap_simps c_guard_clift tcb_null_sched_ptrs_def 1664 clift_heap_update_same[OF h_t_valid_clift] 1665 fpu_state_preservation[OF _ h_t_valid_clift])+ 1666 apply (rule conjI; clarsimp simp: queue_in_range[simplified maxDom_to_H maxPrio_to_H]) 1667 apply (frule (1) valid_queuesD') 1668 apply (drule (1) obj_at_cslift_tcb, clarsimp simp: inQ_def) 1669 apply (frule_tac d="tcbDomain ko" and p="tcbPriority ko" 1670 in rf_sr_sched_queue_relation) 1671 apply (fold_subgoals (prefix))[2] 1672 subgoal premises prems using prems by (fastforce simp: maxDom_to_H maxPrio_to_H)+ 1673 apply (clarsimp simp: h_val_field_clift' 1674 h_t_valid_clift[THEN h_t_valid_field] h_t_valid_clift) 1675 apply (frule_tac s=\<sigma> in tcb_queue_relation_prev_next') 1676 apply fastforce 1677 prefer 3 1678 apply fastforce 1679 apply (fold_subgoals (prefix))[2] 1680 subgoal premises prems using prems by (fastforce simp: ksQ_tcb_at')+ 1681 apply (drule_tac s=\<sigma> in tcbSchedDequeue_update, assumption, 1682 simp_all add: remove1_filter ksQ_tcb_at')[1] 1683 apply (clarsimp simp: filter_noteq_op upd_unless_null_def) 1684 apply (rule conjI; clarsimp) 1685 apply (clarsimp simp: h_val_field_clift' 1686 h_t_valid_clift[THEN h_t_valid_field] h_t_valid_clift) 1687 apply (clarsimp simp: typ_heap_simps) 1688 apply (rule conjI; clarsimp simp: typ_heap_simps) 1689 apply (drule(2) filter_empty_unfiltered_contr[simplified filter_noteq_op], simp) 1690 apply (rule conjI) 1691 apply (fastforce simp: c_invert_assist l2BitmapSize_def' wordRadix_def) 1692 apply (rule conjI; clarsimp) 1693 (* impossible case, C L2 update disagrees with Haskell update *) 1694 apply (subst (asm) Arrays.index_update) 1695 apply (simp add: maxDomain_def numDomains_def word_le_nat_alt) 1696 apply (subst (asm) Arrays.index_update) 1697 subgoal using invert_l1_index_limit 1698 by (fastforce simp add: invert_prioToL1Index_c_simp intro: nat_Suc_less_le_imp) 1699 apply (frule rf_sr_cbitmap_L2_relation) 1700 apply (simp add: invert_prioToL1Index_c_simp) 1701 apply (drule_tac i="invertL1Index (prioToL1Index (tcbPriority ko))" 1702 in cbitmap_L2_relationD, assumption) 1703 subgoal by (simp add: invert_l1_index_limit l2BitmapSize_def') 1704 apply (fastforce simp: prioToL1Index_def invertL1Index_def mask_def wordRadix_def) 1705 1706 apply (simp add: invert_prioToL1Index_c_simp) 1707 apply (subst rf_sr_drop_bitmaps_dequeue_helper_L2, assumption) 1708 subgoal by (fastforce dest: rf_sr_cbitmap_L2_relation elim!: cbitmap_L2_relation_bit_clear) 1709 1710 (* trivial case, setting queue to empty *) 1711 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def 1712 cmachine_state_relation_def) 1713 apply (erule (2) cready_queues_relation_empty_queue_helper) 1714 1715 apply (frule (1) valid_queuesD') 1716 apply (drule (1) obj_at_cslift_tcb, clarsimp simp: inQ_def) 1717 apply (frule_tac d="tcbDomain ko" and p="tcbPriority ko" 1718 in rf_sr_sched_queue_relation) 1719 apply (fold_subgoals (prefix))[2] 1720 subgoal premises prems using prems by (fastforce simp: maxDom_to_H maxPrio_to_H)+ 1721 apply (clarsimp simp: h_val_field_clift' 1722 h_t_valid_clift[THEN h_t_valid_field] h_t_valid_clift) 1723 apply (simp add: invert_prioToL1Index_c_simp) 1724 apply (frule_tac s=\<sigma> in tcb_queue_relation_prev_next') 1725 apply (fastforce simp add: ksQ_tcb_at')+ 1726 apply (drule_tac s=\<sigma> in tcbSchedDequeue_update, assumption, 1727 simp_all add: remove1_filter ksQ_tcb_at')[1] 1728 apply (clarsimp simp: filter_noteq_op upd_unless_null_def) 1729 apply (rule conjI, clarsimp) 1730 apply (clarsimp simp: h_val_field_clift' 1731 h_t_valid_clift[THEN h_t_valid_field] h_t_valid_clift) 1732 apply (clarsimp simp: typ_heap_simps) 1733 apply (rule conjI; clarsimp simp: typ_heap_simps) 1734 apply (erule_tac S="set (ksReadyQueues \<sigma> (tcbDomain ko, tcbPriority ko))" 1735 in state_relation_queue_update_helper', 1736 (simp | rule globals.equality)+, 1737 simp_all add: clift_field_update if_Some_helper numPriorities_def 1738 cready_queues_index_to_C_def2 1739 maxDom_to_H maxPrio_to_H 1740 cong: if_cong split del: if_split)[1] 1741 apply (fastforce simp: tcb_null_sched_ptrs_def) 1742 apply (clarsimp simp: typ_heap_simps) 1743 apply (fastforce simp: typ_heap_simps) 1744 apply (fastforce simp: tcb_null_sched_ptrs_def) 1745 apply (erule_tac S="set (ksReadyQueues \<sigma> (tcbDomain ko, tcbPriority ko))" 1746 in state_relation_queue_update_helper', 1747 (simp | rule globals.equality)+, 1748 simp_all add: clift_field_update if_Some_helper numPriorities_def 1749 cready_queues_index_to_C_def2 1750 maxDom_to_H maxPrio_to_H 1751 cong: if_cong split del: if_split)[1] 1752 apply (fold_subgoals (prefix))[4] 1753 subgoal premises prems using prems 1754 by - (fastforce simp: typ_heap_simps c_guard_clift tcb_null_sched_ptrs_def 1755 clift_heap_update_same[OF h_t_valid_clift] 1756 fpu_state_preservation[OF _ h_t_valid_clift])+ 1757 apply (clarsimp) 1758 apply (rule conjI; clarsimp simp: typ_heap_simps) 1759 apply (rule conjI) 1760 apply (fastforce simp: c_invert_assist l2BitmapSize_def' wordRadix_def) 1761 apply (rule conjI; clarsimp) 1762 (* invalid, missing bitmap updates on haskell side *) 1763 apply (drule tcb_queue_relation'_empty_ksReadyQueues) 1764 apply (fold_subgoals (prefix))[2] 1765 subgoal premises prems using prems by (fastforce elim: obj_at'_weaken)+ 1766 (* invalid, missing bitmap updates on haskell side *) 1767 apply (drule tcb_queue_relation'_empty_ksReadyQueues) 1768 apply (fold_subgoals (prefix))[2] 1769 subgoal premises prems using prems by (fastforce elim: obj_at'_weaken)+ 1770 apply (erule_tac S="set (ksReadyQueues \<sigma> (tcbDomain ko, tcbPriority ko))" 1771 in state_relation_queue_update_helper', 1772 (simp | rule globals.equality)+, 1773 simp_all add: clift_field_update if_Some_helper numPriorities_def 1774 cready_queues_index_to_C_def2 typ_heap_simps 1775 maxDom_to_H maxPrio_to_H 1776 cong: if_cong split del: if_split)[1] 1777 apply (fold_subgoals (prefix))[2] 1778 subgoal premises prems using prems 1779 by (fastforce simp: typ_heap_simps c_guard_clift tcb_null_sched_ptrs_def)+ 1780 apply (simp add: guard_is_UNIV_def) 1781 apply simp 1782 apply (wp threadGet_wp) 1783 apply vcg 1784 apply simp 1785 apply (wp threadGet_wp) 1786 apply vcg 1787 apply (rule ccorres_return_Skip[unfolded dc_def]) 1788 apply simp 1789 apply (wp threadGet_wp) 1790 apply vcg 1791 by (fastforce simp: valid_objs'_def obj_at'_def ran_def projectKOs typ_at'_def 1792 valid_obj'_def valid_tcb'_def inQ_def) 1793qed 1794 1795lemma tcbSchedDequeue_ccorres: 1796 "ccorres dc xfdc 1797 (valid_queues and valid_queues' and tcb_at' t and valid_objs') 1798 (UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>) 1799 [] 1800 (tcbSchedDequeue t) 1801 (Call tcbSchedDequeue_'proc)" 1802 apply (rule ccorres_guard_imp [OF tcbSchedDequeue_ccorres']) 1803 apply (clarsimp simp: valid_queues_def valid_queues_no_bitmap_def) 1804 apply (drule_tac x=d in spec) 1805 apply (drule_tac x=p in spec) 1806 apply (clarsimp) 1807 apply (drule(1) bspec) 1808 apply (erule obj_at'_weakenE) 1809 apply (clarsimp)+ 1810 done 1811 1812lemma tcb_queue_relation_append: 1813 "\<lbrakk> tcb_queue_relation tn tp mp queue qprev qhead; queue \<noteq> []; 1814 qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qend' = Some tcb; 1815 queue = queue' @ [ctcb_ptr_to_tcb_ptr qend]; distinct queue; 1816 \<forall>x \<in> set queue. tcb_ptr_to_ctcb_ptr x \<noteq> NULL; qend' \<noteq> NULL; 1817 \<And>v f g. tn (tn_update f v) = f (tn v) \<and> tp (tp_update g v) = g (tp v) 1818 \<and> tn (tp_update f v) = tn v \<and> tp (tn_update g v) = tp v \<rbrakk> 1819 \<Longrightarrow> tcb_queue_relation tn tp 1820 (mp (qend \<mapsto> tn_update (\<lambda>_. qend') (the (mp qend)), 1821 qend' \<mapsto> tn_update (\<lambda>_. NULL) (tp_update (\<lambda>_. qend) tcb))) 1822 (queue @ [ctcb_ptr_to_tcb_ptr qend']) qprev qhead" 1823 using [[hypsubst_thin = true]] 1824 apply clarsimp 1825 apply (induct queue' arbitrary: qprev qhead) 1826 apply clarsimp 1827 apply clarsimp 1828 done 1829 1830lemma tcbSchedAppend_update: 1831 assumes sr: "sched_queue_relation' mp queue qhead qend" 1832 and qh': "qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue" 1833 and cs_tcb: "mp qend' = Some tcb" 1834 and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 1835 and qhN: "qend' \<noteq> NULL" 1836 shows 1837 "sched_queue_relation' 1838 (upd_unless_null qend (tcbSchedNext_C_update (\<lambda>_. qend') (the (mp qend))) 1839 (mp(qend' \<mapsto> tcb\<lparr>tcbSchedNext_C := NULL, tcbSchedPrev_C := qend\<rparr>))) 1840 (queue @ [ctcb_ptr_to_tcb_ptr qend']) (if queue = [] then qend' else qhead) qend'" 1841 using sr qh' valid_ep cs_tcb qhN 1842 apply - 1843 apply (rule rev_cases[where xs=queue]) 1844 apply (simp add: tcb_queue_relation'_def upd_unless_null_def) 1845 apply (clarsimp simp: tcb_queue_relation'_def upd_unless_null_def tcb_at_not_NULL) 1846 apply (drule_tac qend'=qend' and tn_update=tcbSchedNext_C_update 1847 and tp_update=tcbSchedPrev_C_update and qend="tcb_ptr_to_ctcb_ptr y" 1848 in tcb_queue_relation_append, simp_all) 1849 apply (fastforce simp add: tcb_at_not_NULL) 1850 apply (simp add: fun_upd_twist) 1851 done 1852 1853lemma tcb_queue_relation_qend_mems: 1854 "\<lbrakk> tcb_queue_relation' getNext getPrev mp queue qhead qend; 1855 \<forall>x \<in> set queue. tcb_at' x s \<rbrakk> 1856 \<Longrightarrow> (qend = NULL \<longrightarrow> queue = []) 1857 \<and> (qend \<noteq> NULL \<longrightarrow> ctcb_ptr_to_tcb_ptr qend \<in> set queue)" 1858 apply (clarsimp simp: tcb_queue_relation'_def) 1859 apply (drule bspec, erule last_in_set) 1860 apply (simp add: tcb_at_not_NULL) 1861 done 1862 1863lemma tcbSchedAppend_ccorres: 1864 "ccorres dc xfdc 1865 (valid_queues and tcb_at' t and valid_objs') 1866 (UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>) 1867 [] 1868 (tcbSchedAppend t) 1869 (Call tcbSchedAppend_'proc)" 1870proof - 1871 note prio_and_dom_limit_helpers[simp] word_sle_def[simp] maxDom_to_H[simp] maxPrio_to_H[simp] 1872 1873 show ?thesis 1874 apply (cinit lift: tcb_') 1875 apply (rule_tac r'="\<lambda>rv rv'. rv = to_bool rv'" 1876 and xf'="ret__unsigned_longlong_'" in ccorres_split_nothrow) 1877 apply (rule threadGet_vcg_corres) 1878 apply (rule allI, rule conseqPre, vcg) 1879 apply clarsimp 1880 apply (drule obj_at_ko_at', clarsimp) 1881 apply (drule spec, drule(1) mp, clarsimp) 1882 apply (clarsimp simp: typ_heap_simps ctcb_relation_def) 1883 apply ceqv 1884 apply (simp add: when_def unless_def del: Collect_const split del: if_split) 1885 apply (rule ccorres_cond[where R=\<top>]) 1886 apply (simp add: to_bool_def) 1887 apply (rule ccorres_rhs_assoc)+ 1888 apply csymbr 1889 apply csymbr 1890 apply csymbr 1891 apply csymbr 1892 apply (rule_tac r'="\<lambda>rv rv'. rv' = ucast rv" 1893 and xf'="dom_'" in ccorres_split_nothrow) 1894 apply (rule threadGet_vcg_corres) 1895 apply (rule allI, rule conseqPre, vcg) 1896 apply clarsimp 1897 apply (drule obj_at_ko_at', clarsimp) 1898 apply (drule spec, drule(1) mp, clarsimp) 1899 apply (clarsimp simp: typ_heap_simps ctcb_relation_def) 1900 apply ceqv 1901 apply (rule_tac r'="\<lambda>rv rv'. rv' = ucast rv" 1902 and xf'="prio_'" in ccorres_split_nothrow) 1903 apply (rule threadGet_vcg_corres) 1904 apply (rule allI, rule conseqPre, vcg) 1905 apply clarsimp 1906 apply (drule obj_at_ko_at', clarsimp) 1907 apply (drule spec, drule(1) mp, clarsimp) 1908 apply (clarsimp simp: typ_heap_simps ctcb_relation_def) 1909 apply ceqv 1910 apply (rule ccorres_rhs_assoc2)+ 1911 apply (simp only: bind_assoc[symmetric]) 1912 apply (rule ccorres_split_nothrow_novcg_dc) 1913 prefer 2 1914 apply (rule ccorres_move_c_guard_tcb) 1915 apply (simp only: dc_def[symmetric]) 1916 apply ctac 1917 prefer 2 1918 apply (wp, clarsimp, wp+) 1919 apply (rule_tac P="\<lambda>s. valid_queues s \<and> (\<forall>p. t \<notin> set (ksReadyQueues s p)) 1920 \<and> (\<exists>tcb. ko_at' tcb t s \<and> tcbDomain tcb =rva 1921 \<and> tcbPriority tcb = rvb \<and> valid_tcb' tcb s)" 1922 and P'=UNIV in ccorres_from_vcg) 1923 apply (rule allI, rule conseqPre, vcg) 1924 apply (clarsimp simp: getQueue_def gets_def get_def setQueue_def modify_def 1925 put_def bind_def return_def bitmap_fun_defs null_def) 1926 apply (clarsimp simp: queue_in_range valid_tcb'_def) 1927 apply (rule conjI; clarsimp simp: queue_in_range) 1928 apply (drule (1) obj_at_cslift_tcb) 1929 apply clarsimp 1930 apply (frule_tac d="tcbDomain tcb" and p="tcbPriority tcb" 1931 in rf_sr_sched_queue_relation) 1932 apply clarsimp 1933 apply clarsimp 1934 apply (frule_tac s=\<sigma> in tcb_queue'_head_end_NULL) 1935 apply (simp add: valid_queues_valid_q) 1936 apply (frule_tac s=\<sigma> in tcb_queue_relation_qend_mems, simp add: valid_queues_valid_q) 1937 apply (drule_tac qend'="tcb_ptr_to_ctcb_ptr t" and s=\<sigma> in tcbSchedAppend_update, 1938 simp_all add: valid_queues_valid_q)[1] 1939 apply (rule tcb_at_not_NULL, erule obj_at'_weakenE, simp) 1940 apply (clarsimp simp: h_val_field_clift' h_t_valid_clift) 1941 apply (simp add: invert_prioToL1Index_c_simp) 1942 apply (rule conjI; clarsimp) 1943 apply (rule conjI) 1944 apply (fastforce simp: c_invert_assist l2BitmapSize_def' wordRadix_def) 1945 apply (simp add: t_hrs_ksReadyQueues_upd_absorb) 1946 apply (subst rf_sr_drop_bitmaps_enqueue_helper, assumption) 1947 apply (fastforce intro: cbitmap_L1_relation_bit_set) 1948 subgoal by (fastforce intro: cbitmap_L2_relation_bit_set simp: wordRadix_def mask_def) 1949 apply (erule(1) state_relation_queue_update_helper[where S="{t}"], 1950 (simp | rule globals.equality)+, 1951 simp_all add: cready_queues_index_to_C_def2 numPriorities_def 1952 t_hrs_ksReadyQueues_upd_absorb upd_unless_null_def 1953 typ_heap_simps)[1] 1954 apply (fastforce simp: tcb_null_sched_ptrs_def elim: obj_at'_weaken) 1955 apply (fastforce simp: tcb_null_sched_ptrs_def elim: obj_at'_weaken) 1956 apply (clarsimp simp: upd_unless_null_def cready_queues_index_to_C_def numPriorities_def) 1957 apply (rule conjI; clarsimp simp: queue_in_range) 1958 apply (drule (1) obj_at_cslift_tcb) 1959 apply clarsimp 1960 apply (frule_tac d="tcbDomain tcb" and p="tcbPriority tcb" 1961 in rf_sr_sched_queue_relation) 1962 apply clarsimp 1963 apply clarsimp 1964 apply (frule_tac s=\<sigma> in tcb_queue'_head_end_NULL) 1965 apply (simp add: valid_queues_valid_q) 1966 apply (frule_tac s=\<sigma> in tcb_queue_relation_qend_mems, 1967 simp add: valid_queues_valid_q) 1968 apply (drule_tac qend'="tcb_ptr_to_ctcb_ptr t" and s=\<sigma> in tcbSchedAppend_update, 1969 simp_all add: valid_queues_valid_q)[1] 1970 apply clarsimp 1971 apply (rule tcb_at_not_NULL, erule obj_at'_weakenE, simp) 1972 apply (clarsimp simp: h_val_field_clift' h_t_valid_clift) 1973 apply (clarsimp simp: upd_unless_null_def cready_queues_index_to_C_def numPriorities_def) 1974 apply (drule (1) obj_at_cslift_tcb) 1975 apply clarsimp 1976 apply (frule_tac d="tcbDomain tcb" and p="tcbPriority tcb" 1977 in rf_sr_sched_queue_relation) 1978 apply clarsimp 1979 apply clarsimp 1980 apply (frule_tac s=\<sigma> in tcb_queue'_head_end_NULL) 1981 apply (simp add: valid_queues_valid_q) 1982 apply (frule_tac s=\<sigma> in tcb_queue_relation_qend_mems, 1983 simp add: valid_queues_valid_q) 1984 apply (drule_tac qend'="tcb_ptr_to_ctcb_ptr t" and s=\<sigma> in tcbSchedAppend_update, 1985 simp_all add: valid_queues_valid_q)[1] 1986 apply clarsimp 1987 apply (rule tcb_at_not_NULL, erule obj_at'_weakenE, simp) 1988 apply (clarsimp simp: cready_queues_index_to_C_def2 numPriorities_def) 1989 apply (frule(2) obj_at_cslift_tcb[OF valid_queues_obj_at'D]) 1990 apply (clarsimp simp: h_val_field_clift' h_t_valid_clift) 1991 apply (erule_tac S="{t, v}" for v in state_relation_queue_update_helper, 1992 (simp | rule globals.equality)+, 1993 simp_all add: typ_heap_simps if_Some_helper numPriorities_def 1994 cready_queues_index_to_C_def2 upd_unless_null_def 1995 cong: if_cong split del: if_split 1996 del: fun_upd_restrict_conv)[1] 1997 apply simp 1998 apply (rule conjI) 1999 apply clarsimp 2000 apply (drule_tac s="tcb_ptr_to_ctcb_ptr t" in sym, simp) 2001 apply (clarsimp simp add: fun_upd_twist) 2002 prefer 3 2003 apply (simp add: obj_at'_weakenE[OF _ TrueI]) 2004 apply (rule disjI1, erule valid_queues_obj_at'D) 2005 subgoal by simp 2006 subgoal by simp 2007 subgoal by (fastforce simp: tcb_null_sched_ptrs_def) 2008 apply (simp add: guard_is_UNIV_def) 2009 apply simp 2010 apply (wp threadGet_wp) 2011 apply vcg 2012 apply simp 2013 apply (wp threadGet_wp) 2014 apply vcg 2015 apply (rule ccorres_return_Skip[unfolded dc_def]) 2016 apply simp 2017 apply (wp threadGet_wp) 2018 apply vcg 2019 by (fastforce simp: valid_objs'_def obj_at'_def ran_def projectKOs typ_at'_def 2020 valid_obj'_def inQ_def 2021 dest!: valid_queues_obj_at'D) 2022qed 2023 2024lemma true_eq_from_bool [simp]: 2025 "(scast true = from_bool P) = P" 2026 by (simp add: true_def from_bool_def split: bool.splits) 2027 2028lemma isBlocked_spec: 2029 "\<forall>s. \<Gamma> \<turnstile> ({s} \<inter> {s. cslift s (thread_' s) \<noteq> None}) Call isBlocked_'proc 2030 {s'. ret__unsigned_long_' s' = from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift s (thread_' s))))) \<in> 2031 {scast ThreadState_BlockedOnReply, 2032 scast ThreadState_BlockedOnNotification, scast ThreadState_BlockedOnSend, 2033 scast ThreadState_BlockedOnReceive, scast ThreadState_Inactive}) }" 2034 apply vcg 2035 apply (clarsimp simp: typ_heap_simps) 2036done 2037 2038lemma isRunnable_spec: 2039 "\<forall>s. \<Gamma> \<turnstile> ({s} \<inter> {s. cslift s (thread_' s) \<noteq> None}) Call isRunnable_'proc 2040 {s'. ret__unsigned_long_' s' = from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift s (thread_' s))))) \<in> 2041 { scast ThreadState_Running, scast ThreadState_Restart })}" 2042 apply vcg 2043 apply (clarsimp simp: typ_heap_simps) 2044done 2045 2046(* FIXME: move *) 2047lemma ccorres_setSchedulerAction: 2048 "cscheduler_action_relation a p \<Longrightarrow> 2049 ccorres dc xfdc \<top> UNIV hs 2050 (setSchedulerAction a) 2051 (Basic (\<lambda>s. globals_update (ksSchedulerAction_'_update (\<lambda>_. p)) s))" 2052 apply (rule ccorres_from_vcg) 2053 apply (rule allI, rule conseqPre, vcg) 2054 apply (clarsimp simp: setSchedulerAction_def modify_def get_def put_def bind_def) 2055 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def cmachine_state_relation_def) 2056 done 2057 2058declare ge_0_from_bool [simp] 2059 2060lemma scheduler_action_case_switch_to_if: 2061 "(case act of SwitchToThread t \<Rightarrow> f t | _ \<Rightarrow> g) 2062 = (if \<exists>t. act = SwitchToThread t 2063 then f (case act of SwitchToThread t \<Rightarrow> t) else g)" 2064 by (simp split: scheduler_action.split) 2065 2066lemma tcb_at_1: 2067 "tcb_at' t s \<Longrightarrow> tcb_ptr_to_ctcb_ptr t \<noteq> tcb_Ptr 1" 2068 apply (drule is_aligned_tcb_ptr_to_ctcb_ptr) 2069 apply (clarsimp simp add: is_aligned_def max_word_def ctcb_size_bits_def) 2070 done 2071 2072lemma rescheduleRequired_ccorres: 2073 "ccorres dc xfdc (valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') 2074 UNIV [] rescheduleRequired (Call rescheduleRequired_'proc)" 2075 apply cinit 2076 apply (rule ccorres_symb_exec_l) 2077 apply (rule ccorres_split_nothrow_novcg[where r'=dc and xf'=xfdc]) 2078 apply (simp add: scheduler_action_case_switch_to_if 2079 cong: if_weak_cong split del: if_split) 2080 apply (rule_tac R="\<lambda>s. action = ksSchedulerAction s \<and> weak_sch_act_wf action s" 2081 in ccorres_cond) 2082 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 2083 cscheduler_action_relation_def) 2084 subgoal by (clarsimp simp: weak_sch_act_wf_def tcb_at_1 tcb_at_not_NULL 2085 split: scheduler_action.split_asm dest!: pred_tcb_at') 2086 apply (ctac add: tcbSchedEnqueue_ccorres) 2087 apply (rule ccorres_return_Skip) 2088 apply ceqv 2089 apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV]) 2090 apply (rule allI, rule conseqPre, vcg) 2091 apply (clarsimp simp: setSchedulerAction_def simpler_modify_def) 2092 subgoal by (clarsimp simp: rf_sr_def cstate_relation_def Let_def 2093 cscheduler_action_relation_def 2094 carch_state_relation_def cmachine_state_relation_def 2095 max_word_def) 2096 apply wp 2097 apply (simp add: guard_is_UNIV_def) 2098 apply wp+ 2099 apply (simp add: getSchedulerAction_def) 2100 apply (clarsimp simp: weak_sch_act_wf_def rf_sr_def cstate_relation_def 2101 Let_def cscheduler_action_relation_def) 2102 by (auto simp: tcb_at_not_NULL tcb_at_1 2103 tcb_at_not_NULL[THEN not_sym] tcb_at_1[THEN not_sym] 2104 split: scheduler_action.split_asm) 2105 2106lemma getReadyQueuesL1Bitmap_sp: 2107 "\<lbrace>\<lambda>s. P s \<and> d \<le> maxDomain \<rbrace> 2108 getReadyQueuesL1Bitmap d 2109 \<lbrace>\<lambda>rv s. ksReadyQueuesL1Bitmap s d = rv \<and> d \<le> maxDomain \<and> P s\<rbrace>" 2110 unfolding bitmap_fun_defs 2111 by wp simp 2112 2113(* this doesn't actually carry over d \<le> maxDomain to the rest of the ccorres, 2114 use ccorres_cross_over_guard to do that *) 2115lemma ccorres_pre_getReadyQueuesL1Bitmap: 2116 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 2117 shows "ccorres r xf 2118 (\<lambda>s. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s d = rv \<longrightarrow> P rv s)) 2119 {s. \<forall>rv. (ksReadyQueuesL1Bitmap_' (globals s)).[unat d] = ucast rv 2120 \<longrightarrow> s \<in> P' rv } 2121 hs (getReadyQueuesL1Bitmap d >>= (\<lambda>rv. f rv)) c" 2122 apply (rule ccorres_guard_imp) 2123 apply (rule ccorres_symb_exec_l2) 2124 defer 2125 defer 2126 apply (rule getReadyQueuesL1Bitmap_sp) 2127 apply blast 2128 apply clarsimp 2129 prefer 3 2130 apply (clarsimp simp: bitmap_fun_defs gets_exs_valid) 2131 defer 2132 apply (rule ccorres_guard_imp) 2133 apply (rule cc) 2134 apply blast 2135 apply assumption 2136 apply (drule rf_sr_cbitmap_L1_relation) 2137 apply (clarsimp simp: cbitmap_L1_relation_def) 2138 done 2139 2140lemma getReadyQueuesL2Bitmap_sp: 2141 "\<lbrace>\<lambda>s. P s \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<rbrace> 2142 getReadyQueuesL2Bitmap d i 2143 \<lbrace>\<lambda>rv s. ksReadyQueuesL2Bitmap s (d, i) = rv \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> P s\<rbrace>" 2144 unfolding bitmap_fun_defs 2145 by wp simp 2146 2147lemma ccorres_pre_getReadyQueuesL2Bitmap: 2148 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 2149 shows "ccorres r xf 2150 (\<lambda>s. d \<le> maxDomain \<and> i < l2BitmapSize 2151 \<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d,i) = rv \<longrightarrow> P rv s)) 2152 {s. \<forall>rv. (ksReadyQueuesL2Bitmap_' (globals s)).[unat d].[i] = ucast rv 2153 \<longrightarrow> s \<in> P' rv } 2154 hs (getReadyQueuesL2Bitmap d i >>= (\<lambda>rv. f rv)) c" 2155 apply (rule ccorres_guard_imp) 2156 apply (rule ccorres_symb_exec_l2) 2157 defer 2158 defer 2159 apply (rule getReadyQueuesL2Bitmap_sp) 2160 apply blast 2161 apply clarsimp 2162 prefer 3 2163 apply (clarsimp simp: bitmap_fun_defs gets_exs_valid) 2164 defer 2165 apply (rule ccorres_guard_imp) 2166 apply (rule cc) 2167 apply blast 2168 apply assumption 2169 apply (drule rf_sr_cbitmap_L2_relation) 2170 apply (clarsimp simp: cbitmap_L2_relation_def) 2171 done 2172 2173lemma rf_sr_ksReadyQueuesL1Bitmap_simp: 2174 "\<lbrakk> (\<sigma>, s') \<in> rf_sr ; d \<le> maxDomain \<rbrakk> 2175 \<Longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] = ksReadyQueuesL1Bitmap \<sigma> d" 2176 apply (drule rf_sr_cbitmap_L1_relation) 2177 apply (simp add: cbitmap_L1_relation_def) 2178 done 2179 2180lemma cguard_UNIV: 2181 "P s \<Longrightarrow> s \<in> (if P s then UNIV else {})" 2182 by fastforce 2183 2184lemma lookupBitmapPriority_le_maxPriority: 2185 "\<lbrakk> ksReadyQueuesL1Bitmap s d \<noteq> 0 ; valid_queues s \<rbrakk> 2186 \<Longrightarrow> lookupBitmapPriority d s \<le> maxPriority" 2187 unfolding valid_queues_def valid_queues_no_bitmap_def 2188 by (fastforce dest!: bitmapQ_from_bitmap_lookup bitmapQ_ksReadyQueuesI intro: ccontr) 2189 2190lemma rf_sr_ksReadyQueuesL1Bitmap_not_zero: 2191 "\<lbrakk> (\<sigma>, s') \<in> rf_sr ; d \<le> maxDomain ; ksReadyQueuesL1Bitmap_' (globals s').[unat d] \<noteq> 0 \<rbrakk> 2192 \<Longrightarrow> ksReadyQueuesL1Bitmap \<sigma> d \<noteq> 0" 2193 apply (drule rf_sr_cbitmap_L1_relation) 2194 apply (simp add: cbitmap_L1_relation_def) 2195 done 2196 2197lemma ksReadyQueuesL1Bitmap_word_log2_max: 2198 "\<lbrakk>valid_queues s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk> 2199 \<Longrightarrow> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize" 2200 unfolding valid_queues_def 2201 by (fastforce dest: word_log2_nth_same bitmapQ_no_L1_orphansD) 2202 2203lemma word_log2_max_word64[simp]: 2204 "word_log2 (w :: 64 word) < 64" 2205 using word_log2_max[where w=w] 2206 by (simp add: word_size) 2207 2208lemma rf_sr_ksReadyQueuesL2Bitmap_simp: 2209 "\<lbrakk> (\<sigma>, s') \<in> rf_sr ; d \<le> maxDomain ; valid_queues \<sigma> ; ksReadyQueuesL1Bitmap \<sigma> d \<noteq> 0 \<rbrakk> 2210 \<Longrightarrow> ksReadyQueuesL2Bitmap_' (globals s').[unat d].[word_log2 (ksReadyQueuesL1Bitmap \<sigma> d)] = 2211 ksReadyQueuesL2Bitmap \<sigma> (d, word_log2 (ksReadyQueuesL1Bitmap \<sigma> d))" 2212 apply (frule rf_sr_cbitmap_L2_relation) 2213 apply (frule (1) ksReadyQueuesL1Bitmap_word_log2_max) 2214 apply (drule (3) cbitmap_L2_relationD) 2215 done 2216 2217lemma ksReadyQueuesL2Bitmap_nonzeroI: 2218 "\<lbrakk> d \<le> maxDomain ; valid_queues s ; ksReadyQueuesL1Bitmap s d \<noteq> 0 \<rbrakk> 2219 \<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0" 2220 unfolding valid_queues_def 2221 apply clarsimp 2222 apply (frule bitmapQ_no_L1_orphansD) 2223 apply (erule word_log2_nth_same) 2224 apply clarsimp 2225 done 2226 2227lemma clzl_spec: 2228 "\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> x_' s \<noteq> 0} Call clzl_'proc 2229 \<lbrace>\<acute>ret__long = of_nat (word_clz (x_' s)) \<rbrace>" 2230 apply (rule allI, rule conseqPre, vcg) 2231 apply clarsimp 2232 apply (rule_tac x="ret__long_'_update f x" for f in exI) 2233 apply (simp add: mex_def meq_def) 2234 done 2235 2236lemma l1index_to_prio_spec: 2237 "\<forall>s. \<Gamma> \<turnstile> {s} Call l1index_to_prio_'proc 2238 \<lbrace>\<acute>ret__unsigned_long = l1index_' s << wordRadix \<rbrace>" 2239 by vcg (simp add: word_sle_def wordRadix_def') 2240 2241lemma getHighestPrio_ccorres: 2242 "ccorres (\<lambda>rv rv'. rv' = ucast rv) ret__unsigned_long_' 2243 (\<lambda>s. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) 2244 (UNIV \<inter> {s. dom_' s = ucast d}) hs 2245 (getHighestPrio d) (Call getHighestPrio_'proc)" 2246proof - 2247 2248 note prio_and_dom_limit_helpers [simp] 2249 note Collect_const_mem [simp] 2250 2251 have signed_word_log2: 2252 "\<And>w. w \<noteq> 0 \<Longrightarrow> (0x3F::64 signed word) - of_nat (word_clz (w::machine_word)) = (of_nat (word_log2 w))" 2253 unfolding word_log2_def 2254 by (clarsimp dest!: word_clz_nonzero_max simp: word_size) 2255 2256 have word_log2_def64: 2257 "\<And>w. word_log2 (w::machine_word) = 63 - word_clz w" 2258 unfolding word_log2_def by (simp add: word_size) 2259 2260 (* FIXME generalise *) 2261 have word_clz_sint_upper[simp]: 2262 "\<And>(w::machine_word). sint (of_nat (word_clz w) :: 64 signed word) \<le> 9223372036854775871" 2263 apply (subst sint_eq_uint) 2264 apply (rule not_msb_from_less) 2265 apply simp 2266 apply (rule word_of_nat_less) 2267 apply simp 2268 apply (rule order_le_less_trans[OF word_clz_max]) 2269 apply (simp add: word_size) 2270 apply (subst uint_nat) 2271 apply (simp add: unat_of_nat) 2272 apply (subst Divides.mod_less, simp) 2273 apply (rule order_le_less_trans[OF word_clz_max]) 2274 apply (simp add: word_size) 2275 apply (rule iffD2 [OF le_nat_iff[symmetric]]) 2276 apply simp 2277 apply (rule order_trans[OF word_clz_max]) 2278 apply (simp add: word_size) 2279 done 2280 2281 have word_clz_sint_lower[simp]: 2282 "\<And>(w::machine_word). - sint (of_nat (word_clz w) :: 64 signed word) \<le> 9223372036854775744" 2283 apply (subst sint_eq_uint) 2284 apply (rule not_msb_from_less) 2285 apply simp 2286 apply (rule word_of_nat_less) 2287 apply simp 2288 apply (rule order_le_less_trans[OF word_clz_max]) 2289 apply (simp add: word_size) 2290 apply (subst uint_nat) 2291 apply (simp add: unat_of_nat) 2292 done 2293 2294 have invertL1Index_unat_fold: 2295 "\<And>(w::machine_word). \<lbrakk> w \<noteq> 0 ; word_log2 w < l2BitmapSize \<rbrakk> \<Longrightarrow> 2296 unat (of_nat l2BitmapSize - (1::machine_word) - of_nat (word_log2 w)) 2297 = invertL1Index (word_log2 w)" 2298 apply (subst unat_sub) 2299 apply (clarsimp simp: l2BitmapSize_def') 2300 apply (rule word_of_nat_le) 2301 apply (drule word_log2_nth_same) 2302 apply (clarsimp simp: l2BitmapSize_def') 2303 apply (clarsimp simp: invertL1Index_def l2BitmapSize_def') 2304 apply (simp add: unat_of_nat_eq) 2305 done 2306 2307 show ?thesis 2308 apply (cinit lift: dom_') 2309 apply (clarsimp split del: if_split) 2310 apply (rule ccorres_pre_getReadyQueuesL1Bitmap) 2311 apply (rule ccorres_pre_getReadyQueuesL2Bitmap) 2312 apply (rename_tac l2) 2313 apply (rule ccorres_Guard_Seq|csymbr)+ 2314 apply (rule ccorres_abstract_cleanup) 2315 apply (rule ccorres_Guard_Seq|csymbr)+ 2316 apply (rule ccorres_abstract_cleanup) 2317 apply (rule ccorres_Guard_Seq|csymbr)+ 2318 apply (clarsimp simp: word_log2_def word_size) 2319 apply (rename_tac clz_l1index clz_l2index) 2320 apply (rule_tac P="\<lambda>s. l1 \<noteq> 0 \<and> l2 \<noteq> 0 \<and> word_log2 l1 < l2BitmapSize" 2321 and P'="{s. clz_l1index = of_nat (word_clz l1) \<and> 2322 clz_l2index = of_nat (word_clz l2) }" 2323 in ccorres_from_vcg_throws) 2324 apply (rule allI, rule conseqPre, vcg) 2325 subgoal for l1 l2 _ _ _ 2326 apply (clarsimp simp: return_def l1IndexToPrio_def) 2327 apply (simp add: signed_word_log2 word_log2_def64[symmetric] ucast_or_distrib) 2328 apply (rule_tac f="(||)" in arg_cong2) 2329 apply (subst of_nat_shiftl)+ 2330 apply (subst ucast_of_nat_small, simp add: wordRadix_def l2BitmapSize_def') 2331 apply (rule refl) 2332 apply (subst ucast_of_nat_small, simp add: wordRadix_def) 2333 apply (rule word_log2_max_word64[THEN order_less_le_trans], simp) 2334 apply (rule refl) 2335 done 2336 apply (clarsimp simp: word_sle_def) 2337 2338 apply (frule rf_sr_cbitmap_L1_relation) 2339 apply (subgoal_tac "ksReadyQueuesL1Bitmap_' (globals s').[unat d] \<noteq> 0") 2340 prefer 2 2341 subgoal by (fastforce simp: cbitmap_L1_relation_def) 2342 2343 apply (clarsimp simp: signed_word_log2 cbitmap_L1_relation_def) 2344 apply (frule bitmapQ_no_L1_orphansD, erule word_log2_nth_same) 2345 apply simp 2346 apply (rule conjI, fastforce simp: invertL1Index_def l2BitmapSize_def') 2347 apply (rule conjI, fastforce simp: invertL1Index_unat_fold) 2348 apply (rule conjI) 2349 apply (subst invertL1Index_unat_fold, assumption, fastforce) 2350 apply (frule rf_sr_cbitmap_L2_relation) 2351 apply (fastforce simp: cbitmap_L2_relation_def) 2352 apply (clarsimp simp: l2BitmapSize_def') 2353 apply (fastforce simp: word_less_nat_alt word_le_nat_alt unat_sub unat_of_nat) 2354 done 2355qed 2356 2357lemma ccorres_abstract_ksCurThread: 2358 assumes ceqv: "\<And>rv' t t'. ceqv \<Gamma> (\<lambda>s. ksCurThread_' (globals s)) rv' t t' d (d' rv')" 2359 and cc: "\<And>ct. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (G ct) (G' ct) hs a (d' (tcb_ptr_to_ctcb_ptr ct))" 2360 shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf (\<lambda>s. G (ksCurThread s) s) 2361 {s. s \<in> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} hs a d" 2362 apply (rule ccorres_guard_imp) 2363 prefer 2 2364 apply assumption 2365 apply (rule ccorres_abstract[OF ceqv, where G'="\<lambda>ct. \<lbrace>ct = \<acute>ksCurThread\<rbrace> \<inter> G' (ctcb_ptr_to_tcb_ptr ct)"]) 2366 apply (subgoal_tac "\<exists>t. rv' = tcb_ptr_to_ctcb_ptr t") 2367 apply clarsimp 2368 apply (rule ccorres_guard_imp2) 2369 apply (rule cc) 2370 apply (clarsimp simp: rf_sr_ksCurThread) 2371 apply (metis tcb_ptr_to_tcb_ptr) 2372 apply simp 2373 done 2374 2375lemma ctcb_relation_unat_tcbPriority_C: 2376 "ctcb_relation tcb tcb' \<Longrightarrow> unat (tcbPriority_C tcb') = unat (tcbPriority tcb)" 2377 apply (clarsimp simp: ctcb_relation_def) 2378 apply (rule trans, rule arg_cong[where f=unat], erule sym) 2379 apply (simp(no_asm)) 2380 done 2381 2382lemma ctcb_relation_unat_tcbDomain_C: 2383 "ctcb_relation tcb tcb' \<Longrightarrow> unat (tcbDomain_C tcb') = unat (tcbDomain tcb)" 2384 apply (clarsimp simp: ctcb_relation_def) 2385 apply (rule trans, rule arg_cong[where f=unat], erule sym) 2386 apply (simp(no_asm)) 2387 done 2388 2389lemma getCurDomain_ccorres_dom_': 2390 "ccorres (\<lambda>rv rv'. rv' = ucast rv) dom_' 2391 \<top> UNIV hs curDomain (\<acute>dom :== \<acute>ksCurDomain)" 2392 apply (rule ccorres_from_vcg) 2393 apply (rule allI, rule conseqPre, vcg) 2394 apply (clarsimp simp: curDomain_def simpler_gets_def 2395 rf_sr_ksCurDomain) 2396 done 2397 2398lemma rf_sr_cscheduler_action_relation: 2399 "(s, s') \<in> rf_sr 2400 \<Longrightarrow> cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s'))" 2401 by (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 2402 2403lemma threadGet_get_obj_at'_has_domain: 2404 "\<lbrace> tcb_at' t \<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. rv = tcbDomain tcb) t\<rbrace>" 2405 by (wp threadGet_obj_at') (simp add: obj_at'_def) 2406 2407lemma possibleSwitchTo_ccorres: 2408 shows 2409 "ccorres dc xfdc 2410 (valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) 2411 and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) 2412 and valid_objs') 2413 ({s. target_' s = tcb_ptr_to_ctcb_ptr t} 2414 \<inter> UNIV) [] 2415 (possibleSwitchTo t ) 2416 (Call possibleSwitchTo_'proc)" 2417 supply if_split [split del] 2418 supply Collect_const [simp del] 2419 supply dc_simp [simp del] 2420 supply prio_and_dom_limit_helpers[simp] 2421 (* FIXME: these should likely be in simpset for CRefine, or even in general *) 2422 supply from_bool_eq_if[simp] from_bool_eq_if'[simp] from_bool_0[simp] if_1_0_0[simp] 2423 ccorres_IF_True[simp] 2424 apply (cinit lift: target_') 2425 apply (rule ccorres_move_c_guard_tcb) 2426 apply (rule ccorres_pre_curDomain, rename_tac curDom) 2427 apply (rule ccorres_symb_exec_l3[OF _ threadGet_inv _ empty_fail_threadGet], rename_tac targetDom) 2428 apply (rule ccorres_symb_exec_l3[OF _ gsa_wp _ empty_fail_getSchedulerAction], rename_tac sact) 2429 apply (rule_tac C'="{s. targetDom \<noteq> curDom}" 2430 and Q="\<lambda>s. curDom = ksCurDomain s \<and> obj_at' (\<lambda>tcb. targetDom = tcbDomain tcb) t s" 2431 and Q'=UNIV in ccorres_rewrite_cond_sr) 2432 subgoal 2433 apply clarsimp 2434 apply (drule obj_at_ko_at', clarsimp simp: rf_sr_ksCurDomain) 2435 apply (frule (1) obj_at_cslift_tcb, clarsimp simp: typ_heap_simps') 2436 apply (drule ctcb_relation_unat_tcbDomain_C) 2437 apply unat_arith 2438 done 2439 apply (rule ccorres_cond2[where R=\<top>], simp) 2440 apply (ctac add: tcbSchedEnqueue_ccorres) 2441 apply (rule_tac R="\<lambda>s. sact = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s" 2442 in ccorres_cond) 2443 apply (fastforce dest!: rf_sr_cscheduler_action_relation pred_tcb_at' tcb_at_not_NULL 2444 simp: cscheduler_action_relation_def max_word_def weak_sch_act_wf_def 2445 split: scheduler_action.splits) 2446 apply (ctac add: rescheduleRequired_ccorres) 2447 apply (ctac add: tcbSchedEnqueue_ccorres) 2448 apply wp 2449 apply (vcg exspec=rescheduleRequired_modifies) 2450 apply (rule ccorres_setSchedulerAction, simp add: cscheduler_action_relation_def) 2451 apply clarsimp 2452 apply wp 2453 apply clarsimp 2454 apply (wp hoare_drop_imps threadGet_get_obj_at'_has_domain) 2455 apply (clarsimp simp: pred_tcb_at') 2456 done 2457 2458lemma scheduleTCB_ccorres': 2459 "ccorres dc xfdc 2460 (tcb_at' thread and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_queues 2461 and valid_objs') 2462 (UNIV \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr thread}) 2463 [] 2464 (do (runnable, curThread, action) \<leftarrow> do 2465 runnable \<leftarrow> isRunnable thread; 2466 curThread \<leftarrow> getCurThread; 2467 action \<leftarrow> getSchedulerAction; 2468 return (runnable, curThread, action) od; 2469 when (\<not> runnable \<and> 2470 curThread = thread \<and> action = ResumeCurrentThread) 2471 rescheduleRequired 2472 od) 2473 (Call scheduleTCB_'proc)" 2474 apply (cinit' lift: tptr_' simp del: word_neq_0_conv) 2475 apply (rule ccorres_rhs_assoc2)+ 2476 apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg) 2477 defer 2478 apply ceqv 2479 apply (unfold split_def)[1] 2480 apply (rule ccorres_when[where R=\<top>]) 2481 apply (intro allI impI) 2482 apply (unfold mem_simps)[1] 2483 apply assumption 2484 apply (ctac add: rescheduleRequired_ccorres) 2485 prefer 4 2486 apply (rule ccorres_symb_exec_l) 2487 apply (rule ccorres_pre_getCurThread) 2488 apply (rule ccorres_symb_exec_l) 2489 apply (rule_tac P="\<lambda>s. st_tcb_at' (\<lambda>st. runnable' st = runnable) thread s 2490 \<and> curThread = ksCurThread s 2491 \<and> action = ksSchedulerAction s 2492 \<and> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t s)" 2493 and P'=UNIV in ccorres_from_vcg) 2494 apply (rule allI, rule conseqPre, vcg) 2495 apply (clarsimp simp: return_def if_1_0_0 split del: if_split) 2496 apply (clarsimp simp: from_bool_0 rf_sr_ksCurThread) 2497 apply (rule conjI) 2498 apply (clarsimp simp: st_tcb_at'_def) 2499 apply (drule (1) obj_at_cslift_tcb) 2500 apply (clarsimp simp: typ_heap_simps) 2501 apply (subgoal_tac "ksSchedulerAction \<sigma> = ResumeCurrentThread") 2502 apply (clarsimp simp: ctcb_relation_def cthread_state_relation_def) 2503 apply (case_tac "tcbState ko", simp_all add: "StrictC'_thread_state_defs")[1] 2504 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 2505 cscheduler_action_relation_def max_word_def 2506 tcb_at_not_NULL 2507 split: scheduler_action.split_asm) 2508 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 2509 cscheduler_action_relation_def) 2510 apply wp+ 2511 apply (simp add: isRunnable_def isBlocked_def) 2512 apply wp 2513 apply (simp add: guard_is_UNIV_def) 2514 apply clarsimp 2515 apply (clarsimp simp: st_tcb_at'_def obj_at'_def weak_sch_act_wf_def) 2516 done 2517 2518lemma scheduleTCB_ccorres_valid_queues'_pre: 2519 "ccorresG rf_sr \<Gamma> dc xfdc (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') 2520 (UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>) [] 2521 (do (runnable, curThread, action) \<leftarrow> do 2522 runnable \<leftarrow> isRunnable thread; 2523 curThread \<leftarrow> getCurThread; 2524 action \<leftarrow> getSchedulerAction; 2525 return (runnable, curThread, action) od; 2526 when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired 2527 od) 2528 (Call scheduleTCB_'proc)" 2529 apply (cinit' lift: tptr_' simp del: word_neq_0_conv) 2530 apply (rule ccorres_rhs_assoc2)+ 2531 apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg) 2532 defer 2533 apply ceqv 2534 apply (unfold split_def)[1] 2535 apply (rule ccorres_when[where R=\<top>]) 2536 apply (intro allI impI) 2537 apply (unfold mem_simps)[1] 2538 apply assumption 2539 apply (ctac add: rescheduleRequired_ccorres) 2540 prefer 4 2541 apply (rule ccorres_symb_exec_l) 2542 apply (rule ccorres_pre_getCurThread) 2543 apply (rule ccorres_symb_exec_l) 2544 apply (rule_tac P="\<lambda>s. st_tcb_at' (\<lambda>st. runnable' st = runnable) thread s 2545 \<and> curThread = ksCurThread s 2546 \<and> action = ksSchedulerAction s 2547 \<and> weak_sch_act_wf (ksSchedulerAction s) s" 2548 and P'=UNIV in ccorres_from_vcg) 2549 apply (rule allI, rule conseqPre, vcg) 2550 apply (clarsimp simp: return_def if_1_0_0 split del: if_split) 2551 apply (clarsimp simp: from_bool_0 rf_sr_ksCurThread) 2552 apply (rule conjI) 2553 apply (clarsimp simp: st_tcb_at'_def) 2554 apply (drule (1) obj_at_cslift_tcb) 2555 apply (clarsimp simp: typ_heap_simps) 2556 apply (clarsimp simp: ctcb_relation_def cthread_state_relation_def weak_sch_act_wf_def) 2557 apply (case_tac "tcbState ko", simp_all add: "StrictC'_thread_state_defs")[1] 2558 apply (fold_subgoals (prefix))[6] 2559 subgoal premises prems using prems 2560 by (clarsimp simp: rf_sr_def cstate_relation_def Let_def 2561 cscheduler_action_relation_def max_word_def 2562 tcb_at_not_NULL[OF obj_tcb_at'] st_tcb_at'_def 2563 split: scheduler_action.split_asm)+ 2564 apply (clarsimp simp: rf_sr_def cstate_relation_def cscheduler_action_relation_def 2565 split: scheduler_action.split_asm) 2566 apply wp+ 2567 apply (simp add: isRunnable_def isBlocked_def) 2568 apply wp 2569 apply (simp add: guard_is_UNIV_def) 2570 apply (clarsimp simp: st_tcb_at'_def obj_at'_def) 2571 done 2572 2573 2574lemmas scheduleTCB_ccorres_valid_queues' 2575 = scheduleTCB_ccorres_valid_queues'_pre[unfolded bind_assoc return_bind split_conv] 2576 2577lemma rescheduleRequired_ccorres_valid_queues'_simple: 2578 "ccorresG rf_sr \<Gamma> dc xfdc (valid_queues' and sch_act_simple) UNIV [] rescheduleRequired (Call rescheduleRequired_'proc)" 2579 apply cinit 2580 apply (rule ccorres_symb_exec_l) 2581 apply (rule ccorres_split_nothrow_novcg[where r'=dc and xf'=xfdc]) 2582 apply (simp add: scheduler_action_case_switch_to_if 2583 cong: if_weak_cong split del: if_split) 2584 apply (rule_tac R="\<lambda>s. action = ksSchedulerAction s \<and> sch_act_simple s" 2585 in ccorres_cond) 2586 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 2587 cscheduler_action_relation_def) 2588 apply (clarsimp simp: weak_sch_act_wf_def tcb_at_1 tcb_at_not_NULL 2589 split: scheduler_action.split_asm dest!: st_tcb_strg'[rule_format]) 2590 apply (ctac add: tcbSchedEnqueue_ccorres) 2591 apply (rule ccorres_return_Skip) 2592 apply ceqv 2593 apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV]) 2594 apply (rule allI, rule conseqPre, vcg) 2595 apply (clarsimp simp: setSchedulerAction_def simpler_modify_def) 2596 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 2597 cscheduler_action_relation_def 2598 carch_state_relation_def cmachine_state_relation_def 2599 max_word_def) 2600 apply wp 2601 apply (simp add: guard_is_UNIV_def) 2602 apply wp+ 2603 apply (simp add: getSchedulerAction_def) 2604 apply (clarsimp simp: weak_sch_act_wf_def rf_sr_def cstate_relation_def 2605 Let_def cscheduler_action_relation_def) 2606 by (auto simp: tcb_at_not_NULL tcb_at_1 2607 tcb_at_not_NULL[THEN not_sym] tcb_at_1[THEN not_sym] 2608 split: scheduler_action.split_asm) 2609 2610lemma scheduleTCB_ccorres_valid_queues'_pre_simple: 2611 "ccorresG rf_sr \<Gamma> dc xfdc (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and sch_act_simple) 2612 (UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>) [] 2613 (do (runnable, curThread, action) \<leftarrow> do 2614 runnable \<leftarrow> isRunnable thread; 2615 curThread \<leftarrow> getCurThread; 2616 action \<leftarrow> getSchedulerAction; 2617 return (runnable, curThread, action) od; 2618 when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired 2619 od) 2620 (Call scheduleTCB_'proc)" 2621 apply (cinit' lift: tptr_' simp del: word_neq_0_conv) 2622 apply (rule ccorres_rhs_assoc2)+ 2623 apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg) 2624 defer 2625 apply ceqv 2626 apply (unfold split_def)[1] 2627 apply (rule ccorres_when[where R=\<top>]) 2628 apply (intro allI impI) 2629 apply (unfold mem_simps)[1] 2630 apply assumption 2631 apply (ctac add: rescheduleRequired_ccorres_valid_queues'_simple) 2632 prefer 4 2633 apply (rule ccorres_symb_exec_l) 2634 apply (rule ccorres_pre_getCurThread) 2635 apply (rule ccorres_symb_exec_l) 2636 apply (rule_tac P="\<lambda>s. st_tcb_at' (\<lambda>st. runnable' st = runnable) thread s 2637 \<and> curThread = ksCurThread s 2638 \<and> action = ksSchedulerAction s 2639 \<and> sch_act_simple s" 2640 and P'=UNIV in ccorres_from_vcg) 2641 apply (rule allI, rule conseqPre, vcg) 2642 apply (clarsimp simp: return_def if_1_0_0 split del: if_split) 2643 apply (clarsimp simp: from_bool_0 rf_sr_ksCurThread) 2644 apply (rule conjI) 2645 apply (clarsimp simp: st_tcb_at'_def) 2646 apply (drule (1) obj_at_cslift_tcb) 2647 apply (clarsimp simp: typ_heap_simps) 2648 apply (subgoal_tac "ksSchedulerAction \<sigma> = ResumeCurrentThread") 2649 apply (clarsimp simp: ctcb_relation_def cthread_state_relation_def) 2650 apply (case_tac "tcbState ko", simp_all add: "StrictC'_thread_state_defs")[1] 2651 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 2652 cscheduler_action_relation_def max_word_def 2653 tcb_at_not_NULL 2654 split: scheduler_action.split_asm) 2655 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 2656 cscheduler_action_relation_def) 2657 apply wp+ 2658 apply (simp add: isRunnable_def isBlocked_def) 2659 apply wp 2660 apply (simp add: guard_is_UNIV_def) 2661 apply clarsimp 2662 apply (clarsimp simp: st_tcb_at'_def obj_at'_def valid_queues'_def) 2663 done 2664 2665lemmas scheduleTCB_ccorres_valid_queues'_simple 2666 = scheduleTCB_ccorres_valid_queues'_pre_simple[unfolded bind_assoc return_bind split_conv] 2667 2668lemmas scheduleTCB_ccorres[corres] 2669 = scheduleTCB_ccorres'[unfolded bind_assoc return_bind split_conv] 2670 2671lemma threadSet_weak_sch_act_wf_runnable': 2672 "\<lbrace> \<lambda>s. (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' st) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<rbrace> 2673 threadSet (tcbState_update (\<lambda>_. st)) thread 2674 \<lbrace> \<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s \<rbrace>" 2675 apply (simp add: weak_sch_act_wf_def) 2676 apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift threadSet_pred_tcb_at_state 2677 threadSet_tcbDomain_triv) 2678 apply simp 2679 apply (clarsimp) 2680done 2681 2682lemma threadSet_valid_queues_and_runnable': "\<lbrace>\<lambda>s. valid_queues s \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' st)\<rbrace> 2683 threadSet (tcbState_update (\<lambda>_. st)) thread 2684 \<lbrace>\<lambda>rv s. valid_queues s\<rbrace>" 2685 apply (wp threadSet_valid_queues) 2686 apply (clarsimp simp: inQ_def) 2687done 2688 2689lemma setThreadState_ccorres[corres]: 2690 "ccorres dc xfdc 2691 (\<lambda>s. tcb_at' thread s \<and> valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' st s \<and> 2692 (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' st) \<and> 2693 (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' st) \<and> 2694 sch_act_wf (ksSchedulerAction s) s) 2695 ({s'. (\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := ts_' s' && mask 4\<rparr>, fl))} 2696 \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr thread}) hs 2697 (setThreadState st thread) (Call setThreadState_'proc)" 2698 apply (cinit lift: tptr_' cong add: call_ignore_cong) 2699 apply (ctac (no_vcg) add: threadSet_tcbState_simple_corres) 2700 apply (ctac add: scheduleTCB_ccorres) 2701 apply (wp threadSet_weak_sch_act_wf_runnable' threadSet_valid_queues_and_runnable' 2702 threadSet_valid_objs') 2703 by (clarsimp simp: weak_sch_act_wf_def valid_queues_def valid_tcb'_tcbState_update) 2704 2705lemma threadSet_valid_queues'_and_not_runnable': "\<lbrace>tcb_at' thread and valid_queues' and (\<lambda>s. (\<not> runnable' st))\<rbrace> 2706 threadSet (tcbState_update (\<lambda>_. st)) thread 2707 \<lbrace>\<lambda>rv. tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' \<rbrace>" 2708 2709 apply (wp threadSet_valid_queues' threadSet_tcbState_st_tcb_at') 2710 apply (clarsimp simp: pred_neg_def valid_queues'_def inQ_def)+ 2711done 2712 2713lemma setThreadState_ccorres_valid_queues': 2714 "ccorres dc xfdc 2715 (\<lambda>s. tcb_at' thread s \<and> valid_queues' s \<and> \<not> runnable' st \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> sch_act_not thread s \<and> valid_objs' s \<and> valid_tcb_state' st s) 2716 ({s'. (\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := ts_' s' && mask 4\<rparr>, fl))} 2717 \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr thread}) [] 2718 (setThreadState st thread) (Call setThreadState_'proc)" 2719 apply (cinit lift: tptr_' cong add: call_ignore_cong) 2720 apply (ctac (no_vcg) add: threadSet_tcbState_simple_corres) 2721 apply (ctac add: scheduleTCB_ccorres_valid_queues') 2722 apply (wp threadSet_valid_queues'_and_not_runnable' threadSet_weak_sch_act_wf_runnable' threadSet_valid_queues_and_runnable' threadSet_valid_objs') 2723 by (clarsimp simp: valid_tcb'_def tcb_cte_cases_def) 2724 2725lemma simp_list_case_return: 2726 "(case x of [] \<Rightarrow> return e | y # ys \<Rightarrow> return f) = return (if x = [] then e else f)" 2727 by (clarsimp split: list.splits) 2728 2729lemma cancelSignal_ccorres [corres]: 2730 "ccorres dc xfdc 2731 (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) 2732 (UNIV \<inter> {s. threadPtr_' s = tcb_ptr_to_ctcb_ptr thread} \<inter> {s. ntfnPtr_' s = Ptr ntfn}) 2733 [] (cancelSignal thread ntfn) (Call cancelSignal_'proc)" 2734 apply (cinit lift: threadPtr_' ntfnPtr_' simp add: Let_def list_case_return cong add: call_ignore_cong) 2735 apply (unfold fun_app_def) 2736 apply (simp only: simp_list_case_return return_bind ccorres_seq_skip) 2737 apply (rule ccorres_pre_getNotification) 2738 apply (rule ccorres_assert) 2739 apply (rule ccorres_rhs_assoc2) 2740 apply (rule ccorres_rhs_assoc2) 2741 apply (rule ccorres_rhs_assoc2) 2742 apply (ctac (no_vcg) add: cancelSignal_ccorres_helper) 2743 apply (ctac add: setThreadState_ccorres_valid_queues') 2744 apply ((wp setNotification_nosch setNotification_ksQ hoare_vcg_all_lift set_ntfn_valid_objs' | simp add: valid_tcb_state'_def split del: if_split)+)[1] 2745 apply (simp add: "StrictC'_thread_state_defs") 2746 apply (rule conjI, clarsimp, rule conjI, clarsimp) 2747 apply (frule (1) ko_at_valid_ntfn'[OF _ invs_valid_objs']) 2748 subgoal by ((auto simp: obj_at'_def projectKOs st_tcb_at'_def invs'_def valid_state'_def 2749 isTS_defs cte_wp_at_ctes_of "StrictC'_thread_state_defs" 2750 cthread_state_relation_def sch_act_wf_weak valid_ntfn'_def 2751 dest!: valid_queues_not_runnable'_not_ksQ[where t=thread] | 2752 clarsimp simp: eq_commute)+) 2753 apply (clarsimp) 2754 apply (frule (1) ko_at_valid_ntfn'[OF _ invs_valid_objs']) 2755 apply (frule (2) ntfn_blocked_in_queueD) 2756 by (auto simp: obj_at'_def projectKOs st_tcb_at'_def invs'_def valid_state'_def 2757 isTS_defs cte_wp_at_ctes_of "StrictC'_thread_state_defs" valid_ntfn'_def 2758 cthread_state_relation_def sch_act_wf_weak isWaitingNtfn_def 2759 dest!: valid_queues_not_runnable'_not_ksQ[where t=thread] 2760 split: ntfn.splits option.splits 2761 | clarsimp simp: eq_commute 2762 | drule_tac x=thread in bspec)+ 2763 2764lemma ko_at_valid_ep': 2765 "\<lbrakk>ko_at' ep p s; valid_objs' s\<rbrakk> \<Longrightarrow> valid_ep' ep s" 2766 apply (erule obj_atE') 2767 apply (erule (1) valid_objsE') 2768 apply (simp add: projectKOs valid_obj'_def) 2769 done 2770 2771(* FIXME: MOVE *) 2772lemma ccorres_pre_getEndpoint [corres_pre]: 2773 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 2774 shows "ccorres r xf 2775 (ep_at' p and (\<lambda>s. \<forall>ep. ko_at' ep p s \<longrightarrow> P ep s)) 2776 ({s'. \<forall>ep. cendpoint_relation (cslift s') ep (the (cslift s' (Ptr p))) \<longrightarrow> s' \<in> P' ep}) 2777 hs (getEndpoint p >>= (\<lambda>rv. f rv)) c" 2778 apply (rule ccorres_guard_imp) 2779 apply (rule ccorres_symb_exec_l2) 2780 defer 2781 defer 2782 apply (rule get_ep_sp') 2783 apply assumption 2784 apply clarsimp 2785 prefer 3 2786 apply (clarsimp simp add: getEndpoint_def exs_getObject objBits_simps') 2787 defer 2788 apply (rule ccorres_guard_imp) 2789 apply (rule cc) 2790 apply simp 2791 apply assumption 2792 apply (drule spec, erule mp) 2793 apply (drule cmap_relation_ep) 2794 apply (drule (1) cmap_relation_ko_atD) 2795 apply clarsimp 2796 done 2797 2798lemma ep_blocked_in_queueD: 2799 "\<lbrakk> st_tcb_at' (\<lambda>st. (isBlockedOnSend st \<or> isBlockedOnReceive st) 2800 \<and> blockingObject st = ep) thread \<sigma>; 2801 ko_at' ep' ep \<sigma>; invs' \<sigma> \<rbrakk> 2802 \<Longrightarrow> thread \<in> set (epQueue ep') \<and> (isSendEP ep' \<or> isRecvEP ep')" 2803 apply (drule sym_refs_st_tcb_atD') 2804 apply clarsimp 2805 apply (clarsimp simp: refs_of_rev' obj_at'_def ko_wp_at'_def projectKOs) 2806 apply (clarsimp simp: isTS_defs split: Structures_H.thread_state.split_asm) 2807 apply (cases ep', simp_all add: isSendEP_def isRecvEP_def)[1] 2808 apply (cases ep', simp_all add: isSendEP_def isRecvEP_def)[1] 2809 done 2810 2811lemma ep_ptr_get_queue_spec: 2812 "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>epptr\<rbrace> \<acute>ret__struct_tcb_queue_C :== PROC ep_ptr_get_queue(\<acute>epptr) 2813 \<lbrace>head_C \<acute>ret__struct_tcb_queue_C = Ptr (epQueue_head_CL (endpoint_lift (the (cslift s \<^bsup>s\<^esup>epptr)))) \<and> 2814 end_C \<acute>ret__struct_tcb_queue_C = Ptr (epQueue_tail_CL (endpoint_lift (the (cslift s \<^bsup>s\<^esup>epptr))))\<rbrace>" 2815 apply vcg 2816 apply clarsimp 2817 done 2818 2819(* FIXME x64: bitfield shenanigans *) 2820lemma ep_ptr_set_queue_spec: 2821 "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>epptr\<rbrace> Call ep_ptr_set_queue_'proc 2822 {t. (\<exists>ep'. endpoint_lift ep' = 2823 (endpoint_lift (the (cslift s (\<^bsup>s\<^esup>epptr))))\<lparr> epQueue_head_CL := ptr_val (head_C \<^bsup>s\<^esup>queue) && ~~ mask 4, 2824 epQueue_tail_CL := ptr_val (end_C \<^bsup>s\<^esup>queue) && ~~ mask 4 \<rparr> 2825 \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (\<^bsup>s\<^esup>epptr) ep') 2826 (t_hrs_' (globals s)))}" 2827 apply vcg 2828 apply (auto simp: split_def h_t_valid_clift_Some_iff 2829 typ_heap_simps packed_heap_update_collapse_hrs) 2830 oops 2831 2832lemma valid_ep_blockedD: 2833 "\<lbrakk> valid_ep' ep s; (isSendEP ep \<or> isRecvEP ep) \<rbrakk> \<Longrightarrow> (epQueue ep) \<noteq> [] \<and> (\<forall>t\<in>set (epQueue ep). tcb_at' t s) \<and> distinct (epQueue ep)" 2834 unfolding valid_ep'_def isSendEP_def isRecvEP_def 2835 by (clarsimp split: endpoint.splits) 2836 2837 2838lemma ep_to_ep_queue: 2839 assumes ko: "ko_at' ep' ep s" 2840 and waiting: "(isSendEP ep' \<or> isRecvEP ep')" 2841 and rf: "(s, s') \<in> rf_sr" 2842 shows "ep_queue_relation' (cslift s') (epQueue ep') 2843 (Ptr (epQueue_head_CL 2844 (endpoint_lift (the (cslift s' (Ptr ep)))))) 2845 (Ptr (epQueue_tail_CL 2846 (endpoint_lift (the (cslift s' (Ptr ep))))))" 2847proof - 2848 from rf have 2849 "cmap_relation (map_to_eps (ksPSpace s)) (cslift s') Ptr (cendpoint_relation (cslift s'))" 2850 by (rule cmap_relation_ep) 2851 2852 thus ?thesis using ko waiting 2853 apply - 2854 apply (erule (1) cmap_relation_ko_atE) 2855 apply (clarsimp simp: cendpoint_relation_def Let_def isSendEP_def isRecvEP_def split: endpoint.splits) 2856 done 2857qed 2858 2859lemma ep_ep_disjoint: 2860 assumes srs: "sym_refs (state_refs_of' s)" 2861 and epat: "ko_at' ep epptr s" 2862 and epat': "ko_at' ep' epptr' s" 2863 and epq: "(isSendEP ep \<or> isRecvEP ep)" 2864 and epq': "(isSendEP ep' \<or> isRecvEP ep')" 2865 and neq: "epptr' \<noteq> epptr" 2866 shows "set (epQueue ep) \<inter> set (epQueue ep') = {}" 2867 using srs epat epat' epq epq' neq 2868 apply - 2869 apply (subst disjoint_iff_not_equal, intro ballI, rule notI) 2870 apply (drule sym_refs_ko_atD', clarsimp)+ 2871 apply clarsimp 2872 apply (clarsimp simp: isSendEP_def isRecvEP_def split: endpoint.splits) 2873 apply (simp_all add: st_tcb_at_refs_of_rev') 2874 apply (fastforce simp: st_tcb_at'_def obj_at'_def)+ 2875 done 2876 2877lemma cendpoint_relation_ep_queue: 2878 fixes ep :: "endpoint" 2879 assumes ep: "cendpoint_relation mp ep' b" 2880 and mpeq: "(mp' |` (- S)) = (mp |` (- S))" 2881 and epq: "ep' \<noteq> IdleEP \<Longrightarrow> 2882 set (epQueue ep') \<inter> (ctcb_ptr_to_tcb_ptr ` S) = {}" 2883 shows "cendpoint_relation mp' ep' b" 2884proof - 2885 2886 have rl: "\<And>p list. \<lbrakk> ctcb_ptr_to_tcb_ptr p \<in> set list; 2887 ep' = RecvEP list \<or> ep' = SendEP list \<rbrakk> 2888 \<Longrightarrow> mp' p = mp p" 2889 using epq 2890 apply (cut_tac x=p in fun_cong[OF mpeq]) 2891 apply (cases ep', auto simp: restrict_map_def split: if_split_asm) 2892 done 2893 2894 have rl': "\<And>p list. \<lbrakk> p \<in> tcb_ptr_to_ctcb_ptr ` set list; 2895 ep' = RecvEP list \<or> ep' = SendEP list \<rbrakk> 2896 \<Longrightarrow> mp' p = mp p" 2897 by (clarsimp elim!: rl[rotated]) 2898 2899 show ?thesis using ep rl' mpeq unfolding cendpoint_relation_def 2900 by (simp add: Let_def 2901 cong: Structures_H.endpoint.case_cong tcb_queue_relation'_cong) 2902qed 2903 2904lemma cpspace_relation_ep_update_an_ep: 2905 fixes ep :: "endpoint" 2906 defines "qs \<equiv> if (isSendEP ep \<or> isRecvEP ep) then set (epQueue ep) else {}" 2907 assumes koat: "ko_at' ep epptr s" 2908 and cp: "cmap_relation (map_to_eps (ksPSpace s)) (cslift t) Ptr (cendpoint_relation mp)" 2909 and rel: "cendpoint_relation mp' ep' endpoint" 2910 and mpeq: "(mp' |` (- S)) = (mp |` (- S))" 2911 and pal: "pspace_aligned' s" "pspace_distinct' s" 2912 and others: "\<And>epptr' ep'. \<lbrakk> ko_at' ep' epptr' s; epptr' \<noteq> epptr; ep' \<noteq> IdleEP \<rbrakk> 2913 \<Longrightarrow> set (epQueue ep') \<inter> (ctcb_ptr_to_tcb_ptr ` S) = {}" 2914 shows "cmap_relation (map_to_eps (ksPSpace s(epptr \<mapsto> KOEndpoint ep'))) 2915 (cslift t(Ptr epptr \<mapsto> endpoint)) Ptr (cendpoint_relation mp')" 2916 using cp koat pal rel unfolding cmap_relation_def 2917 apply - 2918 apply (clarsimp elim!: obj_atE' simp: map_comp_update projectKO_opts_defs) 2919 apply (drule (1) bspec [OF _ domI]) 2920 apply simp 2921 apply (erule cendpoint_relation_ep_queue[OF _ mpeq]) 2922 apply (erule(4) others[OF map_to_ko_atI]) 2923 done 2924 2925lemma endpoint_not_idle_cases: 2926 "ep \<noteq> IdleEP \<Longrightarrow> isSendEP ep \<or> isRecvEP ep" 2927 by (clarsimp simp: isRecvEP_def isSendEP_def split: Structures_H.endpoint.split) 2928 2929lemma cpspace_relation_ep_update_ep: 2930 fixes ep :: "endpoint" 2931 defines "qs \<equiv> if (isSendEP ep \<or> isRecvEP ep) then set (epQueue ep) else {}" 2932 assumes koat: "ko_at' ep epptr s" 2933 and invs: "invs' s" 2934 and cp: "cmap_relation (map_to_eps (ksPSpace s)) (cslift t) Ptr (cendpoint_relation mp)" 2935 and rel: "cendpoint_relation mp' ep' endpoint" 2936 and mpeq: "(mp' |` (- (tcb_ptr_to_ctcb_ptr ` qs))) = (mp |` (- (tcb_ptr_to_ctcb_ptr ` qs)))" 2937 shows "cmap_relation (map_to_eps (ksPSpace s(epptr \<mapsto> KOEndpoint ep'))) 2938 (cslift t(Ptr epptr \<mapsto> endpoint)) Ptr (cendpoint_relation mp')" 2939 using invs 2940 apply (intro cpspace_relation_ep_update_an_ep[OF koat cp rel mpeq]) 2941 apply clarsimp+ 2942 apply (clarsimp simp add: qs_def image_image simp del: imp_disjL) 2943 apply (rule ep_ep_disjoint[OF _ _ koat endpoint_not_idle_cases], auto) 2944 done 2945 2946lemma cpspace_relation_ep_update_ep': 2947 fixes ep :: "endpoint" and ep' :: "endpoint" 2948 and epptr :: "machine_word" and s :: "kernel_state" 2949 defines "qs \<equiv> if (isSendEP ep' \<or> isRecvEP ep') then set (epQueue ep') else {}" 2950 defines "s' \<equiv> s\<lparr>ksPSpace := ksPSpace s(epptr \<mapsto> KOEndpoint ep')\<rparr>" 2951 assumes koat: "ko_at' ep epptr s" 2952 and vp: "valid_pspace' s" 2953 and cp: "cmap_relation (map_to_eps (ksPSpace s)) (cslift t) Ptr (cendpoint_relation mp)" 2954 and srs: "sym_refs (state_refs_of' s')" 2955 and rel: "cendpoint_relation mp' ep' endpoint" 2956 and mpeq: "(mp' |` (- (tcb_ptr_to_ctcb_ptr ` qs))) = (mp |` (- (tcb_ptr_to_ctcb_ptr ` qs)))" 2957 shows "cmap_relation (map_to_eps (ksPSpace s(epptr \<mapsto> KOEndpoint ep'))) 2958 (cslift t(Ptr epptr \<mapsto> endpoint)) Ptr (cendpoint_relation mp')" 2959proof - 2960 from koat have koat': "ko_at' ep' epptr s'" 2961 by (clarsimp simp: obj_at'_def s'_def objBitsKO_def ps_clear_def projectKOs) 2962 2963 from koat have koat'': "\<And>ep'' epptr'. \<lbrakk> ko_at' ep'' epptr' s; epptr' \<noteq> epptr \<rbrakk> 2964 \<Longrightarrow> ko_at' ep'' epptr' s'" 2965 by (clarsimp simp: obj_at'_def s'_def objBitsKO_def ps_clear_def projectKOs) 2966 2967 show ?thesis using vp ep_ep_disjoint[OF srs koat'' koat' endpoint_not_idle_cases] 2968 apply (intro cpspace_relation_ep_update_an_ep[OF koat cp rel mpeq]) 2969 apply clarsimp+ 2970 apply (clarsimp simp add: qs_def image_image simp del: imp_disjL) 2971 done 2972qed 2973 2974lemma cnotification_relation_ep_queue: 2975 assumes srs: "sym_refs (state_refs_of' s)" 2976 and koat: "ko_at' ep epptr s" 2977 and iswaiting: "(isSendEP ep \<or> isRecvEP ep)" 2978 and mpeq: "(mp' |` (- (tcb_ptr_to_ctcb_ptr ` set (epQueue ep)))) 2979 = (mp |` (- (tcb_ptr_to_ctcb_ptr ` set (epQueue ep))))" 2980 and koat': "ko_at' a ntfnPtr s" 2981 shows "cnotification_relation mp a b = cnotification_relation mp' a b" 2982proof - 2983 have rl: "\<And>p. \<lbrakk> p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj a)); 2984 isWaitingNtfn (ntfnObj a) \<rbrakk> 2985 \<Longrightarrow> mp p = mp' p" using srs koat' koat iswaiting mpeq 2986 apply - 2987 apply (drule (4) ntfn_ep_disjoint) 2988 apply (erule restrict_map_eqI [symmetric]) 2989 apply (erule imageE) 2990 apply (fastforce simp: disjoint_iff_not_equal inj_eq) 2991 done 2992 2993 show ?thesis 2994 unfolding cnotification_relation_def using rl 2995 apply (simp add: Let_def) 2996 apply (cases "ntfnObj a") 2997 apply (simp add: isWaitingNtfn_def cong: tcb_queue_relation'_cong)+ 2998 done 2999qed 3000 3001(* FIXME: x64 can be removed? *) 3002lemma epQueue_head_mask_2 [simp]: 3003 "epQueue_head_CL (endpoint_lift ko') && ~~ mask 2 = epQueue_head_CL (endpoint_lift ko')" 3004 unfolding endpoint_lift_def 3005 oops (*by (clarsimp simp: mask_def word_bw_assocs) *) 3006 3007lemma epQueue_tail_mask_2 [simp]: 3008 "epQueue_tail_CL (endpoint_lift ko') && ~~ mask 2 = epQueue_tail_CL (endpoint_lift ko')" 3009 unfolding endpoint_lift_def 3010 by (clarsimp simp: mask_def word_bw_assocs sign_extend_def) word_bitwise 3011 3012lemma epQueue_tail_sign[simp]: 3013 "sign_extend 47 (epQueue_tail_CL (endpoint_lift ko)) = epQueue_tail_CL (endpoint_lift ko)" 3014 by (simp add: endpoint_lift_def sign_extend_sign_extend_eq) 3015 3016(* Clag from cancelSignal_ccorres_helper *) 3017 3018lemma cancelIPC_ccorres_helper: 3019 "ccorres dc xfdc (invs' and 3020 st_tcb_at' (\<lambda>st. (isBlockedOnSend st \<or> isBlockedOnReceive st) 3021 \<and> blockingObject st = ep) thread 3022 and ko_at' ep' ep) 3023 {s. epptr_' s = Ptr ep} 3024 [] 3025 (setEndpoint ep (if remove1 thread (epQueue ep') = [] then Structures_H.endpoint.IdleEP 3026 else epQueue_update (\<lambda>_. remove1 thread (epQueue ep')) ep')) 3027 (\<acute>queue :== CALL ep_ptr_get_queue(\<acute>epptr);; 3028 \<acute>queue :== CALL tcbEPDequeue(tcb_ptr_to_ctcb_ptr thread,\<acute>queue);; 3029 CALL ep_ptr_set_queue(\<acute>epptr,\<acute>queue);; 3030 IF head_C \<acute>queue = NULL THEN 3031 CALL endpoint_ptr_set_state(\<acute>epptr,scast EPState_Idle) 3032 FI)" 3033 apply (rule ccorres_from_vcg) 3034 apply (rule allI) 3035 apply (rule conseqPre) 3036 apply vcg 3037 apply (clarsimp split del: if_split simp del: comp_def) 3038 apply (frule (2) ep_blocked_in_queueD) 3039 apply (frule (1) ko_at_valid_ep' [OF _ invs_valid_objs']) 3040 apply (elim conjE) 3041 apply (frule (1) valid_ep_blockedD) 3042 apply (elim conjE) 3043 apply (frule cmap_relation_ep) 3044 apply (erule (1) cmap_relation_ko_atE) 3045 apply (intro conjI) 3046 apply (erule h_t_valid_clift) 3047 apply (rule impI) 3048 apply (rule exI) 3049 apply (rule conjI) 3050 apply (rule_tac x = \<sigma> in exI) 3051 apply (intro conjI) 3052 apply assumption+ 3053 apply (drule (2) ep_to_ep_queue) 3054 apply (simp add: tcb_queue_relation'_def) 3055 apply (clarsimp simp: typ_heap_simps cong: imp_cong split del: if_split simp del: comp_def) 3056 apply (frule null_ep_queue [simplified comp_def] null_ep_queue) 3057 apply (intro impI conjI allI) 3058 \<comment> \<open>empty case\<close> 3059 apply clarsimp 3060 apply (frule iffD1 [OF tcb_queue_head_empty_iff [OF tcb_queue_relation'_queue_rel]]) 3061 apply (rule ballI, erule bspec) 3062 apply (erule subsetD [rotated]) 3063 apply clarsimp 3064 subgoal by simp 3065 apply (simp add: setEndpoint_def split_def) 3066 apply (rule bexI [OF _ setObject_eq]) 3067 apply (simp add: remove1_empty rf_sr_def cstate_relation_def Let_def 3068 cpspace_relation_def update_ep_map_tos typ_heap_simps') 3069 apply (elim conjE) 3070 apply (intro conjI) 3071 \<comment> \<open>tcb relation\<close> 3072 apply (erule ctcb_relation_null_queue_ptrs) 3073 subgoal by (clarsimp simp: comp_def) 3074 \<comment> \<open>ep relation\<close> 3075 apply (rule cpspace_relation_ep_update_ep, assumption+) 3076 subgoal by (simp add: cendpoint_relation_def Let_def EPState_Idle_def) 3077 subgoal by simp 3078 \<comment> \<open>ntfn relation\<close> 3079 apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) 3080 apply simp 3081 apply (rule cnotification_relation_ep_queue [OF invs_sym'], assumption+) 3082 subgoal by simp 3083 apply (erule (1) map_to_ko_atI') 3084 apply (simp add: heap_to_user_data_def Let_def) 3085 \<comment> \<open>queue relation\<close> 3086 apply (rule cready_queues_relation_null_queue_ptrs, assumption+) 3087 subgoal by (clarsimp simp: comp_def) 3088 subgoal by (clarsimp simp: carch_state_relation_def carch_globals_def 3089 fpu_null_state_heap_update_tag_disj_simps 3090 global_ioport_bitmap_heap_update_tag_disj_simps 3091 packed_heap_update_collapse_hrs 3092 elim!: fpu_null_state_typ_heap_preservation) 3093 subgoal by (simp add: cmachine_state_relation_def) 3094 subgoal by (simp add: h_t_valid_clift_Some_iff) 3095 subgoal by (simp add: objBits_simps') 3096 subgoal by (simp add: objBits_simps) 3097 apply assumption 3098 \<comment> \<open>non empty case\<close> 3099 apply clarsimp 3100 apply (frule tcb_queue_head_empty_iff [OF tcb_queue_relation'_queue_rel]) 3101 apply (rule ballI, erule bspec) 3102 apply (erule subsetD [rotated]) 3103 apply clarsimp 3104 apply (simp add: setEndpoint_def split_def) 3105 apply (rule bexI [OF _ setObject_eq]) 3106 apply (frule (1) st_tcb_at_h_t_valid) 3107 apply (simp add: remove1_empty rf_sr_def cstate_relation_def Let_def 3108 cpspace_relation_def update_ep_map_tos typ_heap_simps') 3109 apply (elim conjE) 3110 apply (intro conjI) 3111 \<comment> \<open>tcb relation\<close> 3112 apply (erule ctcb_relation_null_queue_ptrs) 3113 subgoal by (clarsimp simp: comp_def) 3114 \<comment> \<open>ep relation\<close> 3115 apply (rule cpspace_relation_ep_update_ep, assumption+) 3116 apply (simp add: cendpoint_relation_def Let_def isSendEP_def isRecvEP_def split: endpoint.splits split del: if_split) 3117 \<comment> \<open>recv case\<close> 3118 apply (subgoal_tac "pspace_canonical' \<sigma>") 3119 prefer 2 3120 apply fastforce 3121 apply (clarsimp simp add: h_t_valid_clift_Some_iff ctcb_offset_defs 3122 tcb_queue_relation'_next_mask tcb_queue_relation'_prev_mask 3123 tcb_queue_relation'_next_sign tcb_queue_relation'_prev_sign 3124 cong: tcb_queue_relation'_cong) 3125 subgoal by (intro impI conjI; simp) 3126 \<comment> \<open>send case\<close> 3127 apply (subgoal_tac "pspace_canonical' \<sigma>") 3128 prefer 2 3129 apply fastforce 3130 apply (clarsimp simp add: h_t_valid_clift_Some_iff ctcb_offset_defs 3131 tcb_queue_relation'_next_mask tcb_queue_relation'_prev_mask 3132 tcb_queue_relation'_next_sign tcb_queue_relation'_prev_sign 3133 cong: tcb_queue_relation'_cong) 3134 subgoal by (intro impI conjI; simp) 3135 subgoal by simp 3136 \<comment> \<open>ntfn relation\<close> 3137 apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) 3138 apply simp 3139 apply (rule cnotification_relation_ep_queue [OF invs_sym'], assumption+) 3140 apply simp 3141 apply (erule (1) map_to_ko_atI') 3142 \<comment> \<open>queue relation\<close> 3143 apply (rule cready_queues_relation_null_queue_ptrs, assumption+) 3144 subgoal by (clarsimp simp: comp_def) 3145 subgoal by (clarsimp simp: carch_state_relation_def carch_globals_def 3146 fpu_null_state_heap_update_tag_disj_simps 3147 global_ioport_bitmap_heap_update_tag_disj_simps 3148 packed_heap_update_collapse_hrs 3149 elim!: fpu_null_state_typ_heap_preservation) 3150 subgoal by (simp add: cmachine_state_relation_def) 3151 subgoal by (simp add: h_t_valid_clift_Some_iff) 3152 subgoal by (simp add: objBits_simps') 3153 subgoal by (simp add: objBits_simps) 3154 by assumption 3155 3156declare empty_fail_get[iff] 3157 3158lemma getThreadState_ccorres_foo: 3159 "(\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> 3160 ccorres r xf (\<lambda>s. \<forall>ts. st_tcb_at' ((=) ts) t s \<longrightarrow> P ts s) 3161 {s. \<forall>ts tcb'. cslift s (tcb_ptr_to_ctcb_ptr t) = Some tcb' 3162 \<and> cthread_state_relation ts (tcbState_C tcb', tcbFault_C tcb') 3163 \<longrightarrow> s \<in> P' ts} hs 3164 (getThreadState t >>= f) c" 3165 apply (rule ccorres_symb_exec_l' [OF _ gts_inv' gts_sp' empty_fail_getThreadState]) 3166 apply (erule_tac x=rv in meta_allE) 3167 apply (erule ccorres_guard_imp2) 3168 apply (clarsimp simp: st_tcb_at'_def) 3169 apply (drule obj_at_ko_at', clarsimp) 3170 apply (erule cmap_relationE1 [OF cmap_relation_tcb]) 3171 apply (erule ko_at_projectKO_opt) 3172 apply (clarsimp simp: ctcb_relation_def obj_at'_def) 3173 done 3174 3175lemma ep_blocked_in_queueD_recv: 3176 "\<lbrakk>st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnReceive x)) thread \<sigma>; ko_at' ep' x \<sigma>; invs' \<sigma>\<rbrakk> \<Longrightarrow> thread \<in> set (epQueue ep') \<and> isRecvEP ep'" 3177 apply (frule sym_refs_st_tcb_atD', clarsimp) 3178 apply (clarsimp simp: refs_of_rev' obj_at'_def ko_wp_at'_def projectKOs) 3179 apply (cases ep', simp_all add: isSendEP_def isRecvEP_def)[1] 3180 done 3181 3182lemma ep_blocked_in_queueD_send: 3183 "\<lbrakk>st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnSend x xa xb xc)) thread \<sigma>; ko_at' ep' x \<sigma>; invs' \<sigma>\<rbrakk> \<Longrightarrow> thread \<in> set (epQueue ep') \<and> isSendEP ep'" 3184 apply (frule sym_refs_st_tcb_atD', clarsimp) 3185 apply (clarsimp simp: refs_of_rev' obj_at'_def ko_wp_at'_def projectKOs) 3186 apply (cases ep', simp_all add: isSendEP_def isRecvEP_def)[1] 3187 done 3188 3189lemma cancelIPC_ccorres1: 3190 assumes cteDeleteOne_ccorres: 3191 "\<And>w slot. ccorres dc xfdc 3192 (invs' and cte_wp_at' (\<lambda>ct. w = -1 \<or> cteCap ct = NullCap 3193 \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot) 3194 ({s. gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s)) = w} 3195 \<inter> {s. slot_' s = Ptr slot}) [] 3196 (cteDeleteOne slot) (Call cteDeleteOne_'proc)" 3197 shows 3198 "ccorres dc xfdc (tcb_at' thread and invs') 3199 (UNIV \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr thread}) [] 3200 (cancelIPC thread) (Call cancelIPC_'proc)" 3201 apply (cinit lift: tptr_' simp: Let_def cong: call_ignore_cong) 3202 apply (rule ccorres_move_c_guard_tcb) 3203 apply csymbr 3204 apply (rule getThreadState_ccorres_foo) 3205 apply (rule ccorres_symb_exec_r) 3206 apply (rule_tac xf'=ret__unsigned_longlong_' in ccorres_abstract, ceqv) 3207 apply (rule_tac P="rv' = thread_state_to_tsType rv" in ccorres_gen_asm2) 3208 apply wpc 3209 \<comment> \<open>BlockedOnReceive\<close> 3210 apply (simp add: word_sle_def "StrictC'_thread_state_defs" ccorres_cond_iffs cong: call_ignore_cong) 3211 apply (fold dc_def) 3212 apply (rule ccorres_rhs_assoc)+ 3213 apply csymbr 3214 apply csymbr 3215 apply (rule ccorres_pre_getEndpoint) 3216 apply (rule ccorres_assert) 3217 apply (rule ccorres_symb_exec_r) \<comment> \<open>ptr_get lemmas don't work so well :(\<close> 3218 apply (rule ccorres_symb_exec_r) 3219 apply (simp only: fun_app_def simp_list_case_return 3220 return_bind ccorres_seq_skip) 3221 apply (rule ccorres_rhs_assoc2) 3222 apply (rule ccorres_rhs_assoc2) 3223 apply (rule ccorres_rhs_assoc2) 3224 apply (ctac (no_vcg) add: cancelIPC_ccorres_helper) 3225 apply (ctac add: setThreadState_ccorres_valid_queues') 3226 apply (wp hoare_vcg_all_lift set_ep_valid_objs' | simp add: valid_tcb_state'_def split del: if_split)+ 3227 apply (simp add: "StrictC'_thread_state_defs") 3228 apply vcg 3229 apply (rule conseqPre, vcg) 3230 apply clarsimp 3231 apply clarsimp 3232 apply (rule conseqPre, vcg) 3233 apply (rule subset_refl) 3234 apply (rule conseqPre, vcg) 3235 apply clarsimp 3236 \<comment> \<open>BlockedOnReply case\<close> 3237 apply (simp add: "StrictC'_thread_state_defs" ccorres_cond_iffs 3238 Collect_False Collect_True word_sle_def 3239 cong: call_ignore_cong del: Collect_const) 3240 apply (fold dc_def) 3241 apply (rule ccorres_rhs_assoc)+ 3242 apply csymbr 3243 apply csymbr 3244 apply (unfold comp_def)[1] 3245 apply csymbr 3246 apply (rule ccorres_move_c_guard_tcb)+ 3247 apply (rule ccorres_split_nothrow_novcg) 3248 apply (rule_tac P=\<top> in threadSet_ccorres_lemma2) 3249 apply vcg 3250 apply (clarsimp simp: typ_heap_simps') 3251 apply (erule(1) rf_sr_tcb_update_no_queue2, 3252 (simp add: typ_heap_simps')+)[1] 3253 apply (rule ball_tcb_cte_casesI, simp_all)[1] 3254 apply (clarsimp simp: ctcb_relation_def seL4_Fault_lift_NullFault 3255 cfault_rel_def cthread_state_relation_def) 3256 apply (case_tac "tcbState tcb", simp_all add: is_cap_fault_def)[1] 3257 apply ceqv 3258 apply ccorres_remove_UNIV_guard 3259 apply (rule ccorres_move_array_assertion_tcb_ctes) 3260 apply (rule_tac P="tcb_at' thread" in ccorres_cross_over_guard) 3261 apply (simp add: getThreadReplySlot_def) 3262 apply ctac 3263 apply (simp only: liftM_def bind_assoc return_bind del: Collect_const) 3264 apply (rule ccorres_pre_getCTE) 3265 apply (rename_tac slot slot' cte) 3266 apply (rule ccorres_move_c_guard_cte) 3267 apply (rule_tac xf'=ret__unsigned_longlong_' and val="mdbNext (cteMDBNode cte)" 3268 and R="cte_wp_at' ((=) cte) slot and invs'" 3269 in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) 3270 apply vcg 3271 apply (clarsimp simp: cte_wp_at_ctes_of) 3272 apply (erule(1) cmap_relationE1[OF cmap_relation_cte]) 3273 apply (clarsimp simp: typ_heap_simps) 3274 apply (clarsimp simp: ccte_relation_def map_option_Some_eq2) 3275 apply ceqv 3276 apply csymbr 3277 apply (rule ccorres_Cond_rhs) 3278 apply (simp add: nullPointer_def when_def) 3279 apply (rule ccorres_symb_exec_l[OF _ _ _ empty_fail_stateAssert]) 3280 apply (simp only: dc_def[symmetric]) 3281 apply (rule ccorres_symb_exec_r) 3282 apply (ctac add: cteDeleteOne_ccorres[where w1="scast cap_reply_cap"]) 3283 apply vcg 3284 apply (rule conseqPre, vcg, clarsimp simp: rf_sr_def 3285 gs_set_assn_Delete_cstate_relation[unfolded o_def]) 3286 apply (wp | simp)+ 3287 apply (simp add: when_def nullPointer_def dc_def[symmetric]) 3288 apply (rule ccorres_return_Skip) 3289 apply (simp add: guard_is_UNIV_def ghost_assertion_data_get_def 3290 ghost_assertion_data_set_def cap_tag_defs) 3291 apply (simp add: locateSlot_conv, wp) 3292 apply vcg 3293 apply (rule_tac Q="\<lambda>rv. tcb_at' thread and invs'" in hoare_post_imp) 3294 apply (clarsimp simp: cte_wp_at_ctes_of capHasProperty_def 3295 cap_get_tag_isCap ucast_id) 3296 apply (wp threadSet_invs_trivial | simp)+ 3297 apply (clarsimp simp add: guard_is_UNIV_def tcbReplySlot_def 3298 Kernel_C.tcbReply_def tcbCNodeEntries_def) 3299 \<comment> \<open>BlockedOnNotification\<close> 3300 apply (simp add: word_sle_def "StrictC'_thread_state_defs" ccorres_cond_iffs dc_def [symmetric] cong: call_ignore_cong) 3301 apply (rule ccorres_symb_exec_r) 3302 apply (ctac (no_vcg)) 3303 apply clarsimp 3304 apply (rule conseqPre, vcg) 3305 apply (rule subset_refl) 3306 apply (rule conseqPre, vcg) 3307 apply clarsimp 3308 \<comment> \<open>Running, Inactive, and Idle\<close> 3309 apply (simp add: word_sle_def "StrictC'_thread_state_defs" ccorres_cond_iffs dc_def [symmetric] cong: call_ignore_cong, 3310 rule ccorres_return_Skip)+ 3311 \<comment> \<open>BlockedOnSend\<close> 3312 apply (simp add: word_sle_def "StrictC'_thread_state_defs" ccorres_cond_iffs dc_def [symmetric] cong: call_ignore_cong) 3313 \<comment> \<open>clag\<close> 3314 apply (rule ccorres_rhs_assoc)+ 3315 apply csymbr 3316 apply csymbr 3317 apply (rule ccorres_pre_getEndpoint) 3318 apply (rule ccorres_assert) 3319 apply (rule ccorres_symb_exec_r) \<comment> \<open>ptr_get lemmas don't work so well :(\<close> 3320 apply (rule ccorres_symb_exec_r) 3321 apply (simp only: fun_app_def simp_list_case_return return_bind ccorres_seq_skip) 3322 apply (rule ccorres_rhs_assoc2) 3323 apply (rule ccorres_rhs_assoc2) 3324 apply (rule ccorres_rhs_assoc2) 3325 apply (ctac (no_vcg) add: cancelIPC_ccorres_helper) 3326 apply (ctac add: setThreadState_ccorres_valid_queues') 3327 apply (wp hoare_vcg_all_lift set_ep_valid_objs' | simp add: valid_tcb_state'_def split del:if_split)+ 3328 apply (simp add: "StrictC'_thread_state_defs") 3329 apply clarsimp 3330 apply (rule conseqPre, vcg, rule subset_refl) 3331 apply (rule conseqPre, vcg) 3332 apply clarsimp 3333 apply clarsimp 3334 apply (rule conseqPre, vcg, rule subset_refl) 3335 apply (rule conseqPre, vcg) 3336 apply clarsimp 3337 \<comment> \<open>Restart\<close> 3338 apply (simp add: word_sle_def "StrictC'_thread_state_defs" ccorres_cond_iffs dc_def [symmetric] cong: call_ignore_cong, 3339 rule ccorres_return_Skip) 3340 \<comment> \<open>Post wp proofs\<close> 3341 apply vcg 3342 apply clarsimp 3343 apply (rule conseqPre, vcg) 3344 apply clarsimp 3345 apply clarsimp 3346 apply (drule(1) obj_at_cslift_tcb) 3347 apply clarsimp 3348 apply (frule obj_at_valid_objs', clarsimp+) 3349 apply (clarsimp simp: projectKOs valid_obj'_def valid_tcb'_def 3350 valid_tcb_state'_def typ_heap_simps 3351 word_sle_def) 3352 apply (rule conjI, clarsimp) 3353 apply (rule conjI, clarsimp) 3354 apply (rule conjI) 3355 subgoal by (auto simp: projectKOs obj_at'_def pred_tcb_at'_def split: thread_state.splits)[1] 3356 apply (clarsimp) 3357 apply (rule conjI) 3358 subgoal by (auto simp: obj_at'_def projectKOs pred_tcb_at'_def invs'_def valid_state'_def 3359 isTS_defs cte_wp_at_ctes_of 3360 cthread_state_relation_def sch_act_wf_weak valid_ep'_def 3361 dest!: valid_queues_not_runnable'_not_ksQ[where t=thread] split: thread_state.splits) 3362 apply clarsimp 3363 apply (frule (2) ep_blocked_in_queueD_recv) 3364 apply (frule (1) ko_at_valid_ep'[OF _ invs_valid_objs']) 3365 subgoal by (auto simp: obj_at'_def projectKOs pred_tcb_at'_def invs'_def valid_state'_def 3366 isTS_defs cte_wp_at_ctes_of isRecvEP_def 3367 cthread_state_relation_def sch_act_wf_weak valid_ep'_def 3368 dest!: valid_queues_not_runnable'_not_ksQ[where t=thread] split: thread_state.splits endpoint.splits) 3369 apply (rule conjI) 3370 apply (clarsimp simp: inQ_def) 3371 apply (rule conjI) 3372 apply clarsimp 3373 apply clarsimp 3374 apply (rule conjI) 3375 subgoal by (auto simp: obj_at'_def projectKOs pred_tcb_at'_def invs'_def valid_state'_def 3376 isTS_defs cte_wp_at_ctes_of 3377 cthread_state_relation_def sch_act_wf_weak valid_ep'_def 3378 dest!: valid_queues_not_runnable'_not_ksQ[where t=thread] split: thread_state.splits) 3379 apply clarsimp 3380 apply (rule conjI) 3381 subgoal by (auto simp: obj_at'_def projectKOs pred_tcb_at'_def invs'_def valid_state'_def 3382 isTS_defs cte_wp_at_ctes_of 3383 cthread_state_relation_def sch_act_wf_weak valid_ep'_def 3384 dest!: valid_queues_not_runnable'_not_ksQ[where t=thread] split: thread_state.splits) 3385 apply clarsimp 3386 apply (frule (2) ep_blocked_in_queueD_send) 3387 apply (frule (1) ko_at_valid_ep'[OF _ invs_valid_objs']) 3388 subgoal by (auto simp: obj_at'_def projectKOs pred_tcb_at'_def invs'_def valid_state'_def 3389 isTS_defs cte_wp_at_ctes_of isSendEP_def 3390 cthread_state_relation_def sch_act_wf_weak valid_ep'_def 3391 dest!: valid_queues_not_runnable'_not_ksQ[where t=thread] split: thread_state.splits endpoint.splits)[1] 3392 apply (auto simp: isTS_defs cthread_state_relation_def typ_heap_simps weak_sch_act_wf_def) 3393 apply (case_tac ts, 3394 auto simp: isTS_defs cthread_state_relation_def typ_heap_simps) 3395 done 3396 3397end 3398end 3399