--- a/Implementation.thy Thu Jul 07 13:32:09 2016 +0100
+++ b/Implementation.thy Fri Jul 08 01:25:19 2016 +0100
@@ -161,7 +161,7 @@
"ancestors (RAG s) (Cs cs) = {Th th}"
proof -
have "ancestors (RAG s) (Cs cs) = ancestors (RAG s) (Th th) \<union> {Th th}"
- by (rule rtree_RAG.ancestors_accum[OF edge_of_th])
+ by (rule forest_RAG.ancestors_accum[OF edge_of_th])
from this[unfolded ancestors_th] show ?thesis by simp
qed
@@ -193,7 +193,7 @@
"ancestors (RAG s) (Th taker) = {Th th, Cs cs}"
proof -
have "ancestors (RAG s) (Th taker) = ancestors (RAG s) (Cs cs) \<union> {Cs cs}"
- proof(rule rtree_RAG.ancestors_accum)
+ proof(rule forest_RAG.ancestors_accum)
from sub_RAGs' show "(Th taker, Cs cs) \<in> RAG s" by auto
qed
thus ?thesis using ancestors_th ancestors_cs by auto
@@ -311,7 +311,7 @@
lemma subtree_th:
"subtree (RAG (e#s)) (Th th) = subtree (RAG s) (Th th) - {Cs cs}"
-proof(unfold RAG_s, fold subtree_cs, rule rtree_RAG.subtree_del_inside)
+proof(unfold RAG_s, fold subtree_cs, rule forest_RAG.subtree_del_inside)
from edge_of_th
show "(Cs cs, Th th) \<in> edges_in (RAG s) (Th th)"
by (unfold edges_in_def, auto simp:subtree_def)
@@ -482,7 +482,7 @@
assume a_in: "a \<in> ?A"
from 1(2)
show "?f a = ?g a"
- proof(cases rule:vat_es.rtree_s.ancestors_childrenE[case_names in_ch out_ch])
+ proof(cases rule:vat_es.forest_s.ancestors_childrenE[case_names in_ch out_ch])
case in_ch
show ?thesis
proof(cases "a = u")
@@ -494,7 +494,7 @@
proof
assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)"
have "a = u"
- proof(rule vat_es.rtree_s.ancestors_children_unique)
+ proof(rule vat_es.forest_s.ancestors_children_unique)
from a_in' a_in show "a \<in> ancestors (tRAG (e#s)) (Th th) \<inter>
RTree.children (tRAG (e#s)) x" by auto
next
@@ -528,7 +528,7 @@
proof
assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)"
have "a = z"
- proof(rule vat_es.rtree_s.ancestors_children_unique)
+ proof(rule vat_es.forest_s.ancestors_children_unique)
from assms(1) h(1) have "z \<in> ancestors (tRAG (e#s)) (Th th)"
by (auto simp:ancestors_def)
with h(2) show " z \<in> ancestors (tRAG (e#s)) (Th th) \<inter>
--- a/Journal/Paper.thy Thu Jul 07 13:32:09 2016 +0100
+++ b/Journal/Paper.thy Fri Jul 08 01:25:19 2016 +0100
@@ -184,6 +184,9 @@
for a process that inherited a higher priority and exits a critical
section ``{\it it resumes the priority it had at the point of entry
into the critical section}''. This error can also be found in the
+ textbook \cite[Section 16.4.1]{LiYao03} where the authors write
+ ``{\it its priority is immediately lowered to the level originally assigned}'';
+ or in the
more recent textbook \cite[Page 119]{Laplante11} where the authors
state: ``{\it when [the task] exits the critical section that caused
the block, it reverts to the priority it had when it entered that
@@ -207,7 +210,7 @@
priority.}'' The same error is also repeated later in this textbook.
- While \cite{Laplante11,Liu00,book,Sha90,Silberschatz13} are the only
+ While \cite{Laplante11,LiYao03,Liu00,book,Sha90,Silberschatz13} are the only
formal publications we have found that specify the incorrect
behaviour, it seems also many informal descriptions of PIP overlook
the possibility that another high-priority might wait for a
--- a/Journal/document/root.bib Thu Jul 07 13:32:09 2016 +0100
+++ b/Journal/document/root.bib Fri Jul 08 01:25:19 2016 +0100
@@ -23,6 +23,15 @@
edition = {3rd}
}
+
+
+@Book{LiYao03,
+ author = {Q.~Li and C.~Yao},
+ title = {Real-Time Concepts for Embedded Systems},
+ publisher = {CRC Press},
+ year = {2003}
+}
+
@Book{Laplante11,
author = {P.~A.~Laplante and S.~J.~Ovaska},
title = {{R}eal-{T}ime {S}ystems {D}esign and {A}nalysis: {T}ools for the {P}ractitioner},
--- a/PIPBasics.thy Thu Jul 07 13:32:09 2016 +0100
+++ b/PIPBasics.thy Fri Jul 08 01:25:19 2016 +0100
@@ -2835,16 +2835,16 @@
context valid_trace
begin
-lemma rtree_RAG: "rtree (RAG s)"
+lemma forest_RAG: "forest (RAG s)"
using sgv_RAG acyclic_RAG
- by (unfold rtree_def, auto)
+ by (unfold forest_def, auto)
end
-sublocale valid_trace < rtree_RAG?: rtree "RAG s"
- using rtree_RAG .
-
-sublocale valid_trace < fsbtRAGs?: fgraph "RAG s"
+sublocale valid_trace < forest_RAG?: forest "RAG s"
+ using forest_RAG .
+
+sublocale valid_trace < fsbtRAGs?: fforest "RAG s"
proof
show "\<And>x. finite (children (RAG s) x)"
by (smt Collect_empty_eq Range.intros children_def finite.emptyI finite_RAG finite_fbranchI)
@@ -2886,7 +2886,7 @@
finite-branch relational tree (or forest):
*}
-sublocale valid_trace < rtree_s?: rtree "tRAG s"
+sublocale valid_trace < forest_s?: forest "tRAG s"
proof(unfold_locales)
from sgv_tRAG show "single_valued (tRAG s)" .
next
@@ -2894,7 +2894,7 @@
qed
-sublocale valid_trace < fsbttRAGs?: fgraph "tRAG s"
+sublocale valid_trace < fsbttRAGs?: fforest "tRAG s"
proof
fix x
show "finite (children (tRAG s) x)"
@@ -3210,7 +3210,7 @@
obtain xs1 xs2 where "rpath (RAG s) n xs1 (Th th1)"
"rpath (RAG s) n xs2 (Th th2)" by metis
hence False
- proof(cases rule:rtree_RAG.rpath_overlap')
+ proof(cases rule:forest_RAG.rpath_overlap')
case (less_1 xs3)
from rpath_star[OF this(3)]
have "Th th1 \<in> subtree (RAG s) (Th th2)"
--- a/RTree.thy Thu Jul 07 13:32:09 2016 +0100
+++ b/RTree.thy Fri Jul 08 01:25:19 2016 +0100
@@ -21,7 +21,7 @@
*}
-locale rtree =
+locale forest =
fixes r
assumes sgv: "single_valued r"
assumes acl: "acyclic r"
@@ -110,7 +110,7 @@
definition "children r x = {y. (y, x) \<in> r}"
-locale fgraph = rtree +
+locale fforest = forest +
assumes fb: "finite (children r x)"
assumes wf: "wf r"
begin
@@ -721,7 +721,7 @@
subsubsection {* Properties about relational trees *}
-context rtree
+context forest
begin
lemma ancestors_headE:
@@ -1350,7 +1350,7 @@
qed
qed
-end (* of rtree *)
+end (* of forest *)
lemma subtree_trancl:
"subtree r x = {x} \<union> {y. (y, x) \<in> r^+}" (is "?L = ?R")
@@ -1385,7 +1385,7 @@
"subtree r x = ({x} \<union> (\<Union> (subtree r ` (children r x))))" (is "?L = ?R")
by fast
-context fgraph
+context fforest
begin
lemma finite_subtree:
@@ -1557,19 +1557,6 @@
} thus ?thesis by (auto simp:acyclic_def)
qed
-lemma relpow_mult:
- "((r::'a rel) ^^ m) ^^ n = r ^^ (m*n)"
-proof(induct n arbitrary:m)
- case (Suc k m)
- thus ?case
- proof -
- have h: "(m * k + m) = (m + m * k)" by auto
- show ?thesis
- apply (simp add:Suc relpow_add[symmetric])
- by (unfold h, simp)
- qed
-qed simp
-
lemma compose_relpow_2 [intro, simp]:
assumes "r1 \<subseteq> r"
and "r2 \<subseteq> r"
@@ -1584,6 +1571,19 @@
} thus ?thesis by (auto simp:numeral_2_eq_2)
qed
+lemma relpow_mult:
+ "((r::'a rel) ^^ m) ^^ n = r ^^ (m*n)"
+proof(induct n arbitrary:m)
+ case (Suc k m)
+ thus ?case
+ proof -
+ have h: "(m * k + m) = (m + m * k)" by auto
+ show ?thesis
+ apply (simp add:Suc relpow_add[symmetric])
+ by (unfold h, simp)
+ qed
+qed simp
+
lemma acyclic_compose [intro, simp]:
assumes "acyclic r"
and "r1 \<subseteq> r"
@@ -1623,7 +1623,7 @@
show "finite (children r1 ` children r2 x)"
proof(rule finite_imageI)
from h(2) have "x \<in> Range r2" by auto
- from assms(2)[unfolded fgraph_def] this
+ from assms(2)[unfolded fforest_def] this
show "finite (children r2 x)" by auto
qed
next
@@ -1637,7 +1637,7 @@
next
case False
hence "y \<in> Range r1" by (unfold children_def, auto)
- from assms(1)[unfolded fgraph_def] this h1(2)
+ from assms(1)[unfolded fforest_def] this h1(2)
show ?thesis by auto
qed
qed
Binary file journal.pdf has changed