481 unfolding s_holding_abv |
481 unfolding s_holding_abv |
482 unfolding wq_def |
482 unfolding wq_def |
483 by (simp) |
483 by (simp) |
484 |
484 |
485 text {* \noindent |
485 text {* \noindent |
486 Observation @{text "cntCS s th"} returns the number of resources held by thread @{text "th"} in |
|
487 state @{text "s"}: |
|
488 *} |
|
489 definition cntCS :: "state \<Rightarrow> thread \<Rightarrow> nat" |
|
490 where "cntCS s th = card (holdents s th)" |
|
491 |
|
492 text {* \noindent |
|
493 According to the convention of Paulson's inductive method, |
486 According to the convention of Paulson's inductive method, |
494 the decision made by a protocol that event @{text "e"} is eligible to happen next under state @{text "s"} |
487 the decision made by a protocol that event @{text "e"} is eligible to happen next under state @{text "s"} |
495 is expressed as @{text "step s e"}. The predicate @{text "step"} is inductively defined as |
488 is expressed as @{text "step s e"}. The predicate @{text "step"} is inductively defined as |
496 follows (notice how the decision is based on the {\em observation function}s |
489 follows (notice how the decision is based on the {\em observation function}s |
497 defined above, and also notice how a complicated protocol is modeled by a few simple |
490 defined above, and also notice how a complicated protocol is modeled by a few simple |
611 in list @{text "l"}: |
604 in list @{text "l"}: |
612 *} |
605 *} |
613 definition count :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat" |
606 definition count :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat" |
614 where "count Q l = length (filter Q l)" |
607 where "count Q l = length (filter Q l)" |
615 |
608 |
616 text {* \noindent |
609 text {* |
617 The following observation @{text "cntP s"} returns the number of operation @{text "P"} happened |
610 The operation @{term P} is used by a thread to request for resources, while |
618 before reaching state @{text "s"}. |
611 @{term V} is used to release. Therefore, the number of resources |
619 *} |
612 held by a thread roughly equals to the number of @{term P} it made minus |
|
613 the number of @{term V}. The equality is rough because the @{term P}-operation |
|
614 might be blocked and fail to give back the holding of the requested resource. |
|
615 In the following, @{text "cntP"} and @{text "cntV"} are the number of @{term P} |
|
616 and @{term "V"} respectively, while @{term cntCS} is the number |
|
617 resources held by a thread and @{text "pvD"} is introduced to account for |
|
618 the above mentioned situation when @{term P} is blocked, so that |
|
619 a equation between @{text cntP}, @{text "cntV"}, @{text "cntCS"} can be established |
|
620 (in the lemma named @{text "valid_trace.cnp_cnv_cncs"}). |
|
621 |
|
622 Such a equation, once established, is very handy, because the number of resources |
|
623 held by a thread can be calculated by counting the number of @{term P} and @{text V}, |
|
624 which is relatively easy. |
|
625 *} |
|
626 |
620 definition cntP :: "state \<Rightarrow> thread \<Rightarrow> nat" |
627 definition cntP :: "state \<Rightarrow> thread \<Rightarrow> nat" |
621 where "cntP s th = count (\<lambda> e. \<exists> cs. e = P th cs) s" |
628 where "cntP s th = count (\<lambda> e. \<exists> cs. e = P th cs) s" |
622 |
629 |
623 text {* \noindent |
|
624 The following observation @{text "cntV s"} returns the number of operation @{text "V"} happened |
|
625 before reaching state @{text "s"}. |
|
626 *} |
|
627 definition cntV :: "state \<Rightarrow> thread \<Rightarrow> nat" |
630 definition cntV :: "state \<Rightarrow> thread \<Rightarrow> nat" |
628 where "cntV s th = count (\<lambda> e. \<exists> cs. e = V th cs) s" |
631 where "cntV s th = count (\<lambda> e. \<exists> cs. e = V th cs) s" |
|
632 |
|
633 definition cntCS :: "state \<Rightarrow> thread \<Rightarrow> nat" |
|
634 where "cntCS s th = card (holdents s th)" |
629 |
635 |
630 definition "pvD s th = (if (th \<in> readys s \<or> th \<notin> threads s) then 0 else (1::nat))" |
636 definition "pvD s th = (if (th \<in> readys s \<or> th \<notin> threads s) then 0 else (1::nat))" |
631 |
637 |
632 text {* @{text "the_preced"} is also the same as @{text "preced"}, the only |
638 text {* @{text "the_preced"} is also the same as @{text "preced"}, the only |
633 difference is the order of arguemts. *} |
639 difference is the order of arguemts. *} |
634 definition "the_preced s th = preced th s" |
640 definition "the_preced s th = preced th s" |
635 |
|
636 |
641 |
637 text {* @{term "the_thread"} extracts thread out of RAG node. *} |
642 text {* @{term "the_thread"} extracts thread out of RAG node. *} |
638 fun the_thread :: "node \<Rightarrow> thread" where |
643 fun the_thread :: "node \<Rightarrow> thread" where |
639 "the_thread (Th th) = th" |
644 "the_thread (Th th) = th" |
640 |
645 |
661 lemma tRAG_alt_def: |
666 lemma tRAG_alt_def: |
662 "tRAG s = {(Th th1, Th th2) | th1 th2. |
667 "tRAG s = {(Th th1, Th th2) | th1 th2. |
663 \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}" |
668 \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}" |
664 by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def) |
669 by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def) |
665 |
670 |
666 definition "cp_gen s x = |
|
667 Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)" |
|
668 |
|
669 lemma cp_gen_alt_def: |
|
670 "cp_gen s = (Max \<circ> (\<lambda>x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x))" |
|
671 by (auto simp:cp_gen_def) |
|
672 |
|
673 |
|
674 (*<*) |
671 (*<*) |
675 |
672 |
676 end |
673 end |
677 (*>*) |
674 (*>*) |
678 |
675 |