358 by (simp add: s_dependants_abv wq_def) |
358 by (simp add: s_dependants_abv wq_def) |
359 |
359 |
360 lemma inj_the_preced: |
360 lemma inj_the_preced: |
361 "inj_on (the_preced s) (threads s)" |
361 "inj_on (the_preced s) (threads s)" |
362 by (metis inj_onI preced_unique the_preced_def) |
362 by (metis inj_onI preced_unique the_preced_def) |
|
363 |
|
364 lemma holding_next_thI: |
|
365 assumes "holding s th cs" |
|
366 and "length (wq s cs) > 1" |
|
367 obtains th' where "next_th s th cs th'" |
|
368 proof - |
|
369 from assms(1)[folded holding_eq, unfolded cs_holding_def] |
|
370 have " th \<in> set (wq s cs) \<and> th = hd (wq s cs)" |
|
371 by (unfold s_holding_def, fold wq_def, auto) |
|
372 then obtain rest where h1: "wq s cs = th#rest" |
|
373 by (cases "wq s cs", auto) |
|
374 with assms(2) have h2: "rest \<noteq> []" by auto |
|
375 let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)" |
|
376 have "next_th s th cs ?th'" using h1(1) h2 |
|
377 by (unfold next_th_def, auto) |
|
378 from that[OF this] show ?thesis . |
|
379 qed |
363 |
380 |
364 (* ccc *) |
381 (* ccc *) |
365 |
382 |
366 section {* Locales used to investigate the execution of PIP *} |
383 section {* Locales used to investigate the execution of PIP *} |
367 |
384 |
2646 by (unfold eq_n tRAG_alt_def, auto) |
2663 by (unfold eq_n tRAG_alt_def, auto) |
2647 qed |
2664 qed |
2648 } ultimately show ?thesis by auto |
2665 } ultimately show ?thesis by auto |
2649 qed |
2666 qed |
2650 |
2667 |
|
2668 lemma subtree_tRAG_thread: |
|
2669 assumes "th \<in> threads s" |
|
2670 shows "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" (is "?L \<subseteq> ?R") |
|
2671 proof - |
|
2672 have "?L = {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}" |
|
2673 by (unfold tRAG_subtree_eq, simp) |
|
2674 also have "... \<subseteq> ?R" |
|
2675 proof |
|
2676 fix x |
|
2677 assume "x \<in> {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}" |
|
2678 then obtain th' where h: "x = Th th'" "Th th' \<in> subtree (RAG s) (Th th)" by auto |
|
2679 from this(2) |
|
2680 show "x \<in> ?R" |
|
2681 proof(cases rule:subtreeE) |
|
2682 case 1 |
|
2683 thus ?thesis by (simp add: assms h(1)) |
|
2684 next |
|
2685 case 2 |
|
2686 thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) |
|
2687 qed |
|
2688 qed |
|
2689 finally show ?thesis . |
|
2690 qed |
|
2691 |
2651 lemma dependants_alt_def: |
2692 lemma dependants_alt_def: |
2652 "dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}" |
2693 "dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}" |
2653 by (metis eq_RAG s_dependants_def tRAG_trancl_eq) |
2694 by (metis eq_RAG s_dependants_def tRAG_trancl_eq) |
2654 |
2695 |
2655 lemma dependants_alt_def1: |
2696 lemma dependants_alt_def1: |
2915 by (rule Max_fg_mono, |
2956 by (rule Max_fg_mono, |
2916 simp add: finite_threads, |
2957 simp add: finite_threads, |
2917 simp add: le_cp the_preced_def) |
2958 simp add: le_cp the_preced_def) |
2918 ultimately show ?thesis by auto |
2959 ultimately show ?thesis by auto |
2919 qed |
2960 qed |
|
2961 |
|
2962 lemma threads_alt_def: |
|
2963 "(threads s) = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})" |
|
2964 (is "?L = ?R") |
|
2965 proof - |
|
2966 { fix th1 |
|
2967 assume "th1 \<in> ?L" |
|
2968 from th_chain_to_ready[OF this] |
|
2969 have "th1 \<in> readys s \<or> (\<exists>th'. th' \<in> readys s \<and> (Th th1, Th th') \<in> (RAG s)\<^sup>+)" . |
|
2970 hence "th1 \<in> ?R" by (auto simp:subtree_def) |
|
2971 } moreover |
|
2972 { fix th' |
|
2973 assume "th' \<in> ?R" |
|
2974 then obtain th where h: "th \<in> readys s" " Th th' \<in> subtree (RAG s) (Th th)" |
|
2975 by auto |
|
2976 from this(2) |
|
2977 have "th' \<in> ?L" |
|
2978 proof(cases rule:subtreeE) |
|
2979 case 1 |
|
2980 with h(1) show ?thesis by (auto simp:readys_def) |
|
2981 next |
|
2982 case 2 |
|
2983 from tranclD[OF this(2)[unfolded ancestors_def, simplified]] |
|
2984 have "Th th' \<in> Domain (RAG s)" by auto |
|
2985 from dm_RAG_threads[OF this] |
|
2986 show ?thesis . |
|
2987 qed |
|
2988 } ultimately show ?thesis by auto |
|
2989 qed |
|
2990 |
|
2991 |
|
2992 text {* (* ccc *) \noindent |
|
2993 Since the current precedence of the threads in ready queue will always be boosted, |
|
2994 there must be one inside it has the maximum precedence of the whole system. |
|
2995 *} |
|
2996 lemma max_cp_readys_threads: |
|
2997 shows "Max (cp s ` readys s) = Max (cp s ` threads s)" (is "?L = ?R") |
|
2998 proof(cases "readys s = {}") |
|
2999 case False |
|
3000 have "?R = Max (the_preced s ` threads s)" by (unfold max_cp_eq, simp) |
|
3001 also have "... = |
|
3002 Max (the_preced s ` (\<Union>th\<in>readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)}))" |
|
3003 by (unfold threads_alt_def, simp) |
|
3004 also have "... = |
|
3005 Max ((\<Union>th\<in>readys s. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}))" |
|
3006 by (unfold image_UN, simp) |
|
3007 also have "... = |
|
3008 Max (Max ` (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}) ` readys s)" |
|
3009 proof(rule Max_UNION) |
|
3010 show "\<forall>M\<in>(\<lambda>x. the_preced s ` |
|
3011 {th'. Th th' \<in> subtree (RAG s) (Th x)}) ` readys s. finite M" |
|
3012 using finite_subtree_threads by auto |
|
3013 qed (auto simp:False subtree_def) |
|
3014 also have "... = |
|
3015 Max ((Max \<circ> (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})) ` readys s)" |
|
3016 by (unfold image_comp, simp) |
|
3017 also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)") |
|
3018 proof - |
|
3019 have "(?f ` ?A) = (?g ` ?A)" |
|
3020 proof(rule f_image_eq) |
|
3021 fix th1 |
|
3022 assume "th1 \<in> ?A" |
|
3023 thus "?f th1 = ?g th1" |
|
3024 by (unfold cp_alt_def, simp) |
|
3025 qed |
|
3026 thus ?thesis by simp |
|
3027 qed |
|
3028 finally show ?thesis by simp |
|
3029 qed (auto simp:threads_alt_def) |
2920 |
3030 |
2921 end |
3031 end |
2922 |
3032 |
2923 section {* Relating @{term cntP}, @{term cntV}, @{term cntCS} and @{term pvD} *} |
3033 section {* Relating @{term cntP}, @{term cntV}, @{term cntCS} and @{term pvD} *} |
2924 |
3034 |
4445 by (unfold tRAG_alt_def, auto simp:children_def) |
4555 by (unfold tRAG_alt_def, auto simp:children_def) |
4446 qed |
4556 qed |
4447 thus ?thesis by (subst (1) h(1), unfold h(2), simp) |
4557 thus ?thesis by (subst (1) h(1), unfold h(2), simp) |
4448 qed |
4558 qed |
4449 qed |
4559 qed |
4450 |
4560 end |
4451 section {* Relating @{term cp}-values of @{term threads} and @{term readys }*} |
4561 |
4452 |
4562 section {* Other properties useful in Implementation.thy or Correctness.thy *} |
4453 lemma threads_alt_def: |
|
4454 "(threads s) = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})" |
|
4455 (is "?L = ?R") |
|
4456 proof - |
|
4457 { fix th1 |
|
4458 assume "th1 \<in> ?L" |
|
4459 from th_chain_to_ready[OF this] |
|
4460 have "th1 \<in> readys s \<or> (\<exists>th'. th' \<in> readys s \<and> (Th th1, Th th') \<in> (RAG s)\<^sup>+)" . |
|
4461 hence "th1 \<in> ?R" by (auto simp:subtree_def) |
|
4462 } moreover |
|
4463 { fix th' |
|
4464 assume "th' \<in> ?R" |
|
4465 then obtain th where h: "th \<in> readys s" " Th th' \<in> subtree (RAG s) (Th th)" |
|
4466 by auto |
|
4467 from this(2) |
|
4468 have "th' \<in> ?L" |
|
4469 proof(cases rule:subtreeE) |
|
4470 case 1 |
|
4471 with h(1) show ?thesis by (auto simp:readys_def) |
|
4472 next |
|
4473 case 2 |
|
4474 from tranclD[OF this(2)[unfolded ancestors_def, simplified]] |
|
4475 have "Th th' \<in> Domain (RAG s)" by auto |
|
4476 from dm_RAG_threads[OF this] |
|
4477 show ?thesis . |
|
4478 qed |
|
4479 } ultimately show ?thesis by auto |
|
4480 qed |
|
4481 |
|
4482 |
|
4483 text {* (* ccc *) \noindent |
|
4484 Since the current precedence of the threads in ready queue will always be boosted, |
|
4485 there must be one inside it has the maximum precedence of the whole system. |
|
4486 *} |
|
4487 lemma max_cp_readys_threads: |
|
4488 shows "Max (cp s ` readys s) = Max (cp s ` threads s)" (is "?L = ?R") |
|
4489 proof(cases "readys s = {}") |
|
4490 case False |
|
4491 have "?R = Max (the_preced s ` threads s)" by (unfold max_cp_eq, simp) |
|
4492 also have "... = |
|
4493 Max (the_preced s ` (\<Union>th\<in>readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)}))" |
|
4494 by (unfold threads_alt_def, simp) |
|
4495 also have "... = |
|
4496 Max ((\<Union>th\<in>readys s. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}))" |
|
4497 by (unfold image_UN, simp) |
|
4498 also have "... = |
|
4499 Max (Max ` (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}) ` readys s)" |
|
4500 proof(rule Max_UNION) |
|
4501 show "\<forall>M\<in>(\<lambda>x. the_preced s ` |
|
4502 {th'. Th th' \<in> subtree (RAG s) (Th x)}) ` readys s. finite M" |
|
4503 using finite_subtree_threads by auto |
|
4504 qed (auto simp:False subtree_def) |
|
4505 also have "... = |
|
4506 Max ((Max \<circ> (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})) ` readys s)" |
|
4507 by (unfold image_comp, simp) |
|
4508 also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)") |
|
4509 proof - |
|
4510 have "(?f ` ?A) = (?g ` ?A)" |
|
4511 proof(rule f_image_eq) |
|
4512 fix th1 |
|
4513 assume "th1 \<in> ?A" |
|
4514 thus "?f th1 = ?g th1" |
|
4515 by (unfold cp_alt_def, simp) |
|
4516 qed |
|
4517 thus ?thesis by simp |
|
4518 qed |
|
4519 finally show ?thesis by simp |
|
4520 qed (auto simp:threads_alt_def) |
|
4521 |
|
4522 end |
|
4523 |
|
4524 section {* Pending properties *} |
|
4525 |
|
4526 lemma next_th_unique: |
|
4527 assumes nt1: "next_th s th cs th1" |
|
4528 and nt2: "next_th s th cs th2" |
|
4529 shows "th1 = th2" |
|
4530 using assms by (unfold next_th_def, auto) |
|
4531 |
|
4532 lemma holding_next_thI: |
|
4533 assumes "holding s th cs" |
|
4534 and "length (wq s cs) > 1" |
|
4535 obtains th' where "next_th s th cs th'" |
|
4536 proof - |
|
4537 from assms(1)[folded holding_eq, unfolded cs_holding_def] |
|
4538 have " th \<in> set (wq s cs) \<and> th = hd (wq s cs)" |
|
4539 by (unfold s_holding_def, fold wq_def, auto) |
|
4540 then obtain rest where h1: "wq s cs = th#rest" |
|
4541 by (cases "wq s cs", auto) |
|
4542 with assms(2) have h2: "rest \<noteq> []" by auto |
|
4543 let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)" |
|
4544 have "next_th s th cs ?th'" using h1(1) h2 |
|
4545 by (unfold next_th_def, auto) |
|
4546 from that[OF this] show ?thesis . |
|
4547 qed |
|
4548 |
4563 |
4549 context valid_trace_e |
4564 context valid_trace_e |
4550 begin |
4565 begin |
4551 |
4566 |
4552 lemma actor_inv: |
4567 lemma actor_inv: |
4553 assumes "\<not> isCreate e" |
4568 assumes "\<not> isCreate e" |
4554 shows "actor e \<in> runing s" |
4569 shows "actor e \<in> runing s" |
4555 using pip_e assms |
4570 using pip_e assms |
4556 by (induct, auto) |
4571 by (induct, auto) |
4557 |
|
4558 end |
4572 end |
4559 |
4573 |
4560 context valid_trace |
4574 context valid_trace |
4561 begin |
4575 begin |
4562 |
|
4563 lemma create_pre: |
|
4564 assumes stp: "step s e" |
|
4565 and not_in: "th \<notin> threads s" |
|
4566 and is_in: "th \<in> threads (e#s)" |
|
4567 obtains prio where "e = Create th prio" |
|
4568 proof - |
|
4569 from assms |
|
4570 show ?thesis |
|
4571 proof(cases) |
|
4572 case (thread_create thread prio) |
|
4573 with is_in not_in have "e = Create th prio" by simp |
|
4574 from that[OF this] show ?thesis . |
|
4575 next |
|
4576 case (thread_exit thread) |
|
4577 with assms show ?thesis by (auto intro!:that) |
|
4578 next |
|
4579 case (thread_P thread) |
|
4580 with assms show ?thesis by (auto intro!:that) |
|
4581 next |
|
4582 case (thread_V thread) |
|
4583 with assms show ?thesis by (auto intro!:that) |
|
4584 next |
|
4585 case (thread_set thread) |
|
4586 with assms show ?thesis by (auto intro!:that) |
|
4587 qed |
|
4588 qed |
|
4589 |
|
4590 lemma subtree_tRAG_thread: |
|
4591 assumes "th \<in> threads s" |
|
4592 shows "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" (is "?L \<subseteq> ?R") |
|
4593 proof - |
|
4594 have "?L = {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}" |
|
4595 by (unfold tRAG_subtree_eq, simp) |
|
4596 also have "... \<subseteq> ?R" |
|
4597 proof |
|
4598 fix x |
|
4599 assume "x \<in> {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}" |
|
4600 then obtain th' where h: "x = Th th'" "Th th' \<in> subtree (RAG s) (Th th)" by auto |
|
4601 from this(2) |
|
4602 show "x \<in> ?R" |
|
4603 proof(cases rule:subtreeE) |
|
4604 case 1 |
|
4605 thus ?thesis by (simp add: assms h(1)) |
|
4606 next |
|
4607 case 2 |
|
4608 thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) |
|
4609 qed |
|
4610 qed |
|
4611 finally show ?thesis . |
|
4612 qed |
|
4613 |
4576 |
4614 lemma readys_root: |
4577 lemma readys_root: |
4615 assumes "th \<in> readys s" |
4578 assumes "th \<in> readys s" |
4616 shows "root (RAG s) (Th th)" |
4579 shows "root (RAG s) (Th th)" |
4617 proof - |
4580 proof - |