diff -r e3cf792db636 -r 0f124691c191 PIPDefs.thy --- a/PIPDefs.thy Tue Jun 14 15:06:16 2016 +0100 +++ b/PIPDefs.thy Fri Jun 17 09:46:25 2016 +0100 @@ -1,6 +1,6 @@ (*<*) theory PIPDefs -imports Precedence_ord RTree Max +imports Precedence_ord Max begin (*>*) @@ -8,8 +8,8 @@ text {* - In this section, the formal model of Priority Inheritance Protocol (PIP) - is presented. The model is based on Paulson's inductive protocol + In this chapter, the formal model of the Priority Inheritance Protocol + (PIP) is presented. The model is based on Paulson's inductive protocol verification method, where the state of the system is modelled as a list of events (trace) happened so far with the latest event put at the head. *} @@ -18,12 +18,12 @@ To define events, the identifiers of {\em threads}, {\em priority} and {\em critical resources } (abbreviated as @{text "cs"}) need to be - represented. All three are represetned using standard Isabelle/HOL type + represented. All three are represented using standard Isabelle/HOL type @{typ "nat"}: *} -type_synonym thread = nat -- {* Type for thread identifiers. *} +type_synonym thread = nat -- {* Type for thread identifiers. *} type_synonym priority = nat -- {* Type for priorities. *} -type_synonym cs = nat -- {* Type for critical sections (or critical resources). *} +type_synonym cs = nat -- {* Type for critical sections (or critical resources). *} text {* @@ -38,33 +38,13 @@ | V thread cs -- {* Thread @{text "thread"} releasing critical resource @{text "cs"}. *} | Set thread priority -- {* Thread @{text "thread"} resets its priority to @{text "priority"}. *} -fun actor where - "actor (Exit th) = th" | - "actor (P th cs) = th" | - "actor (V th cs) = th" | - "actor (Set th pty) = th" | - "actor (Create th prio) = th" --- {* The actions of a set of threads *} -definition "actions_of ths s = filter (\ e. actor e \ ths) s" - -fun isCreate :: "event \ bool" where - "isCreate (Create th pty) = True" | - "isCreate _ = False" - -fun isP :: "event \ bool" where - "isP (P th cs) = True" | - "isP _ = False" - -fun isV :: "event \ bool" where - "isV (V th cs) = True" | - "isV _ = False" text {* - As mentioned earlier, in Paulson's inductive method, the states of system - are represented as lists of events, which is defined by the following type - @{text "state"}: *} + As mentioned earlier, in Paulson's inductive method, the states of the + system are represented as lists of events, which is defined by the + following type @{text "state"}: *} type_synonym state = "event list" @@ -91,7 +71,7 @@ function}s which forms the very basis of Paulson's inductive protocol verification method. Each observation function {\em observes} one particular aspect (or attribute) of the system. For example, the attribute - observed by @{text "threads s"} is the set of threads living in state + observed by @{text "threads s"} is the set of threads being live in state @{text "s"}. The protocol being modelled The decision made the protocol being modelled is based on the {\em observation}s returned by {\em observation function}s. Since {\observation function}s forms the very @@ -102,11 +82,10 @@ text {* - \noindent Observation @{text "priority th s"} is the {\em original - priority} of thread @{text "th"} in state @{text "s"}. The {\em original - priority} is the priority assigned to a thread when it is created or when - it is reset by system call (represented by event @{text "Set thread - priority"}). *} + Observation @{text "priority th s"} is the {\em original priority} of + thread @{text "th"} in state @{text "s"}. The {\em original priority} is + the priority assigned to a thread when it is created or when it is reset + by system call (represented by event @{text "Set thread priority"}). *} fun priority :: "thread \ state \ priority" where @@ -209,10 +188,10 @@ text {* - \begin{minipage}{0.9\textwidth} The following @{text "dependants wq th"} - represents the set of threads which are RAGing on thread @{text "th"} in - Resource Allocation Graph @{text "RAG wq"}. Here, "RAGing" means waiting - directly or indirectly on the critical resource. \end{minipage} *} + \noindent The following @{text "dependants wq th"} represents the set of + threads which are waiting on thread @{text "th"} in Resource Allocation + Graph @{text "RAG wq"}. Here, "waiting" means waiting directly or + indirectly on the critical resource. *} definition dependants_raw :: "(cs \ thread list) \ thread \ thread set" @@ -233,7 +212,9 @@ definition cpreced :: "(cs \ thread list) \ state \ thread \ precedence" where - "cpreced wq s th = Max ((\th'. preced th' s) ` ({th} \ dependants_raw wq th))" + "cpreced wq s th \ Max ({preced th s} \ preceds (dependants_raw wq th) s)" + + text {* @@ -245,12 +226,18 @@ from. *} lemma cpreced_def2: - "cpreced wq s th \ Max ({preced th s} \ preceds (dependants_raw wq th) s)" + "cpreced wq s th \ Max ((\th'. preced th' s) ` ({th} \ dependants_raw wq th))" unfolding cpreced_def image_def preceds_def apply(rule eq_reflection) apply(rule_tac f="Max" in arg_cong) by (auto) +definition + cpreceds :: "(cs \ thread list) \ state \ thread set \ precedence set" + where + "cpreceds wq s ths \ {cpreced wq s th | th. th \ ths}" + + text {* \noindent Assuming @{text "qs"} be the waiting queue of a critical @@ -392,7 +379,7 @@ apply(rule ext) apply(simp add: cpreced_def) apply(simp add: dependants_raw_def RAG_raw_def waiting_raw_def holding_raw_def) -apply(simp add: preced_def) +apply(simp add: preced_def preceds_def) done text {* @@ -420,37 +407,19 @@ definition s_holding_abv: - "holding (s::state) \ holding_raw (wq_fun (schs s))" + "holding (s::state) \ holding_raw (wq s)" definition s_waiting_abv: - "waiting (s::state) \ waiting_raw (wq_fun (schs s))" + "waiting (s::state) \ waiting_raw (wq s)" definition s_RAG_abv: - "RAG (s::state) \ RAG_raw (wq_fun (schs s))" + "RAG (s::state) \ RAG_raw (wq s)" definition s_dependants_abv: - "dependants (s::state) \ dependants_raw (wq_fun (schs s))" - -text {* - - The following four lemmas relate the @{term wq} and non-@{term wq} - versions of @{term waiting}, @{term holding}, @{term dependants} and - @{term cp}. *} - -lemma waiting_eq: - shows "waiting s th cs = waiting_raw (wq s) th cs" - by (simp add: s_waiting_abv wq_def) - -lemma holding_eq: - shows "holding s th cs = holding_raw (wq s) th cs" - by (simp add: s_holding_abv wq_def) - -lemma eq_dependants: - shows "dependants_raw (wq s) = dependants s" - by (simp add: s_dependants_abv wq_def) + "dependants (s::state) \ dependants_raw (wq s)" lemma cp_eq: shows "cp s th = cpreced (wq s) s th" @@ -472,8 +441,8 @@ lemma s_holding_def: - "holding (s::state) th cs \ (th \ set (wq_fun (schs s) cs) \ th = hd (wq_fun (schs s) cs))" - by (auto simp:s_holding_abv wq_def holding_raw_def) + "holding (s::state) th cs \ (th \ set (wq s cs) \ th = hd (wq s cs))" + by(simp add: s_holding_abv holding_raw_def) lemma s_waiting_def: "waiting (s::state) th cs \ (th \ set (wq_fun (schs s) cs) \ th \ hd (wq_fun (schs s) cs))" @@ -721,14 +690,37 @@ text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *} lemma RAG_split: "RAG s = (wRAG s \ hRAG s)" - by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv - s_holding_abv RAG_raw_def, auto) +using hRAG_def s_RAG_def s_holding_abv s_waiting_abv wRAG_def wq_def by auto lemma tRAG_alt_def: "tRAG s = {(Th th1, Th th2) | th1 th2. \ cs. (Th th1, Cs cs) \ RAG s \ (Cs cs, Th th2) \ RAG s}" by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def) + +fun actor where + "actor (Exit th) = th" | + "actor (P th cs) = th" | + "actor (V th cs) = th" | + "actor (Set th pty) = th" | + "actor (Create th prio) = th" + +-- {* The actions of a set of threads *} +definition "actions_of ths s = filter (\ e. actor e \ ths) s" + +fun isCreate :: "event \ bool" where + "isCreate (Create th pty) = True" | + "isCreate _ = False" + +fun isP :: "event \ bool" where + "isP (P th cs) = True" | + "isP _ = False" + +fun isV :: "event \ bool" where + "isV (V th cs) = True" | + "isV _ = False" + + (*<*) end