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 TcbQueue_C 12imports SR_lemmas_C 13begin 14 15context kernel 16begin 17 18lemma tcb_queueD: 19 assumes queue_rel: "tcb_queue_relation getNext getPrev mp queue qprev qhead" 20 and valid_ntfn: "distinct queue" 21 and in_queue: "tcbp \<in> set queue" 22 and cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 23 shows "(if tcbp = hd queue then getPrev tcb = qprev 24 else (\<exists>n < (length queue) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) 25 \<and> tcbp = queue ! Suc n)) 26 \<and> (if tcbp = last queue then getNext tcb = NULL 27 else (\<exists>n < (length queue) - 1. tcbp = queue ! n 28 \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)))" 29 (is "?prev tcb queue qprev \<and> ?next tcb queue") 30 using queue_rel in_queue valid_ntfn 31proof (induct queue arbitrary: qprev qhead) 32 case Nil 33 thus ?case by simp 34next 35 case (Cons tcb' tcbs qprev' qhead') 36 have "tcbp = tcb' \<or> tcbp \<in> set tcbs" using Cons.prems by simp 37 thus ?case 38 proof 39 assume tcbp: "tcbp = tcb'" 40 hence "?prev tcb (tcb' # tcbs) qprev'" 41 using Cons.prems cs_tcb by clarsimp 42 moreover 43 have "?next tcb (tcb' # tcbs)" 44 proof (cases "tcbs = []") 45 case True 46 thus ?thesis using tcbp Cons.prems cs_tcb by clarsimp 47 next 48 case False 49 hence "tcbp \<noteq> last tcbs" using tcbp Cons.prems by clarsimp 50 thus ?thesis using False tcbp Cons.prems cs_tcb 51 apply clarsimp 52 apply (rule exI [where x = 0]) 53 apply simp 54 apply (cases tcbs) 55 apply simp_all 56 done 57 qed 58 ultimately show ?thesis .. 59 next 60 assume tcbp: "tcbp \<in> set tcbs" 61 obtain tcb2 where cs_tcb2: "mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2" 62 and rel2: "tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcb2)" 63 using Cons.prems 64 by clarsimp 65 66 have ih: "?prev tcb tcbs (tcb_ptr_to_ctcb_ptr tcb') \<and> ?next tcb tcbs" 67 proof (rule Cons.hyps) 68 from Cons.prems show (* "\<forall>t\<in>set tcbs. tcb_at' t s" 69 and *) "distinct tcbs" by simp_all 70 qed fact+ 71 72 from tcbp Cons.prems have tcbp_not_tcb': "tcbp \<noteq> tcb'" by clarsimp 73 from tcbp have tcbsnz: "tcbs \<noteq> []" by clarsimp 74 hence hd_tcbs: "hd tcbs = tcbs ! 0" by (simp add: hd_conv_nth) 75 76 show ?case 77 proof (rule conjI) 78 show "?prev tcb (tcb' # tcbs) qprev'" 79 using ih [THEN conjunct1] tcbp_not_tcb' hd_tcbs tcbsnz 80 apply (clarsimp split: if_split_asm) 81 apply fastforce 82 apply (rule_tac x = "Suc n" in exI) 83 apply simp 84 done 85 next 86 show "?next tcb (tcb' # tcbs)" 87 using ih [THEN conjunct2] tcbp_not_tcb' hd_tcbs tcbsnz 88 apply (clarsimp split: if_split_asm) 89 apply (rule_tac x = "Suc n" in exI) 90 apply simp 91 done 92 qed 93 qed 94qed 95 96lemma tcb_queue_memberD: 97 assumes queue_rel: "tcb_queue_relation getNext getPrev (cslift s') queue qprev qhead" 98 and in_queue: "tcbp \<in> set queue" 99 and valid_ntfn: "\<forall>t\<in>set queue. tcb_at' t s" 100 and rf_sr: "(s, s') \<in> rf_sr" 101 shows "\<exists>tcb. cslift s' (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 102 using assms 103 apply - 104 apply (drule (1) bspec) 105 apply (drule (1) tcb_at_h_t_valid) 106 apply (clarsimp simp add: h_t_valid_clift_Some_iff) 107 done 108 109lemma tcb_queue_valid_ptrsD: 110 assumes in_queue: "tcbp \<in> set queue" 111 and rf_sr: "(s, s') \<in> rf_sr" 112 and valid_ntfn: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 113 and queue_rel: "tcb_queue_relation getNext getPrev (cslift s') queue NULL qhead" 114 shows "\<exists>tcb. cslift s' (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb 115 \<and> (getPrev tcb \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c (getPrev tcb) 116 \<and> getPrev tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue) 117 \<and> (getNext tcb \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c (getNext tcb) 118 \<and> getNext tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue)" 119 using assms 120 apply - 121 apply (frule (3) tcb_queue_memberD) 122 apply (elim exE) 123 apply (frule (3) tcb_queueD) 124 apply (auto intro!: tcb_at_h_t_valid elim!: bspec split: if_split_asm) 125 done 126 127lemma tcb_queue_relation_restrict0: 128 "set queue \<subseteq> S \<Longrightarrow> tcb_queue_relation getNext getPrev mp queue qprev qhead = 129 tcb_queue_relation getNext getPrev (restrict_map mp (tcb_ptr_to_ctcb_ptr ` S)) queue qprev qhead" 130proof (induct queue arbitrary: S qprev qhead) 131 case Nil thus ?case by simp 132next 133 case (Cons tcb tcbs S' qprev' qhead') 134 thus ?case 135 using Cons by auto 136qed 137 138lemma tcb_queue_relation_restrict: 139 "tcb_queue_relation getNext getPrev mp queue qprev qhead = 140 tcb_queue_relation getNext getPrev (restrict_map mp (tcb_ptr_to_ctcb_ptr ` set queue)) queue qprev qhead" 141 apply (rule tcb_queue_relation_restrict0) 142 apply simp 143 done 144 145lemma tcb_queue_relation_only_next_prev: 146 assumes mapeq: "option_map getNext \<circ> mp = option_map getNext \<circ> mp'" "option_map getPrev \<circ> mp = option_map getPrev \<circ> mp'" 147 shows "tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev mp' queue qprev qhead" 148proof (induct queue arbitrary: qprev qhead) 149 case Nil thus ?case by simp 150next 151 case (Cons tcb tcbs qprev' qhead') 152 thus ?case 153 apply clarsimp 154 apply (rule iffI) 155 apply clarsimp 156 apply (frule compD [OF mapeq(1)]) 157 apply clarsimp 158 apply (frule compD [OF mapeq(2)]) 159 apply clarsimp 160 apply clarsimp 161 apply (frule compD [OF mapeq(1) [symmetric]]) 162 apply clarsimp 163 apply (frule compD [OF mapeq(2) [symmetric]]) 164 apply clarsimp 165 done 166qed 167 168 169lemma tcb_queue_relation_cong: 170 assumes queuec: "queue = queue'" 171 and qpc: "qprev = qprev'" 172 and qhc: "qhead = qhead'" 173 and mpc: "\<And>p. p \<in> tcb_ptr_to_ctcb_ptr ` set queue' \<Longrightarrow> mp p = mp' p" 174 shows "tcb_queue_relation getNext getPrev mp queue qprev qhead = 175 tcb_queue_relation getNext getPrev mp' queue' qprev' qhead'" (is "?LHS = ?RHS") 176proof - 177 have "?LHS = tcb_queue_relation getNext getPrev (mp |` (tcb_ptr_to_ctcb_ptr ` set queue')) queue' qprev' qhead'" 178 by (simp add: queuec qpc qhc, subst tcb_queue_relation_restrict, rule refl) 179 180 also have "\<dots> = tcb_queue_relation getNext getPrev (mp' |` (tcb_ptr_to_ctcb_ptr ` set queue')) queue' qprev' qhead'" 181 by (simp add: mpc cong: restrict_map_cong) 182 183 also have "\<dots> = ?RHS" 184 by (simp add: tcb_queue_relation_restrict [symmetric]) 185 186 finally show ?thesis . 187qed 188 189lemma tcb_queue_relation'_cong: 190 assumes queuec: "queue = queue'" 191 and qhc: "qhead = qhead'" 192 and qpc: "qend = qend'" 193 and mpc: "\<And>p. p \<in> tcb_ptr_to_ctcb_ptr ` set queue' \<Longrightarrow> mp p = mp' p" 194 shows "tcb_queue_relation' getNext getPrev mp queue qhead qend = 195 tcb_queue_relation' getNext getPrev mp' queue' qhead' qend'" (is "?LHS = ?RHS") 196proof - 197 have "?LHS = tcb_queue_relation' getNext getPrev (mp |` (tcb_ptr_to_ctcb_ptr ` set queue')) queue' qhead' qend'" 198 by (clarsimp simp add: queuec qpc qhc tcb_queue_relation'_def , subst tcb_queue_relation_restrict, rule refl) 199 200 also have "\<dots> = tcb_queue_relation' getNext getPrev (mp' |` (tcb_ptr_to_ctcb_ptr ` set queue')) queue' qhead' qend'" 201 by (simp add: mpc cong: restrict_map_cong) 202 203 also have "\<dots> = ?RHS" 204 by (simp add: tcb_queue_relation'_def tcb_queue_relation_restrict [symmetric]) 205 206 finally show ?thesis . 207qed 208 209 210(* MOVE *) 211lemma tcb_aligned': 212 "tcb_at' t s \<Longrightarrow> is_aligned t tcbBlockSizeBits" 213 apply (drule obj_at_aligned') 214 apply (simp add: objBits_simps) 215 apply (simp add: objBits_simps) 216 done 217 218lemma tcb_at_not_NULL: 219 assumes tat: "tcb_at' t s" 220 shows "tcb_ptr_to_ctcb_ptr t \<noteq> NULL" 221proof 222 assume "tcb_ptr_to_ctcb_ptr t = NULL" 223 with tat have "tcb_at' (ctcb_ptr_to_tcb_ptr NULL) s" 224 apply - 225 apply (erule subst) 226 apply simp 227 done 228 229 hence "is_aligned (ctcb_ptr_to_tcb_ptr NULL) tcbBlockSizeBits" 230 by (rule tcb_aligned') 231 232 moreover have "ctcb_ptr_to_tcb_ptr NULL !! ctcb_size_bits" 233 unfolding ctcb_ptr_to_tcb_ptr_def ctcb_offset_defs 234 by simp 235 ultimately show False by (simp add: is_aligned_nth ctcb_offset_defs objBits_defs) 236qed 237 238lemma tcb_queue_relation_not_NULL: 239 assumes tq: "tcb_queue_relation getNext getPrev mp queue qprev qhead" 240 and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" 241 shows "\<forall>t \<in> set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL" 242proof (cases "queue = []") 243 case True thus ?thesis by simp 244next 245 case False 246 show ?thesis 247 proof (rule ballI, rule notI) 248 fix t 249 assume tq: "t \<in> set queue" and "tcb_ptr_to_ctcb_ptr t = NULL" 250 hence "ctcb_ptr_to_tcb_ptr NULL \<in> set queue" 251 apply - 252 apply (erule subst) 253 apply simp 254 done 255 256 with valid_ep(1) have "tcb_at' (ctcb_ptr_to_tcb_ptr NULL) s" .. 257 thus False 258 apply - 259 apply (drule tcb_at_not_NULL) 260 apply simp 261 done 262 qed 263qed 264 265lemmas tcb_queue_relation_not_NULL' = bspec [OF tcb_queue_relation_not_NULL] 266 267lemma tcb_queue_relation_head_hd: 268 assumes tq: "tcb_queue_relation getNext getPrev mp queue qprev qhead" 269 and tcbs: "queue \<noteq> []" 270 shows "ctcb_ptr_to_tcb_ptr qhead = hd queue" 271 using assms 272 apply (cases queue) 273 apply simp 274 apply simp 275 done 276 277lemma tcb_queue_relation_next_not_NULL: 278 assumes tq: "tcb_queue_relation getNext getPrev mp queue qprev qhead" 279 and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 280 and tcbs: "queue \<noteq> []" 281 shows "qhead \<noteq> NULL" 282proof - 283 have "ctcb_ptr_to_tcb_ptr qhead \<in> set queue" using tq tcbs 284 by (simp add: tcb_queue_relation_head_hd) 285 286 with tq valid_ep(1) have "tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr qhead) \<noteq> NULL" 287 by (rule tcb_queue_relation_not_NULL') 288 289 thus ?thesis by simp 290qed 291 292lemma tcb_queue_relation_ptr_rel: 293 assumes tq: "tcb_queue_relation getNext getPrev mp queue qprev qhead" 294 and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 295 and cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 296 and prev_not_queue: "ctcb_ptr_to_tcb_ptr qprev \<notin> set queue" 297 and in_queue: "tcbp \<in> set queue" 298 shows "tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb 299 \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb)" 300 using tq valid_ep in_queue cs_tcb prev_not_queue 301 apply - 302 apply (frule (3) tcb_queueD) 303 apply (frule (2) tcb_queue_relation_not_NULL') 304 apply (simp split: if_split_asm) 305 apply (rule not_sym) 306 apply (rule notI) 307 apply simp 308 apply (clarsimp simp: inj_eq distinct_conv_nth) 309 apply (intro conjI impI) 310 apply (clarsimp simp: inj_eq distinct_conv_nth) 311 apply (rule not_sym) 312 apply clarsimp 313 apply clarsimp 314 apply (clarsimp simp: inj_eq) 315 apply (intro conjI impI) 316 apply (clarsimp simp: distinct_conv_nth) 317 apply (erule_tac s = "queue ! Suc n" in subst) 318 apply (clarsimp simp: distinct_conv_nth) 319 apply clarsimp 320 apply (case_tac "na = Suc n") 321 apply hypsubst 322 apply (clarsimp simp: distinct_conv_nth) 323 apply (clarsimp simp: distinct_conv_nth) 324 done 325 326lemma distinct_cons_nth: 327 assumes dxs: "distinct xs" 328 and ln: "n < length xs" 329 and x: "x \<notin> set xs" 330 shows "(x # xs) ! n \<noteq> xs ! n" 331proof 332 assume n: "(x # xs) ! n = xs ! n" 333 have ln': "n < length (x # xs)" using ln by simp 334 have sln: "Suc n < length (x # xs)" using ln by simp 335 336 from n have "(x # xs) ! n = (x # xs) ! Suc n" by simp 337 moreover have "distinct (x # xs)" using dxs x by simp 338 ultimately show False 339 unfolding distinct_conv_nth 340 apply - 341 apply (drule spec, drule mp [OF _ ln']) 342 apply (drule spec, drule mp [OF _ sln]) 343 apply simp 344 done 345qed 346 347lemma distinct_nth: 348 assumes dist: "distinct xs" 349 and ln: "n < length xs" 350 and lm: "m < length xs" 351 shows "(xs ! n = xs ! m) = (n = m)" 352 using dist ln lm 353 apply (cases "n = m") 354 apply simp 355 apply (clarsimp simp: distinct_conv_nth) 356 done 357 358lemma distinct_nth_cons: 359 assumes dist: "distinct xs" 360 and xxs: "x \<notin> set xs" 361 and ln: "n < length xs" 362 and lm: "m < length xs" 363 shows "((x # xs) ! n = xs ! m) = (n = Suc m)" 364proof (cases "n = Suc m") 365 case True 366 thus ?thesis by simp 367next 368 case False 369 370 have ln': "n < length (x # xs)" using ln by simp 371 have lm': "Suc m < length (x # xs)" using lm by simp 372 373 have "distinct (x # xs)" using dist xxs by simp 374 thus ?thesis using False 375 unfolding distinct_conv_nth 376 apply - 377 apply (drule spec, drule mp [OF _ ln']) 378 apply (drule spec, drule mp [OF _ lm']) 379 apply clarsimp 380 done 381qed 382 383lemma distinct_nth_cons': 384 assumes dist: "distinct xs" 385 and xxs: "x \<notin> set xs" 386 and ln: "n < length xs" 387 and lm: "m < length xs" 388 shows "(xs ! n = (x # xs) ! m) = (m = Suc n)" 389proof (cases "m = Suc n") 390 case True 391 thus ?thesis by simp 392next 393 case False 394 395 have ln': "Suc n < length (x # xs)" using ln by simp 396 have lm': "m < length (x # xs)" using lm by simp 397 398 have "distinct (x # xs)" using dist xxs by simp 399 thus ?thesis using False 400 unfolding distinct_conv_nth 401 apply - 402 apply (drule spec, drule mp [OF _ ln']) 403 apply (drule spec, drule mp [OF _ lm']) 404 apply clarsimp 405 done 406qed 407 408lemma nth_first_not_member: 409 assumes xxs: "x \<notin> set xs" 410 and ln: "n < length xs" 411 shows "((x # xs) ! n = x) = (n = 0)" 412 using xxs ln 413 apply (cases n) 414 apply simp 415 apply clarsimp 416 done 417 418lemma tcb_queue_next_prev: 419 assumes qr: "tcb_queue_relation getNext getPrev mp queue qprev qhead" 420 and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 421 and tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 422 and tcb': "mp (tcb_ptr_to_ctcb_ptr tcbp') = Some tcb'" 423 and tq: "tcbp \<in> set queue" "tcbp' \<in> set queue" 424 and prev_not_queue: "ctcb_ptr_to_tcb_ptr qprev \<notin> set queue" 425 and tcbs: "tcbp \<noteq> tcbp'" 426 shows "(getNext tcb = tcb_ptr_to_ctcb_ptr tcbp') = 427 (getPrev tcb' = tcb_ptr_to_ctcb_ptr tcbp)" 428 using qr valid_ep prev_not_queue tq tcb tcb' tcbs 429 apply - 430 apply (frule (1) tcb_queueD) 431 apply (rule tq(1)) 432 apply (rule tcb) 433 apply (frule (1) tcb_queueD) 434 apply (rule tq(2)) 435 apply (rule tcb') 436 apply (cases queue) 437 apply simp 438 apply (cut_tac bspec [OF tcb_queue_relation_not_NULL, OF qr valid_ep(1) tq(1)]) 439 apply (cut_tac bspec [OF tcb_queue_relation_not_NULL, OF qr valid_ep(1) tq(2)]) 440 apply (simp add: inj_eq split: if_split_asm) 441 apply clarsimp 442 apply clarsimp 443 subgoal by (clarsimp simp: last_conv_nth distinct_nth distinct_nth_cons) 444 apply (clarsimp simp: last_conv_nth distinct_nth distinct_nth_cons) 445 apply (subgoal_tac "list ! Suc na \<noteq> tcbp'") 446 apply clarsimp 447 apply clarsimp 448 subgoal by (clarsimp simp: last_conv_nth distinct_nth distinct_nth_cons nth_first_not_member) 449 subgoal by (fastforce simp: last_conv_nth distinct_nth distinct_nth_cons nth_first_not_member) 450 subgoal by (clarsimp simp: last_conv_nth distinct_nth distinct_nth_cons distinct_nth_cons' nth_first_not_member) 451 by (fastforce simp: last_conv_nth distinct_nth distinct_nth_cons distinct_nth_cons' nth_first_not_member) 452 453 454lemma null_not_in: 455 "\<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue\<rbrakk> 456 \<Longrightarrow> ctcb_ptr_to_tcb_ptr NULL \<notin> set queue" 457 apply - 458 apply (rule notI) 459 apply (drule (2) tcb_queue_relation_not_NULL') 460 apply simp 461 done 462 463lemma tcb_queue_relationI': 464 "\<lbrakk> tcb_queue_relation getNext getPrev hp queue NULL qhead; 465 qend = (if queue = [] then NULL else (tcb_ptr_to_ctcb_ptr (last queue))) \<rbrakk> 466 \<Longrightarrow> tcb_queue_relation' getNext getPrev hp queue qhead qend" 467 unfolding tcb_queue_relation'_def 468 by simp 469 470lemma tcb_queue_relationE': 471 "\<lbrakk> tcb_queue_relation' getNext getPrev hp queue qhead qend; 472 \<lbrakk> tcb_queue_relation getNext getPrev hp queue NULL qhead; 473 qend = (if queue = [] then NULL else (tcb_ptr_to_ctcb_ptr (last queue))) \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" 474 unfolding tcb_queue_relation'_def 475 by simp 476 477lemma tcb_queue_relation'_queue_rel: 478 "tcb_queue_relation' getNext getPrev hp queue qhead qend 479 \<Longrightarrow> tcb_queue_relation getNext getPrev hp queue NULL qhead" 480 unfolding tcb_queue_relation'_def 481 by simp 482 483lemma tcb_queue_singleton_iff: 484 assumes queue_rel: "tcb_queue_relation getNext getPrev mp queue NULL qhead" 485 and in_queue: "tcbp \<in> set queue" 486 and valid_ntfn: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 487 and cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 488 shows "(queue = [tcbp]) = (getNext tcb = NULL \<and> getPrev tcb = NULL)" 489proof (rule iffI) 490 assume "queue = [tcbp]" 491 thus "(getNext tcb = NULL \<and> getPrev tcb = NULL)" using queue_rel cs_tcb 492 by clarsimp 493next 494 assume asms: "getNext tcb = NULL \<and> getPrev tcb = NULL" 495 hence "hd queue = tcbp" using queue_rel valid_ntfn in_queue cs_tcb 496 apply - 497 apply (drule (3) tcb_queueD) 498 apply (rule classical) 499 apply clarsimp 500 apply (cut_tac x = "queue ! n" in bspec [OF tcb_queue_relation_not_NULL [OF queue_rel valid_ntfn(1)]]) 501 apply clarsimp 502 apply simp 503 done 504 moreover have "last queue = tcbp" using queue_rel valid_ntfn in_queue cs_tcb asms 505 apply - 506 apply (drule (3) tcb_queueD) 507 apply (rule classical) 508 apply clarsimp 509 apply (cut_tac x = "queue ! Suc n" in bspec [OF tcb_queue_relation_not_NULL [OF queue_rel valid_ntfn(1)]]) 510 apply clarsimp 511 apply simp 512 done 513 moreover have "queue \<noteq> []" using in_queue by clarsimp 514 ultimately show "queue = [tcbp]" using valid_ntfn in_queue 515 apply clarsimp 516 apply (simp add: hd_conv_nth last_conv_nth nth_eq_iff_index_eq) 517 apply (cases queue) 518 apply simp 519 apply simp 520 done 521qed 522 523 524lemma distinct_remove1_take_drop: 525 "\<lbrakk> distinct ls; n < length ls \<rbrakk> \<Longrightarrow> remove1 (ls ! n) ls = (take n ls) @ drop (Suc n) ls" 526proof (induct ls arbitrary: n) 527 case Nil thus ?case by simp 528next 529 case (Cons x xs n) 530 531 show ?case 532 proof (cases n) 533 case 0 534 thus ?thesis by simp 535 next 536 case (Suc m) 537 538 hence "((x # xs) ! n) \<noteq> x" using Cons.prems by clarsimp 539 thus ?thesis using Suc Cons.prems by (clarsimp simp add: Cons.hyps) 540 qed 541qed 542 543 544definition 545 "upd_unless_null \<equiv> \<lambda>p v f. if p = NULL then f else fun_upd f p (Some v)" 546 547lemma upd_unless_null_cong_helper: 548 "\<And>p p' v mp S. \<lbrakk> p' \<in> tcb_ptr_to_ctcb_ptr ` S; ctcb_ptr_to_tcb_ptr p \<notin> S \<rbrakk> \<Longrightarrow> (upd_unless_null p v mp) p' = mp p'" 549 unfolding upd_unless_null_def 550 apply simp 551 apply (intro impI conjI) 552 apply (erule imageE) 553 apply hypsubst 554 apply (simp only: ctcb_ptr_to_ctcb_ptr) 555 apply blast 556 done 557 558lemma tcbDequeue_update0: 559 assumes in_queue: "tcbp \<in> set queue" 560 and valid_ntfn: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 561 and queue_rel: "tcb_queue_relation tn tp mp queue qprev qhead" 562 and prev_not_queue: "ctcb_ptr_to_tcb_ptr qprev \<notin> set queue" 563 and cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 564 and f: "\<And>v f g. tn (tn_update f v) = f (tn v) \<and> tp (tp_update g v) = g (tp v) 565 \<and> tn (tp_update f v) = tn v \<and> tp (tn_update g v) = tp v" 566 shows "tcb_queue_relation tn tp 567 (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) 568 (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) 569 (remove1 tcbp queue) 570 (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else qprev) 571 (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead)" 572 (is "tcb_queue_relation tn tp ?mp (remove1 tcbp queue) (?qprev qprev qhead) (?qhead qhead)") 573 using queue_rel valid_ntfn prev_not_queue in_queue 574proof (induct queue arbitrary: qprev qhead) 575 case Nil 576 thus ?case by simp 577next 578 case (Cons tcb' tcbs qprev' qhead') 579 580 have "tcbp = tcb' \<or> tcbp \<in> set tcbs" using Cons.prems by simp 581 thus ?case 582 proof 583 assume tcbp: "tcbp = tcb'" 584 hence qp: "qprev' = tp tcb" and qh: "qhead' = tcb_ptr_to_ctcb_ptr tcb'" 585 using Cons.prems cs_tcb by auto 586 587 from Cons.prems have tq: "tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb)" 588 using Cons.prems cs_tcb tcbp by clarsimp 589 590 note ind_prems = Cons.prems 591 note ind_hyp = Cons.hyps 592 593 show ?thesis 594 proof (cases tcbs) 595 case Nil thus ?thesis using Cons.prems tcbp cs_tcb by clarsimp 596 next 597 case (Cons tcbs_hd tcbss) 598 599 have nnull: "tn tcb \<noteq> NULL" using tq 600 proof (rule tcb_queue_relation_next_not_NULL) 601 from ind_prems show "\<forall>t\<in>set tcbs. tcb_at' t s" 602 and "distinct tcbs" by simp_all 603 show "tcbs \<noteq> []" using Cons by simp 604 qed 605 606 from Cons ind_prems have "tcbs_hd \<notin> set tcbss" by simp 607 hence mpeq: "\<And>p. p \<in> tcb_ptr_to_ctcb_ptr ` set tcbss \<Longrightarrow> ?mp p = mp p" 608 using tq cs_tcb tcbp Cons nnull ind_prems 609 apply - 610 apply (subst upd_unless_null_cong_helper, assumption, clarsimp)+ 611 apply simp 612 done 613 614 have "tcb_ptr_to_ctcb_ptr tcbp \<noteq> tn tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> tp tcb 615 \<and> tn tcb \<noteq> tp tcb" using tq cs_tcb ind_prems nnull 616 apply - 617 apply (drule (5) tcb_queue_relation_ptr_rel) 618 apply clarsimp 619 done 620 621 hence "?mp (tcb_ptr_to_ctcb_ptr tcbs_hd) = Some (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb))))" 622 using qp qh tq cs_tcb tcbp Cons nnull 623 by (simp add: upd_unless_null_def) 624 625 thus ?thesis using qp qh tq cs_tcb tcbp Cons nnull 626 apply (simp (no_asm) add: tcbp Cons split del: if_split) 627 apply (subst tcb_queue_relation_cong [OF refl refl refl mpeq]) 628 apply assumption 629 apply (clarsimp simp: f) 630 done 631 qed 632 next 633 assume inset: "tcbp \<in> set tcbs" 634 hence tcbp: "tcbp \<noteq> tcb'" using Cons.prems by clarsimp 635 636 obtain tcb2 where cs_tcb2: "mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2" 637 and rel2: "tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb2)" 638 and qh: "qhead' = tcb_ptr_to_ctcb_ptr tcb'" 639 and qp: "qprev' = tp tcb2" 640 using Cons.prems 641 by clarsimp 642 643 have nnull: "tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL" using Cons.prems 644 apply - 645 apply (erule (1) tcb_queue_relation_not_NULL') 646 apply simp 647 done 648 649 have ih: "tcb_queue_relation tn tp ?mp (remove1 tcbp tcbs) 650 (?qprev (tcb_ptr_to_ctcb_ptr tcb') (tn tcb2)) 651 (?qhead (tn tcb2))" using rel2 652 proof (rule Cons.hyps) 653 from Cons.prems show "\<forall>t\<in>set tcbs. tcb_at' t s" 654 and "distinct tcbs" 655 and "ctcb_ptr_to_tcb_ptr (tcb_ptr_to_ctcb_ptr tcb') \<notin> set tcbs" by simp_all 656 qed fact 657 658 have tcb_next: "tn tcb \<noteq> tcb_ptr_to_ctcb_ptr tcb'" 659 using Cons.prems tcb_queue_next_prev[OF Cons.prems(1), OF _ _ cs_tcb cs_tcb2] 660 tcbp qp[symmetric] 661 by auto 662 663 show ?thesis using tcbp 664 proof (cases "tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp") 665 case True 666 hence tcb_prev: "tp tcb = tcb_ptr_to_ctcb_ptr tcb'" using Cons.prems cs_tcb2 cs_tcb not_sym [OF tcbp] 667 apply - 668 apply (subst tcb_queue_next_prev [symmetric], assumption+) 669 apply simp 670 apply simp 671 apply simp 672 apply (rule not_sym [OF tcbp]) 673 apply simp 674 done 675 676 hence "?mp (tcb_ptr_to_ctcb_ptr tcb') = Some (tn_update (\<lambda>_. tn tcb) tcb2)" 677 using tcb_next nnull cs_tcb2 unfolding upd_unless_null_def by simp 678 679 thus ?thesis using tcbp cs_tcb qh qp True ih tcb_prev 680 by (simp add: inj_eq f) 681 next 682 case False 683 hence tcb_prev: "tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcb'" 684 using Cons.prems cs_tcb2 cs_tcb not_sym [OF tcbp] 685 apply - 686 apply (subst tcb_queue_next_prev [symmetric], assumption+) 687 apply simp 688 apply simp 689 apply simp 690 apply (rule not_sym [OF tcbp]) 691 apply simp 692 done 693 hence "?mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2" 694 using tcb_next nnull cs_tcb2 unfolding upd_unless_null_def by simp 695 696 thus ?thesis using tcbp cs_tcb qh qp False ih tcb_prev 697 by (simp add: inj_eq) 698 qed 699 qed 700qed 701 702lemma tcbDequeue_update: 703 assumes queue_rel: "tcb_queue_relation' tn tp mp queue qhead qend" 704 and in_queue: "tcbp \<in> set queue" 705 and valid_ntfn: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 706 and cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 707 and f: "\<And>v f g. tn (tn_update f v) = f (tn v) \<and> tp (tp_update g v) = g (tp v) 708 \<and> tn (tp_update f v) = tn v \<and> tp (tn_update g v) = tp v" 709 shows "tcb_queue_relation' tn tp 710 (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) 711 (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) 712 (remove1 tcbp queue) 713 (if tp tcb = NULL then tn tcb else qhead) 714 (if tn tcb = NULL then tp tcb else qend)" 715proof - 716 have ne: "NULL = (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else NULL)" 717 using queue_rel in_queue cs_tcb 718 apply - 719 apply (drule tcb_queue_relation'_queue_rel) 720 apply (clarsimp split: if_split) 721 apply (cases queue) 722 apply simp 723 apply clarsimp 724 done 725 726 have if2: "(if tp tcb = NULL then tn tcb else qhead) = 727 (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead)" 728 using tcb_queue_relation'_queue_rel [OF queue_rel] in_queue cs_tcb valid_ntfn 729 apply - 730 apply (cases queue) 731 apply simp 732 apply (frule (3) tcb_queueD) 733 apply (simp add: inj_eq) 734 apply (intro impI) 735 apply simp 736 apply (elim conjE exE) 737 apply (cut_tac x = "queue ! n" 738 in bspec [OF tcb_queue_relation_not_NULL [OF tcb_queue_relation'_queue_rel [OF queue_rel] valid_ntfn(1)]]) 739 apply (rule nth_mem) 740 apply clarsimp 741 apply clarsimp 742 done 743 744 note null_not_in' = null_not_in [OF tcb_queue_relation'_queue_rel [OF queue_rel] valid_ntfn(1) valid_ntfn(2)] 745 746 show ?thesis 747 proof (rule tcb_queue_relationI') 748 show "tcb_queue_relation tn tp 749 (upd_unless_null (tn tcb) 750 (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) 751 (upd_unless_null (tp tcb) 752 (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) 753 (remove1 tcbp queue) NULL 754 (if tp tcb = NULL then tn tcb else qhead)" 755 using in_queue valid_ntfn tcb_queue_relation'_queue_rel [OF queue_rel] null_not_in' cs_tcb 756 by (subst ne, subst if2, rule tcbDequeue_update0[rotated -1, OF f]) 757 next 758 have r1: "(remove1 tcbp queue = []) = (tn tcb = NULL \<and> tp tcb = NULL)" 759 using in_queue tcb_queue_relation'_queue_rel [OF queue_rel] cs_tcb valid_ntfn null_not_in' 760 apply - 761 apply (subst tcb_queue_singleton_iff [symmetric], assumption+) 762 apply (fastforce simp: remove1_empty) 763 done 764 have "queue \<noteq> []" using in_queue by clarsimp 765 thus "(if tn tcb = NULL then tp tcb else qend) = 766 (if remove1 tcbp queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last (remove1 tcbp queue)))" 767 using queue_rel in_queue cs_tcb valid_ntfn 768 tcb_queue_relation_not_NULL [OF tcb_queue_relation'_queue_rel [OF queue_rel] valid_ntfn(1)] 769 apply - 770 apply (erule tcb_queue_relationE') 771 apply (frule (3) tcb_queueD) 772 apply (subst r1) 773 apply simp 774 apply (intro impI conjI) 775 apply (subgoal_tac "tcbp = last queue") 776 apply simp 777 apply (subgoal_tac "(remove1 (last queue) queue) \<noteq> []") 778 apply (clarsimp simp: inj_eq last_conv_nth nth_eq_iff_index_eq length_remove1 779 distinct_remove1_take_drop split: if_split_asm) 780 apply arith 781 apply (clarsimp simp: remove1_empty last_conv_nth hd_conv_nth nth_eq_iff_index_eq not_le split: if_split_asm) 782 apply (cases queue) 783 apply simp 784 apply simp 785 apply (fastforce simp: inj_eq split: if_split_asm) 786 apply (clarsimp simp: last_conv_nth distinct_remove1_take_drop nth_eq_iff_index_eq inj_eq split: if_split_asm) 787 apply arith 788 apply (simp add: nth_append min_def nth_eq_iff_index_eq) 789 apply clarsimp 790 apply arith 791 done 792 qed 793qed 794 795lemmas tcbEPDequeue_update 796 = tcbDequeue_update[where tn=tcbEPNext_C and tn_update=tcbEPNext_C_update 797 and tp=tcbEPPrev_C and tp_update=tcbEPPrev_C_update, 798 simplified] 799 800lemma tcb_queue_relation_ptr_rel': 801 assumes tq: "tcb_queue_relation getNext getPrev mp queue NULL qhead" 802 and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 803 and cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 804 and in_queue: "tcbp \<in> set queue" 805 shows "tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb 806 \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb)" 807 using tq valid_ep cs_tcb null_not_in [OF tq valid_ep(1) valid_ep(2)] in_queue 808 by (rule tcb_queue_relation_ptr_rel) 809 810lemma tcb_queue_head_empty_iff: 811 "\<lbrakk> tcb_queue_relation getNext getPrev mp queue NULL qhead; \<forall>t \<in> set queue. tcb_at' t s \<rbrakk> \<Longrightarrow> 812 (qhead = NULL) = (queue = [])" 813 apply (rule classical) 814 apply (cases queue) 815 apply simp 816 apply (frule (1) tcb_queue_relation_not_NULL) 817 apply clarsimp 818 done 819 820lemma ctcb_ptr_to_tcb_ptr_aligned: 821 assumes al: "is_aligned (ctcb_ptr_to_tcb_ptr ptr) tcbBlockSizeBits" 822 shows "is_aligned (ptr_val ptr) ctcb_size_bits" 823proof - 824 have "is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr ptr))) ctcb_size_bits" 825 unfolding tcb_ptr_to_ctcb_ptr_def using al 826 apply simp 827 apply (erule aligned_add_aligned) 828 apply (unfold ctcb_offset_defs, rule is_aligned_triv) 829 apply (simp add: word_bits_conv objBits_defs)+ 830 done 831 thus ?thesis by simp 832qed 833 834 835lemma ctcb_size_bits_ge_4: "4 \<le> ctcb_size_bits" 836 by (simp add: ctcb_size_bits_def) 837 838lemma tcb_queue_relation_next_mask: 839 assumes tq: "tcb_queue_relation getNext getPrev mp queue NULL qhead" 840 and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 841 and cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 842 and in_queue: "tcbp \<in> set queue" 843 and bits: "bits \<le> ctcb_size_bits" 844 shows "ptr_val (getNext tcb) && ~~ mask bits = ptr_val (getNext tcb)" 845proof (cases "(getNext tcb) = NULL") 846 case True 847 thus ?thesis by simp 848next 849 case False 850 851 hence "ctcb_ptr_to_tcb_ptr (getNext tcb) \<in> set queue" using assms 852 apply - 853 apply (drule (3) tcb_queueD) 854 apply (clarsimp split: if_split_asm) 855 done 856 857 with valid_ep(1) have "tcb_at' (ctcb_ptr_to_tcb_ptr (getNext tcb)) s" .. 858 hence "is_aligned (ctcb_ptr_to_tcb_ptr (getNext tcb)) tcbBlockSizeBits" by (rule tcb_aligned') 859 hence "is_aligned (ptr_val (getNext tcb)) ctcb_size_bits" by (rule ctcb_ptr_to_tcb_ptr_aligned) 860 thus ?thesis using bits by simp 861qed 862 863lemma tcb_queue_relation_prev_mask: 864 assumes tq: "tcb_queue_relation getNext getPrev mp queue NULL qhead" 865 and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 866 and cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 867 and in_queue: "tcbp \<in> set queue" 868 and bits: "bits \<le> ctcb_size_bits" 869 shows "ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb)" 870proof (cases "(getPrev tcb) = NULL") 871 case True 872 thus ?thesis by simp 873next 874 case False 875 876 hence "ctcb_ptr_to_tcb_ptr (getPrev tcb) \<in> set queue" using assms 877 apply - 878 apply (drule (3) tcb_queueD) 879 apply (clarsimp split: if_split_asm) 880 done 881 882 with valid_ep(1) have "tcb_at' (ctcb_ptr_to_tcb_ptr (getPrev tcb)) s" .. 883 hence "is_aligned (ctcb_ptr_to_tcb_ptr (getPrev tcb)) tcbBlockSizeBits" by (rule tcb_aligned') 884 hence "is_aligned (ptr_val (getPrev tcb)) ctcb_size_bits" by (rule ctcb_ptr_to_tcb_ptr_aligned) 885 thus ?thesis using bits by simp 886qed 887 888lemma tcb_queue_relation'_next_mask: 889 assumes tq: "tcb_queue_relation' getNext getPrev mp queue qhead qend" 890 and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 891 and cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 892 and in_queue: "tcbp \<in> set queue" 893 and bits: "bits \<le> ctcb_size_bits" 894 shows "ptr_val (getNext tcb) && ~~ mask bits = ptr_val (getNext tcb)" 895 by (rule tcb_queue_relation_next_mask [OF tcb_queue_relation'_queue_rel], fact+) 896 897lemma tcb_queue_relation'_prev_mask: 898 assumes tq: "tcb_queue_relation' getNext getPrev mp queue qhead qend" 899 and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 900 and cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 901 and in_queue: "tcbp \<in> set queue" 902 and bits: "bits \<le> ctcb_size_bits" 903 shows "ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb)" 904 by (rule tcb_queue_relation_prev_mask [OF tcb_queue_relation'_queue_rel], fact+) 905 906 907lemma cready_queues_relation_null_queue_ptrs: 908 assumes rel: "cready_queues_relation mp cq aq" 909 and same: "option_map tcb_null_ep_ptrs \<circ> mp' = option_map tcb_null_ep_ptrs \<circ> mp" 910 shows "cready_queues_relation mp' cq aq" 911 using rel 912 apply (clarsimp simp: cready_queues_relation_def Let_def all_conj_distrib) 913 apply (drule spec, drule spec, drule mp, (erule conjI)+, assumption) 914 apply (clarsimp simp: tcb_queue_relation'_def) 915 apply (erule iffD2 [OF tcb_queue_relation_only_next_prev, rotated -1]) 916 apply (rule ext) 917 apply (case_tac "mp' x") 918 apply (frule compD [OF same]) 919 apply simp 920 apply (frule compD [OF same]) 921 apply (clarsimp simp: tcb_null_ep_ptrs_def) 922 apply (case_tac z, case_tac a) 923 apply simp 924 \<comment> \<open>clag\<close> 925 apply (rule ext) 926 apply (case_tac "mp' x") 927 apply (frule compD [OF same]) 928 apply simp 929 apply (frule compD [OF same]) 930 apply (clarsimp simp: tcb_null_ep_ptrs_def) 931 apply (case_tac z, case_tac a) 932 apply simp 933 done 934 935lemma cready_queues_relation_not_queue_ptrs: 936 assumes rel: "cready_queues_relation mp cq aq" 937 and same: "option_map tcbSchedNext_C \<circ> mp' = option_map tcbSchedNext_C \<circ> mp" 938 "option_map tcbSchedPrev_C \<circ> mp' = option_map tcbSchedPrev_C \<circ> mp" 939 shows "cready_queues_relation mp' cq aq" 940 using rel 941 apply (clarsimp simp: cready_queues_relation_def tcb_queue_relation'_def Let_def all_conj_distrib) 942 apply (drule spec, drule spec, drule mp, (erule conjI)+, assumption) 943 apply clarsimp 944 apply (erule iffD2 [OF tcb_queue_relation_only_next_prev, rotated -1]) 945 apply (rule same) 946 apply (rule same) 947 done 948 949lemma ntfn_ep_disjoint: 950 assumes srs: "sym_refs (state_refs_of' s)" 951 and epat: "ko_at' ep epptr s" 952 and ntfnat: "ko_at' ntfn ntfnptr s" 953 and ntfnq: "isWaitingNtfn (ntfnObj ntfn)" 954 and epq: "isSendEP ep \<or> isRecvEP ep" 955 shows "set (epQueue ep) \<inter> set (ntfnQueue (ntfnObj ntfn)) = {}" 956 using srs epat ntfnat ntfnq epq 957 apply - 958 apply (subst disjoint_iff_not_equal, intro ballI, rule notI) 959 apply (drule sym_refs_ko_atD', clarsimp)+ 960 apply clarsimp 961 apply (clarsimp simp: isWaitingNtfn_def isSendEP_def isRecvEP_def 962 split: ntfn.splits endpoint.splits) 963 apply (drule bspec, fastforce simp: ko_wp_at'_def)+ 964 apply (fastforce simp: ko_wp_at'_def refs_of_rev') 965 apply (drule bspec, fastforce simp: ko_wp_at'_def)+ 966 apply (fastforce simp: ko_wp_at'_def refs_of_rev') 967 done 968 969lemma ntfn_ntfn_disjoint: 970 assumes srs: "sym_refs (state_refs_of' s)" 971 and ntfnat: "ko_at' ntfn ntfnptr s" 972 and ntfnat': "ko_at' ntfn' ntfnptr' s" 973 and ntfnq: "isWaitingNtfn (ntfnObj ntfn)" 974 and ntfnq': "isWaitingNtfn (ntfnObj ntfn')" 975 and neq: "ntfnptr' \<noteq> ntfnptr" 976 shows "set (ntfnQueue (ntfnObj ntfn)) \<inter> set (ntfnQueue (ntfnObj ntfn')) = {}" 977 using srs ntfnat ntfnat' ntfnq ntfnq' neq 978 apply - 979 apply (subst disjoint_iff_not_equal, intro ballI, rule notI) 980 apply (drule sym_refs_ko_atD', clarsimp)+ 981 apply clarsimp 982 apply (clarsimp simp: isWaitingNtfn_def split: ntfn.splits) 983 apply (drule bspec, fastforce simp: ko_wp_at'_def)+ 984 apply (clarsimp simp: ko_wp_at'_def refs_of_rev') 985 done 986 987lemma tcb_queue_relation'_empty[simp]: 988 "tcb_queue_relation' getNext getPrev mp [] qhead qend = 989 (qend = tcb_Ptr 0 \<and> qhead = tcb_Ptr 0)" 990 by (simp add: tcb_queue_relation'_def) 991 992lemma cnotification_relation_ntfn_queue: 993 fixes ntfn :: "Structures_H.notification" 994 defines "qs \<equiv> if isWaitingNtfn (ntfnObj ntfn) then set (ntfnQueue (ntfnObj ntfn)) else {}" 995 assumes ntfn: "cnotification_relation (cslift t) ntfn' b" 996 and srs: "sym_refs (state_refs_of' s)" 997 and koat: "ko_at' ntfn ntfnptr s" 998 and koat': "ko_at' ntfn' ntfnptr' s" 999 and mpeq: "(cslift t' |` (- (tcb_ptr_to_ctcb_ptr ` qs))) = (cslift t |` (- (tcb_ptr_to_ctcb_ptr ` qs)))" 1000 and neq: "ntfnptr' \<noteq> ntfnptr" 1001 shows "cnotification_relation (cslift t') ntfn' b" 1002proof - 1003 have rl: "\<And>p. \<lbrakk> p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn')); 1004 isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn')\<rbrakk> 1005 \<Longrightarrow> cslift t p = cslift t' p" using srs koat' koat mpeq neq 1006 apply - 1007 apply (drule (3) ntfn_ntfn_disjoint [OF _ koat koat']) 1008 apply (erule restrict_map_eqI [symmetric]) 1009 apply (erule imageE) 1010 apply (fastforce simp: disjoint_iff_not_equal inj_eq qs_def) 1011 done 1012 1013 show ?thesis using ntfn rl mpeq unfolding cnotification_relation_def 1014 apply (simp add: Let_def) 1015 apply (cases "ntfnObj ntfn'") 1016 apply simp 1017 apply simp 1018 apply (cases "isWaitingNtfn (ntfnObj ntfn)") 1019 apply (simp add: isWaitingNtfn_def cong: tcb_queue_relation'_cong) 1020 apply (simp add: qs_def) 1021 done 1022qed 1023 1024lemma cpspace_relation_ntfn_update_ntfn: 1025 fixes ntfn :: "Structures_H.notification" 1026 defines "qs \<equiv> if isWaitingNtfn (ntfnObj ntfn) then set (ntfnQueue (ntfnObj ntfn)) else {}" 1027 assumes koat: "ko_at' ntfn ntfnptr s" 1028 and invs: "invs' s" 1029 and cp: "cpspace_ntfn_relation (ksPSpace s) (t_hrs_' (globals t))" 1030 and rel: "cnotification_relation (cslift t') ntfn' notification" 1031 and mpeq: "(cslift t' |` (- (tcb_ptr_to_ctcb_ptr ` qs))) = (cslift t |` (- (tcb_ptr_to_ctcb_ptr ` qs)))" 1032 shows "cmap_relation (map_to_ntfns (ksPSpace s(ntfnptr \<mapsto> KONotification ntfn'))) 1033 (cslift t(Ptr ntfnptr \<mapsto> notification)) Ptr (cnotification_relation (cslift t'))" 1034 using koat invs cp rel 1035 apply - 1036 apply (subst map_comp_update) 1037 apply (simp add: projectKO_opts_defs) 1038 apply (frule ko_at_projectKO_opt) 1039 apply (rule cmap_relationE1, assumption+) 1040 apply (erule (3) cmap_relation_upd_relI) 1041 apply (erule (1) cnotification_relation_ntfn_queue [OF _ invs_sym' koat]) 1042 apply (erule (1) map_to_ko_atI') 1043 apply (fold qs_def, rule mpeq) 1044 apply assumption 1045 apply simp 1046 done 1047 1048lemma cendpoint_relation_upd_tcb_no_queues: 1049 assumes cs: "mp thread = Some tcb" 1050 and next_pres: "option_map tcbEPNext_C \<circ> mp = option_map tcbEPNext_C \<circ> mp'" 1051 and prev_pres: "option_map tcbEPPrev_C \<circ> mp = option_map tcbEPPrev_C \<circ> mp'" 1052 shows "cendpoint_relation mp a b = cendpoint_relation mp' a b" 1053proof - 1054 show ?thesis 1055 unfolding cendpoint_relation_def 1056 apply (simp add: Let_def) 1057 apply (cases a) 1058 apply (simp add: tcb_queue_relation'_def tcb_queue_relation_only_next_prev [OF next_pres prev_pres, symmetric])+ 1059 done 1060qed 1061 1062lemma cnotification_relation_upd_tcb_no_queues: 1063 assumes cs: "mp thread = Some tcb" 1064 and next_pres: "option_map tcbEPNext_C \<circ> mp = option_map tcbEPNext_C \<circ> mp'" 1065 and prev_pres: "option_map tcbEPPrev_C \<circ> mp = option_map tcbEPPrev_C \<circ> mp'" 1066 shows "cnotification_relation mp a b = cnotification_relation mp' a b" 1067proof - 1068 show ?thesis 1069 unfolding cnotification_relation_def 1070 apply (simp add: Let_def) 1071 apply (cases "ntfnObj a") 1072 apply (simp add: tcb_queue_relation'_def tcb_queue_relation_only_next_prev [OF next_pres prev_pres, symmetric])+ 1073 done 1074qed 1075 1076lemma cendpoint_relation_ntfn_queue: 1077 assumes srs: "sym_refs (state_refs_of' s)" 1078 and koat: "ko_at' ntfn ntfnptr s" 1079 and iswaiting: "isWaitingNtfn (ntfnObj ntfn)" 1080 and mpeq: "(cslift t' |` (- (tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn))))) 1081 = (cslift t |` (- (tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn)))))" 1082 and koat': "ko_at' a epptr s" 1083 shows "cendpoint_relation (cslift t) a b = cendpoint_relation (cslift t') a b" 1084proof - 1085 have rl: "\<And>p. \<lbrakk> p \<in> tcb_ptr_to_ctcb_ptr ` set (epQueue a); isSendEP a \<or> isRecvEP a \<rbrakk> 1086 \<Longrightarrow> cslift t p = cslift t' p" using srs koat' koat iswaiting mpeq 1087 apply - 1088 apply (drule (4) ntfn_ep_disjoint) 1089 apply (erule restrict_map_eqI [symmetric]) 1090 apply (erule imageE) 1091 apply (clarsimp simp: disjoint_iff_not_equal inj_eq) 1092 done 1093 1094 show ?thesis 1095 unfolding cendpoint_relation_def using rl 1096 apply (simp add: Let_def) 1097 apply (cases a) 1098 apply (simp add: isRecvEP_def cong: tcb_queue_relation'_cong) 1099 apply simp 1100 apply (simp add: isSendEP_def isRecvEP_def cong: tcb_queue_relation'_cong) 1101 done 1102qed 1103 1104lemma cvariable_relation_upd_const: 1105 "m x \<noteq> None 1106 \<Longrightarrow> cvariable_array_map_relation (m (x \<mapsto> y)) (\<lambda>x. n) 1107 = cvariable_array_map_relation m (\<lambda>x. n)" 1108 by (auto simp: fun_eq_iff cvariable_array_map_relation_def) 1109 1110lemma rf_sr_tcb_update_no_queue: 1111 "\<lbrakk> (s, s') \<in> rf_sr; ko_at' tcb thread s; 1112 t_hrs_' (globals t) = hrs_mem_update (heap_update 1113 (tcb_ptr_to_ctcb_ptr thread) ctcb) (t_hrs_' (globals s')); 1114 tcbEPNext_C ctcb = tcbEPNext_C (the (cslift s' (tcb_ptr_to_ctcb_ptr thread))); 1115 tcbEPPrev_C ctcb = tcbEPPrev_C (the (cslift s' (tcb_ptr_to_ctcb_ptr thread))); 1116 tcbSchedNext_C ctcb = tcbSchedNext_C (the (cslift s' (tcb_ptr_to_ctcb_ptr thread))); 1117 tcbSchedPrev_C ctcb = tcbSchedPrev_C (the (cslift s' (tcb_ptr_to_ctcb_ptr thread))); 1118 (\<forall>x\<in>ran tcb_cte_cases. (\<lambda>(getF, setF). getF tcb' = getF tcb) x); 1119 ctcb_relation tcb' ctcb 1120 \<rbrakk> 1121 \<Longrightarrow> (s\<lparr>ksPSpace := ksPSpace s(thread \<mapsto> KOTCB tcb')\<rparr>, x\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr" 1122 unfolding rf_sr_def state_relation_def cstate_relation_def cpspace_relation_def 1123 apply (clarsimp simp: Let_def update_tcb_map_tos map_to_ctes_upd_tcb_no_ctes 1124 heap_to_user_data_def) 1125 apply (frule (1) cmap_relation_ko_atD) 1126 apply (erule obj_atE') 1127 apply (clarsimp simp: projectKOs) 1128 apply (clarsimp simp: map_comp_update projectKO_opt_tcb cvariable_relation_upd_const 1129 typ_heap_simps') 1130 apply (intro conjI) 1131 subgoal by (clarsimp simp: cmap_relation_def map_comp_update projectKO_opts_defs inj_eq) 1132 apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) 1133 apply simp 1134 apply (rule cendpoint_relation_upd_tcb_no_queues, assumption+) 1135 subgoal by (clarsimp intro!: ext) 1136 subgoal by (clarsimp intro!: ext) 1137 apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) 1138 apply simp 1139 apply (rule cnotification_relation_upd_tcb_no_queues, assumption+) 1140 subgoal by (clarsimp intro!: ext) 1141 subgoal by (clarsimp intro!: ext) 1142 apply (erule cready_queues_relation_not_queue_ptrs) 1143 subgoal by (clarsimp intro!: ext) 1144 subgoal by (clarsimp intro!: ext) 1145 subgoal by (simp add: carch_state_relation_def typ_heap_simps') 1146 by (simp add: cmachine_state_relation_def) 1147 1148lemma rf_sr_tcb_update_no_queue_helper: 1149 "(s, s'\<lparr> globals := globals s' \<lparr> t_hrs_' := t_hrs_' (globals (undefined 1150 \<lparr> globals := (undefined \<lparr> t_hrs_' := f (globals s') (t_hrs_' (globals s')) \<rparr>)\<rparr>))\<rparr>\<rparr>) \<in> rf_sr 1151 \<Longrightarrow> (s, globals_update (\<lambda>v. t_hrs_'_update (f v) v) s') \<in> rf_sr" 1152 by (simp cong: StateSpace.state.fold_congs globals.fold_congs) 1153 1154lemmas rf_sr_tcb_update_no_queue2 1155 = rf_sr_tcb_update_no_queue_helper [OF rf_sr_tcb_update_no_queue, simplified] 1156 1157lemma tcb_queue_relation_not_in_q: 1158 "ctcb_ptr_to_tcb_ptr x \<notin> set xs \<Longrightarrow> 1159 tcb_queue_relation' nxtFn prvFn (hp(x := v)) xs start end 1160 = tcb_queue_relation' nxtFn prvFn hp xs start end" 1161 by (rule tcb_queue_relation'_cong, auto) 1162 1163lemma rf_sr_tcb_update_not_in_queue: 1164 "\<lbrakk> (s, s') \<in> rf_sr; ko_at' tcb thread s; 1165 t_hrs_' (globals t) = hrs_mem_update (heap_update 1166 (tcb_ptr_to_ctcb_ptr thread) ctcb) (t_hrs_' (globals s')); 1167 \<not> live' (KOTCB tcb); invs' s; 1168 (\<forall>x\<in>ran tcb_cte_cases. (\<lambda>(getF, setF). getF tcb' = getF tcb) x); 1169 ctcb_relation tcb' ctcb \<rbrakk> 1170 \<Longrightarrow> (s\<lparr>ksPSpace := ksPSpace s(thread \<mapsto> KOTCB tcb')\<rparr>, 1171 x\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr" 1172 unfolding rf_sr_def state_relation_def cstate_relation_def cpspace_relation_def 1173 apply (clarsimp simp: Let_def update_tcb_map_tos map_to_ctes_upd_tcb_no_ctes 1174 heap_to_user_data_def live'_def) 1175 apply (frule (1) cmap_relation_ko_atD) 1176 apply (erule obj_atE') 1177 apply (clarsimp simp: projectKOs) 1178 apply (clarsimp simp: map_comp_update projectKO_opt_tcb cvariable_relation_upd_const 1179 typ_heap_simps') 1180 apply (subgoal_tac "\<forall>rf. \<not> ko_wp_at' (\<lambda>ko. rf \<in> refs_of' ko) thread s") 1181 prefer 2 1182 apply clarsimp 1183 apply (auto simp: obj_at'_def ko_wp_at'_def)[1] 1184 apply (intro conjI) 1185 subgoal by (clarsimp simp: cmap_relation_def map_comp_update projectKO_opts_defs inj_eq) 1186 apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) 1187 apply clarsimp 1188 apply (subgoal_tac "thread \<notin> (fst ` ep_q_refs_of' a)") 1189 apply (clarsimp simp: cendpoint_relation_def Let_def split: Structures_H.endpoint.split) 1190 subgoal by (intro conjI impI allI, simp_all add: image_def tcb_queue_relation_not_in_q)[1] 1191 apply (drule(1) map_to_ko_atI') 1192 apply (drule sym_refs_ko_atD', clarsimp+) 1193 subgoal by blast 1194 apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) 1195 apply clarsimp 1196 apply (subgoal_tac "thread \<notin> (fst ` ntfn_q_refs_of' (ntfnObj a))") 1197 apply (clarsimp simp: cnotification_relation_def Let_def 1198 split: ntfn.splits) 1199 subgoal by (simp add: image_def tcb_queue_relation_not_in_q)[1] 1200 apply (drule(1) map_to_ko_atI') 1201 apply (drule sym_refs_ko_atD', clarsimp+) 1202 subgoal by blast 1203 apply (simp add: cready_queues_relation_def, erule allEI) 1204 apply (clarsimp simp: Let_def) 1205 apply (subst tcb_queue_relation_not_in_q) 1206 apply clarsimp 1207 apply (drule valid_queues_obj_at'D, clarsimp) 1208 apply (clarsimp simp: obj_at'_def projectKOs inQ_def) 1209 subgoal by simp 1210 subgoal by (simp add: carch_state_relation_def carch_globals_def 1211 typ_heap_simps') 1212 by (simp add: cmachine_state_relation_def) 1213 1214lemmas rf_sr_tcb_update_not_in_queue2 1215 = rf_sr_tcb_update_no_queue_helper [OF rf_sr_tcb_update_not_in_queue, simplified] 1216 1217end 1218end 1219