68 To minimize the cost of the recalculation, we derived the following localized alternative |
68 To minimize the cost of the recalculation, we derived the following localized alternative |
69 definition of @{term cp}: |
69 definition of @{term cp}: |
70 *} |
70 *} |
71 |
71 |
72 lemma cp_rec_tG: |
72 lemma cp_rec_tG: |
73 "cp s th = Max ({preced th s} \<union> cprecs (children (tG s) th) s)" |
73 "cp s th = Max (preceds {th} s \<union> cprecs (children (tG s) th) s)" |
74 proof - |
74 proof - |
75 have [simp]: "(cp s \<circ> the_thread \<circ> Th) = cp s" by (rule ext, simp) |
75 have [simp]: "(cp s \<circ> the_thread \<circ> Th) = cp s" by (rule ext, simp) |
76 have [simp]: "(cp s \<circ> the_thread) ` children (tRAG s) (Th th) = |
76 have [simp]: "(cp s \<circ> the_thread) ` children (tRAG s) (Th th) = |
77 cp s ` children (tG s) th" |
77 cp s ` children (tG s) th" |
78 apply (unfold tRAG_def_tG) |
78 apply (unfold tRAG_def_tG) |
98 |
98 |
99 section {* The @{term Set} operation *} |
99 section {* The @{term Set} operation *} |
100 |
100 |
101 context valid_trace_set |
101 context valid_trace_set |
102 begin |
102 begin |
|
103 |
|
104 find_theorems RAG "(e#s)" "_ = _" |
103 |
105 |
104 text {* (* ddd *) |
106 text {* (* ddd *) |
105 The following two lemmas confirm that @{text "Set"}-operation |
107 The following two lemmas confirm that @{text "Set"}-operation |
106 only changes the precedence of the initiating thread (or actor) |
108 only changes the precedence of the initiating thread (or actor) |
107 of the operation (or event). |
109 of the operation (or event). |
298 More specifically, the lemma says the change of @{text RAG} |
300 More specifically, the lemma says the change of @{text RAG} |
299 is by first removing the chain linking @{text taker}, @{text cs} and |
301 is by first removing the chain linking @{text taker}, @{text cs} and |
300 @{text th} and then adding in one edge from @{text cs} to @{text taker}. |
302 @{text th} and then adding in one edge from @{text cs} to @{text taker}. |
301 The added edge represents acquisition of @{text cs} by @{text taker}. |
303 The added edge represents acquisition of @{text cs} by @{text taker}. |
302 *} |
304 *} |
|
305 |
303 lemma RAG_s: |
306 lemma RAG_s: |
304 "RAG (e#s) = (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) \<union> |
307 "RAG (e#s) = (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) \<union> |
305 {(Cs cs, Th taker)}" |
308 {(Cs cs, Th taker)}" |
306 by (unfold RAG_es waiting_set_eq holding_set_eq, auto) |
309 by (unfold RAG_es waiting_set_eq holding_set_eq, auto) |
307 |
310 |
378 threads other than @{text th} and @{text taker}) do not need to do any @{text cp}-recalculation. |
381 threads other than @{text th} and @{text taker}) do not need to do any @{text cp}-recalculation. |
379 The reason is simple: according to @{thm subtree_kept}, the sub-trees of such threads |
382 The reason is simple: according to @{thm subtree_kept}, the sub-trees of such threads |
380 are not changed , additionally, since the @{text V}-operation does not change any precedence, |
383 are not changed , additionally, since the @{text V}-operation does not change any precedence, |
381 the @{text "cp"}-value of such threads are not changed. |
384 the @{text "cp"}-value of such threads are not changed. |
382 *} |
385 *} |
|
386 |
383 lemma cp_kept: |
387 lemma cp_kept: |
384 assumes "th1 \<notin> {th, taker}" |
388 assumes "th1 \<notin> {th, taker}" |
385 shows "cp (e#s) th1 = cp s th1" |
389 shows "cp (e#s) th1 = cp s th1" |
386 by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp) |
390 by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp) |
387 |
391 |
394 neither of these two threads has children with changed @{text cp}-value. |
398 neither of these two threads has children with changed @{text cp}-value. |
395 It means the recursive calls in @{thm cp_rec_tG} will not descend when recalculating |
399 It means the recursive calls in @{thm cp_rec_tG} will not descend when recalculating |
396 the @{text cp}-values for @{text th} and @{text taker}. |
400 the @{text cp}-values for @{text th} and @{text taker}. |
397 *} |
401 *} |
398 |
402 |
399 lemma t1: "taker \<notin> children (tG (e#s)) th" |
403 lemma "taker \<notin> children (tG (e#s)) th" |
400 by (metis children_subtree empty_iff in_mono neq_taker_th root_def set_mp |
404 by (metis children_subtree empty_iff in_mono neq_taker_th root_def set_mp |
401 subtree_ancestorsI taker_ready_es vat_es.root_readys_tG) |
405 subtree_ancestorsI taker_ready_es vat_es.root_readys_tG) |
402 |
406 |
403 |
407 |
404 lemma t2: "th \<notin> children (tG (e#s)) taker" |
408 lemma "th \<notin> children (tG (e#s)) taker" |
405 by (metis children_subtree empty_iff neq_taker_th root_def |
409 by (metis children_subtree empty_iff neq_taker_th root_def |
406 subsetD subtree_ancestorsI th_ready_es vat_es.root_readys_tG) |
410 subsetD subtree_ancestorsI th_ready_es vat_es.root_readys_tG) |
407 |
411 |
408 |
412 |
409 end |
413 end |
509 |
513 |
510 text {* |
514 text {* |
511 By combining @{thm cp_kept_1} and @{thm cp_kept_2}, it is shown that no @{text cp}-recalculation |
515 By combining @{thm cp_kept_1} and @{thm cp_kept_2}, it is shown that no @{text cp}-recalculation |
512 is needed at all for this sub-case of @{text V}-operation. |
516 is needed at all for this sub-case of @{text V}-operation. |
513 *} |
517 *} |
514 lemma eq_cp: |
518 lemma eq_cp_pre: |
515 shows "cp (e#s) th' = cp s th'" |
519 shows "cp (e#s) th' = cp s th'" |
516 using cp_kept_1 cp_kept_2 |
520 using cp_kept_1 cp_kept_2 |
517 by (cases "th' = th", auto) |
521 by (cases "th' = th", auto) |
|
522 |
|
523 lemma eq_cp: |
|
524 shows "cp (e#s) = cp s" |
|
525 by (rule ext, unfold eq_cp_pre, simp) |
518 |
526 |
519 end |
527 end |
520 |
528 |
521 section {* The @{term P} operation *} |
529 section {* The @{term P} operation *} |
522 |
530 |
586 |
594 |
587 context valid_trace_p_h |
595 context valid_trace_p_h |
588 begin |
596 begin |
589 |
597 |
590 text {* |
598 text {* |
591 According to @{thm RAG_es}, the only change to @{text RAG} by |
599 It can be shown that the @{text tG} is not changed by |
592 the @{text P}-operation is the addition of the edge @{text "(Cs cs, Th th)"}, |
600 the @{text P}-action. The reason is that the edge added to @{text RAG} |
593 representing the newly acquisition of @{text cs} by @{text th}. |
601 by the @{text P}-action, namely @{text "(Cs cs, Th th)"}, |
594 The following lemma shows that this newly added edge only change the sub-tree |
602 does not bring any new thread into graph @{text tG}, because |
595 of @{text th}, the reason is that @{text th} is in no other sub-trees. |
603 the node of @{text cs} is isolated from the original @{text RAG}. |
596 *} |
604 *} |
597 |
605 |
598 lemma subtree_kept: |
606 lemma tG_es: "tG (e # s) = tG s" |
599 assumes "th' \<noteq> th" |
607 proof - |
600 shows "subtree (RAG (e#s)) (Th th') = subtree (RAG s) (Th th')" |
608 have [simp]: "\<And> th1. (Th th1, Cs cs) \<notin> RAG s" |
601 proof(unfold RAG_es, rule subtree_insert_next) |
609 by (metis in_RAG_E no_holder node.simps(4) the_cs.simps waiting_holding) |
602 from in_no_others_subtree[OF assms] |
610 show ?thesis |
603 show "Th th \<notin> subtree (RAG s) (Th th')" . |
611 apply (unfold tG_def_tRAG tRAG_alt_def RAG_es) |
604 qed |
612 by (auto) |
605 |
613 qed |
606 text {* |
614 |
607 With both sub-tree and precdences unchanged, the @{text cp}-values of |
615 text {* |
608 threads other than @{text th} are not changed. Therefore, the |
616 Since both @{text tG} and precedences are not changed, it is easy |
609 only recalculation of @{text cp}-value happens at @{text th}, and |
617 to show that all @{text cp}-value are not changed, therefore, |
610 the recalculation can be done locally using the |
618 no @{text cp}-recalculation is needed: |
611 {\em local recalculation principle}, because the @{text cp}-values |
619 *} |
612 of its children are not changed. |
620 |
613 *} |
621 lemma cp_kept: "cp (e#s) = cp s" |
614 lemma cp_kept: |
622 by (rule ext, simp add: cp_alt_def2 preced_kept tG_es) |
615 assumes "th' \<noteq> th" |
|
616 shows "cp (e#s) th' = cp s th'" |
|
617 proof - |
|
618 have "(the_preced (e#s) ` {th'a. Th th'a \<in> subtree (RAG (e#s)) (Th th')}) = |
|
619 (the_preced s ` {th'a. Th th'a \<in> subtree (RAG s) (Th th')})" |
|
620 by (unfold preced_kept subtree_kept[OF assms], simp) |
|
621 thus ?thesis by (unfold cp_alt_def, simp) |
|
622 qed |
|
623 |
623 |
624 end |
624 end |
625 |
625 |
626 text {* |
626 text {* |
627 The following locale @{text valid_trace_p_w} corresponds to |
627 The following locale @{text valid_trace_p_w} corresponds to |
1009 text {* |
1009 text {* |
1010 Because of @{thm preced_kept}, @{thm tG_kept} and @{thm th_tRAG}, |
1010 Because of @{thm preced_kept}, @{thm tG_kept} and @{thm th_tRAG}, |
1011 the @{text cp}-values of all other threads are not changed. |
1011 the @{text cp}-values of all other threads are not changed. |
1012 The reasoning is almost the same as that of @{term Create}: |
1012 The reasoning is almost the same as that of @{term Create}: |
1013 *} |
1013 *} |
|
1014 |
1014 lemma eq_cp: |
1015 lemma eq_cp: |
1015 assumes neq_th: "th' \<noteq> th" |
1016 assumes neq_th: "th' \<noteq> th" |
1016 shows "cp (e#s) th' = cp s th'" |
1017 shows "cp (e#s) th' = cp s th'" |
1017 proof - |
1018 proof - |
1018 have "(the_preced (e # s) ` subtree (tG (e # s)) th') = |
1019 have "(the_preced (e # s) ` subtree (tG (e # s)) th') = |