added some of the comments of the reviewers and made it compile with current Isabelle
--- a/prio/Moment.thy Fri Apr 13 13:12:43 2012 +0000
+++ b/prio/Moment.thy Sun Apr 15 21:53:12 2012 +0000
@@ -112,12 +112,37 @@
qed
lemma moment_restm_s: "(restm n s)@(moment n s) = s"
-by (metis firstn_restn_s moment_def restm_def rev_append rev_rev_ident)
+proof -
+ have " rev ((firstn n (rev s)) @ (restn n (rev s))) = s" (is "rev ?x = s")
+ proof -
+ have "?x = rev s" by (simp only:firstn_restn_s)
+ thus ?thesis by auto
+ qed
+ thus ?thesis
+ by (auto simp:restm_def moment_def)
+qed
declare restn.simps [simp del] firstn.simps[simp del]
lemma length_firstn_ge: "length s \<le> n \<Longrightarrow> length (firstn n s) = length s"
-by (metis firstn_ge)
+proof(induct n arbitrary:s, simp add:firstn.simps)
+ case (Suc k)
+ assume ih: "\<And> s. length (s::'a list) \<le> k \<Longrightarrow> length (firstn k s) = length s"
+ and le: "length s \<le> Suc k"
+ show ?case
+ proof(cases s)
+ case Nil
+ from Nil show ?thesis by simp
+ next
+ case (Cons x xs)
+ from le and Cons have "length xs \<le> k" by simp
+ from ih [OF this] have "length (firstn k xs) = length xs" .
+ moreover from Cons have "length (firstn (Suc k) s) = Suc (length (firstn k xs))"
+ by (simp add:firstn.simps)
+ moreover note Cons
+ ultimately show ?thesis by simp
+ qed
+qed
lemma length_firstn_le: "n \<le> length s \<Longrightarrow> length (firstn n s) = n"
proof(induct n arbitrary:s, simp add:firstn.simps)
@@ -141,26 +166,78 @@
lemma app_firstn_restn:
fixes s1 s2
shows "s1 = firstn (length s1) (s1 @ s2) \<and> s2 = restn (length s1) (s1 @ s2)"
-by (metis append_eq_conv_conj firstn_ge firstn_le firstn_restn_s le_refl)
+proof(rule length_eq_elim_l)
+ have "length s1 \<le> length (s1 @ s2)" by simp
+ from length_firstn_le [OF this]
+ show "length s1 = length (firstn (length s1) (s1 @ s2))" by simp
+next
+ from firstn_restn_s
+ show "s1 @ s2 = firstn (length s1) (s1 @ s2) @ restn (length s1) (s1 @ s2)"
+ by metis
+qed
+
+
lemma length_moment_le:
fixes k s
assumes le_k: "k \<le> length s"
shows "length (moment k s) = k"
-by (metis assms length_firstn_le length_rev moment_def)
+proof -
+ have "length (rev (firstn k (rev s))) = k"
+ proof -
+ have "length (rev (firstn k (rev s))) = length (firstn k (rev s))" by simp
+ also have "\<dots> = k"
+ proof(rule length_firstn_le)
+ from le_k show "k \<le> length (rev s)" by simp
+ qed
+ finally show ?thesis .
+ qed
+ thus ?thesis by (simp add:moment_def)
+qed
lemma app_moment_restm:
fixes s1 s2
shows "s1 = restm (length s2) (s1 @ s2) \<and> s2 = moment (length s2) (s1 @ s2)"
-by (metis app_firstn_restn length_rev moment_def restm_def rev_append rev_rev_ident)
+proof(rule length_eq_elim_r)
+ have "length s2 \<le> length (s1 @ s2)" by simp
+ from length_moment_le [OF this]
+ show "length s2 = length (moment (length s2) (s1 @ s2))" by simp
+next
+ from moment_restm_s
+ show "s1 @ s2 = restm (length s2) (s1 @ s2) @ moment (length s2) (s1 @ s2)"
+ by metis
+qed
lemma length_moment_ge:
fixes k s
assumes le_k: "length s \<le> k"
shows "length (moment k s) = (length s)"
-by (metis assms firstn_ge length_rev moment_def)
+proof -
+ have "length (rev (firstn k (rev s))) = length s"
+ proof -
+ have "length (rev (firstn k (rev s))) = length (firstn k (rev s))" by simp
+ also have "\<dots> = length s"
+ proof -
+ have "\<dots> = length (rev s)"
+ proof(rule length_firstn_ge)
+ from le_k show "length (rev s) \<le> k" by simp
+ qed
+ also have "\<dots> = length s" by simp
+ finally show ?thesis .
+ qed
+ finally show ?thesis .
+ qed
+ thus ?thesis by (simp add:moment_def)
+qed
lemma length_firstn: "(length (firstn n s) = length s) \<or> (length (firstn n s) = n)"
-by (metis length_firstn_ge length_firstn_le nat_le_linear)
+proof(cases "n \<le> length s")
+ case True
+ from length_firstn_le [OF True] show ?thesis by auto
+next
+ case False
+ from False have "length s \<le> n" by simp
+ from firstn_ge [OF this] show ?thesis by auto
+qed
lemma firstn_conc:
fixes m n
@@ -193,7 +270,45 @@
fixes i j k s
assumes eq_k: "j + i = k"
shows "restn k s = restn j (restn i s)"
-by (metis app_moment_restm append_take_drop_id assms drop_drop length_drop moment_def restn.simps)
+proof -
+ have "(firstn (length s - k) (rev s)) =
+ (firstn (length (rev (firstn (length s - i) (rev s))) - j)
+ (rev (rev (firstn (length s - i) (rev s)))))"
+ proof -
+ have "(firstn (length s - k) (rev s)) =
+ (firstn (length (rev (firstn (length s - i) (rev s))) - j)
+ (firstn (length s - i) (rev s)))"
+ proof -
+ have " (length (rev (firstn (length s - i) (rev s))) - j) = length s - k"
+ proof -
+ have "(length (rev (firstn (length s - i) (rev s))) - j) = (length s - i) - j"
+ proof -
+ have "(length (rev (firstn (length s - i) (rev s))) - j) =
+ length ((firstn (length s - i) (rev s))) - j"
+ by simp
+ also have "\<dots> = length ((firstn (length (rev s) - i) (rev s))) - j" by simp
+ also have "\<dots> = (length (rev s) - i) - j"
+ proof -
+ have "length ((firstn (length (rev s) - i) (rev s))) = (length (rev s) - i)"
+ by (rule length_firstn_le, simp)
+ thus ?thesis by simp
+ qed
+ also have "\<dots> = (length s - i) - j" by simp
+ finally show ?thesis .
+ qed
+ with eq_k show ?thesis by auto
+ qed
+ moreover have "(firstn (length s - k) (rev s)) =
+ (firstn (length s - k) (firstn (length s - i) (rev s)))"
+ proof(rule firstn_conc)
+ from eq_k show "length s - k \<le> length s - i" by simp
+ qed
+ ultimately show ?thesis by simp
+ qed
+ thus ?thesis by simp
+ qed
+ thus ?thesis by (simp only:restn.simps)
+qed
(*
value "down_to 2 0 [5, 4, 3, 2, 1, 0]"
@@ -204,12 +319,28 @@
by (simp add:from_to_def restn.simps)
lemma moment_app [simp]:
- assumes ile: "i \<le> length s"
+ assumes
+ ile: "i \<le> length s"
shows "moment i (s'@s) = moment i s"
-by (metis assms firstn_le length_rev moment_def rev_append)
+proof -
+ have "moment i (s'@s) = rev (firstn i (rev (s'@s)))" by (simp add:moment_def)
+ moreover have "firstn i (rev (s'@s)) = firstn i (rev s @ rev s')" by simp
+ moreover have "\<dots> = firstn i (rev s)"
+ proof(rule firstn_le)
+ have "length (rev s) = length s" by simp
+ with ile show "i \<le> length (rev s)" by simp
+ qed
+ ultimately show ?thesis by (simp add:moment_def)
+qed
lemma moment_eq [simp]: "moment (length s) (s'@s) = s"
-by (metis app_moment_restm)
+proof -
+ have "length s \<le> length s" by simp
+ from moment_app [OF this, of s']
+ have " moment (length s) (s' @ s) = moment (length s) s" .
+ moreover have "\<dots> = s" by (simp add:moment_def)
+ ultimately show ?thesis by simp
+qed
lemma moment_ge [simp]: "length s \<le> n \<Longrightarrow> moment n s = s"
by (unfold moment_def, simp)
@@ -403,16 +534,42 @@
assumes le_ij: "i \<le> j"
and le_jk: "j \<le> k"
shows "down_to k j s @ down_to j i s = down_to k i s"
-by (metis down_to_def from_to_conc le_ij le_jk rev_append)
+proof -
+ have "rev (from_to j k (rev s)) @ rev (from_to i j (rev s)) = rev (from_to i k (rev s))"
+ (is "?L = ?R")
+ proof -
+ have "?L = rev (from_to i j (rev s) @ from_to j k (rev s))" by simp
+ also have "\<dots> = ?R" (is "rev ?x = rev ?y")
+ proof -
+ have "?x = ?y" by (rule from_to_conc[OF le_ij le_jk])
+ thus ?thesis by simp
+ qed
+ finally show ?thesis .
+ qed
+ thus ?thesis by (simp add:down_to_def)
+qed
lemma restn_ge:
fixes s k
assumes le_k: "length s \<le> k"
shows "restn k s = []"
-by (metis assms diff_is_0_eq moment_def moment_zero restn.simps)
+proof -
+ from firstn_restn_s [of k s, symmetric] have "s = (firstn k s) @ (restn k s)" .
+ hence "length s = length \<dots>" by simp
+ also have "\<dots> = length (firstn k s) + length (restn k s)" by simp
+ finally have "length s = ..." by simp
+ moreover from length_firstn_ge and le_k
+ have "length (firstn k s) = length s" by simp
+ ultimately have "length (restn k s) = 0" by auto
+ thus ?thesis by auto
+qed
lemma from_to_ge: "length s \<le> k \<Longrightarrow> from_to k j s = []"
-by (metis firstn_nil from_to_def restn_ge)
+proof(simp only:from_to_def)
+ assume "length s \<le> k"
+ from restn_ge [OF this]
+ show "firstn (j - k) (restn k s) = []" by simp
+qed
(*
value "from_to 2 5 [0, 1, 2, 3, 4]"
@@ -423,31 +580,166 @@
fixes k j s
assumes le_j: "length s \<le> j"
shows "from_to k j s = restn k s"
-by (metis app_moment_restm append_Nil2 append_take_drop_id assms diff_is_0_eq' drop_take firstn_restn_s from_to_def length_drop moment_def moment_zero restn.simps)
+proof -
+ have "from_to 0 k s @ from_to k j s = from_to 0 j s"
+ proof(cases "k \<le> j")
+ case True
+ from from_to_conc True show ?thesis by auto
+ next
+ case False
+ from False le_j have lek: "length s \<le> k" by auto
+ from from_to_ge [OF this] have "from_to k j s = []" .
+ hence "from_to 0 k s @ from_to k j s = from_to 0 k s" by simp
+ also have "\<dots> = s"
+ proof -
+ from from_to_firstn [of k s]
+ have "\<dots> = firstn k s" .
+ also have "\<dots> = s" by (rule firstn_ge [OF lek])
+ finally show ?thesis .
+ qed
+ finally have "from_to 0 k s @ from_to k j s = s" .
+ moreover have "from_to 0 j s = s"
+ proof -
+ have "from_to 0 j s = firstn j s" by (simp add:from_to_firstn)
+ also have "\<dots> = s"
+ proof(rule firstn_ge)
+ from le_j show "length s \<le> j " by simp
+ qed
+ finally show ?thesis .
+ qed
+ ultimately show ?thesis by auto
+ qed
+ also have "\<dots> = s"
+ proof -
+ from from_to_firstn have "\<dots> = firstn j s" .
+ also have "\<dots> = s"
+ proof(rule firstn_ge)
+ from le_j show "length s \<le> j" by simp
+ qed
+ finally show ?thesis .
+ qed
+ finally have "from_to 0 k s @ from_to k j s = s" .
+ moreover have "from_to 0 k s @ restn k s = s"
+ proof -
+ from from_to_firstn [of k s]
+ have "from_to 0 k s = firstn k s" .
+ thus ?thesis by (simp add:firstn_restn_s)
+ qed
+ ultimately have "from_to 0 k s @ from_to k j s =
+ from_to 0 k s @ restn k s" by simp
+ thus ?thesis by auto
+qed
lemma down_to_moment: "down_to k 0 s = moment k s"
-by (metis down_to_def from_to_firstn moment_def)
+proof -
+ have "rev (from_to 0 k (rev s)) = rev (firstn k (rev s))"
+ using from_to_firstn by metis
+ thus ?thesis by (simp add:down_to_def moment_def)
+qed
lemma down_to_restm:
assumes le_s: "length s \<le> j"
shows "down_to j k s = restm k s"
-by (metis assms down_to_def from_to_restn length_rev restm_def)
+proof -
+ have "rev (from_to k j (rev s)) = rev (restn k (rev s))" (is "?L = ?R")
+ proof -
+ from le_s have "length (rev s) \<le> j" by simp
+ from from_to_restn [OF this, of k] show ?thesis by simp
+ qed
+ thus ?thesis by (simp add:down_to_def restm_def)
+qed
lemma moment_split: "moment (m+i) s = down_to (m+i) i s @down_to i 0 s"
-by (metis down_to_conc down_to_moment le0 le_add1 nat_add_commute)
+proof -
+ have "moment (m + i) s = down_to (m+i) 0 s" using down_to_moment by metis
+ also have "\<dots> = (down_to (m+i) i s) @ (down_to i 0 s)"
+ by(rule down_to_conc[symmetric], auto)
+ finally show ?thesis .
+qed
lemma length_restn: "length (restn i s) = length s - i"
-by (metis diff_le_self length_firstn_le length_rev restn.simps)
+proof(cases "i \<le> length s")
+ case True
+ from length_firstn_le [OF this] have "length (firstn i s) = i" .
+ moreover have "length s = length (firstn i s) + length (restn i s)"
+ proof -
+ have "s = firstn i s @ restn i s" using firstn_restn_s by metis
+ hence "length s = length \<dots>" by simp
+ thus ?thesis by simp
+ qed
+ ultimately show ?thesis by simp
+next
+ case False
+ hence "length s \<le> i" by simp
+ from restn_ge [OF this] have "restn i s = []" .
+ with False show ?thesis by simp
+qed
lemma length_from_to_in:
fixes i j s
assumes le_ij: "i \<le> j"
and le_j: "j \<le> length s"
shows "length (from_to i j s) = j - i"
-by (metis diff_le_mono from_to_def le_j length_firstn_le length_restn)
+proof -
+ have "from_to 0 j s = from_to 0 i s @ from_to i j s"
+ by (rule from_to_conc[symmetric, OF _ le_ij], simp)
+ moreover have "length (from_to 0 j s) = j"
+ proof -
+ have "from_to 0 j s = firstn j s" using from_to_firstn by metis
+ moreover have "length \<dots> = j" by (rule length_firstn_le [OF le_j])
+ ultimately show ?thesis by simp
+ qed
+ moreover have "length (from_to 0 i s) = i"
+ proof -
+ have "from_to 0 i s = firstn i s" using from_to_firstn by metis
+ moreover have "length \<dots> = i"
+ proof (rule length_firstn_le)
+ from le_ij le_j show "i \<le> length s" by simp
+ qed
+ ultimately show ?thesis by simp
+ qed
+ ultimately show ?thesis by auto
+qed
lemma firstn_restn_from_to: "from_to i (m + i) s = firstn m (restn i s)"
-by (metis diff_add_inverse2 from_to_def)
+proof(cases "m+i \<le> length s")
+ case True
+ have "restn i s = from_to i (m+i) s @ from_to (m+i) (length s) s"
+ proof -
+ have "restn i s = from_to i (length s) s"
+ by(rule from_to_restn[symmetric], simp)
+ also have "\<dots> = from_to i (m+i) s @ from_to (m+i) (length s) s"
+ by(rule from_to_conc[symmetric, OF _ True], simp)
+ finally show ?thesis .
+ qed
+ hence "firstn m (restn i s) = firstn m \<dots>" by simp
+ moreover have "\<dots> = firstn (length (from_to i (m+i) s))
+ (from_to i (m+i) s @ from_to (m+i) (length s) s)"
+ proof -
+ have "length (from_to i (m+i) s) = m"
+ proof -
+ have "length (from_to i (m+i) s) = (m+i) - i"
+ by(rule length_from_to_in [OF _ True], simp)
+ thus ?thesis by simp
+ qed
+ thus ?thesis by simp
+ qed
+ ultimately show ?thesis using app_firstn_restn by metis
+next
+ case False
+ hence "length s \<le> m + i" by simp
+ from from_to_restn [OF this]
+ have "from_to i (m + i) s = restn i s" .
+ moreover have "firstn m (restn i s) = restn i s"
+ proof(rule firstn_ge)
+ show "length (restn i s) \<le> m"
+ proof -
+ have "length (restn i s) = length s - i" using length_restn by metis
+ with False show ?thesis by simp
+ qed
+ qed
+ ultimately show ?thesis by simp
+qed
lemma down_to_moment_restm:
fixes m i s
@@ -457,9 +749,25 @@
lemma moment_plus_split:
fixes m i s
shows "moment (m + i) s = moment m (restm i s) @ moment i s"
-by (metis down_to_moment down_to_moment_restm moment_split)
+proof -
+ from moment_split [of m i s]
+ have "moment (m + i) s = down_to (m + i) i s @ down_to i 0 s" .
+ also have "\<dots> = down_to (m+i) i s @ moment i s" using down_to_moment by simp
+ also from down_to_moment_restm have "\<dots> = moment m (restm i s) @ moment i s"
+ by simp
+ finally show ?thesis .
+qed
lemma length_restm: "length (restm i s) = length s - i"
-by (metis length_restn length_rev restm_def)
+proof -
+ have "length (rev (restn i (rev s))) = length s - i" (is "?L = ?R")
+ proof -
+ have "?L = length (restn i (rev s))" by simp
+ also have "\<dots> = length (rev s) - i" using length_restn by metis
+ also have "\<dots> = ?R" by simp
+ finally show ?thesis .
+ qed
+ thus ?thesis by (simp add:restm_def)
+qed
end
\ No newline at end of file
--- a/prio/Paper/Paper.thy Fri Apr 13 13:12:43 2012 +0000
+++ b/prio/Paper/Paper.thy Sun Apr 15 21:53:12 2012 +0000
@@ -55,10 +55,10 @@
$H$(igh), $M$(edium) and $L$(ow). We would expect that the thread
$H$ blocks any other thread with lower priority and itself cannot
be blocked by any thread with lower priority. Alas, in a naive
- implementation of resource looking and priorities this property can
+ implementation of resource locking and priorities this property can
be violated. Even worse, $H$ can be delayed indefinitely by
threads with lower priorities. For this let $L$ be in the
- possession of a lock for a resource that also $H$ needs. $H$ must
+ possession of a lock for a resource that $H$ also needs. $H$ must
therefore wait for $L$ to exit the critical section and release this
lock. The problem is that $L$ might in turn be blocked by any
thread with priority $M$, and so $H$ sits there potentially waiting
@@ -76,9 +76,9 @@
craft could only resume the next day (the mission and data already
collected were fortunately not lost, because of a clever system
design). The reason for the shutdowns was that the scheduling
- software fell victim of Priority Inversion: a low priority thread
+ software fell victim to Priority Inversion: a low priority thread
locking a resource prevented a high priority thread from running in
- time leading to a system reset. Once the problem was found, it was
+ time, leading to a system reset. Once the problem was found, it was
rectified by enabling the \emph{Priority Inheritance Protocol} (PIP)
\cite{Sha90}\footnote{Sha et al.~call it the \emph{Basic Priority
Inheritance Protocol} \cite{Sha90} and others sometimes also call it
@@ -114,7 +114,7 @@
\end{quote}
\noindent
- He suggests to avoid PIP altogether by not allowing critical
+ He suggests avoiding PIP altogether by not allowing critical
sections to be preempted. Unfortunately, this solution does not
help in real-time systems with hard deadlines for high-priority
threads.
@@ -136,10 +136,10 @@
\end{quote}
\noindent
- The criticism by Yodaiken, Baker and others suggests to us to look
- again at PIP from a more abstract level (but still concrete enough
- to inform an implementation), and makes PIP an ideal candidate for a
- formal verification. One reason, of course, is that the original
+ The criticism by Yodaiken, Baker and others suggests another look
+ at PIP from a more abstract level (but still concrete enough
+ to inform an implementation), and makes PIP a good candidate for a
+ formal verification. An additional reason is that the original
presentation of PIP~\cite{Sha90}, despite being informally
``proved'' correct, is actually \emph{flawed}.
@@ -155,7 +155,7 @@
$H'$ each wait for one of them. If $L$ releases one resource
so that $H$, say, can proceed, then we still have Priority Inversion
with $H'$ (which waits for the other resource). The correct
- behaviour for $L$ is to revert to the highest remaining priority of
+ behaviour for $L$ is to switch to the highest remaining priority of
the threads that it blocks. The advantage of formalising the
correctness of a high-level specification of PIP in a theorem prover
is that such issues clearly show up and cannot be overlooked as in
@@ -173,8 +173,8 @@
to prove stronger properties that, as we will show, can inform an
efficient implementation. For example, we found by ``playing'' with the formalisation
that the choice of the next thread to take over a lock when a
- resource is released is irrelevant for PIP being correct. Something
- which has not been mentioned in the relevant literature.
+ resource is released is irrelevant for PIP being correct---a fact
+ that has not been mentioned in the relevant literature.
*}
section {* Formal Model of the Priority Inheritance Protocol *}
@@ -512,7 +512,7 @@
\noindent
With these abbreviations in place we can introduce
- the notion of threads being @{term readys} in a state (i.e.~threads
+ the notion of a thread being @{term ready} in a state (i.e.~threads
that do not wait for any resource) and the running thread.
\begin{isabelle}\ \ \ \ \ %%%
@@ -538,7 +538,7 @@
Finally we can define what a \emph{valid state} is in our model of PIP. For
example we cannot expect to be able to exit a thread, if it was not
- created yet. This would cause havoc in any scheduler.
+ created yet.
These validity constraints on states are characterised by the
inductive predicate @{term "step"} and @{term vt}. We first give five inference rules
for @{term step} relating a state and an event that can happen next.
@@ -627,7 +627,7 @@
programmers must ensure that threads are programmed in this way. However, even
taking this assumption into account, the correctness properties of
Sha et al.~are
- \emph{not} true for their version of PIP---despide being ``proved''. As Yodaiken
+ \emph{not} true for their version of PIP---despite being ``proved''. As Yodaiken
\cite{Yodaiken02} pointed out: If a low-priority thread possesses
locks to two resources for which two high-priority threads are
waiting for, then lowering the priority prematurely after giving up
@@ -734,7 +734,7 @@
In what follows we will describe properties of PIP that allow us to prove
Theorem~\ref{mainthm} and, when instructive, briefly describe our argument.
- It is relatively easily to see that
+ It is relatively easy to see that
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@@ -776,7 +776,7 @@
\end{isabelle}
\noindent
- The acyclicity property follow from how we restricted the events in
+ The acyclicity property follows from how we restricted the events in
@{text step}; similarly the finiteness and well-foundedness property.
The last two properties establish that every thread in a @{text "RAG"}
(either holding or waiting for a resource) is a live thread.
@@ -786,7 +786,7 @@
\begin{lemma}\label{mainlem}
Given the assumptions about states @{text "s"} and @{text "s' @ s"},
the thread @{text th} and the events in @{text "s'"},
- if @{term "th' \<in> treads (s' @ s)"}, @{text "th' \<noteq> th"} and @{text "detached (s' @ s) th'"}\\
+ if @{term "th' \<in> threads (s' @ s)"}, @{text "th' \<noteq> th"} and @{text "detached (s' @ s) th'"}\\
then @{text "th' \<notin> running (s' @ s)"}.
\end{lemma}
@@ -978,7 +978,7 @@
\end{isabelle}
\noindent
- where a child is a thread that is only one ``hop'' away from the tread
+ where a child is a thread that is only one ``hop'' away from the thread
@{text th} in the @{term RAG} (and waiting for @{text th} to release
a resource). We can prove the following lemma.
@@ -1190,7 +1190,7 @@
As can be seen, a pleasing byproduct of our formalisation is that the properties in
this section closely inform an implementation of PIP, namely whether the
@{text RAG} needs to be reconfigured or current precedences need to
- by recalculated for an event. This information is provided by the lemmas we proved.
+ be recalculated for an event. This information is provided by the lemmas we proved.
*}
section {* Conclusion *}
@@ -1269,7 +1269,7 @@
definitions and proofs span over 770 lines of code. The properties relevant
for an implementation require 2000 lines. The code of our formalisation
can be downloaded from
- \url{http://www.dcs.kcl.ac.uk/staff/urbanc/pip.html}.
+ \url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}.
\bibliographystyle{plain}
\bibliography{root}
--- a/prio/PrioG.thy Fri Apr 13 13:12:43 2012 +0000
+++ b/prio/PrioG.thy Sun Apr 15 21:53:12 2012 +0000
@@ -2,7 +2,6 @@
imports PrioGDef
begin
-
lemma runing_ready:
shows "runing s \<subseteq> readys s"
unfolding runing_def readys_def
@@ -416,7 +415,26 @@
and xz: "(x, z) \<in> r^+"
and neq: "y \<noteq> z"
shows "(y, z) \<in> r^+"
-by (metis neq rtranclD tranclD unique xy xz)
+proof -
+ from xz and neq show ?thesis
+ proof(induct)
+ case (base ya)
+ have "(x, ya) \<in> r" by fact
+ from unique [OF xy this] have "y = ya" .
+ with base show ?case by auto
+ next
+ case (step ya z)
+ show ?case
+ proof(cases "y = ya")
+ case True
+ from step True show ?thesis by simp
+ next
+ case False
+ from step False
+ show ?thesis by auto
+ qed
+ qed
+qed
lemma unique_base:
fixes r x y z
@@ -425,7 +443,25 @@
and xz: "(x, z) \<in> r^+"
and neq_yz: "y \<noteq> z"
shows "(y, z) \<in> r^+"
-by (metis neq_yz unique unique_minus xy xz)
+proof -
+ from xz neq_yz show ?thesis
+ proof(induct)
+ case (base ya)
+ from xy unique base show ?case by auto
+ next
+ case (step ya z)
+ show ?case
+ proof(cases "y = ya")
+ case True
+ from True step show ?thesis by auto
+ next
+ case False
+ from False step
+ have "(y, ya) \<in> r\<^sup>+" by auto
+ with step show ?thesis by auto
+ qed
+ qed
+qed
lemma unique_chain:
fixes r x y z
@@ -636,7 +672,25 @@
"\<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)
-by (metis (lifting, full_types) List.member_def distinct.simps(2) hd_in_set member_rec(2) someI_ex step_back_vt wq_def wq_distinct)
+proof -
+ fix rest
+ 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)
+ \<notin> set (SOME q. distinct q \<and> set q = set rest)"
+ have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
+ proof(rule someI2)
+ from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq
+ show "distinct rest \<and> set rest = set rest" by auto
+ next
+ fix x assume "distinct x \<and> set x = set rest"
+ hence "set x = set rest" by auto
+ with nrest
+ show "x \<noteq> []" by (case_tac x, auto)
+ qed
+ with ni show "False" by auto
+qed
lemma step_v_release_inv[elim_format]:
"\<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>
@@ -664,7 +718,61 @@
lemma step_v_waiting_mono:
"\<And>t c. \<lbrakk>vt (V th cs # s); waiting (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> waiting (wq s) t c"
-by (metis abs2 block_pre cs_waiting_def event.simps(20))
+proof -
+ fix t c
+ let ?s' = "(V th cs # s)"
+ assume vt: "vt ?s'"
+ and wt: "waiting (wq ?s') t c"
+ show "waiting (wq s) t c"
+ proof(cases "c = cs")
+ case False
+ assume neq_cs: "c \<noteq> cs"
+ hence "waiting (wq ?s') t c = waiting (wq s) t c"
+ by (unfold cs_waiting_def wq_def, auto simp:Let_def)
+ with wt show ?thesis by simp
+ next
+ case True
+ with wt show ?thesis
+ apply (unfold cs_waiting_def wq_def, auto simp:Let_def split:list.splits)
+ proof -
+ 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: "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]
+ show "distinct list \<and> set list = set list" by auto
+ next
+ fix x assume "distinct x \<and> set x = set list"
+ thus "set x = set list" by auto
+ qed
+ with not_in is_in show "t = a" by auto
+ next
+ fix list
+ assume is_waiting: "waiting (wq (V th cs # s)) t cs"
+ 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 -
+ assume " t \<in> set (SOME q. distinct q \<and> set q = set list)"
+ moreover have "\<dots> = set list"
+ proof(rule someI2)
+ from wq_distinct [OF step_back_vt[OF vt], of cs]
+ and eq_wq[folded wq_def]
+ show "distinct list \<and> set list = set list" by auto
+ next
+ fix x assume "distinct x \<and> set x = set list"
+ thus "set x = set list" by auto
+ qed
+ ultimately show "t \<in> set list" by simp
+ qed
+ with eq_wq and wq_distinct [OF step_back_vt[OF vt], of cs, unfolded wq_def]
+ show False by auto
+ qed
+ qed
+qed
lemma step_depend_v:
fixes th::thread
@@ -700,7 +808,13 @@
fixes A
assumes h: "\<And> x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x = y"
shows "A = {} \<or> (\<exists> a. A = {a})"
-by (metis assms insertCI nonempty_iff)
+proof(cases "A = {}")
+ case True thus ?thesis by simp
+next
+ case False then obtain a where "a \<in> A" by auto
+ with h have "A = {a}" by auto
+ thus ?thesis by simp
+qed
lemma depend_target_th: "(Th th, x) \<in> depend (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
by (unfold s_depend_def, auto)
@@ -962,7 +1076,13 @@
fixes s
assumes vt: "vt s"
shows "wf ((depend s)^-1)"
-by (metis acyclic_depend assms finite_acyclic_wf_converse finite_depend)
+proof(rule finite_acyclic_wf_converse)
+ from finite_depend [OF vt]
+ show "finite (depend s)" .
+next
+ from acyclic_depend[OF vt]
+ show "acyclic (depend s)" .
+qed
lemma hd_np_in: "x \<in> set l \<Longrightarrow> hd l \<in> set l"
by (induct l, auto)
@@ -1083,17 +1203,31 @@
and eq_wq: "wq s cs = thread#rest"
and not_in: "th \<notin> set rest"
shows "(th \<in> readys (V thread cs#s)) = (th \<in> readys s)"
-using assms
-apply (auto simp:readys_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)
-by (metis (lifting, full_types) distinct.simps(2) someI_ex wq_def wq_distinct)
+proof -
+ from assms show ?thesis
+ apply (auto simp:readys_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"
+ 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, 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
+ qed
+ with th_nin th_in show False by auto
+ qed
+qed
lemma chain_building:
assumes vt: "vt s"
@@ -1270,8 +1404,51 @@
apply (insert wq_distinct[OF step_back_vt[OF vtv], of cs])
apply (unfold holdents_def, unfold step_depend_v[OF vtv],
auto simp:next_th_def)
- apply (metis (lifting, full_types) hd_in_set hd_np_in someI_ex)
- by (metis (lifting, full_types) hd_in_set hd_np_in someI_ex)
+ proof -
+ fix rest
+ assume dst: "distinct (rest::thread list)"
+ and ne: "rest \<noteq> []"
+ and hd_ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
+ moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
+ proof(rule someI2)
+ from dst 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
+ qed
+ ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<notin>
+ set (SOME q. distinct q \<and> set q = set rest)" by simp
+ moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
+ proof(rule someI2)
+ from dst show "distinct rest \<and> set rest = set rest" by auto
+ next
+ fix x assume " distinct x \<and> set x = set rest" with ne
+ show "x \<noteq> []" by auto
+ qed
+ ultimately
+ show "(Cs cs, Th (hd (SOME q. distinct q \<and> set q = set rest))) \<in> depend s"
+ by auto
+ next
+ fix rest
+ assume dst: "distinct (rest::thread list)"
+ and ne: "rest \<noteq> []"
+ and hd_ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
+ moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
+ proof(rule someI2)
+ from dst 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
+ qed
+ ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<notin>
+ set (SOME q. distinct q \<and> set q = set rest)" by simp
+ moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
+ proof(rule someI2)
+ from dst show "distinct rest \<and> set rest = set rest" by auto
+ next
+ fix x assume " distinct x \<and> set x = set rest" with ne
+ show "x \<noteq> []" by auto
+ qed
+ ultimately show "False" by auto
+ qed
ultimately
have "holdents s thread = insert cs (holdents (V thread cs#s) thread)"
by auto
@@ -1368,7 +1545,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 thread_P vt stp ih have vtp: "vt (P thread cs#s)" by auto
+ from thread_P vt stp ih 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
@@ -2052,8 +2229,9 @@
with eq_th12 eq_th' have "th1 \<in> dependents (wq s) th2" by simp
hence "(Th th1, Th th2) \<in> (depend s)^+"
by (unfold cs_dependents_def s_depend_def cs_depend_def, simp)
- hence "Th th1 \<in> Domain ((depend s)^+)" using Domain_def [of "(depend s)^+"]
- by auto
+ hence "Th th1 \<in> Domain ((depend s)^+)"
+ apply (unfold cs_dependents_def cs_depend_def s_depend_def)
+ by (auto simp:Domain_def)
hence "Th th1 \<in> Domain (depend s)" by (simp add:trancl_domain)
then obtain n where d: "(Th th1, n) \<in> depend s" by (auto simp:Domain_def)
from depend_target_th [OF this]
@@ -2073,8 +2251,9 @@
with th1'_in eq_th12 have "th2 \<in> dependents (wq s) th1" by simp
hence "(Th th2, Th th1) \<in> (depend s)^+"
by (unfold cs_dependents_def s_depend_def cs_depend_def, simp)
- hence "Th th2 \<in> Domain ((depend s)^+)" using Domain_def [of "(depend s)^+"]
- by auto
+ hence "Th th2 \<in> Domain ((depend s)^+)"
+ apply (unfold cs_dependents_def cs_depend_def s_depend_def)
+ by (auto simp:Domain_def)
hence "Th th2 \<in> Domain (depend s)" by (simp add:trancl_domain)
then obtain n where d: "(Th th2, n) \<in> depend s" by (auto simp:Domain_def)
from depend_target_th [OF this]
@@ -2131,20 +2310,106 @@
assumes le_ij: "i \<le> j"
and le_js: "j \<le> length s"
shows "length (down_to j i s) = j - i"
-by (metis down_to_def le_ij le_js length_from_to_in length_rev)
+proof -
+ have "length (down_to j i s) = length (from_to i j (rev s))"
+ by (unfold down_to_def, auto)
+ also have "\<dots> = j - i"
+ proof(rule length_from_to_in[OF le_ij])
+ from le_js show "j \<le> length (rev s)" by simp
+ qed
+ finally show ?thesis .
+qed
lemma moment_head:
assumes le_it: "Suc i \<le> length t"
obtains e where "moment (Suc i) t = e#moment i t"
-by (metis assms moment_plus)
+proof -
+ have "i \<le> Suc i" by simp
+ from length_down_to_in [OF this le_it]
+ have "length (down_to (Suc i) i t) = 1" by auto
+ then obtain e where "down_to (Suc i) i t = [e]"
+ apply (cases "(down_to (Suc i) i t)") by auto
+ moreover have "down_to (Suc i) 0 t = down_to (Suc i) i t @ down_to i 0 t"
+ by (rule down_to_conc[symmetric], auto)
+ ultimately have eq_me: "moment (Suc i) t = e#(moment i t)"
+ by (auto simp:down_to_moment)
+ from that [OF this] show ?thesis .
+qed
lemma cnp_cnv_eq:
fixes th s
assumes "vt s"
and "th \<notin> threads s"
shows "cntP s th = cntV s th"
-by (metis (full_types) add_0_right assms(1) assms(2) cnp_cnv_cncs not_thread_cncs)
+proof -
+ from assms show ?thesis
+ proof(induct)
+ case (vt_cons s e)
+ have ih: "th \<notin> threads s \<Longrightarrow> cntP s th = cntV s th" by fact
+ have not_in: "th \<notin> threads (e # s)" by fact
+ have "step s e" by fact
+ thus ?case proof(cases)
+ case (thread_create thread prio)
+ assume eq_e: "e = Create thread prio"
+ hence "thread \<in> threads (e#s)" by simp
+ with not_in and eq_e have "th \<notin> threads s" by auto
+ from ih [OF this] show ?thesis using eq_e
+ by (auto simp:cntP_def cntV_def count_def)
+ next
+ case (thread_exit thread)
+ assume eq_e: "e = Exit thread"
+ and not_holding: "holdents s thread = {}"
+ 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)
+ moreover note cnp_cnv_cncs[OF vt_s, of thread]
+ ultimately have eq_thread: "cntP s thread = cntV s thread" by auto
+ show ?thesis
+ proof(cases "th = thread")
+ case True
+ with eq_thread eq_e show ?thesis
+ by (auto simp:cntP_def cntV_def count_def)
+ next
+ case False
+ with not_in and eq_e have "th \<notin> threads s" by simp
+ from ih[OF this] and eq_e show ?thesis
+ by (auto simp:cntP_def cntV_def count_def)
+ qed
+ next
+ case (thread_P thread cs)
+ assume eq_e: "e = P thread cs"
+ have "thread \<in> runing s" by fact
+ with not_in eq_e have neq_th: "thread \<noteq> th"
+ by (auto simp:runing_def readys_def)
+ from not_in eq_e have "th \<notin> threads s" by simp
+ from ih[OF this] and neq_th and eq_e show ?thesis
+ by (auto simp:cntP_def cntV_def count_def)
+ next
+ case (thread_V thread cs)
+ assume eq_e: "e = V thread cs"
+ have "thread \<in> runing s" by fact
+ with not_in eq_e have neq_th: "thread \<noteq> th"
+ by (auto simp:runing_def readys_def)
+ from not_in eq_e have "th \<notin> threads s" by simp
+ from ih[OF this] and neq_th and eq_e show ?thesis
+ by (auto simp:cntP_def cntV_def count_def)
+ next
+ case (thread_set thread prio)
+ assume eq_e: "e = Set thread prio"
+ and "thread \<in> runing s"
+ hence "thread \<in> threads (e#s)"
+ by (simp add:runing_def readys_def)
+ with not_in and eq_e have "th \<notin> threads s" by auto
+ from ih [OF this] show ?thesis using eq_e
+ by (auto simp:cntP_def cntV_def count_def)
+ qed
+ next
+ case vt_nil
+ show ?case by (auto simp:cntP_def cntV_def count_def)
+ qed
+qed
lemma eq_depend:
"depend (wq s) = depend s"
@@ -2252,8 +2517,43 @@
lemma le_cp:
assumes vt: "vt s"
shows "preced th s \<le> cp s th"
-apply(unfold cp_eq_cpreced preced_def cpreced_def, simp)
-by (metis (mono_tags) Max_ge assms dependents_threads finite_imageI finite_insert finite_threads insertI1 preced_def rev_finite_subset)
+proof(unfold cp_eq_cpreced preced_def cpreced_def, simp)
+ show "Prc (original_priority th s) (birthtime th s)
+ \<le> Max (insert (Prc (original_priority th s) (birthtime th s))
+ ((\<lambda>th. Prc (original_priority th s) (birthtime th s)) ` dependents (wq s) th))"
+ (is "?l \<le> Max (insert ?l ?A)")
+ proof(cases "?A = {}")
+ case False
+ have "finite ?A" (is "finite (?f ` ?B)")
+ proof -
+ have "finite ?B"
+ proof-
+ have "finite {th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+}"
+ proof -
+ let ?F = "\<lambda> (x, y). the_th x"
+ have "{th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+} \<subseteq> ?F ` ((depend (wq s))\<^sup>+)"
+ apply (auto simp:image_def)
+ by (rule_tac x = "(Th x, Th th)" in bexI, auto)
+ moreover have "finite \<dots>"
+ proof -
+ from finite_depend[OF vt] have "finite (depend s)" .
+ hence "finite ((depend (wq s))\<^sup>+)"
+ apply (unfold finite_trancl)
+ by (auto simp: s_depend_def cs_depend_def wq_def)
+ thus ?thesis by auto
+ qed
+ ultimately show ?thesis by (auto intro:finite_subset)
+ qed
+ thus ?thesis by (simp add:cs_dependents_def)
+ qed
+ thus ?thesis by simp
+ qed
+ from Max_insert [OF this False, of ?l] show ?thesis by auto
+ next
+ case True
+ thus ?thesis by auto
+ qed
+qed
lemma max_cp_eq:
assumes vt: "vt s"
Binary file prio/paper.pdf has changed