--- 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 (\<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"}: *}
+ 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 \<Rightarrow> state \<Rightarrow> 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 \<Rightarrow> thread list) \<Rightarrow> thread \<Rightarrow> thread set"
@@ -233,7 +212,9 @@
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 {*
@@ -245,12 +226,18 @@
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
@@ -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) \<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))"
-
-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) \<equiv> 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 \<equiv> (th \<in> set (wq_fun (schs s) cs) \<and> th = hd (wq_fun (schs s) cs))"
- by (auto simp:s_holding_abv wq_def holding_raw_def)
+ "holding (s::state) th cs \<equiv> (th \<in> set (wq s cs) \<and> th = hd (wq s cs))"
+ 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))"
@@ -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 \<union> 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.
\<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