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 Schedule_C 12imports Tcb_C 13begin 14 15context begin interpretation Arch . (*FIXME: arch_split*) 16 17(* FIXME move to REFINE *) 18crunch valid_queues'[wp]: "Arch.switchToThread" valid_queues' 19 (ignore: ) 20crunch ksCurDomain[wp]: switchToIdleThread "\<lambda>s. P (ksCurDomain s)" 21crunch valid_pspace'[wp]: switchToIdleThread, switchToThread valid_pspace' 22 (simp: whenE_def ignore: getObject) 23 24lemma setCurrentUserCR3_valid_arch_state'[wp]: 25 "\<lbrace>valid_arch_state' and K (valid_cr3' c)\<rbrace> setCurrentUserCR3 c \<lbrace>\<lambda>_. valid_arch_state'\<rbrace>" 26 by (wpsimp simp: setCurrentUserCR3_def valid_arch_state'_def) 27 28lemma setVMRoot_valid_arch_state': 29 "\<lbrace>valid_arch_state'\<rbrace> setVMRoot t \<lbrace>\<lambda>_. valid_arch_state'\<rbrace>" 30 apply (simp add: setVMRoot_def getThreadVSpaceRoot_def setCurrentUserVSpaceRoot_def) 31 apply (wp hoare_whenE_wp getCurrentUserCR3_wp findVSpaceForASID_vs_at_wp 32 | wpcw 33 | clarsimp simp: if_apply_def2 asid_wf_0 34 | strengthen valid_cr3'_makeCR3)+ 35 done 36 37crunch valid_arch_state'[wp]: switchToThread valid_arch_state' 38 (wp: crunch_wps simp: crunch_simps) 39 40end 41 42(*FIXME: arch_split: move up?*) 43context Arch begin 44context begin global_naming global 45requalify_facts 46 Thread_H.switchToIdleThread_def 47 Thread_H.switchToThread_def 48end 49end 50 51context kernel_m begin 52 53(* FIXME: move to Refine *) 54lemma valid_idle'_tcb_at'_ksIdleThread: 55 "valid_idle' s \<Longrightarrow> tcb_at' (ksIdleThread s) s" 56 by (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def) 57 58(* FIXME: move to Refine *) 59lemma invs_no_cicd'_valid_idle': 60 "invs_no_cicd' s \<Longrightarrow> valid_idle' s" 61 by (simp add: invs_no_cicd'_def) 62 63lemma Arch_switchToIdleThread_ccorres: 64 "ccorres dc xfdc invs_no_cicd' UNIV [] 65 Arch.switchToIdleThread (Call Arch_switchToIdleThread_'proc)" 66 apply (cinit simp: X64_H.switchToIdleThread_def) 67 apply (rule ccorres_pre_getIdleThread) 68 apply (rule ccorres_symb_exec_r) 69 apply (ctac (no_vcg) add: setVMRoot_ccorres) 70 apply vcg 71 apply (rule conseqPre, vcg) 72 apply clarsimp 73 apply (clarsimp simp: invs_no_cicd'_def valid_pspace'_def valid_idle'_tcb_at'_ksIdleThread) 74 done 75 76(* FIXME: move *) 77lemma empty_fail_getIdleThread [simp,intro!]: 78 "empty_fail getIdleThread" 79 by (simp add: getIdleThread_def) 80 81lemma switchToIdleThread_ccorres: 82 "ccorres dc xfdc invs_no_cicd' UNIV hs 83 switchToIdleThread (Call switchToIdleThread_'proc)" 84 apply (cinit) 85 apply (rule ccorres_symb_exec_l) 86 apply (ctac (no_vcg) add: Arch_switchToIdleThread_ccorres) 87 apply (simp add: setCurThread_def) 88 apply (rule_tac P="\<lambda>s. thread = ksIdleThread s" and P'=UNIV in ccorres_from_vcg) 89 apply (rule allI, rule conseqPre, vcg) 90 apply (clarsimp simp: simpler_modify_def) 91 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 92 carch_state_relation_def cmachine_state_relation_def) 93 apply (wpsimp simp: X64_H.switchToIdleThread_def)+ 94 done 95 96lemma Arch_switchToThread_ccorres: 97 "ccorres dc xfdc 98 (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t) 99 (UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>) 100 [] 101 (Arch.switchToThread t) (Call Arch_switchToThread_'proc)" 102 apply (cinit lift: tcb_') 103 apply (unfold X64_H.switchToThread_def)[1] 104 apply (ctac (no_vcg) add: setVMRoot_ccorres) 105 apply (simp (no_asm) del: Collect_const) 106 apply clarsimp 107 done 108 109(* FIXME: move *) 110lemma switchToThread_ccorres: 111 "ccorres dc xfdc 112 (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t) 113 (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>) 114 hs 115 (switchToThread t) 116 (Call switchToThread_'proc)" 117 apply (cinit lift: thread_') 118 apply (ctac (no_vcg) add: Arch_switchToThread_ccorres) 119 apply (ctac (no_vcg) add: tcbSchedDequeue_ccorres) 120 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg) 121 apply clarsimp 122 apply (rule conseqPre, vcg) 123 apply (clarsimp simp: setCurThread_def simpler_modify_def) 124 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 125 carch_state_relation_def cmachine_state_relation_def) 126 apply wp+ 127 apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def) 128 done 129 130lemma get_tsType_ccorres2: 131 "ccorres (\<lambda>r r'. r' = thread_state_to_tsType r) ret__unsigned_longlong_' (tcb_at' thread) 132 (UNIV \<inter> {s. f s = tcb_ptr_to_ctcb_ptr thread} \<inter> 133 {s. cslift s (Ptr &(f s\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}) [] 134 (getThreadState thread) (Call thread_state_get_tsType_'proc)" 135 unfolding getThreadState_def 136 apply (rule ccorres_from_spec_modifies [where P=\<top>, simplified]) 137 apply (rule thread_state_get_tsType_spec) 138 apply (rule thread_state_get_tsType_modifies) 139 apply simp 140 apply (frule (1) obj_at_cslift_tcb) 141 apply (clarsimp simp: typ_heap_simps) 142 apply (rule bexI [rotated, OF threadGet_eq], assumption) 143 apply simp 144 apply (drule ctcb_relation_thread_state_to_tsType) 145 apply simp 146 done 147 148lemma activateThread_ccorres: 149 "ccorres dc xfdc 150 (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) 151 and valid_queues and valid_objs') 152 UNIV [] 153 activateThread 154 (Call activateThread_'proc)" 155 apply (cinit) 156 apply (rule ccorres_pre_getCurThread) 157 apply (ctac add: get_tsType_ccorres2 [where f="\<lambda>s. ksCurThread_' (globals s)"]) 158 apply (rule_tac P="activatable' rv" in ccorres_gen_asm) 159 apply (wpc) 160 apply (rule_tac P=\<top> and P'=UNIV in ccorres_inst, simp) 161 apply (rule_tac P=\<top> and P'=UNIV in ccorres_inst, simp) 162 apply (rule_tac P=\<top> and P'=UNIV in ccorres_inst, simp) 163 apply simp 164 apply (rule ccorres_cond_true) 165 apply (rule ccorres_return_Skip) 166 apply (rule_tac P=\<top> and P'=UNIV in ccorres_inst, simp) 167 apply (simp add: "StrictC'_thread_state_defs" del: Collect_const) 168 apply (rule ccorres_cond_false) 169 apply (rule ccorres_cond_false) 170 apply (rule ccorres_cond_true) 171 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg) 172 apply (rule allI, rule conseqPre, vcg) 173 apply (clarsimp simp: activateIdleThread_def return_def) 174 apply (rule_tac P=\<top> and P'=UNIV in ccorres_inst, simp) 175 apply (simp add: "StrictC'_thread_state_defs" del: Collect_const) 176 apply (rule ccorres_cond_false) 177 apply (rule ccorres_cond_true) 178 apply (rule ccorres_rhs_assoc)+ 179 apply csymbr 180 apply (ctac) 181 apply (ctac add: setNextPC_ccorres) 182 apply ctac 183 apply (wp | simp add: valid_tcb_state'_def)+ 184 apply vcg 185 apply wp 186 apply vcg 187 apply (wp gts_wp') 188 apply vcg 189 apply (clarsimp simp: ct_in_state'_def) 190 apply (rule conjI, clarsimp) 191 apply (clarsimp simp: st_tcb_at'_def) 192 apply (rule conjI, clarsimp simp: obj_at'_def) 193 apply clarsimp 194 apply (drule (1) obj_at_cslift_tcb) 195 apply (subgoal_tac "ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s)") 196 prefer 2 197 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 198 apply (clarsimp simp: typ_heap_simps ThreadState_Running_def mask_def) 199 done 200 201lemma ceqv_Guard_UNIV_Skip: 202 "ceqv Gamma xf v s s' (a ;; Guard F UNIV Skip) a" 203 apply (rule ceqvI) 204 apply (safe elim!: exec_Normal_elim_cases) 205 apply (case_tac s'a, auto intro: exec.intros elim!: exec_Normal_elim_cases)[1] 206 apply (cases s', auto intro: exec.intros) 207 done 208 209lemma ceqv_tail_Guard_onto_Skip: 210 "ceqv Gamma xf v s s' 211 (a ;; Guard F G b) ((a ;; Guard F G Skip) ;; b)" 212 apply (rule ceqvI) 213 apply (safe elim!: exec_Normal_elim_cases) 214 apply (case_tac s'a, auto intro: exec.intros elim!: exec_Normal_elim_cases)[1] 215 apply (case_tac s'aa, auto intro: exec.intros elim!: exec_Normal_elim_cases)[1] 216 done 217 218lemma ceqv_remove_tail_Guard_Skip: 219 "\<lbrakk> \<And>s. s \<in> G \<rbrakk> \<Longrightarrow> ceqv Gamma xf v s s' (a ;; Guard F G Skip) a" 220 apply (rule ceqvI) 221 apply (safe elim!: exec_Normal_elim_cases) 222 apply (case_tac s'a, auto intro: exec.intros elim!: exec_Normal_elim_cases)[1] 223 apply (case_tac s', auto intro: exec.intros elim!: exec_Normal_elim_cases)[1] 224 done 225 226lemmas ccorres_remove_tail_Guard_Skip 227 = ccorres_abstract[where xf'="\<lambda>_. ()", OF ceqv_remove_tail_Guard_Skip] 228 229(* FIXME x64: does this need machine_word? *) 230lemma queue_in_range_pre: 231 "\<lbrakk> (qdom :: word32) \<le> ucast maxDom; prio \<le> ucast maxPrio \<rbrakk> 232 \<Longrightarrow> qdom * of_nat numPriorities + prio < of_nat (numDomains * numPriorities)" 233 by (clarsimp simp: cready_queues_index_to_C_def word_less_nat_alt 234 word_le_nat_alt unat_ucast maxDom_def seL4_MaxPrio_def 235 numPriorities_def unat_word_ariths numDomains_def) 236 237lemmas queue_in_range' = queue_in_range_pre[unfolded numDomains_def numPriorities_def, simplified] 238 239lemma switchToThread_ccorres': 240 "ccorres (\<lambda>_ _. True) xfdc 241 (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t) 242 (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>) 243 hs 244 (switchToThread t) 245 (Call switchToThread_'proc)" 246 apply (rule ccorres_guard_imp2) 247 apply (ctac (no_vcg) add: switchToThread_ccorres[simplified dc_def]) 248 apply auto 249 done 250 251lemmas word_log2_max_word_word_size = word_log2_max[where 'a=machine_word_len, simplified word_size, simplified] 252 253lemma chooseThread_ccorres: 254 "ccorres dc xfdc all_invs_but_ct_idle_or_in_cur_domain' UNIV [] chooseThread (Call chooseThread_'proc)" 255proof - 256 257 note prio_and_dom_limit_helpers [simp] 258 note ksReadyQueuesL2Bitmap_nonzeroI [simp] 259 note Collect_const_mem [simp] 260 261 have invs_no_cicd'_max_CurDomain[intro]: 262 "\<And>s. invs_no_cicd' s \<Longrightarrow> ksCurDomain s \<le> maxDomain" 263 by (simp add: invs_no_cicd'_def) 264 265 show ?thesis 266 apply (cinit) 267 apply (simp add: numDomains_def word_sless_alt word_sle_def) 268 apply (ctac (no_vcg) add: getCurDomain_ccorres_dom_') 269 apply clarsimp 270 apply (rename_tac curdom) 271 apply (rule_tac P="curdom \<le> maxDomain" in ccorres_cross_over_guard_no_st) 272 apply (rule ccorres_Guard) 273 apply (rule ccorres_pre_getReadyQueuesL1Bitmap) 274 apply (rename_tac l1) 275 apply (rule_tac R="\<lambda>s. l1 = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain" 276 in ccorres_cond) 277 subgoal by (fastforce dest!: rf_sr_cbitmap_L1_relation simp: cbitmap_L1_relation_def) 278 prefer 2 \<comment> \<open>switchToIdleThread\<close> 279 apply (ctac(no_vcg) add: switchToIdleThread_ccorres) 280 apply clarsimp 281 apply (rule ccorres_rhs_assoc)+ 282 283 apply (rule ccorres_split_nothrow_novcg) 284 apply (rule_tac xf'=prio_' in ccorres_call) 285 apply (rule getHighestPrio_ccorres[simplified getHighestPrio_def']) 286 apply simp+ 287 apply ceqv 288 apply clarsimp 289 apply (rename_tac prio) 290 apply (rule_tac P="curdom \<le> maxDomain" in ccorres_cross_over_guard_no_st) 291 apply (rule_tac P="prio \<le> maxPriority" in ccorres_cross_over_guard_no_st) 292 apply (rule ccorres_pre_getQueue) 293 apply (rule_tac P="queue \<noteq> []" in ccorres_cross_over_guard_no_st) 294 apply (rule ccorres_symb_exec_l) 295 apply (rule ccorres_assert) 296 apply csymbr 297 apply (rule ccorres_Guard_Seq)+ 298 apply (rule ccorres_symb_exec_r) 299 apply (simp only: ccorres_seq_skip) 300 apply (rule ccorres_call[OF switchToThread_ccorres']; simp) 301 apply vcg 302 apply (rule conseqPre, vcg) 303 apply clarsimp 304 apply (wp isRunnable_wp)+ 305 apply (simp add: isRunnable_def) 306 apply wp 307 apply (clarsimp simp: Let_def guard_is_UNIV_def) 308 apply (drule invs_no_cicd'_queues) 309 apply (case_tac queue, simp) 310 apply (clarsimp simp: tcb_queue_relation'_def cready_queues_index_to_C_def 311 numPriorities_def ) 312 apply (simp add: word_less_nat_alt word_le_nat_alt) 313 apply (rule_tac x="unat curdom * 256" and xmax="unat maxDomain * 256" in nat_add_less_by_max) 314 subgoal by (simp add: word_le_nat_alt[symmetric]) 315 subgoal by (simp add: maxDomain_def numDomains_def maxPriority_def numPriorities_def) 316 apply wp 317 apply clarsimp 318 apply (frule invs_no_cicd'_queues) 319 apply (frule invs_no_cicd'_max_CurDomain) 320 apply (frule invs_no_cicd'_queues) 321 apply (clarsimp simp: valid_queues_def lookupBitmapPriority_le_maxPriority) 322 apply (intro conjI impI) 323 apply (fastforce dest: bitmapQ_from_bitmap_lookup simp: valid_bitmapQ_bitmapQ_simp) 324 apply (fastforce dest: lookupBitmapPriority_obj_at' 325 simp: pred_conj_def comp_def obj_at'_def st_tcb_at'_def) 326 done 327qed 328 329lemma ksDomSched_length_relation[simp]: 330 "\<lbrakk>cstate_relation s s'\<rbrakk> \<Longrightarrow> length (kernel_state.ksDomSchedule s) = unat (ksDomScheduleLength)" 331 apply (auto simp: cstate_relation_def cdom_schedule_relation_def Let_def ksDomScheduleLength_def) 332 done 333 334lemma ksDomSched_length_dom_relation[simp]: 335 "\<lbrakk>cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule \<rbrakk> \<Longrightarrow> length (kernel_state.ksDomSchedule s) = unat (ksDomScheduleLength)" 336 apply (auto simp: cstate_relation_def cdom_schedule_relation_def Let_def ksDomScheduleLength_def) 337 done 338 339lemma nextDomain_ccorres: 340 "ccorres dc xfdc invs' UNIV [] nextDomain (Call nextDomain_'proc)" 341 apply (cinit) 342 apply (simp add: ksDomScheduleLength_def sdiv_word_def sdiv_int_def) 343 apply (rule_tac P=invs' and P'=UNIV in ccorres_from_vcg) 344 apply (rule allI, rule conseqPre, vcg) 345 apply (clarsimp simp: simpler_modify_def Let_def 346 rf_sr_def cstate_relation_def 347 carch_state_relation_def cmachine_state_relation_def) 348 apply (rule conjI) 349 apply clarsimp 350 apply (subgoal_tac "ksDomScheduleIdx \<sigma> = unat (ksDomScheduleLength - 1)") 351 apply (fastforce simp add: cdom_schedule_relation_def dom_schedule_entry_relation_def dschDomain_def dschLength_def ksDomScheduleLength_def sdiv_word_def sdiv_int_def simp del: ksDomSched_length_dom_relation) 352 apply (simp add: ksDomScheduleLength_def) 353 apply (frule invs'_ksDomScheduleIdx) 354 apply (simp add: invs'_ksDomSchedule newKernelState_def) 355 apply (simp only: Abs_fnat_hom_1 Abs_fnat_hom_add) 356 apply (drule unat_le_helper) 357 apply (simp add: sdiv_int_def sdiv_word_def) 358 apply (clarsimp simp: cdom_schedule_relation_def) 359 apply (simp only: Abs_fnat_hom_1 Abs_fnat_hom_add word_not_le) 360 apply clarsimp 361 apply (subst (asm) of_nat_Suc[symmetric]) 362 apply (drule iffD1[OF of_nat_mono_maybe'[where x=3, simplified, symmetric], rotated 2]) 363 apply simp 364 apply (frule invs'_ksDomScheduleIdx) 365 apply (simp add: invs'_ksDomSchedule newKernelState_def) 366 apply (clarsimp simp: cdom_schedule_relation_def) 367 apply (clarsimp simp: ksDomScheduleLength_def) 368 apply (subst of_nat_Suc[symmetric])+ 369 apply (subst unat_of_nat64) 370 apply (simp add: word_bits_def) 371 apply (subst unat_of_nat64) 372 apply (simp add: word_bits_def) 373 apply (fastforce simp add: cdom_schedule_relation_def dom_schedule_entry_relation_def dschDomain_def dschLength_def simp del: ksDomSched_length_dom_relation) 374 apply simp 375 done 376 377lemma scheduleChooseNewThread_ccorres: 378 "ccorres dc xfdc 379 (\<lambda>s. invs' s \<and> ksSchedulerAction s = ChooseNewThread) UNIV hs 380 (do domainTime \<leftarrow> getDomainTime; 381 y \<leftarrow> when (domainTime = 0) nextDomain; 382 chooseThread 383 od) 384 (Call scheduleChooseNewThread_'proc)" 385 apply (cinit') 386 apply (rule ccorres_pre_getDomainTime) 387 apply (rule ccorres_split_nothrow) 388 apply (rule_tac R="\<lambda>s. ksDomainTime s = domainTime" in ccorres_when) 389 apply (fastforce simp: rf_sr_ksDomainTime) 390 apply (rule_tac xf'=xfdc in ccorres_call[OF nextDomain_ccorres] ; simp) 391 apply ceqv 392 apply (ctac (no_vcg) add: chooseThread_ccorres) 393 apply (wp nextDomain_invs_no_cicd') 394 apply clarsimp 395 apply (vcg exspec=nextDomain_modifies) 396 apply (clarsimp simp: if_apply_def2 invs'_invs_no_cicd') 397 done 398 399lemma isHighestPrio_ccorres: 400 "ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' 401 (\<lambda>s. d \<le> maxDomain \<and> bitmapQ_no_L1_orphans s) 402 (UNIV \<inter> \<lbrace>\<acute>dom = ucast d\<rbrace> \<inter> \<lbrace>\<acute>prio = ucast p\<rbrace>) hs 403 (isHighestPrio d p) 404 (Call isHighestPrio_'proc)" 405 supply Collect_const [simp del] 406 supply dc_simp [simp del] 407 supply prio_and_dom_limit_helpers[simp] 408 supply Collect_const_mem [simp] 409 (* FIXME: these should likely be in simpset for CRefine, or even in general *) 410 supply from_bool_eq_if[simp] from_bool_eq_if'[simp] from_bool_0[simp] if_1_0_0[simp] 411 ccorres_IF_True[simp] 412 apply (cinit lift: dom_' prio_') 413 apply clarsimp 414 apply (rule ccorres_move_const_guard) 415 apply (rule ccorres_pre_getReadyQueuesL1Bitmap, rename_tac l1) 416 apply (rule ccorres_rhs_assoc2) 417 apply (rule ccorres_cond_seq2[THEN iffD1]) 418 apply ccorres_rewrite 419 apply (rule_tac xf'=ret__int_' and val="from_bool (l1 = 0)" 420 and R="\<lambda>s. l1 = ksReadyQueuesL1Bitmap s d \<and> d \<le> maxDomain" and R'=UNIV 421 in ccorres_symb_exec_r_known_rv) 422 apply vcg 423 apply clarsimp 424 apply (fastforce simp: rf_sr_ksReadyQueuesL1Bitmap_simp) 425 apply ceqv 426 apply clarsimp 427 apply (rule ccorres_cond[where R=\<top>], blast) 428 apply (rule_tac P="l1 = 0" in ccorres_gen_asm, clarsimp) 429 apply (rule ccorres_return_C; clarsimp) 430 apply (rule ccorres_rhs_assoc)+ 431 apply (ctac add: getHighestPrio_ccorres[simplified]) 432 apply (rename_tac hprio hprio') 433 apply csymbr 434 apply (rule ccorres_return_C, simp, simp, simp) 435 apply (rule wp_post_taut) 436 apply (vcg exspec=getHighestPrio_modifies)+ 437 apply (clarsimp simp: word_le_nat_alt true_def to_bool_def split: if_splits) 438 done 439 440lemma schedule_ccorres: 441 "ccorres dc xfdc invs' UNIV [] schedule (Call schedule_'proc)" 442 supply Collect_const [simp del] 443 supply dc_simp [simp del] 444 supply prio_and_dom_limit_helpers[simp] 445 supply Collect_const_mem [simp] 446 (* FIXME: these should likely be in simpset for CRefine, or even in general *) 447 supply from_bool_eq_if[simp] from_bool_eq_if'[simp] from_bool_0[simp] if_1_0_0[simp] 448 ccorres_IF_True[simp] 449 apply (cinit) 450 apply (rule ccorres_pre_getCurThread) 451 apply (rule ccorres_pre_getSchedulerAction) 452 apply wpc 453 (* toplevel case: action is resume current thread *) 454 apply (rule ccorres_cond_false_seq) 455 apply simp 456 apply (rule_tac P=\<top> and P'="{s. ksSchedulerAction_' (globals s) = NULL }" in ccorres_from_vcg) 457 apply (clarsimp simp: dc_def return_def split: prod.splits) 458 apply (rule conseqPre, vcg, clarsimp) 459 (* toplevel case: action is choose new thread *) 460 apply (rule ccorres_cond_true_seq) 461 apply (rule ccorres_rhs_assoc)+ 462 apply csymbr 463 (* ct runnable? *) 464 apply (ctac add: isRunnable_ccorres, rename_tac runnable) 465 apply (clarsimp simp: to_bool_def) 466 apply (rule ccorres_split_nothrow_dc) 467 (* enqueue if runnable *) 468 apply (simp add: when_def) 469 apply (rule ccorres_cond[where R=\<top>], clarsimp) 470 apply csymbr 471 apply (ctac add: tcbSchedEnqueue_ccorres) 472 apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV]) 473 apply (clarsimp, rule conseqPre, vcg) 474 apply (clarsimp simp: dc_def return_def) 475 apply (rule ccorres_cond_true_seq) 476 (* isolate haskell part before setting thread action *) 477 apply (simp add: scheduleChooseNewThread_def) 478 apply (rule ccorres_lhs_assoc)+ 479 apply (rule ccorres_split_nothrow_dc) 480 apply (simp add: bind_assoc) 481 apply (ctac add: scheduleChooseNewThread_ccorres) 482 apply (ctac(no_simp) add: ccorres_setSchedulerAction) 483 apply (wpsimp simp: cscheduler_action_relation_def 484 | vcg exspec=scheduleChooseNewThread_modifies exspec=tcbSchedEnqueue_modifies)+ 485 (* toplevel case: action is switch to candidate *) 486 apply (rename_tac candidate) 487 apply (rule_tac P="\<lambda>s. ksSchedulerAction s = SwitchToThread candidate \<and> invs' s" in ccorres_cross_over_guard) 488 apply (rule ccorres_cond_true_seq) 489 apply (rule ccorres_rhs_assoc)+ 490 apply csymbr 491 (* ct runnable? *) 492 apply (ctac add: isRunnable_ccorres, rename_tac runnable runnable') 493 apply (clarsimp simp: to_bool_def) 494 apply (rule ccorres_split_nothrow_dc) 495 (* enqueue if runnable *) 496 apply (simp add: when_def) 497 apply (rule ccorres_cond[where R=\<top>], clarsimp) 498 apply csymbr 499 apply (ctac add: tcbSchedEnqueue_ccorres) 500 apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV]) 501 apply (clarsimp, rule conseqPre, vcg) 502 apply (clarsimp simp: dc_def return_def) 503 apply (rule ccorres_cond_false_seq) 504 505 apply (rule_tac xf'=was_runnable_' in ccorres_abstract, ceqv) 506 apply (rename_tac was_runnable') 507 apply (rule_tac P="was_runnable' = runnable'" in ccorres_gen_asm2, clarsimp) 508 apply (rule ccorres_symb_exec_l3[OF _ git_wp _ empty_fail_getIdleThread], rename_tac it) 509 apply (rule ccorres_pre_threadGet, rename_tac targetPrio) 510 apply (rule ccorres_pre_threadGet, rename_tac curPrio) 511 apply (rule ccorres_rhs_assoc)+ 512 apply (rule_tac xf'=candidate_' and val="tcb_ptr_to_ctcb_ptr candidate" 513 and R="\<lambda>s. ksSchedulerAction s = SwitchToThread candidate" and R'=UNIV 514 in ccorres_symb_exec_r_known_rv) 515 apply (rule conseqPre, vcg, clarsimp) 516 apply (fastforce dest!: rf_sr_cscheduler_relation simp: cscheduler_action_relation_def) 517 apply ceqv 518 (* split off fastfail calculation *) 519 apply (rule ccorres_rhs_assoc2) 520 apply (rule ccorres_rhs_assoc2) 521 apply (rule_tac r'="\<lambda>rv rv'. rv = to_bool rv'" and xf'=fastfail_' in ccorres_split_nothrow) 522 apply (clarsimp simp: scheduleSwitchThreadFastfail_def dc_simp) 523 apply (rule ccorres_cond_seq2[THEN iffD1]) 524 apply (rule_tac xf'=ret__int_' and val="from_bool (curThread = it)" 525 and R="\<lambda>s. it = ksIdleThread s \<and> curThread = ksCurThread s" and R'=UNIV 526 in ccorres_symb_exec_r_known_rv) 527 apply (rule conseqPre, vcg, fastforce simp: rf_sr_ksCurThread rf_sr_ksIdleThread) 528 apply ceqv 529 apply clarsimp 530 apply (rule ccorres_cond2'[where R=\<top>], fastforce) 531 apply clarsimp 532 apply (rule ccorres_return[where R'=UNIV], clarsimp, vcg) 533 apply (rule_tac P="\<lambda>s. obj_at' (\<lambda>tcb. tcbPriority tcb = curPrio) curThread s 534 \<and> curThread = ksCurThread s 535 \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = targetPrio) candidate s" 536 and P'=UNIV in ccorres_from_vcg) 537 apply clarsimp 538 apply (rule conseqPre, vcg) 539 apply (clarsimp simp: return_def cur_tcb'_def rf_sr_ksCurThread) 540 apply (drule (1) obj_at_cslift_tcb)+ 541 apply (clarsimp simp: typ_heap_simps ctcb_relation_def to_bool_def split: if_split) 542 apply unat_arith 543 apply (wpsimp wp: threadGet_obj_at2) 544 apply vcg 545 apply ceqv 546 (* fastfail calculation complete *) 547 apply (rename_tac fastfail fastfail') 548 apply (rule ccorres_pre_curDomain) 549 (* rest of the calculation: fastfail \<and> \<not> highest *) 550 apply (rule ccorres_rhs_assoc2) 551 apply (rule_tac r'="\<lambda>hprio rv'. to_bool rv' = (fastfail \<and> \<not>hprio)" and xf'=ret__int_' 552 in ccorres_split_nothrow) 553 apply (csymbr) 554 apply (clarsimp simp: to_bool_def) 555 apply (rule ccorres_Cond_rhs ; clarsimp) 556 apply (rule ccorres_move_c_guard_tcb) 557 apply (rule ccorres_add_return2) 558 apply (ctac add: isHighestPrio_ccorres, clarsimp) 559 apply (clarsimp simp: to_bool_def) 560 apply (rule ccorres_inst[where P=\<top> and P'=UNIV]) 561 apply (rule ccorres_return) 562 apply (rule conseqPre, vcg) 563 apply clarsimp 564 apply (rule wp_post_taut) 565 apply (vcg exspec=isHighestPrio_modifies) 566 apply (rule_tac P=\<top> and P'="{s. ret__int_' s = 0}" in ccorres_from_vcg) 567 apply clarsimp 568 apply (rule conseqPre, vcg) 569 apply (fastforce simp: isHighestPrio_def' gets_def return_def get_def 570 NonDetMonad.bind_def 571 split: prod.split) 572 apply ceqv 573 apply (clarsimp simp: to_bool_def) 574 (* done with calculation of main acceptance criterion for candidate *) 575 apply (rule ccorres_cond_seq) 576 apply (rule ccorres_cond[where R=\<top>], blast) 577 (* candidate is not the best one, enqueue and choose new thread *) 578 apply (rule ccorres_rhs_assoc)+ 579 apply (ctac add: tcbSchedEnqueue_ccorres) 580 apply clarsimp 581 apply (ctac(no_simp) add: ccorres_setSchedulerAction) 582 apply (clarsimp simp: cscheduler_action_relation_def) 583 (* isolate haskell part before setting thread action *) 584 apply (simp add: scheduleChooseNewThread_def) 585 apply (rule ccorres_lhs_assoc)+ 586 apply (rule ccorres_split_nothrow_dc) 587 apply (simp add: bind_assoc) 588 apply (ctac add: scheduleChooseNewThread_ccorres) 589 apply (ctac(no_simp) add: ccorres_setSchedulerAction) 590 apply (wpsimp simp: cscheduler_action_relation_def)+ 591 apply (vcg exspec=scheduleChooseNewThread_modifies) 592 apply (wp add: setSchedulerAction_invs' setSchedulerAction_direct del: ssa_wp) 593 apply (clarsimp | vcg exspec=tcbSchedEnqueue_modifies | wp wp_post_taut)+ 594 (* secondary check, when on equal prio and ct was running, prefer ct *) 595 apply (rule ccorres_rhs_assoc) 596 apply (rule_tac xf'=ret__int_' and val="from_bool (runnable' \<noteq> 0 \<and> curPrio = targetPrio)" 597 and R="\<lambda>s. curThread = ksCurThread s 598 \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = curPrio) (ksCurThread s) s 599 \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = targetPrio) candidate s" 600 and R'=UNIV 601 in ccorres_symb_exec_r_known_rv) 602 apply clarsimp 603 apply (rule conseqPre, vcg) 604 apply (clarsimp simp: false_def cur_tcb'_def rf_sr_ksCurThread) 605 606 apply (drule (1) obj_at_cslift_tcb)+ 607 apply (clarsimp simp: typ_heap_simps ctcb_relation_def to_bool_def split: if_split) 608 apply (solves unat_arith) 609 apply ceqv 610 apply clarsimp 611 apply (rule ccorres_cond_seq) 612 apply (rule ccorres_cond[where R=\<top>], blast) 613 (* candidate does not beat running ct, append and choose new thread *) 614 apply (rule ccorres_rhs_assoc)+ 615 apply (ctac add: tcbSchedAppend_ccorres) 616 apply clarsimp 617 apply (ctac(no_simp) add: ccorres_setSchedulerAction) 618 apply (clarsimp simp: cscheduler_action_relation_def) 619 (* isolate haskell part before setting thread action *) 620 apply (simp add: scheduleChooseNewThread_def) 621 apply (rule ccorres_lhs_assoc)+ 622 apply (rule ccorres_split_nothrow_dc) 623 apply (simp add: bind_assoc) 624 apply (ctac add: scheduleChooseNewThread_ccorres) 625 apply (ctac(no_simp) add: ccorres_setSchedulerAction) 626 apply (wpsimp simp: cscheduler_action_relation_def)+ 627 apply (vcg exspec=scheduleChooseNewThread_modifies) 628 apply (wp add: setSchedulerAction_invs' setSchedulerAction_direct del: ssa_wp) 629 apply (clarsimp | vcg exspec=tcbSchedEnqueue_modifies | wp wp_post_taut)+ 630 (* candidate is best, switch to it *) 631 apply (ctac add: switchToThread_ccorres) 632 apply clarsimp 633 apply (ctac(no_simp) add: ccorres_setSchedulerAction) 634 apply (clarsimp simp: cscheduler_action_relation_def) 635 apply (wpsimp wp: wp_post_taut) 636 apply (vcg exspec=switchToThread_modifies) 637 apply clarsimp 638 apply vcg 639 apply clarsimp 640 apply (strengthen invs'_invs_no_cicd') 641 apply (wp | wp_once hoare_drop_imp)+ 642 apply clarsimp 643 apply (vcg exspec=isHighestPrio_modifies) 644 apply clarsimp 645 apply (wp_once hoare_drop_imps) 646 apply wp 647 apply (strengthen strenghten_False_imp[where P="a = ResumeCurrentThread" for a]) 648 apply (clarsimp simp: conj_ac invs_queues invs_valid_objs' cong: conj_cong) 649 apply wp 650 apply (clarsimp, vcg exspec=tcbSchedEnqueue_modifies) 651 apply (clarsimp, vcg exspec=tcbSchedEnqueue_modifies) 652 apply (clarsimp simp: to_bool_def true_def) 653 apply (strengthen ko_at'_obj_at'_field) 654 apply (clarsimp cong: imp_cong simp: ko_at'_obj_at'_field to_bool_def true_def) 655 apply wp 656 apply clarsimp 657 (* when runnable tcbSchedEnqueue curThread *) 658 apply (rule_tac Q="\<lambda>rv s. invs' s \<and> ksCurThread s = curThread 659 \<and> ksSchedulerAction s = SwitchToThread candidate" in hoare_post_imp) 660 apply (clarsimp simp: invs'_bitmapQ_no_L1_orphans invs_ksCurDomain_maxDomain') 661 apply (fastforce dest: invs_sch_act_wf') 662 663 apply (wp | clarsimp simp: dc_def)+ 664 apply (vcg exspec=tcbSchedEnqueue_modifies) 665 apply wp 666 apply (clarsimp simp: to_bool_def false_def) 667 apply vcg 668 669 apply (clarsimp simp: tcb_at_invs' rf_sr_ksCurThread if_apply_def2 invs_queues invs_valid_objs' 670 dc_def)+ 671 apply (frule invs_sch_act_wf') 672 apply (frule tcb_at_invs') 673 apply (rule conjI) 674 apply (clarsimp dest!: rf_sr_cscheduler_relation simp: cscheduler_action_relation_def) 675 apply (rule conjI; clarsimp) 676 apply (frule (1) obj_at_cslift_tcb) 677 apply (clarsimp simp: cscheduler_action_relation_def typ_heap_simps max_word_not_0 678 split: scheduler_action.splits) 679 apply (frule (1) obj_at_cslift_tcb) 680 apply (clarsimp dest!: rf_sr_cscheduler_relation invs_sch_act_wf' 681 simp: cscheduler_action_relation_def) 682 apply (intro conjI impI allI; clarsimp simp: typ_heap_simps ctcb_relation_def to_bool_def) 683 apply (fastforce simp: tcb_at_not_NULL tcb_at_1 dest: pred_tcb_at')+ 684 done 685 686(* FIXME: move *) 687lemma map_to_tcbs_upd: 688 "map_to_tcbs (ksPSpace s(t \<mapsto> KOTCB tcb')) = map_to_tcbs (ksPSpace s)(t \<mapsto> tcb')" 689 apply (rule ext) 690 apply (clarsimp simp: map_comp_def projectKOs split: option.splits if_splits) 691 done 692 693(* FIXME: move *) 694lemma cep_relations_drop_fun_upd: 695 "\<lbrakk> f x = Some v; tcbEPNext_C v' = tcbEPNext_C v; tcbEPPrev_C v' = tcbEPPrev_C v \<rbrakk> 696 \<Longrightarrow> cendpoint_relation (f (x \<mapsto> v')) = cendpoint_relation f" 697 "\<lbrakk> f x = Some v; tcbEPNext_C v' = tcbEPNext_C v; tcbEPPrev_C v' = tcbEPPrev_C v \<rbrakk> 698 \<Longrightarrow> cnotification_relation (f (x \<mapsto> v')) = cnotification_relation f" 699 by (intro ext cendpoint_relation_upd_tcb_no_queues[where thread=x] 700 cnotification_relation_upd_tcb_no_queues[where thread=x] 701 | simp split: if_split)+ 702 703lemma threadSet_timeSlice_ccorres [corres]: 704 "ccorres dc xfdc (tcb_at' thread) {s. thread' s = tcb_ptr_to_ctcb_ptr thread \<and> unat (v' s) = v} hs 705 (threadSet (tcbTimeSlice_update (\<lambda>_. v)) thread) 706 (Basic (\<lambda>s. globals_update (t_hrs_'_update (hrs_mem_update (heap_update (Ptr &(thread' s\<rightarrow>[''tcbTimeSlice_C''])::machine_word ptr) (v' s)))) s))" 707 apply (rule ccorres_guard_imp2) 708 apply (rule threadSet_ccorres_lemma4 [where P=\<top> and P'=\<top>]) 709 apply vcg 710 prefer 2 711 apply (rule conjI, simp) 712 apply assumption 713 apply clarsimp 714 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 715 apply (clarsimp simp: cmachine_state_relation_def carch_state_relation_def cpspace_relation_def 716 fpu_null_state_heap_update_tag_disj_simps) 717 apply (clarsimp simp: update_tcb_map_tos typ_heap_simps') 718 apply (simp add: map_to_ctes_upd_tcb_no_ctes tcb_cte_cases_def 719 map_to_tcbs_upd) 720 apply (simp add: cep_relations_drop_fun_upd cvariable_relation_upd_const 721 ko_at_projectKO_opt) 722 apply (rule conjI) 723 defer 724 apply (erule cready_queues_relation_not_queue_ptrs) 725 apply (rule ext, simp split: if_split) 726 apply (rule ext, simp split: if_split) 727 apply (drule ko_at_projectKO_opt) 728 apply (erule (2) cmap_relation_upd_relI) 729 apply (simp add: ctcb_relation_def) 730 apply assumption 731 apply simp 732 done 733 734lemma timerTick_ccorres: 735 "ccorres dc xfdc invs' UNIV [] timerTick (Call timerTick_'proc)" 736 apply (cinit) 737 apply (rule ccorres_pre_getCurThread) 738 apply (ctac add: get_tsType_ccorres2 [where f="\<lambda>s. ksCurThread_' (globals s)"]) 739 apply (rule ccorres_split_nothrow_novcg) 740 apply wpc 741 apply (simp add: "StrictC'_thread_state_defs", rule ccorres_cond_false, rule ccorres_return_Skip[unfolded dc_def])+ 742 (* thread_state.Running *) 743 apply simp 744 apply (rule ccorres_cond_true) 745 apply (rule ccorres_pre_threadGet) 746 apply (rule_tac P="cur_tcb'" and P'=\<top> in ccorres_move_c_guards(8)) 747 apply (clarsimp simp: cur_tcb'_def) 748 apply (drule (1) tcb_at_h_t_valid) 749 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 750 apply (rule_tac Q="\<lambda>s. obj_at' (\<lambda>tcb. tcbTimeSlice tcb = rva) (ksCurThread s) s" 751 and Q'=\<top> in ccorres_cond_both') 752 apply clarsimp 753 apply (drule (1) obj_at_cslift_tcb) 754 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 755 apply (clarsimp simp: typ_heap_simps) 756 apply (clarsimp simp: ctcb_relation_def word_less_nat_alt) 757 apply (rule_tac P="cur_tcb'" and P'=\<top> in ccorres_move_c_guards(8)) 758 apply (clarsimp simp: cur_tcb'_def) 759 apply (fastforce simp: rf_sr_def cstate_relation_def Let_def typ_heap_simps dest: tcb_at_h_t_valid) 760 apply (rule_tac P="cur_tcb'" and P'=\<top> in ccorres_move_c_guards(8)) 761 apply (clarsimp simp: cur_tcb'_def) 762 apply (fastforce simp: rf_sr_def cstate_relation_def Let_def typ_heap_simps dest: tcb_at_h_t_valid) 763 apply (ctac add: threadSet_timeSlice_ccorres[unfolded dc_def]) 764 apply (rule ccorres_rhs_assoc)+ 765 apply (ctac) 766 apply simp 767 apply (ctac (no_vcg) add: tcbSchedAppend_ccorres) 768 apply (ctac add: rescheduleRequired_ccorres[unfolded dc_def]) 769 apply (wp weak_sch_act_wf_lift_linear threadSet_valid_queues 770 threadSet_pred_tcb_at_state tcbSchedAppend_valid_objs' threadSet_valid_objs' threadSet_tcbDomain_triv 771 | clarsimp simp: st_tcb_at'_def o_def split: if_splits)+ 772 apply (vcg exspec=tcbSchedDequeue_modifies) 773 apply (simp add: "StrictC'_thread_state_defs", rule ccorres_cond_false, rule ccorres_return_Skip[unfolded dc_def])+ 774 apply ceqv 775 apply (simp add: when_def numDomains_def decDomainTime_def) 776 apply (rule ccorres_split_nothrow_novcg) 777 apply (rule_tac rrel=dc and xf=xfdc and P=\<top> and P'=UNIV in ccorres_from_vcg) 778 apply (rule allI, rule conseqPre, vcg) 779 apply (clarsimp simp: simpler_modify_def) 780 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 781 carch_state_relation_def cmachine_state_relation_def) 782 apply ceqv 783 apply (rule ccorres_pre_getDomainTime) 784 apply (rename_tac rva rv'a rvb) 785 apply (rule_tac P'="{s. ksDomainTime_' (globals s) = rvb}" in ccorres_inst, simp) 786 apply (case_tac "rvb = 0") 787 apply clarsimp 788 apply (rule ccorres_guard_imp2) 789 apply (rule ccorres_cond_true) 790 apply (ctac add: rescheduleRequired_ccorres[unfolded dc_def]) 791 apply clarsimp 792 apply assumption 793 apply clarsimp 794 apply (rule ccorres_guard_imp2) 795 apply (rule ccorres_cond_false) 796 apply (rule ccorres_return_Skip[unfolded dc_def]) 797 apply clarsimp 798 apply wp 799 apply (clarsimp simp: guard_is_UNIV_def) 800 apply (wp hoare_vcg_conj_lift hoare_vcg_all_lift hoare_drop_imps) 801 apply (wpc | wp threadSet_weak_sch_act_wf threadSet_valid_objs' rescheduleRequired_weak_sch_act_wf 802 tcbSchedAppend_valid_objs' weak_sch_act_wf_lift_linear threadSet_st_tcb_at2 threadGet_wp 803 | simp split del: if_splits)+ 804 apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem word_sle_def word_sless_def) 805 apply (wp gts_wp') 806 apply vcg 807 apply (clarsimp simp: invs_weak_sch_act_wf) 808 apply (fold cur_tcb'_def) 809 apply (rule conjI, clarsimp) 810 apply (rule conjI, clarsimp) 811 apply (rule conjI) 812 apply (clarsimp simp: invs'_def valid_state'_def) 813 apply (auto simp: obj_at'_def inQ_def weak_sch_act_wf_def st_tcb_at'_def 814 valid_pspace'_def ct_idle_or_in_cur_domain'_def valid_tcb'_def valid_idle'_def projectKOs)[1] 815 apply (rule conjI, clarsimp simp: invs'_def valid_state'_def valid_tcb'_def)+ 816 apply (auto simp: obj_at'_def inQ_def weak_sch_act_wf_def st_tcb_at'_def 817 valid_pspace'_def ct_idle_or_in_cur_domain'_def valid_tcb'_def valid_idle'_def projectKOs)[1] 818 apply (auto simp: invs'_def valid_state'_def valid_tcb'_def tcb_cte_cases_def)[1] 819 820 apply (frule invs_cur') 821 apply (clarsimp simp: cur_tcb'_def) 822 apply (drule (1) obj_at_cslift_tcb) 823 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def typ_heap_simps' timeSlice_def) 824 apply (subst unat_sub) 825 apply simp 826 apply (clarsimp simp: ctcb_relation_def) 827 done 828 829end 830 831end 832