pip: comparison PIPDefs.thy

equal deleted inserted replaced

-:e3cf792db636
+:0f124691c191
 (*<*)
 theory PIPDefs
-imports Precedence_ord RTree Max
+imports Precedence_ord Max
 begin
 (*>*)
 chapter {* Definitions *}
 text {*
-In this section, the formal model of Priority Inheritance Protocol (PIP)
+In this chapter, the formal model of the Priority Inheritance Protocol
-is presented. The model is based on Paulson's inductive 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.
 *}
 text {*
 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 {*
 \noindent The abstraction of Priority Inheritance Protocol (PIP) is set at
 the system call level. Every system call is represented as an event. The
 | Exit thread              -- {* Thread @{text "thread"} finishing its execution. *}
 | P thread cs              -- {* Thread @{text "thread"} requesting critical resource @{text "cs"}. *}
 | 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" |
+text {*
-"actor (V th cs) = th" |
-"actor (Set th pty) = th" |
+As mentioned earlier, in Paulson's inductive method, the states of the
-"actor (Create th prio) = th"
+system are represented as lists of events, which is defined by the
+following type @{text "state"}: *}
--- {* The actions of a set of threads *}
-definition "actions_of ths s = filter (\<lambda> e. actor e \<in> ths) s"
-fun isCreate :: "event \<Rightarrow> bool" where
-"isCreate (Create th pty) = True" |
-"isCreate _ = False"
-fun isP :: "event \<Rightarrow> bool" where
-"isP (P th cs) = True" |
-"isP _ = False"
-fun isV :: "event \<Rightarrow> 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"}: *}
 type_synonym state = "event list"
 text {*
 \noindent The function @{text "threads"} is one of the {\em observation
 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
 basis on which Paulson's inductive method is based, there will be a lot of
 such observation functions introduced in the following. In fact, any
 function which takes event list as argument is a {\em observation
 function}. *}
 text {*
-\noindent Observation @{text "priority th s"} is the {\em original
+Observation @{text "priority th s"} is the {\em original priority} of
-priority} of thread @{text "th"} in state @{text "s"}. The {\em original
+thread @{text "th"} in state @{text "s"}. The {\em original priority} is
-priority} is the priority assigned to a thread when it is created or when
+the priority assigned to a thread when it is created or when it is reset
-it is reset by system call (represented by event @{text "Set thread
+by system call (represented by event @{text "Set thread priority"}). *}
-priority"}). *}
 fun priority :: "thread \<Rightarrow> state \<Rightarrow> priority"
 where
 -- {* @{text "0"} is assigned to threads which have never been created: *}
 "priority th [] = 0" |
 {(Th th, Cs cs) | th cs. waiting_raw wq th cs} \<union>
 {(Cs cs, Th th) | cs th. holding_raw wq th cs}"
 text {*
-\begin{minipage}{0.9\textwidth} The following @{text "dependants wq th"}
+\noindent The following @{text "dependants wq th"} represents the set of
-represents the set of threads which are RAGing on thread @{text "th"} in
+threads which are waiting on thread @{text "th"} in Resource Allocation
-Resource Allocation Graph @{text "RAG wq"}. Here, "RAGing" means waiting
+Graph @{text "RAG wq"}. Here, "waiting" means waiting directly or
-directly or indirectly on the critical resource. \end{minipage} *}
+indirectly on the critical resource. *}
 definition
 dependants_raw :: "(cs \<Rightarrow> thread list) \<Rightarrow> thread \<Rightarrow> thread set"
 where
 "dependants_raw wq th \<equiv> {th' . (Th th', Th th) \<in> (RAG_raw wq)^+}"
 precedence, i.e. @{text "preced th s"}. *}
 definition
 cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"
 where
-"cpreced wq s th = Max ((\<lambda>th'. preced th' s) ` ({th} \<union> dependants_raw wq th))"
+"cpreced wq s th \<equiv> Max ({preced th s} \<union> preceds (dependants_raw wq th) s)"
 text {*
 Notice that the current precedence (@{text "cpreced"}) of one thread
 @{text "th"} can be boosted (increased) by those threads in the @{text
 the priority (or, more precisely, the precedence) of its dependants. This
 is whrere the word "Inheritance" in Priority Inheritance Protocol comes
 from. *}
 lemma cpreced_def2:
-"cpreced wq s th \<equiv> Max ({preced th s} \<union> preceds (dependants_raw wq th) s)"
+"cpreced wq s th \<equiv> Max ((\<lambda>th'. preced th' s) ` ({th} \<union> 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 \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread set \<Rightarrow> precedence set"
+where
+"cpreceds wq s ths \<equiv> {cpreced wq s th | th. th \<in> ths}"
 text {*
 \noindent Assuming @{text "qs"} be the waiting queue of a critical
 resource, the following abbreviation "release qs" is the waiting queue
 lemma cpreced_initial:
 "cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))"
 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 {*
 \noindent The following @{text "wq"} is a shorthand for @{text "wq_fun"}.
 that they no longer RAG on the fictitious {\em waiting queue function}
 @{text "wq"}, but on system state @{text "s"}. *}
 definition
 s_holding_abv:
-"holding (s::state) \<equiv> holding_raw (wq_fun (schs s))"
+"holding (s::state) \<equiv> holding_raw (wq s)"
 definition
 s_waiting_abv:
-"waiting (s::state) \<equiv> waiting_raw (wq_fun (schs s))"
+"waiting (s::state) \<equiv> waiting_raw (wq s)"
 definition
 s_RAG_abv:
-"RAG (s::state) \<equiv> RAG_raw (wq_fun (schs s))"
+"RAG (s::state) \<equiv> RAG_raw (wq s)"
 definition
 s_dependants_abv:
-"dependants (s::state) \<equiv> dependants_raw (wq_fun (schs s))"
+"dependants (s::state) \<equiv> dependants_raw (wq 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)
 lemma cp_eq:
 shows "cp s th = cpreced (wq s) s th"
 unfolding cp_def wq_def
 apply(induct s rule: schs.induct)
 The following lemma can be proved easily, and the meaning is obvious. *}
 lemma
 s_holding_def:
-"holding (s::state) th cs \<equiv> (th \<in> set (wq_fun (schs s) cs) \<and> th = hd (wq_fun (schs s) cs))"
+"holding (s::state) th cs \<equiv> (th \<in> set (wq s cs) \<and> th = hd (wq s cs))"
-by (auto simp:s_holding_abv wq_def holding_raw_def)
+by(simp add: s_holding_abv holding_raw_def)
 lemma s_waiting_def:
 "waiting (s::state) th cs \<equiv> (th \<in> set (wq_fun (schs s) cs) \<and> th \<noteq> hd (wq_fun (schs s) cs))"
 by (auto simp:s_waiting_abv wq_def waiting_raw_def)
 definition "tRAG s = wRAG s O hRAG s"
 text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *}
 lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)"
-by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv
+using hRAG_def s_RAG_def s_holding_abv s_waiting_abv wRAG_def wq_def by auto
-s_holding_abv RAG_raw_def, auto)
 lemma tRAG_alt_def:
 "tRAG s = {(Th th1, Th th2) | th1 th2.
 \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> 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 (\<lambda> e. actor e \<in> ths) s"
+fun isCreate :: "event \<Rightarrow> bool" where
+"isCreate (Create th pty) = True" |
+"isCreate _ = False"
+fun isP :: "event \<Rightarrow> bool" where
+"isP (P th cs) = True" |
+"isP _ = False"
+fun isV :: "event \<Rightarrow> bool" where
+"isV (V th cs) = True" |
+"isV _ = False"
 (*<*)
 end
 (*>*)

changeset 130	0f124691c191
parent 129	e3cf792db636
child 136	fb3f52fe99d1