--- a/prio/CpsG.thy Sat Feb 11 19:39:50 2012 +0000
+++ b/prio/CpsG.thy Sun Feb 12 04:45:20 2012 +0000
@@ -4,14 +4,14 @@
lemma not_thread_holdents:
fixes th s
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and not_in: "th \<notin> threads s"
shows "holdents s th = {}"
proof -
from vt not_in show ?thesis
proof(induct arbitrary:th)
case (vt_cons s e th)
- assume vt: "vt step s"
+ assume vt: "vt s"
and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> holdents s th = {}"
and stp: "step s e"
and not_in: "th \<notin> threads (e # s)"
@@ -49,7 +49,7 @@
case (thread_P thread cs)
assume eq_e: "e = P thread cs"
and is_runing: "thread \<in> runing s"
- from prems have vtp: "vt step (P thread cs#s)" by auto
+ from prems have vtp: "vt (P thread cs#s)" by auto
have neq_th: "th \<noteq> thread"
proof -
from not_in eq_e have "th \<notin> threads s" by simp
@@ -77,10 +77,10 @@
by (simp add:runing_def readys_def)
ultimately show ?thesis by auto
qed
- from prems have vtv: "vt step (V thread cs#s)" by auto
+ from prems have vtv: "vt (V thread cs#s)" by auto
from hold obtain rest
where eq_wq: "wq s cs = thread # rest"
- by (case_tac "wq s cs", auto simp:s_holding_def)
+ by (case_tac "wq s cs", auto simp: wq_def s_holding_def)
from not_in eq_e eq_wq
have "\<not> next_th s thread cs th"
apply (auto simp:next_th_def)
@@ -128,7 +128,7 @@
lemma next_th_neq:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and nt: "next_th s th cs th'"
shows "th' \<noteq> th"
proof -
@@ -167,7 +167,7 @@
by auto
lemma wf_depend:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "wf (depend s)"
proof(rule finite_acyclic_wf)
from finite_depend[OF vt] show "finite (depend s)" .
@@ -256,7 +256,7 @@
by (unfold children_def child_def cs_dependents_def, auto simp:eq_depend)
lemma child_unique:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and ch1: "(Th th, Th th1) \<in> child s"
and ch2: "(Th th, Th th2) \<in> child s"
shows "th1 = th2"
@@ -329,7 +329,7 @@
by (unfold child_def, auto)
lemma wf_child:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "wf (child s)"
proof(rule wf_subset)
from wf_trancl[OF wf_depend[OF vt]]
@@ -339,7 +339,7 @@
qed
lemma depend_child_pre:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows
"(Th th, n) \<in> (depend s)^+ \<longrightarrow> (\<forall> th'. n = (Th th') \<longrightarrow> (Th th, Th th') \<in> (child s)^+)" (is "?P n")
proof -
@@ -371,7 +371,7 @@
qed
qed
-lemma depend_child: "\<lbrakk>vt step s; (Th th, Th th') \<in> (depend s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"
+lemma depend_child: "\<lbrakk>vt s; (Th th, Th th') \<in> (depend s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"
by (insert depend_child_pre, auto)
lemma child_depend_p:
@@ -392,7 +392,7 @@
qed
lemma child_depend_eq:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows
"((Th th1, Th th2) \<in> (child s)^+) =
((Th th1, Th th2) \<in> (depend s)^+)"
@@ -400,7 +400,7 @@
lemma children_no_dep:
fixes s th th1 th2 th3
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and ch1: "(Th th1, Th th) \<in> child s"
and ch2: "(Th th2, Th th) \<in> child s"
and ch3: "(Th th1, Th th2) \<in> (depend s)^+"
@@ -433,7 +433,7 @@
qed
lemma unique_depend_p:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and dp1: "(n, n1) \<in> (depend s)^+"
and dp2: "(n, n2) \<in> (depend s)^+"
and neq: "n1 \<noteq> n2"
@@ -445,7 +445,7 @@
lemma dependents_child_unique:
fixes s th th1 th2 th3
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and ch1: "(Th th1, Th th) \<in> child s"
and ch2: "(Th th2, Th th) \<in> child s"
and dp1: "th3 \<in> dependents s th1"
@@ -472,7 +472,7 @@
lemma cp_rec:
fixes s th
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"
proof(unfold cp_eq_cpreced_f cpreced_def)
let ?f = "(\<lambda>th. preced th s)"
@@ -625,7 +625,7 @@
locale step_set_cps =
fixes s' th prio s
defines s_def : "s \<equiv> (Set th prio#s')"
- assumes vt_s: "vt step s"
+ assumes vt_s: "vt s"
context step_set_cps
begin
@@ -936,12 +936,12 @@
end
lemma next_waiting:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and nxt: "next_th s th cs th'"
shows "waiting s th' cs"
proof -
from assms show ?thesis
- apply (auto simp:next_th_def s_waiting_def)
+ apply (auto simp:next_th_def s_waiting_def[folded wq_def])
proof -
fix rest
assume ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
@@ -994,7 +994,7 @@
locale step_v_cps =
fixes s' th cs s
defines s_def : "s \<equiv> (V th cs#s')"
- assumes vt_s: "vt step s"
+ assumes vt_s: "vt s"
locale step_v_cps_nt = step_v_cps +
fixes th'
@@ -1054,7 +1054,7 @@
proof -
from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
have "(Th th', Cs cs) \<in> depend s'"
- by (auto simp:s_waiting_def s_depend_def cs_waiting_def)
+ by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)
from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this dp']
show ?thesis by simp
qed
@@ -1072,7 +1072,7 @@
proof -
from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
have "(Th th', Cs cs) \<in> depend s'"
- by (auto simp:s_waiting_def s_depend_def cs_waiting_def)
+ by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)
from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] dps' this]
show ?thesis .
qed
@@ -1115,7 +1115,7 @@
proof -
from step_back_step[OF vt_s[unfolded s_def]]
have "(Cs cs, Th th) \<in> depend s'"
- by(cases, auto simp: s_depend_def cs_holding_def s_holding_def)
+ by(cases, auto simp: wq_def s_depend_def cs_holding_def s_holding_def)
from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this dp_yz]
show ?thesis by simp
qed
@@ -1126,7 +1126,7 @@
have "th \<in> readys s'" by (cases, simp add:runing_def)
moreover note eq_z
ultimately show False
- by (auto simp:readys_def s_depend_def s_waiting_def cs_waiting_def)
+ by (auto simp:readys_def wq_def s_depend_def s_waiting_def cs_waiting_def)
qed
next
show "y \<noteq> Th th'"
@@ -1137,14 +1137,14 @@
proof -
from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
have "(Th th', Cs cs) \<in> depend s'"
- by (auto simp:s_waiting_def s_depend_def cs_waiting_def)
+ by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)
from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] dps this]
show ?thesis .
qed
with ztp have cs_i: "(Cs cs, Th th'') \<in> (depend s')\<^sup>+" by simp
from step_back_step[OF vt_s[unfolded s_def]]
have cs_th: "(Cs cs, Th th) \<in> depend s'"
- by(cases, auto simp: s_depend_def cs_holding_def s_holding_def)
+ by(cases, auto simp: s_depend_def wq_def cs_holding_def s_holding_def)
have "(Cs cs, Th th'') \<notin> depend s'"
proof
assume "(Cs cs, Th th'') \<in> depend s'"
@@ -1165,7 +1165,7 @@
moreover from step_back_step[OF vt_s[unfolded s_def]]
have "th \<in> readys s'" by (cases, simp add:runing_def)
ultimately show False
- by (auto simp:readys_def s_depend_def s_waiting_def cs_waiting_def)
+ by (auto simp:readys_def wq_def s_depend_def s_waiting_def cs_waiting_def)
qed
qed
with depend_s yz have "(y, z) \<in> depend s" by auto
@@ -1223,7 +1223,7 @@
assume "holding s' th cs"
then obtain rest where
eq_wq: "wq s' cs = th#rest"
- apply (unfold s_holding_def)
+ apply (unfold s_holding_def wq_def[symmetric])
by (case_tac "(wq s' cs)", auto)
with h1 h2 have ne: "rest \<noteq> []" by auto
with eq_wq
@@ -1351,7 +1351,7 @@
locale step_P_cps =
fixes s' th cs s
defines s_def : "s \<equiv> (P th cs#s')"
- assumes vt_s: "vt step s"
+ assumes vt_s: "vt s"
locale step_P_cps_ne =step_P_cps +
assumes ne: "wq s' cs \<noteq> []"
@@ -1814,7 +1814,7 @@
locale step_create_cps =
fixes s' th prio s
defines s_def : "s \<equiv> (Create th prio#s')"
- assumes vt_s: "vt step s"
+ assumes vt_s: "vt s"
context step_create_cps
begin
@@ -1902,7 +1902,7 @@
locale step_exit_cps =
fixes s' th prio s
defines s_def : "s \<equiv> (Exit th#s')"
- assumes vt_s: "vt step s"
+ assumes vt_s: "vt s"
context step_exit_cps
begin
@@ -1930,7 +1930,7 @@
assume "th \<in> runing s'"
with bk show ?thesis
apply (unfold runing_def readys_def s_waiting_def s_depend_def)
- by (auto simp:cs_waiting_def)
+ by (auto simp:cs_waiting_def wq_def)
qed
qed
have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
--- a/prio/ExtGG.thy Sat Feb 11 19:39:50 2012 +0000
+++ b/prio/ExtGG.thy Sun Feb 12 04:45:20 2012 +0000
@@ -29,7 +29,7 @@
locale highest_gen =
fixes s th prio tm
- assumes vt_s: "vt step s"
+ assumes vt_s: "vt s"
and threads_s: "th \<in> threads s"
and highest: "preced th s = Max ((cp s)`threads s)"
and preced_th: "preced th s = Prc prio tm"
@@ -88,14 +88,14 @@
locale extend_highest_gen = highest_gen +
fixes t
- assumes vt_t: "vt step (t@s)"
+ assumes vt_t: "vt (t@s)"
and create_low: "Create th' prio' \<in> set t \<Longrightarrow> prio' \<le> prio"
and set_diff_low: "Set th' prio' \<in> set t \<Longrightarrow> th' \<noteq> th \<and> prio' \<le> prio"
and exit_diff: "Exit th' \<in> set t \<Longrightarrow> th' \<noteq> th"
lemma step_back_vt_app:
- assumes vt_ts: "vt cs (t@s)"
- shows "vt cs s"
+ assumes vt_ts: "vt (t@s)"
+ shows "vt s"
proof -
from vt_ts show ?thesis
proof(induct t)
@@ -103,13 +103,13 @@
from Nil show ?case by auto
next
case (Cons e t)
- assume ih: " vt cs (t @ s) \<Longrightarrow> vt cs s"
- and vt_et: "vt cs ((e # t) @ s)"
+ assume ih: " vt (t @ s) \<Longrightarrow> vt s"
+ and vt_et: "vt ((e # t) @ s)"
show ?case
proof(rule ih)
- show "vt cs (t @ s)"
+ show "vt (t @ s)"
proof(rule step_back_vt)
- from vt_et show "vt cs (e # t @ s)" by simp
+ from vt_et show "vt (e # t @ s)" by simp
qed
qed
qed
@@ -127,7 +127,7 @@
lemma ind [consumes 0, case_names Nil Cons, induct type]:
assumes
h0: "R []"
- and h2: "\<And> e t. \<lbrakk>vt step (t@s); step (t@s) e;
+ and h2: "\<And> e t. \<lbrakk>vt (t@s); step (t@s) e;
extend_highest_gen s th prio tm t;
extend_highest_gen s th prio tm (e#t); R t\<rbrakk> \<Longrightarrow> R (e#t)"
shows "R t"
@@ -137,11 +137,11 @@
from h0 show "R []" .
next
case (Cons e t')
- assume ih: "\<lbrakk>vt step (t' @ s); extend_highest_gen s th prio tm t'\<rbrakk> \<Longrightarrow> R t'"
- and vt_e: "vt step ((e # t') @ s)"
+ assume ih: "\<lbrakk>vt (t' @ s); extend_highest_gen s th prio tm t'\<rbrakk> \<Longrightarrow> R t'"
+ and vt_e: "vt ((e # t') @ s)"
and et: "extend_highest_gen s th prio tm (e # t')"
from vt_e and step_back_step have stp: "step (t'@s) e" by auto
- from vt_e and step_back_vt have vt_ts: "vt step (t'@s)" by auto
+ from vt_e and step_back_vt have vt_ts: "vt (t'@s)" by auto
show ?case
proof(rule h2 [OF vt_ts stp _ _ _ ])
show "R t'"
@@ -149,7 +149,7 @@
from et show ext': "extend_highest_gen s th prio tm t'"
by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt)
next
- from vt_ts show "vt step (t' @ s)" .
+ from vt_ts show "vt (t' @ s)" .
qed
next
from et show "extend_highest_gen s th prio tm (e # t')" .
@@ -264,7 +264,7 @@
by (unfold eq_e, simp)
moreover have "\<dots> = max (?f thread) (Max (?f ` (threads (t@s))))"
proof(rule Max_insert)
- from Cons have "vt step (t @ s)" by auto
+ from Cons have "vt (t @ s)" by auto
from finite_threads[OF this]
show "finite (?f ` (threads (t@s)))" by simp
next
@@ -310,7 +310,7 @@
next
case (Exit thread)
assume eq_e: "e = Exit thread"
- from Cons have vt_e: "vt step (e#(t @ s))" by auto
+ from Cons have vt_e: "vt (e#(t @ s))" by auto
from Cons and eq_e have stp: "step (t@s) (Exit thread)" by auto
from stp have thread_ts: "thread \<in> threads (t @ s)"
by(cases, unfold runing_def readys_def, auto)
@@ -353,7 +353,7 @@
(is "?t = Max (?g ` ?B)") by simp
moreover have "?g thread \<le> \<dots>"
proof(rule Max_ge)
- have "vt step (t@s)" by fact
+ have "vt (t@s)" by fact
from finite_threads [OF this]
show "finite (?g ` ?B)" by simp
next
@@ -428,7 +428,7 @@
next
show "finite ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))"
proof -
- from Cons have "vt step (t @ s)" by auto
+ from Cons have "vt (t @ s)" by auto
from finite_threads[OF this] show ?thesis by auto
qed
qed
@@ -601,7 +601,7 @@
show ?case
proof(cases e)
case (V thread cs)
- from Cons and V have vt_v: "vt step (V thread cs#(t@s))" by auto
+ from Cons and V have vt_v: "vt (V thread cs#(t@s))" by auto
show ?thesis
proof -
@@ -729,7 +729,7 @@
by blast
from red_moment[of "Suc(i+k)"]
and eq_me have "extend_highest_gen s th prio tm (e # moment (i + k) t)" by simp
- hence vt_e: "vt step (e#(moment (i + k) t)@s)"
+ hence vt_e: "vt (e#(moment (i + k) t)@s)"
by (unfold extend_highest_gen_def extend_highest_gen_axioms_def
highest_gen_def, auto)
have not_runing': "th' \<notin> runing (moment (i + k) t @ s)"
@@ -847,7 +847,7 @@
eq_me: "moment (Suc i) t = e # moment i t" by blast
from red_moment[of "Suc i"] and eq_me
have "extend_highest_gen s th prio tm (e # moment i t)" by simp
- hence vt_e: "vt step (e#(moment i t)@s)"
+ hence vt_e: "vt (e#(moment i t)@s)"
by (unfold extend_highest_gen_def extend_highest_gen_axioms_def
highest_gen_def, auto)
from step_back_step[OF this] have stp_i: "step (moment i t @ s) e" .
@@ -858,7 +858,7 @@
have "cntP (moment i t@s) th' = cntV (moment i t@s) th'"
proof(rule cnp_cnv_eq)
from step_back_vt [OF vt_e]
- show "vt step (moment i t @ s)" .
+ show "vt (moment i t @ s)" .
next
from eq_e and stp_i
have "step (moment i t @ s) (Create th' prio)" by simp
--- a/prio/Paper/Paper.thy Sat Feb 11 19:39:50 2012 +0000
+++ b/prio/Paper/Paper.thy Sun Feb 12 04:45:20 2012 +0000
@@ -23,6 +23,8 @@
preced ("prec") and
cpreced ("cprec") and
dependents ("dependants") and
+ cp ("cprec") and
+ holdents ("resources") and
DUMMY ("\<^raw:\mbox{$\_\!\_$}>")
(*>*)
@@ -165,7 +167,7 @@
later to the case of PIP on multi-processor systems.} Our model of
PIP is based on Paulson's inductive approach to protocol
verification \cite{Paulson98}, where the \emph{state} of a system is
- given by a list of events that happened so far. \emph{Events} in PIP fall
+ given by a list of events that happened so far. \emph{Events} of PIP fall
into five categories defined as the datatype:
\begin{isabelle}\ \ \ \ \ %%%
@@ -184,7 +186,7 @@
as natural numbers. The event @{term Set} models the situation that
a thread obtains a new priority given by the programmer or
user (for example via the {\tt nice} utility under UNIX). As in Paulson's work, we
- need to define functions that allow one to make some observations
+ need to define functions that allow us to make some observations
about states. One, called @{term threads}, calculates the set of
``live'' threads that we have seen so far:
@@ -256,7 +258,7 @@
Next, we introduce the concept of \emph{waiting queues}. They are
lists of threads associated with every resource. The first thread in
- this list (the head, or short @{term hd}) is chosen to be the one
+ this list (i.e.~the head, or short @{term hd}) is chosen to be the one
that is in possession of the
``lock'' of the corresponding resource. We model waiting queues as
functions, below abbreviated as @{text wq}. They take a resource as
@@ -273,8 +275,8 @@
\noindent
In this definition we assume @{text "set"} converts a list into a set.
- At the beginning, that is in the state where no process is created yet,
- the waiting queue function will be the function that just returns the
+ At the beginning, that is in the state where no thread is created yet,
+ the waiting queue function will be the function that returns the
empty list for every resource.
\begin{isabelle}\ \ \ \ \ %%%
@@ -302,7 +304,7 @@
\end{isabelle}
\noindent
- An instance of a RAG is as follows:
+ Given three threads and three resources, an instance of a RAG is as follows:
\begin{center}
\newcommand{\fnt}{\fontsize{7}{8}\selectfont}
@@ -314,13 +316,15 @@
\node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}};
\node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}};
\node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}};
+ \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}};
\node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};
\draw [->,line width=0.6mm] (A) to node [pos=0.45,sloped,above=-0.5mm] {\fnt{}holding} (B);
\draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting} (B);
- \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting} (B);
- \draw [->,line width=0.6mm] (D) to node [pos=0.45,sloped,above=-0.5mm] {\fnt{}holding} (E);
- \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,above=-0.5mm] {\fnt{}waiting} (E);
+ \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waiting} (B);
+ \draw [->,line width=0.6mm] (D) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}holding} (E);
+ \draw [->,line width=0.6mm] (D) to node [pos=0.45,sloped,above=-0.5mm] {\fnt{}holding} (E1);
+ \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting} (E);
\end{tikzpicture}
\end{center}
@@ -335,17 +339,18 @@
\noindent
This definition needs to account for all threads that wait for a thread to
release a resource. This means we need to include threads that transitively
- wait for a resource being released (in the picture above this means also @{text "th\<^isub>3"},
- which cannot make any progress unless @{text "th\<^isub>2"} makes progress which
- in turn needs to wait for @{text "th\<^isub>1"}). If there is a circle in a RAG, then clearly
+ wait for a resource being released (in the picture above this means the dependants
+ of @{text "th\<^isub>0"} are @{text "th\<^isub>1"} and @{text "th\<^isub>2"}, but also @{text "th\<^isub>3"},
+ which cannot make any progress unless @{text "th\<^isub>2"} makes progress, which
+ in turn needs to wait for @{text "th\<^isub>1"} to finish). If there is a circle in a RAG, then clearly
we have a deadlock. Therefore when a thread requests a resource,
- we must ensure that the resulting RAG is not not circular.
+ we must ensure that the resulting RAG is not circular.
- Next we introduce the notion of the \emph{current precedence} for a thread @{text th} in a
- state @{text s}, which is defined as
+ Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a
+ state @{text s}. It is defined as
\begin{isabelle}\ \ \ \ \ %%%
- @{thm cpreced_def2}
+ @{thm cpreced_def2}\numbered{permprops}
\end{isabelle}
\noindent
@@ -359,9 +364,9 @@
problem in the algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
lowered prematurely.
- The next function, called @{term schs}, defines the behaviour of the scheduler. It is defined
- by recursion on the state (a list of events); @{term "schs"} takes a state as argument
- and returns a \emph{schedule state}, which we define as a record consisting of two
+ The next function, called @{term schs}, defines the behaviour of the scheduler. It will be defined
+ by recursion on the state (a list of events); @{term "schs"} returns a \emph{schedule state}, which
+ we represent as a record consisting of two
functions:
\begin{isabelle}\ \ \ \ \ %%%
@@ -369,13 +374,14 @@
\end{isabelle}
\noindent
- The first is a waiting queue function (that is takes a @{text "cs"} and returns the
+ The first function is a waiting queue function (that is takes a @{text "cs"} and returns the
corresponding list of threads that wait for it), the second is a function that takes
- a thread and returns its current precedence (see ???). We have the usual getter and
+ a thread and returns its current precedence (see ???). We assume the usual getter and
setter methods for such records.
In the initial state, the scheduler starts with all resources unlocked and the
- precedence of every thread is initialised with @{term "Prc 0 0"}. Therefore
+ current precedence of every thread is initialised with @{term "Prc 0 0"}; that means
+ @{abbrev initial_cprec}. Therefore
we have
\begin{isabelle}\ \ \ \ \ %%%
@@ -388,15 +394,16 @@
\noindent
The cases for @{term Create}, @{term Exit} and @{term Set} are also straightforward:
we calculate the waiting queue function of the (previous) state @{text s};
- this waiting queue function @{text wq} is unchanged in the next schedule state;
+ this waiting queue function @{text wq} is unchanged in the next schedule state---because
+ none of these events lock or release any resources;
for calculating the next @{term "cprec_fun"}, we use @{text wq} and the function
- @{term cpreced}. This gives the following three clauses:
+ @{term cpreced}. This gives the following three clauses for @{term schs}:
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@{thm (lhs) schs.simps(2)} @{text "\<equiv>"}\\
\hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
- \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Create th prio # s)|)"}\\
+ \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Create th prio # s)|)"}\smallskip\\
@{thm (lhs) schs.simps(3)} @{text "\<equiv>"}\\
\hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
\hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Exit th # s)|)"}\smallskip\\
@@ -408,9 +415,9 @@
\noindent
More interesting are the cases when a resource, say @{text cs}, is locked or released. In this case
- we need to calculate a new waiting queue function. In case of @{term P}, we update
+ we need to calculate a new waiting queue function. For the event @{term P}, we have to update
the function so that the new thread list for @{text cs} is old thread list plus the thread @{text th}
- appended to the end (remember the head of this list is in the possession of the
+ appended to the end of that list (remember the head of this list is seen to be in the possession of the
resource).
\begin{isabelle}\ \ \ \ \ %%%
@@ -423,10 +430,10 @@
\end{isabelle}
\noindent
- The case for @{term V} is similar, except that we need to update the waiting queue function
- so that the thread that possessed the lock is eliminated. For this we use
+ The clause for event @{term V} is similar, except that we need to update the waiting queue function
+ so that the thread that possessed the lock is deleted from the corresponding thread list. For this we use
the auxiliary function @{term release}. A simple version of @{term release} would
- just delete this thread and return the rest like so
+ just delete this thread and return the rest, namely
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}lcl}
@@ -436,7 +443,7 @@
\end{isabelle}
\noindent
- However in practice often the thread with the highest precedence will get the
+ In practice, however, often the thread with the highest precedence will get the
lock next. We have implemented this choice, but later found out that the choice
about which thread is chosen next is actually irrelevant for the correctness of PIP.
Therefore we prove the stronger result where @{term release} is defined as
@@ -450,8 +457,8 @@
\noindent
@{text "SOME"} stands for Hilbert's epsilon and implements an arbitrary
- choice for the next waiting list, it just has to be a distinct list and
- contain the same elements as @{text "qs"}. This gives for @{term V} and @{term schs} the clause:
+ choice for the next waiting list. It just has to be a list of distinctive threads and
+ contain the same elements as @{text "qs"}. This gives for @{term V} the clause:
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@@ -462,60 +469,107 @@
\end{tabular}
\end{isabelle}
-
- TODO
+ Having the scheduler function @{term schs} at our disposal, we can ``lift'' the notions
+ @{term waiting}, @{term holding} @{term depend} and @{term cp} such that they only depend
+ on states.
\begin{isabelle}\ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- @{thm s_depend_def}\\
+ \begin{tabular}{@ {}rcl}
+ @{thm (lhs) s_holding_abv} & @{text "\<equiv>"} & @{thm (rhs) s_holding_abv}\\
+ @{thm (lhs) s_waiting_abv} & @{text "\<equiv>"} & @{thm (rhs) s_waiting_abv}\\
+ @{thm (lhs) s_depend_abv} & @{text "\<equiv>"} & @{thm (rhs) s_depend_abv}\\
+ @{thm (lhs) cp_def} & @{text "\<equiv>"} & @{thm (rhs) cp_def}
\end{tabular}
\end{isabelle}
+ \noindent
+ With them we can introduce the notion of threads being @{term readys} (i.e.~threads
+ that do not wait for any resource) and the running thread.
+
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@{thm readys_def}\\
- \end{tabular}
- \end{isabelle}
-
- \begin{isabelle}\ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
@{thm runing_def}\\
\end{tabular}
\end{isabelle}
-
- resources
+ \noindent
+ Note that in the initial case, that is where the list of events is empty, the set
+ @{term threads} is empty and therefore there is no thread ready nor a running.
+ If there is one or more threads ready, then there can only be \emph{one} thread
+ running, namely the one whose current precedence is equal to the maximum of all ready
+ threads. We can also define the set of resources that are locked by a thread in a
+ given state.
- done: threads not done: running
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{thm holdents_def}
+ \end{isabelle}
- step relation:
+ \noindent
+ These resources are given by the holding edges in the RAG.
+
+ Finally we can define what a \emph{valid state} is. For example we cannot exptect to
+ be able to exit a thread, if it was not created yet. These validity constraints
+ are characterised by the inductive predicate @{term "step"} by the following five
+ inference rules relating a state and an event that can happen next.
\begin{center}
\begin{tabular}{c}
@{thm[mode=Rule] thread_create[where thread=th]}\hspace{1cm}
- @{thm[mode=Rule] thread_exit[where thread=th]}\medskip\\
+ @{thm[mode=Rule] thread_exit[where thread=th]}
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ The first rule states that a thread can only be created, if it does not yet exists.
+ Similarly, the second rule states that a thread can only be terminated if it was
+ running and does not lock any resources anymore. The event @{text Set} can happen
+ if the corresponding thread is running.
- @{thm[mode=Rule] thread_set[where thread=th]}\medskip\\
+ \begin{center}
+ @{thm[mode=Rule] thread_set[where thread=th]}
+ \end{center}
+
+ \noindent
+ If a thread wants to lock a resource, then the thread needs to be running and
+ also we have to make sure that the resource lock doe not lead to a cycle in the
+ RAG. Similarly, if a thread wants to release a lock on a resource, then it must
+ be running and in the possession of that lock. This is formally given by the
+ last two inference rules of @{term step}.
+
+ \begin{center}
+ \begin{tabular}{c}
@{thm[mode=Rule] thread_P[where thread=th]}\medskip\\
@{thm[mode=Rule] thread_V[where thread=th]}\\
\end{tabular}
\end{center}
-
- valid state:
+
+ \noindent
+ A valid state of PIP can then be conveniently be defined as follows:
\begin{center}
\begin{tabular}{c}
- @{thm[mode=Axiom] vt_nil[where cs=step]}\hspace{1cm}
- @{thm[mode=Rule] vt_cons[where cs=step]}
+ @{thm[mode=Axiom] vt_nil}\hspace{1cm}
+ @{thm[mode=Rule] vt_cons}
\end{tabular}
\end{center}
+ \noindent
+ This completes our formal model of PIP. In the next section we present
+ properties that show our version of PIP is correct.
+*}
- 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 @{typ "nat"}:
-*}
+section {* Correctness Proof *}
+
+text {* TO DO *}
+
+section {* Properties for an Implementation *}
+
+text {* TO DO *}
+
+section {* Conclusion *}
+
+text {* TO DO *}
text {*
\bigskip
--- a/prio/Paper/document/root.tex Sat Feb 11 19:39:50 2012 +0000
+++ b/prio/Paper/document/root.tex Sun Feb 12 04:45:20 2012 +0000
@@ -31,12 +31,11 @@
\renewcommand{\isasymequiv}{$\dn$}
\renewcommand{\isasymemptyset}{$\varnothing$}
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
-
-\newcommand{\isasymcalL}{\ensuremath{\cal{L}}}
-\newcommand{\isasymbigplus}{\ensuremath{\bigplus}}
\renewcommand{\isasymiota}{}
-\newcommand{\bigplus}{\mbox{\Large\bf$+$}}
+\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
+
+
\begin{document}
\title{Priority Inheritance Protocol Proved Correct}
--- a/prio/PrioG.thy Sat Feb 11 19:39:50 2012 +0000
+++ b/prio/PrioG.thy Sun Feb 12 04:45:20 2012 +0000
@@ -9,7 +9,7 @@
"cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'"
by (auto simp:wq_def Let_def cp_def split:list.splits)
-lemma wq_distinct: "vt step s \<Longrightarrow> distinct (wq s cs)"
+lemma wq_distinct: "vt s \<Longrightarrow> distinct (wq s cs)"
proof(erule_tac vt.induct, simp add:wq_def)
fix s e
assume h1: "step s e"
@@ -44,15 +44,15 @@
qed
qed
-lemma step_back_vt: "vt ccs (e#s) \<Longrightarrow> vt ccs s"
- by(ind_cases "vt ccs (e#s)", simp)
+lemma step_back_vt: "vt (e#s) \<Longrightarrow> vt s"
+ by(ind_cases "vt (e#s)", simp)
-lemma step_back_step: "vt ccs (e#s) \<Longrightarrow> ccs s e"
- by(ind_cases "vt ccs (e#s)", simp)
+lemma step_back_step: "vt (e#s) \<Longrightarrow> step s e"
+ by(ind_cases "vt (e#s)", simp)
lemma block_pre:
fixes thread cs s
- assumes vt_e: "vt step (e#s)"
+ assumes vt_e: "vt (e#s)"
and s_ni: "thread \<notin> set (wq s cs)"
and s_i: "thread \<in> set (wq (e#s) cs)"
shows "e = P thread cs"
@@ -84,7 +84,7 @@
assume h1: "thread \<notin> set (wq_fun (schs s) cs)"
and h2: "q # qs = wq_fun (schs s) cs"
and h3: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)"
- and vt: "vt step (V th cs # s)"
+ and vt: "vt (V th cs # s)"
from h1 and h2[symmetric] have "thread \<notin> set (q # qs)" by simp
moreover have "thread \<in> set qs"
proof -
@@ -104,9 +104,9 @@
qed
qed
-lemma p_pre: "\<lbrakk>vt step ((P thread cs)#s)\<rbrakk> \<Longrightarrow>
+lemma p_pre: "\<lbrakk>vt ((P thread cs)#s)\<rbrakk> \<Longrightarrow>
thread \<in> runing s \<and> (Cs cs, Th thread) \<notin> (depend s)^+"
-apply (ind_cases "vt step ((P thread cs)#s)")
+apply (ind_cases "vt ((P thread cs)#s)")
apply (ind_cases "step s (P thread cs)")
by auto
@@ -124,10 +124,10 @@
lemma q_head: "Q (hd es) \<Longrightarrow> hd es = hd [th\<leftarrow>es . Q th]"
by (cases es, auto)
-inductive_cases evt_cons: "vt cs (a#s)"
+inductive_cases evt_cons: "vt (a#s)"
lemma abs2:
- assumes vt: "vt step (e#s)"
+ assumes vt: "vt (e#s)"
and inq: "thread \<in> set (wq s cs)"
and nh: "thread = hd (wq s cs)"
and qt: "thread \<noteq> hd (wq (e#s) cs)"
@@ -141,7 +141,7 @@
apply (auto simp:wq_def simp:Let_def split:if_splits list.splits)
proof -
fix th qs
- assume vt: "vt step (V th cs # s)"
+ assume vt: "vt (V th cs # s)"
and th_in: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)"
and eq_wq: "wq_fun (schs s) cs = thread # qs"
show "False"
@@ -166,13 +166,13 @@
qed
qed
-lemma vt_moment: "\<And> t. \<lbrakk>vt cs s; t \<le> length s\<rbrakk> \<Longrightarrow> vt cs (moment t s)"
+lemma vt_moment: "\<And> t. \<lbrakk>vt s; t \<le> length s\<rbrakk> \<Longrightarrow> vt (moment t s)"
proof(induct s, simp)
fix a s t
- assume h: "\<And>t.\<lbrakk>vt cs s; t \<le> length s\<rbrakk> \<Longrightarrow> vt cs (moment t s)"
- and vt_a: "vt cs (a # s)"
+ assume h: "\<And>t.\<lbrakk>vt s; t \<le> length s\<rbrakk> \<Longrightarrow> vt (moment t s)"
+ and vt_a: "vt (a # s)"
and le_t: "t \<le> length (a # s)"
- show "vt cs (moment t (a # s))"
+ show "vt (moment t (a # s))"
proof(cases "t = length (a#s)")
case True
from True have "moment t (a#s) = a#s" by simp
@@ -180,9 +180,9 @@
next
case False
with le_t have le_t1: "t \<le> length s" by simp
- from vt_a have "vt cs s"
+ from vt_a have "vt s"
by (erule_tac evt_cons, simp)
- from h [OF this le_t1] have "vt cs (moment t s)" .
+ from h [OF this le_t1] have "vt (moment t s)" .
moreover have "moment t (a#s) = moment t s"
proof -
from moment_app [OF le_t1, of "[a]"]
@@ -198,7 +198,7 @@
lemma waiting_unique_pre:
fixes cs1 cs2 s thread
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and h11: "thread \<in> set (wq s cs1)"
and h12: "thread \<noteq> hd (wq s cs1)"
assumes h21: "thread \<in> set (wq s cs2)"
@@ -235,10 +235,10 @@
from nn2 [rule_format, OF this] and eq_m
have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and
h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto
- have vt_e: "vt step (e#moment t2 s)"
+ have vt_e: "vt (e#moment t2 s)"
proof -
from vt_moment [OF vt le_t3]
- have "vt step (moment ?t3 s)" .
+ have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
have ?thesis
@@ -252,11 +252,11 @@
case False
from block_pre [OF vt_e False h1]
have "e = P thread cs2" .
- with vt_e have "vt step ((P thread cs2)# moment t2 s)" by simp
+ with vt_e have "vt ((P thread cs2)# moment t2 s)" by simp
from p_pre [OF this] have "thread \<in> runing (moment t2 s)" by simp
with runing_ready have "thread \<in> readys (moment t2 s)" by auto
with nn1 [rule_format, OF lt12]
- show ?thesis by (simp add:readys_def s_waiting_def, auto)
+ show ?thesis by (simp add:readys_def wq_def s_waiting_def, auto)
qed
} moreover {
assume lt12: "t2 < t1"
@@ -268,10 +268,10 @@
from nn1 [rule_format, OF this] and eq_m
have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and
h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto
- have vt_e: "vt step (e#moment t1 s)"
+ have vt_e: "vt (e#moment t1 s)"
proof -
from vt_moment [OF vt le_t3]
- have "vt step (moment ?t3 s)" .
+ have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
have ?thesis
@@ -285,11 +285,11 @@
case False
from block_pre [OF vt_e False h1]
have "e = P thread cs1" .
- with vt_e have "vt step ((P thread cs1)# moment t1 s)" by simp
+ with vt_e have "vt ((P thread cs1)# moment t1 s)" by simp
from p_pre [OF this] have "thread \<in> runing (moment t1 s)" by simp
with runing_ready have "thread \<in> readys (moment t1 s)" by auto
with nn2 [rule_format, OF lt12]
- show ?thesis by (simp add:readys_def s_waiting_def, auto)
+ show ?thesis by (simp add:readys_def wq_def s_waiting_def, auto)
qed
} moreover {
assume eqt12: "t1 = t2"
@@ -301,10 +301,10 @@
from nn1 [rule_format, OF this] and eq_m
have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and
h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto
- have vt_e: "vt step (e#moment t1 s)"
+ have vt_e: "vt (e#moment t1 s)"
proof -
from vt_moment [OF vt le_t3]
- have "vt step (moment ?t3 s)" .
+ have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
have ?thesis
@@ -328,15 +328,15 @@
case True
from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"
by auto
- from vt_e and eqt12 have "vt step (e#moment t2 s)" by simp
+ from vt_e and eqt12 have "vt (e#moment t2 s)" by simp
from abs2 [OF this True eq_th h2 h1]
show ?thesis .
next
case False
- have vt_e: "vt step (e#moment t2 s)"
+ have vt_e: "vt (e#moment t2 s)"
proof -
from vt_moment [OF vt le_t3] eqt12
- have "vt step (moment (Suc t2) s)" by auto
+ have "vt (moment (Suc t2) s)" by auto
with eq_m eqt12 show ?thesis by simp
qed
from block_pre [OF vt_e False h1]
@@ -350,18 +350,18 @@
lemma waiting_unique:
fixes s cs1 cs2
- assumes "vt step s"
+ assumes "vt s"
and "waiting s th cs1"
and "waiting s th cs2"
shows "cs1 = cs2"
proof -
from waiting_unique_pre and prems
show ?thesis
- by (auto simp add:s_waiting_def)
+ by (auto simp add: wq_def s_waiting_def)
qed
lemma held_unique:
- assumes "vt step s"
+ assumes "vt s"
and "holding s th1 cs"
and "holding s th2 cs"
shows "th1 = th2"
@@ -512,11 +512,11 @@
lemma step_v_hold_inv[elim_format]:
- "\<And>c t. \<lbrakk>vt step (V th cs # s);
+ "\<And>c t. \<lbrakk>vt (V th cs # s);
\<not> holding (wq s) t c; holding (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> next_th s th cs t \<and> c = cs"
proof -
fix c t
- assume vt: "vt step (V th cs # s)"
+ assume vt: "vt (V th cs # s)"
and nhd: "\<not> holding (wq s) t c"
and hd: "holding (wq (V th cs # s)) t c"
show "next_th s th cs t \<and> c = cs"
@@ -561,12 +561,12 @@
qed
lemma step_v_wait_inv[elim_format]:
- "\<And>t c. \<lbrakk>vt step (V th cs # s); \<not> waiting (wq (V th cs # s)) t c; waiting (wq s) t c
+ "\<And>t c. \<lbrakk>vt (V th cs # s); \<not> waiting (wq (V th cs # s)) t c; waiting (wq s) t c
\<rbrakk>
\<Longrightarrow> (next_th s th cs t \<and> cs = c)"
proof -
fix t c
- assume vt: "vt step (V th cs # s)"
+ assume vt: "vt (V th cs # s)"
and nw: "\<not> waiting (wq (V th cs # s)) t c"
and wt: "waiting (wq s) t c"
show "next_th s th cs t \<and> cs = c"
@@ -623,13 +623,13 @@
qed
lemma step_v_not_wait[consumes 3]:
- "\<lbrakk>vt step (V th cs # s); next_th s th cs t; waiting (wq (V th cs # s)) t cs\<rbrakk> \<Longrightarrow> False"
+ "\<lbrakk>vt (V th cs # s); next_th s th cs t; waiting (wq (V th cs # s)) t cs\<rbrakk> \<Longrightarrow> False"
by (unfold next_th_def cs_waiting_def wq_def, auto simp:Let_def)
lemma step_v_release:
- "\<lbrakk>vt step (V th cs # s); holding (wq (V th cs # s)) th cs\<rbrakk> \<Longrightarrow> False"
+ "\<lbrakk>vt (V th cs # s); holding (wq (V th cs # s)) th cs\<rbrakk> \<Longrightarrow> False"
proof -
- assume vt: "vt step (V th cs # s)"
+ assume vt: "vt (V th cs # s)"
and hd: "holding (wq (V th cs # s)) th cs"
from step_back_step [OF vt] and hd
show "False"
@@ -664,12 +664,12 @@
qed
lemma step_v_get_hold:
- "\<And>th'. \<lbrakk>vt step (V th cs # s); \<not> holding (wq (V th cs # s)) th' cs; next_th s th cs th'\<rbrakk> \<Longrightarrow> False"
+ "\<And>th'. \<lbrakk>vt (V th cs # s); \<not> holding (wq (V th cs # s)) th' cs; next_th s th cs th'\<rbrakk> \<Longrightarrow> False"
apply (unfold cs_holding_def next_th_def wq_def,
auto simp:Let_def)
proof -
fix rest
- assume vt: "vt step (V th cs # s)"
+ assume vt: "vt (V th cs # s)"
and eq_wq[folded wq_def]: " wq_fun (schs s) cs = th # rest"
and nrest: "rest \<noteq> []"
and ni: "hd (SOME q. distinct q \<and> set q = set rest)
@@ -688,12 +688,12 @@
qed
lemma step_v_release_inv[elim_format]:
-"\<And>c t. \<lbrakk>vt step (V th cs # s); \<not> holding (wq (V th cs # s)) t c; holding (wq s) t c\<rbrakk> \<Longrightarrow>
+"\<And>c t. \<lbrakk>vt (V th cs # s); \<not> holding (wq (V th cs # s)) t c; holding (wq s) t c\<rbrakk> \<Longrightarrow>
c = cs \<and> t = th"
apply (unfold cs_holding_def wq_def, auto simp:Let_def split:if_splits list.splits)
proof -
fix a list
- assume vt: "vt step (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"
+ assume vt: "vt (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"
from step_back_step [OF vt] show "a = th"
proof(cases)
assume "holding s th cs" with eq_wq
@@ -702,7 +702,7 @@
qed
next
fix a list
- assume vt: "vt step (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"
+ assume vt: "vt (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"
from step_back_step [OF vt] show "a = th"
proof(cases)
assume "holding s th cs" with eq_wq
@@ -712,11 +712,11 @@
qed
lemma step_v_waiting_mono:
- "\<And>t c. \<lbrakk>vt step (V th cs # s); waiting (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> waiting (wq s) t c"
+ "\<And>t c. \<lbrakk>vt (V th cs # s); waiting (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> waiting (wq s) t c"
proof -
fix t c
let ?s' = "(V th cs # s)"
- assume vt: "vt step ?s'"
+ assume vt: "vt ?s'"
and wt: "waiting (wq ?s') t c"
show "waiting (wq s) t c"
proof(cases "c = cs")
@@ -772,7 +772,7 @@
lemma step_depend_v:
fixes th::thread
assumes vt:
- "vt step (V th cs#s)"
+ "vt (V th cs#s)"
shows "
depend (V th cs # s) =
depend s - {(Cs cs, Th th)} -
@@ -787,7 +787,7 @@
done
lemma step_depend_p:
- "vt step (P th cs#s) \<Longrightarrow>
+ "vt (P th cs#s) \<Longrightarrow>
depend (P th cs # s) = (if (wq s cs = []) then depend s \<union> {(Cs cs, Th th)}
else depend s \<union> {(Th th, Cs cs)})"
apply(simp only: s_depend_def wq_def)
@@ -816,7 +816,7 @@
lemma acyclic_depend:
fixes s
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "acyclic (depend s)"
proof -
from vt show ?thesis
@@ -824,7 +824,7 @@
case (vt_cons s e)
assume ih: "acyclic (depend s)"
and stp: "step s e"
- and vt: "vt step s"
+ and vt: "vt s"
show ?case
proof(cases e)
case (Create th prio)
@@ -835,7 +835,7 @@
with ih show ?thesis by (simp add:depend_exit_unchanged)
next
case (V th cs)
- from V vt stp have vtt: "vt step (V th cs#s)" by auto
+ from V vt stp have vtt: "vt (V th cs#s)" by auto
from step_depend_v [OF this]
have eq_de:
"depend (e # s) =
@@ -849,7 +849,7 @@
proof(cases)
assume "holding s th cs"
hence th_in: "th \<in> set (wq s cs)" and
- eq_hd: "th = hd (wq s cs)" by (unfold s_holding_def, auto)
+ eq_hd: "th = hd (wq s cs)" unfolding s_holding_def wq_def by auto
then obtain rest where
eq_wq: "wq s cs = th#rest"
by (cases "wq s cs", auto)
@@ -871,19 +871,19 @@
obtain cs' where eq_x: "x = Cs cs'" by auto
with th_d have "(Th ?th', Cs cs') \<in> ?A" by simp
hence wt_th': "waiting s ?th' cs'"
- unfolding s_depend_def s_waiting_def cs_waiting_def by simp
+ unfolding s_depend_def s_waiting_def cs_waiting_def wq_def by simp
hence "cs' = cs"
proof(rule waiting_unique [OF vt])
from eq_wq wq_distinct[OF vt, of cs]
show "waiting s ?th' cs"
- apply (unfold s_waiting_def, auto)
+ apply (unfold s_waiting_def wq_def, auto)
proof -
assume hd_in: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
- and eq_wq: "wq s cs = th # rest"
+ and eq_wq: "wq_fun (schs s) cs = th # rest"
have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
proof(rule someI2)
from wq_distinct[OF vt, of cs] and eq_wq
- show "distinct rest \<and> set rest = set rest" by auto
+ show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
next
fix x assume "distinct x \<and> set x = set rest"
with False show "x \<noteq> []" by auto
@@ -893,7 +893,7 @@
moreover have "\<dots> = set rest"
proof(rule someI2)
from wq_distinct[OF vt, of cs] and eq_wq
- show "distinct rest \<and> set rest = set rest" by auto
+ show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
next
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
qed
@@ -940,7 +940,7 @@
qed
next
case (P th cs)
- from P vt stp have vtt: "vt step (P th cs#s)" by auto
+ from P vt stp have vtt: "vt (P th cs#s)" by auto
from step_depend_p [OF this] P
have "depend (e # s) =
(if wq s cs = [] then depend s \<union> {(Cs cs, Th th)} else
@@ -992,7 +992,7 @@
lemma finite_depend:
fixes s
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "finite (depend s)"
proof -
from vt show ?thesis
@@ -1000,7 +1000,7 @@
case (vt_cons s e)
assume ih: "finite (depend s)"
and stp: "step s e"
- and vt: "vt step s"
+ and vt: "vt s"
show ?case
proof(cases e)
case (Create th prio)
@@ -1011,7 +1011,7 @@
with ih show ?thesis by (simp add:depend_exit_unchanged)
next
case (V th cs)
- from V vt stp have vtt: "vt step (V th cs#s)" by auto
+ from V vt stp have vtt: "vt (V th cs#s)" by auto
from step_depend_v [OF this]
have eq_de: "depend (e # s) =
depend s - {(Cs cs, Th th)} - {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>
@@ -1035,7 +1035,7 @@
ultimately show ?thesis by simp
next
case (P th cs)
- from P vt stp have vtt: "vt step (P th cs#s)" by auto
+ from P vt stp have vtt: "vt (P th cs#s)" by auto
from step_depend_p [OF this] P
have "depend (e # s) =
(if wq s cs = [] then depend s \<union> {(Cs cs, Th th)} else
@@ -1069,7 +1069,7 @@
lemma wf_dep_converse:
fixes s
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "wf ((depend s)^-1)"
proof(rule finite_acyclic_wf_converse)
from finite_depend [OF vt]
@@ -1087,7 +1087,7 @@
lemma wq_threads:
fixes s cs
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and h: "th \<in> set (wq s cs)"
shows "th \<in> threads s"
proof -
@@ -1096,7 +1096,7 @@
case (vt_cons s e)
assume ih: "\<And>th cs. th \<in> set (wq s cs) \<Longrightarrow> th \<in> threads s"
and stp: "step s e"
- and vt: "vt step s"
+ and vt: "vt s"
and h: "th \<in> set (wq (e # s) cs)"
show ?case
proof(cases e)
@@ -1187,13 +1187,13 @@
qed
qed
-lemma range_in: "\<lbrakk>vt step s; (Th th) \<in> Range (depend (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s"
+lemma range_in: "\<lbrakk>vt s; (Th th) \<in> Range (depend (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s"
apply(unfold s_depend_def cs_waiting_def cs_holding_def)
by (auto intro:wq_threads)
lemma readys_v_eq:
fixes th thread cs rest
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and neq_th: "th \<noteq> thread"
and eq_wq: "wq s cs = thread#rest"
and not_in: "th \<notin> set rest"
@@ -1201,19 +1201,21 @@
proof -
from prems show ?thesis
apply (auto simp:readys_def)
- apply (case_tac "cs = csa", simp add:s_waiting_def)
+ apply(simp add:s_waiting_def[folded wq_def])
apply (erule_tac x = csa in allE)
apply (simp add:s_waiting_def wq_def Let_def split:if_splits)
apply (case_tac "csa = cs", simp)
apply (erule_tac x = cs in allE)
+ apply(auto simp add: s_waiting_def[folded wq_def] Let_def split: list.splits)
+ apply(auto simp add: wq_def)
apply (auto simp:s_waiting_def wq_def Let_def split:list.splits)
proof -
- assume th_nin: "th \<notin> set rest"
+ assume th_nin: "th \<notin> set rest"
and th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)"
and eq_wq: "wq_fun (schs s) cs = thread # rest"
have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
proof(rule someI2)
- from wq_distinct[OF vt, of cs] and eq_wq[folded wq_def]
+ from wq_distinct[OF vt, of cs, unfolded wq_def] and eq_wq[unfolded wq_def]
show "distinct rest \<and> set rest = set rest" by auto
next
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
@@ -1223,7 +1225,7 @@
qed
lemma chain_building:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "node \<in> Domain (depend s) \<longrightarrow> (\<exists> th'. th' \<in> readys s \<and> (node, Th th') \<in> (depend s)^+)"
proof -
from wf_dep_converse [OF vt]
@@ -1259,7 +1261,7 @@
case False
from th'_d and range_in [OF vt] have "th' \<in> threads s" by auto
with False have "Th th' \<in> Domain (depend s)"
- by (auto simp:readys_def s_waiting_def s_depend_def cs_waiting_def Domain_def)
+ by (auto simp:readys_def wq_def s_waiting_def s_depend_def cs_waiting_def Domain_def)
from ih [OF th'_d this]
obtain th'' where
th''_r: "th'' \<in> readys s" and
@@ -1275,7 +1277,7 @@
lemma th_chain_to_ready:
fixes s th
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and th_in: "th \<in> threads s"
shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (depend s)^+)"
proof(cases "th \<in> readys s")
@@ -1284,21 +1286,21 @@
next
case False
from False and th_in have "Th th \<in> Domain (depend s)"
- by (auto simp:readys_def s_waiting_def s_depend_def cs_waiting_def Domain_def)
+ by (auto simp:readys_def s_waiting_def s_depend_def wq_def cs_waiting_def Domain_def)
from chain_building [rule_format, OF vt this]
show ?thesis by auto
qed
lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"
- by (unfold s_waiting_def cs_waiting_def, auto)
+ by (unfold s_waiting_def cs_waiting_def wq_def, auto)
lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs"
- by (unfold s_holding_def cs_holding_def, simp)
+ by (unfold s_holding_def wq_def cs_holding_def, simp)
lemma holding_unique: "\<lbrakk>holding (s::state) th1 cs; holding s th2 cs\<rbrakk> \<Longrightarrow> th1 = th2"
by (unfold s_holding_def cs_holding_def, auto)
-lemma unique_depend: "\<lbrakk>vt step s; (n, n1) \<in> depend s; (n, n2) \<in> depend s\<rbrakk> \<Longrightarrow> n1 = n2"
+lemma unique_depend: "\<lbrakk>vt s; (n, n1) \<in> depend s; (n, n2) \<in> depend s\<rbrakk> \<Longrightarrow> n1 = n2"
apply(unfold s_depend_def, auto, fold waiting_eq holding_eq)
by(auto elim:waiting_unique holding_unique)
@@ -1306,7 +1308,7 @@
by (induct rule:trancl_induct, auto)
lemma dchain_unique:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and th1_d: "(n, Th th1) \<in> (depend s)^+"
and th1_r: "th1 \<in> readys s"
and th2_d: "(n, Th th2) \<in> (depend s)^+"
@@ -1325,7 +1327,7 @@
then obtain cs where eq_n: "n = Cs cs"
by (auto simp:s_depend_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in)
from dd eq_n have "th1 \<notin> readys s"
- by (auto simp:readys_def s_depend_def s_waiting_def cs_waiting_def)
+ by (auto simp:readys_def s_depend_def wq_def s_waiting_def cs_waiting_def)
with th1_r show ?thesis by auto
next
assume "(Th th2, Th th1) \<in> (depend s)\<^sup>+"
@@ -1334,7 +1336,7 @@
then obtain cs where eq_n: "n = Cs cs"
by (auto simp:s_depend_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in)
from dd eq_n have "th2 \<notin> readys s"
- by (auto simp:readys_def s_depend_def s_waiting_def cs_waiting_def)
+ by (auto simp:readys_def wq_def s_depend_def s_waiting_def cs_waiting_def)
with th2_r show ?thesis by auto
qed
} thus ?thesis by auto
@@ -1343,7 +1345,7 @@
lemma step_holdents_p_add:
fixes th cs s
- assumes vt: "vt step (P th cs#s)"
+ assumes vt: "vt (P th cs#s)"
and "wq s cs = []"
shows "holdents (P th cs#s) th = holdents s th \<union> {cs}"
proof -
@@ -1353,7 +1355,7 @@
lemma step_holdents_p_eq:
fixes th cs s
- assumes vt: "vt step (P th cs#s)"
+ assumes vt: "vt (P th cs#s)"
and "wq s cs \<noteq> []"
shows "holdents (P th cs#s) th = holdents s th"
proof -
@@ -1364,7 +1366,7 @@
lemma finite_holding:
fixes s th cs
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "finite (holdents s th)"
proof -
let ?F = "\<lambda> (x, y). the_cs x"
@@ -1385,13 +1387,13 @@
lemma cntCS_v_dec:
fixes s thread cs
- assumes vtv: "vt step (V thread cs#s)"
+ assumes vtv: "vt (V thread cs#s)"
shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread"
proof -
from step_back_step[OF vtv]
have cs_in: "cs \<in> holdents s thread"
apply (cases, unfold holdents_def s_depend_def, simp)
- by (unfold cs_holding_def s_holding_def, auto)
+ by (unfold cs_holding_def s_holding_def wq_def, auto)
moreover have cs_not_in:
"(holdents (V thread cs#s) thread) = holdents s thread - {cs}"
apply (insert wq_distinct[OF step_back_vt[OF vtv], of cs])
@@ -1458,14 +1460,14 @@
lemma cnp_cnv_cncs:
fixes s th
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "cntP s th = cntV s th + (if (th \<in> readys s \<or> th \<notin> threads s)
then cntCS s th else cntCS s th + 1)"
proof -
from vt show ?thesis
proof(induct arbitrary:th)
case (vt_cons s e)
- assume vt: "vt step s"
+ assume vt: "vt s"
and ih: "\<And>th. cntP s th = cntV s th +
(if (th \<in> readys s \<or> th \<notin> threads s) then cntCS s th else cntCS s th + 1)"
and stp: "step s e"
@@ -1519,10 +1521,9 @@
(th \<in> readys (s) \<or> th \<notin> threads (s))"
apply (simp add:threads.simps readys_def)
apply (subst s_waiting_def)
- apply (subst (1 2) wq_def)
apply (simp add:Let_def)
apply (subst s_waiting_def, simp)
- by (fold wq_def, simp)
+ done
with eq_cnp eq_cnv eq_cncs ih
have ?thesis by simp
} moreover {
@@ -1539,7 +1540,7 @@
assume eq_e: "e = P thread cs"
and is_runing: "thread \<in> runing s"
and no_dep: "(Cs cs, Th thread) \<notin> (depend s)\<^sup>+"
- from prems have vtp: "vt step (P thread cs#s)" by auto
+ from prems have vtp: "vt (P thread cs#s)" by auto
show ?thesis
proof -
{ have hh: "\<And> A B C. (B = C) \<Longrightarrow> (A \<and> B) = (A \<and> C)" by blast
@@ -1621,7 +1622,7 @@
hence "\<forall>cs. \<not> waiting (e # s) th cs" by (simp add:readys_def)
from this[rule_format, of cs] have " \<not> waiting (e # s) th cs" .
hence "th \<in> set (wq (e#s) cs) \<Longrightarrow> th = hd (wq (e#s) cs)"
- by (simp add:s_waiting_def)
+ by (simp add:s_waiting_def wq_def)
moreover from eq_wq have "th \<in> set (wq (e#s) cs)" by auto
ultimately have "th = hd (wq (e#s) cs)" by blast
with eq_wq have "th = hd (wq s cs @ [th])" by simp
@@ -1644,13 +1645,13 @@
qed
next
case (thread_V thread cs)
- from prems have vtv: "vt step (V thread cs # s)" by auto
+ from prems have vtv: "vt (V thread cs # s)" by auto
assume eq_e: "e = V thread cs"
and is_runing: "thread \<in> runing s"
and hold: "holding s thread cs"
from hold obtain rest
where eq_wq: "wq s cs = thread # rest"
- by (case_tac "wq s cs", auto simp:s_holding_def)
+ by (case_tac "wq s cs", auto simp: wq_def s_holding_def)
have eq_threads: "threads (e#s) = threads s" by (simp add: eq_e)
have eq_set: "set (SOME q. distinct q \<and> set q = set rest) = set rest"
proof(rule someI2)
@@ -1693,7 +1694,7 @@
with wq_distinct[OF step_back_vt[OF vtv], of cs]
and eq_wq show False by auto
qed
- thus ?thesis by (simp add:s_waiting_def)
+ thus ?thesis by (simp add:wq_def s_waiting_def)
qed
} moreover {
assume neq_cs: "cs1 \<noteq> cs"
@@ -1708,7 +1709,7 @@
thus ?thesis by (simp add:readys_def)
qed
ultimately show ?thesis
- by (auto simp:s_waiting_def eq_e)
+ by (auto simp:wq_def s_waiting_def eq_e)
qed
} ultimately show "\<not> waiting (e # s) thread cs1" by blast
qed
@@ -1778,7 +1779,7 @@
have "\<not> th \<in> readys s"
apply (auto simp:readys_def s_waiting_def)
apply (rule_tac x = cs in exI, auto)
- by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto)
+ by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp add: wq_def)
moreover
from eq_wq and th_in and neq_hd
have "\<not> (th \<in> readys (e # s))"
@@ -1844,7 +1845,7 @@
from True eq_wq neq_th th_in
show ?thesis
apply (unfold readys_def s_waiting_def, auto)
- by (rule_tac x = cs in exI, auto)
+ by (rule_tac x = cs in exI, auto simp add: wq_def)
qed
moreover have "th \<in> threads s"
proof -
@@ -1931,14 +1932,14 @@
lemma not_thread_cncs:
fixes th s
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and not_in: "th \<notin> threads s"
shows "cntCS s th = 0"
proof -
from vt not_in show ?thesis
proof(induct arbitrary:th)
case (vt_cons s e th)
- assume vt: "vt step s"
+ assume vt: "vt s"
and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> cntCS s th = 0"
and stp: "step s e"
and not_in: "th \<notin> threads (e # s)"
@@ -1977,7 +1978,7 @@
case (thread_P thread cs)
assume eq_e: "e = P thread cs"
and is_runing: "thread \<in> runing s"
- from prems have vtp: "vt step (P thread cs#s)" by auto
+ from prems have vtp: "vt (P thread cs#s)" by auto
have neq_th: "th \<noteq> thread"
proof -
from not_in eq_e have "th \<notin> threads s" by simp
@@ -2005,10 +2006,10 @@
by (simp add:runing_def readys_def)
ultimately show ?thesis by auto
qed
- from prems have vtv: "vt step (V thread cs#s)" by auto
+ from prems have vtv: "vt (V thread cs#s)" by auto
from hold obtain rest
where eq_wq: "wq s cs = thread # rest"
- by (case_tac "wq s cs", auto simp:s_holding_def)
+ by (case_tac "wq s cs", auto simp: wq_def s_holding_def)
from not_in eq_e eq_wq
have "\<not> next_th s thread cs th"
apply (auto simp:next_th_def)
@@ -2055,11 +2056,11 @@
qed
lemma eq_waiting: "waiting (wq (s::state)) th cs = waiting s th cs"
- by (auto simp:s_waiting_def cs_waiting_def)
+ by (auto simp:s_waiting_def cs_waiting_def wq_def)
lemma dm_depend_threads:
fixes th s
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and in_dom: "(Th th) \<in> Domain (depend s)"
shows "th \<in> threads s"
proof -
@@ -2087,7 +2088,7 @@
lemma runing_unique:
fixes th1 th2 s
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and runing_1: "th1 \<in> runing s"
and runing_2: "th2 \<in> runing s"
shows "th1 = th2"
@@ -2331,7 +2332,7 @@
lemma cnp_cnv_eq:
fixes th s
- assumes "vt step s"
+ assumes "vt s"
and "th \<notin> threads s"
shows "cntP s th = cntV s th"
proof -
@@ -2352,7 +2353,7 @@
case (thread_exit thread)
assume eq_e: "e = Exit thread"
and not_holding: "holdents s thread = {}"
- have vt_s: "vt step s" by fact
+ have vt_s: "vt s" by fact
from finite_holding[OF vt_s] have "finite (holdents s thread)" .
with not_holding have "cntCS s thread = 0" by (unfold cntCS_def, auto)
moreover have "thread \<in> readys s" using thread_exit by (auto simp:runing_def)
@@ -2408,7 +2409,7 @@
by (unfold cs_depend_def s_depend_def, auto)
lemma count_eq_dependents:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and eq_pv: "cntP s th = cntV s th"
shows "dependents (wq s) th = {}"
proof -
@@ -2442,7 +2443,7 @@
lemma dependents_threads:
fixes s th
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "dependents (wq s) th \<subseteq> threads s"
proof
{ fix th th'
@@ -2465,13 +2466,13 @@
qed
lemma finite_threads:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "finite (threads s)"
proof -
from vt show ?thesis
proof(induct)
case (vt_cons s e)
- assume vt: "vt step s"
+ assume vt: "vt s"
and step: "step s e"
and ih: "finite (threads s)"
from step
@@ -2518,7 +2519,7 @@
qed
lemma cp_le:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and th_in: "th \<in> threads s"
shows "cp s th \<le> Max ((\<lambda> th. (preced th s)) ` threads s)"
proof(unfold cp_eq_cpreced cpreced_def cs_dependents_def)
@@ -2541,7 +2542,7 @@
qed
lemma le_cp:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "preced th s \<le> cp s th"
proof(unfold cp_eq_cpreced preced_def cpreced_def, simp)
show "Prc (original_priority th s) (birthtime th s)
@@ -2582,7 +2583,7 @@
qed
lemma max_cp_eq:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "Max ((cp s) ` threads s) = Max ((\<lambda> th. (preced th s)) ` threads s)"
(is "?l = ?r")
proof(cases "threads s = {}")
@@ -2630,7 +2631,7 @@
qed
lemma max_cp_readys_threads_pre:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and np: "threads s \<noteq> {}"
shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
proof(unfold max_cp_eq[OF vt])
@@ -2773,7 +2774,7 @@
qed
lemma max_cp_readys_threads:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
proof(cases "threads s = {}")
case True
@@ -2794,7 +2795,7 @@
qed
lemma eq_holding: "holding (wq s) th cs = holding s th cs"
- apply (unfold s_holding_def cs_holding_def, simp)
+ apply (unfold s_holding_def cs_holding_def wq_def, simp)
done
lemma f_image_eq:
--- a/prio/PrioGDef.thy Sat Feb 11 19:39:50 2012 +0000
+++ b/prio/PrioGDef.thy Sun Feb 12 04:45:20 2012 +0000
@@ -300,7 +300,7 @@
The following @{text "cp"} is a shorthand for @{text "cprec_fun"}.
*}
definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"
- where "cp s = cprec_fun (schs s)"
+ where "cp s \<equiv> cprec_fun (schs s)"
text {* \noindent
Functions @{text "holding"}, @{text "waiting"}, @{text "depend"} and
@@ -311,13 +311,13 @@
*}
defs (overloaded)
s_holding_abv:
- "holding (s::state) \<equiv> holding (wq s)"
+ "holding (s::state) \<equiv> holding (wq_fun (schs s))"
s_waiting_abv:
- "waiting (s::state) \<equiv> waiting (wq s)"
+ "waiting (s::state) \<equiv> waiting (wq_fun (schs s))"
s_depend_abv:
- "depend (s::state) \<equiv> depend (wq s)"
+ "depend (s::state) \<equiv> depend (wq_fun (schs s))"
s_dependents_abv:
- "dependents (s::state) th \<equiv> dependents (wq s) th"
+ "dependents (s::state) \<equiv> dependents (wq_fun (schs s))"
text {*
@@ -325,11 +325,11 @@
*}
lemma
s_holding_def:
- "holding (s::state) thread cs = (thread \<in> set (wq s cs) \<and> thread = hd (wq s cs))"
+ "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 cs_holding_def)
lemma s_waiting_def:
- "waiting (s::state) thread cs = (thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs))"
+ "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 cs_waiting_def)
lemma s_depend_def:
@@ -354,14 +354,14 @@
thread with the highest precedence.
*}
definition runing :: "state \<Rightarrow> thread set"
- where "runing s = {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}"
+ where "runing s \<equiv> {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}"
text {* \noindent
The following function @{text "holdents s th"} returns the set of resources held by thread
@{text "th"} in state @{text "s"}.
*}
definition holdents :: "state \<Rightarrow> thread \<Rightarrow> cs set"
- where "holdents s th = {cs . (Cs cs, Th th) \<in> depend s}"
+ where "holdents s th \<equiv> {cs . (Cs cs, Th th) \<in> depend s}"
text {* \noindent
@{text "cntCS s th"} returns the number of resources held by thread @{text "th"} in
@@ -412,18 +412,17 @@
Priority Inheritance protocol can be expressed as: @{text "vt step s"}, where
the predicate @{text "vt"} can be defined as the following:
*}
-inductive vt :: "(state \<Rightarrow> event \<Rightarrow> bool) \<Rightarrow> state \<Rightarrow> bool"
- for cs -- {* @{text "cs"} is an argument representing any step predicate. *}
+inductive vt :: "state \<Rightarrow> bool"
where
-- {* Empty list @{text "[]"} is a legal state in any protocol:*}
- vt_nil[intro]: "vt cs []" |
+ vt_nil[intro]: "vt []" |
-- {*
\begin{minipage}{0.9\textwidth}
If @{text "s"} a legal state, and event @{text "e"} is eligible to happen
in state @{text "s"}, then @{text "e#s"} is a legal state as well:
\end{minipage}
*}
- vt_cons[intro]: "\<lbrakk>vt cs s; cs s e\<rbrakk> \<Longrightarrow> vt cs (e#s)"
+ vt_cons[intro]: "\<lbrakk>vt s; step s e\<rbrakk> \<Longrightarrow> vt (e#s)"
text {* \noindent
It is easy to see that the definition of @{text "vt"} is generic. It can be applied to
Binary file prio/paper.pdf has changed