--- a/prio/Paper/Paper.thy Sat Feb 11 09:14:14 2012 +0000
+++ b/prio/Paper/Paper.thy Sat Feb 11 09:34:46 2012 +0000
@@ -23,8 +23,6 @@
preced ("prec") and
cpreced ("cprec") and
dependents ("dependants") and
- waiting_queue ("wq_fun") and
- cur_preced ("cprec_fun") and
DUMMY ("\<^raw:\mbox{$\_\!\_$}>")
(*>*)
@@ -362,13 +360,16 @@
@{text "\<lparr>wq_fun, cprec_fun\<rparr>"}
\end{isabelle}
+ \noindent
+ We have 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"}.
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@{thm (lhs) schs.simps(1)} @{text "\<equiv>"}\\
- \hspace{5mm}@{term "(|waiting_queue = all_unlocked, cur_preced = (\<lambda>_::thread. Prc 0 0)|)"}
+ \hspace{5mm}@{term "(|wq_fun = all_unlocked, cprec_fun = (\<lambda>_::thread. Prc 0 0)|)"}
\end{tabular}
\end{isabelle}
@@ -382,14 +383,14 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@{thm (lhs) schs.simps(2)} @{text "\<equiv>"}\\
- \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
- \hspace{8mm}@{term "(|waiting_queue = wq\<iota>, cur_preced = cpreced wq\<iota> (Create th prio # s)|)"}\\
+ \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)|)"}\\
@{thm (lhs) schs.simps(3)} @{text "\<equiv>"}\\
- \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
- \hspace{8mm}@{term "(|waiting_queue = wq\<iota>, cur_preced = cpreced wq\<iota> (Exit th # s)|)"}\smallskip\\
+ \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\\
@{thm (lhs) schs.simps(4)} @{text "\<equiv>"}\\
- \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
- \hspace{8mm}@{term "(|waiting_queue = wq\<iota>, cur_preced = cpreced wq\<iota> (Set th prio # s)|)"}
+ \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
+ \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Set th prio # s)|)"}
\end{tabular}
\end{isabelle}
@@ -403,9 +404,9 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@{thm (lhs) schs.simps(5)} @{text "\<equiv>"}\\
- \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
+ \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
\hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := (wq cs @ [th]))"} @{text "in"}\\
- \hspace{8mm}@{term "(|waiting_queue = new_wq, cur_preced = cpreced new_wq (P th cs # s)|)"}
+ \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|)"}
\end{tabular}
\end{isabelle}
@@ -423,9 +424,9 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\
- \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
+ \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
\hspace{5mm}@{text "let"} @{text "new_wq = release (wq cs)"} @{text "in"}\\
- \hspace{8mm}@{term "(|waiting_queue = new_wq, cur_preced = cpreced new_wq (V th cs # s)|)"}
+ \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|)"}
\end{tabular}
\end{isabelle}
--- a/prio/PrioG.thy Sat Feb 11 09:14:14 2012 +0000
+++ b/prio/PrioG.thy Sat Feb 11 09:34:46 2012 +0000
@@ -18,14 +18,14 @@
proof(induct rule:step.induct, auto simp: wq_def Let_def split:list.splits)
fix thread s
assume h1: "(Cs cs, Th thread) \<notin> (depend s)\<^sup>+"
- and h2: "thread \<in> set (waiting_queue (schs s) cs)"
+ and h2: "thread \<in> set (wq_fun (schs s) cs)"
and h3: "thread \<in> runing s"
show "False"
proof -
- from h3 have "\<And> cs. thread \<in> set (waiting_queue (schs s) cs) \<Longrightarrow>
- thread = hd ((waiting_queue (schs s) cs))"
+ from h3 have "\<And> cs. thread \<in> set (wq_fun (schs s) cs) \<Longrightarrow>
+ thread = hd ((wq_fun (schs s) cs))"
by (simp add:runing_def readys_def s_waiting_def wq_def)
- from this [OF h2] have "thread = hd (waiting_queue (schs s) cs)" .
+ from this [OF h2] have "thread = hd (wq_fun (schs s) cs)" .
with h2
have "(Cs cs, Th thread) \<in> (depend s)"
by (simp add:s_depend_def s_holding_def wq_def cs_holding_def)
@@ -81,8 +81,8 @@
apply (auto simp:wq_def Let_def split:if_splits)
proof -
fix q qs
- assume h1: "thread \<notin> set (waiting_queue (schs s) cs)"
- and h2: "q # qs = waiting_queue (schs s) cs"
+ 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)"
from h1 and h2[symmetric] have "thread \<notin> set (q # qs)" by simp
@@ -143,7 +143,7 @@
fix th qs
assume vt: "vt step (V th cs # s)"
and th_in: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)"
- and eq_wq: "waiting_queue (schs s) cs = thread # qs"
+ and eq_wq: "wq_fun (schs s) cs = thread # qs"
show "False"
proof -
from wq_distinct[OF step_back_vt[OF vt], of cs]
@@ -193,7 +193,7 @@
qed
(* Wrong:
- lemma \<lbrakk>thread \<in> set (waiting_queue cs1 s); thread \<in> set (waiting_queue cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"
+ lemma \<lbrakk>thread \<in> set (wq_fun cs1 s); thread \<in> set (wq_fun cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"
*)
lemma waiting_unique_pre:
@@ -583,7 +583,7 @@
fix a list
assume t_in: "t \<in> set list"
and t_ni: "t \<notin> set (SOME q. distinct q \<and> set q = set list)"
- and eq_wq: "waiting_queue (schs s) cs = a # list"
+ and eq_wq: "wq_fun (schs s) cs = a # list"
have " set (SOME q. distinct q \<and> set q = set list) = set list"
proof(rule someI2)
from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def]
@@ -597,7 +597,7 @@
fix a list
assume t_in: "t \<in> set list"
and t_ni: "t \<notin> set (SOME q. distinct q \<and> set q = set list)"
- and eq_wq: "waiting_queue (schs s) cs = a # list"
+ and eq_wq: "wq_fun (schs s) cs = a # list"
have " set (SOME q. distinct q \<and> set q = set list) = set list"
proof(rule someI2)
from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def]
@@ -609,7 +609,7 @@
with t_ni and t_in show "t = hd (SOME q. distinct q \<and> set q = set list)" by auto
next
fix a list
- assume eq_wq: "waiting_queue (schs s) cs = a # list"
+ assume eq_wq: "wq_fun (schs s) cs = a # list"
from step_back_step[OF vt]
show "a = th"
proof(cases)
@@ -641,7 +641,7 @@
proof -
fix list
assume eq_wq[folded wq_def]:
- "waiting_queue (schs s) cs = hd (SOME q. distinct q \<and> set q = set list) # list"
+ "wq_fun (schs s) cs = hd (SOME q. distinct q \<and> set q = set list) # list"
and hd_in: "hd (SOME q. distinct q \<and> set q = set list)
\<in> set (SOME q. distinct q \<and> set q = set list)"
have "set (SOME q. distinct q \<and> set q = set list) = set list"
@@ -670,7 +670,7 @@
proof -
fix rest
assume vt: "vt step (V th cs # s)"
- and eq_wq[folded wq_def]: " waiting_queue (schs s) cs = th # rest"
+ 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)
\<notin> set (SOME q. distinct q \<and> set q = set rest)"
@@ -693,7 +693,7 @@
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: "waiting_queue (schs s) cs = a # list"
+ assume vt: "vt step (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: "waiting_queue (schs s) cs = a # list"
+ assume vt: "vt step (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
@@ -733,7 +733,7 @@
fix a list
assume not_in: "t \<notin> set list"
and is_in: "t \<in> set (SOME q. distinct q \<and> set q = set list)"
- and eq_wq: "waiting_queue (schs s) cs = a # list"
+ and eq_wq: "wq_fun (schs s) cs = a # list"
have "set (SOME q. distinct q \<and> set q = set list) = set list"
proof(rule someI2)
from wq_distinct [OF step_back_vt[OF vt], of cs]
@@ -747,7 +747,7 @@
next
fix list
assume is_waiting: "waiting (wq (V th cs # s)) t cs"
- and eq_wq: "waiting_queue (schs s) cs = t # list"
+ and eq_wq: "wq_fun (schs s) cs = t # list"
hence "t \<in> set list"
apply (unfold wq_def, auto simp:Let_def cs_waiting_def)
proof -
@@ -1125,25 +1125,25 @@
from h
show ?thesis
proof(unfold V wq_def)
- assume th_in: "th \<in> set (waiting_queue (schs (V th' cs' # s)) cs)" (is "th \<in> set ?l")
+ assume th_in: "th \<in> set (wq_fun (schs (V th' cs' # s)) cs)" (is "th \<in> set ?l")
show "th \<in> threads (V th' cs' # s)"
proof(cases "cs = cs'")
case False
- hence "?l = waiting_queue (schs s) cs" by (simp add:Let_def)
+ hence "?l = wq_fun (schs s) cs" by (simp add:Let_def)
with th_in have " th \<in> set (wq s cs)"
by (fold wq_def, simp)
from ih [OF this] show ?thesis by simp
next
case True
show ?thesis
- proof(cases "waiting_queue (schs s) cs'")
+ proof(cases "wq_fun (schs s) cs'")
case Nil
with h V show ?thesis
apply (auto simp:wq_def Let_def split:if_splits)
by (fold wq_def, drule_tac ih, simp)
next
case (Cons a rest)
- assume eq_wq: "waiting_queue (schs s) cs' = a # rest"
+ assume eq_wq: "wq_fun (schs s) cs' = a # rest"
with h V show ?thesis
apply (auto simp:Let_def wq_def split:if_splits)
proof -
@@ -1156,10 +1156,10 @@
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest"
by auto
qed
- with eq_wq th_in have "th \<in> set (waiting_queue (schs s) cs')" by auto
+ with eq_wq th_in have "th \<in> set (wq_fun (schs s) cs')" by auto
from ih[OF this[folded wq_def]] show "th \<in> threads s" .
next
- assume th_in: "th \<in> set (waiting_queue (schs s) cs)"
+ assume th_in: "th \<in> set (wq_fun (schs s) cs)"
from ih[OF this[folded wq_def]]
show "th \<in> threads s" .
qed
@@ -1210,7 +1210,7 @@
proof -
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: "waiting_queue (schs s) cs = thread # 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]
@@ -1550,9 +1550,9 @@
apply (rule_tac hh, clarify)
apply (intro iffI allI, clarify)
apply (erule_tac x = csa in allE, auto)
- apply (subgoal_tac "waiting_queue (schs s) cs \<noteq> []", auto)
+ apply (subgoal_tac "wq_fun (schs s) cs \<noteq> []", auto)
apply (erule_tac x = cs in allE, auto)
- by (case_tac "(waiting_queue (schs s) cs)", auto)
+ by (case_tac "(wq_fun (schs s) cs)", auto)
moreover from neq_th eq_e have "cntCS (e # s) th = cntCS s th"
apply (simp add:cntCS_def holdents_def)
by (unfold step_depend_p [OF vtp], auto)
@@ -1807,7 +1807,7 @@
apply (auto simp:eq_e readys_def s_waiting_def wq_def
Let_def next_th_def)
proof -
- assume eq_wq: "waiting_queue (schs s) cs = thread # rest"
+ assume eq_wq: "wq_fun (schs s) cs = thread # rest"
and t_in: "?t \<in> set rest"
show "?t \<in> threads s"
proof(rule wq_threads[OF step_back_vt[OF vtv]])
@@ -1816,13 +1816,13 @@
qed
next
fix csa
- assume eq_wq: "waiting_queue (schs s) cs = thread # rest"
+ assume eq_wq: "wq_fun (schs s) cs = thread # rest"
and t_in: "?t \<in> set rest"
and neq_cs: "csa \<noteq> cs"
- and t_in': "?t \<in> set (waiting_queue (schs s) csa)"
- show "?t = hd (waiting_queue (schs s) csa)"
+ and t_in': "?t \<in> set (wq_fun (schs s) csa)"
+ show "?t = hd (wq_fun (schs s) csa)"
proof -
- { assume neq_hd': "?t \<noteq> hd (waiting_queue (schs s) csa)"
+ { assume neq_hd': "?t \<noteq> hd (wq_fun (schs s) csa)"
from wq_distinct[OF step_back_vt[OF vtv], of cs] and
eq_wq[folded wq_def] and t_in eq_wq
have "?t \<noteq> thread" by auto
--- a/prio/PrioGDef.thy Sat Feb 11 09:14:14 2012 +0000
+++ b/prio/PrioGDef.thy Sat Feb 11 09:34:46 2012 +0000
@@ -176,8 +176,8 @@
threads:
*}
record schedule_state =
- waiting_queue :: "cs \<Rightarrow> thread list" -- {* The function assigning waiting queue. *}
- cur_preced :: "thread \<Rightarrow> precedence" -- {* The function assigning precedence. *}
+ wq_fun :: "cs \<Rightarrow> thread list" -- {* The function assigning waiting queue. *}
+ cprec_fun :: "thread \<Rightarrow> precedence" -- {* The function assigning precedence. *}
text {* \noindent
The following
@@ -220,7 +220,7 @@
*}
fun schs :: "state \<Rightarrow> schedule_state"
where
- "schs [] = (| waiting_queue = \<lambda> cs. [], cur_preced = (\<lambda>_. Prc 0 0) |)" |
+ "schs [] = (| wq_fun = \<lambda> cs. [], cprec_fun = (\<lambda>_. Prc 0 0) |)" |
-- {*
\begin{minipage}{0.9\textwidth}
@@ -248,22 +248,22 @@
\end{minipage}
*}
"schs (Create th prio # s) =
- (let wq = waiting_queue (schs s) in
- (|waiting_queue = wq, cur_preced = cpreced wq (Create th prio # s)|))"
+ (let wq = wq_fun (schs s) in
+ (|wq_fun = wq, cprec_fun = cpreced wq (Create th prio # s)|))"
| "schs (Exit th # s) =
- (let wq = waiting_queue (schs s) in
- (|waiting_queue = wq, cur_preced = cpreced wq (Exit th # s)|))"
+ (let wq = wq_fun (schs s) in
+ (|wq_fun = wq, cprec_fun = cpreced wq (Exit th # s)|))"
| "schs (Set th prio # s) =
- (let wq = waiting_queue (schs s) in
- (|waiting_queue = wq, cur_preced = cpreced wq (Set th prio # s)|))"
+ (let wq = wq_fun (schs s) in
+ (|wq_fun = wq, cprec_fun = cpreced wq (Set th prio # s)|))"
| "schs (P th cs # s) =
- (let wq = waiting_queue (schs s) in
+ (let wq = wq_fun (schs s) in
let new_wq = wq(cs := (wq cs @ [th])) in
- (|waiting_queue = new_wq, cur_preced = cpreced new_wq (P th cs # s)|))"
+ (|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|))"
| "schs (V th cs # s) =
- (let wq = waiting_queue (schs s) in
+ (let wq = wq_fun (schs s) in
let new_wq = wq(cs := release (wq cs)) in
- (|waiting_queue = new_wq, cur_preced = cpreced new_wq (V th cs # s)|))"
+ (|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|))"
lemma cpreced_initial:
"cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))"
@@ -274,7 +274,7 @@
lemma sch_old_def:
"schs (e#s) = (let ps = schs s in
- let pwq = waiting_queue ps in
+ let pwq = wq_fun ps in
let nwq = case e of
P th cs \<Rightarrow> pwq(cs:=(pwq cs @ [th])) |
V th cs \<Rightarrow> let nq = case (pwq cs) of
@@ -283,7 +283,7 @@
in pwq(cs:=nq) |
_ \<Rightarrow> pwq
in let ncp = cpreced nwq (e#s) in
- \<lparr>waiting_queue = nwq, cur_preced = ncp\<rparr>
+ \<lparr>wq_fun = nwq, cprec_fun = ncp\<rparr>
)"
apply(cases e)
apply(simp_all)
@@ -292,16 +292,16 @@
text {*
\noindent
- The following @{text "wq"} is a shorthand for @{text "waiting_queue"}.
+ The following @{text "wq"} is a shorthand for @{text "wq_fun"}.
*}
definition wq :: "state \<Rightarrow> cs \<Rightarrow> thread list"
- where "wq s = waiting_queue (schs s)"
+ where "wq s = wq_fun (schs s)"
text {* \noindent
- The following @{text "cp"} is a shorthand for @{text "cur_preced"}.
+ The following @{text "cp"} is a shorthand for @{text "cprec_fun"}.
*}
definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"
- where "cp s = cur_preced (schs s)"
+ where "cp s = cprec_fun (schs s)"
text {* \noindent
Functions @{text "holding"}, @{text "waiting"}, @{text "depend"} and
Binary file prio/paper.pdf has changed