# HG changeset patch
# User urbanc
# Date 1329147765 0
# Node ID 3d154253d5fef00c0fa9b6a7dce3eecdeeb1268a
# Parent  09281ccb31bd179f8dc2137e096db29c2354b861
proof idea

diff -r 09281ccb31bd -r 3d154253d5fe prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Mon Feb 13 15:35:08 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Feb 13 15:42:45 2012 +0000
@@ -814,6 +814,78 @@
 end
 (*>*)
 
+subsection {* Proof idea *}
+
+(*<*)
+context extend_highest_gen
+begin
+print_locale extend_highest_gen
+thm extend_highest_gen_def
+thm extend_highest_gen_axioms_def
+thm highest_gen_def
+(*>*)
+
+text {*
+The reason that only threads which already held some resoures
+can be runing and block @{text "th"} is that if , otherwise, one thread 
+does not hold any resource, it may never have its prioirty raised
+and will not get a chance to run. This fact is supported by 
+lemma @{text "moment_blocked"}:
+@{thm [display] moment_blocked}
+When instantiating  @{text "i"} to @{text "0"}, the lemma means threads which did not hold any
+resource in state @{text "s"} will not have a change to run latter. Rephrased, it means 
+any thread which is running after @{text "th"} became the highest must have already held
+some resource at state @{text "s"}.
+
+
+  When instantiating @{text "i"} to a number larger than @{text "0"}, the lemma means 
+  if a thread releases all its resources at some moment in @{text "t"}, after that, 
+  it may never get a change to run. If every thread releases its resource in finite duration,
+  then after a while, only thread @{text "th"} is left running. This shows how indefinite 
+  priority inversion can be avoided. 
+
+  So, the key of the proof is to establish the correctness of @{text "moment_blocked"}.
+  We are going to show how this lemma is proved. At the heart of this proof, is 
+  lemma @{text "pv_blocked"}:
+  @{thm [display] pv_blocked}
+  This lemma says: for any @{text "s"}-extension {text "t"}, if thread @{text "th'"}
+  does not hold any resource, it can not be running at @{text "t@s"}.
+
+
+  \noindent Proof: 
+  \begin{enumerate}
+  \item Since thread @{text "th'"} does not hold any resource, no thread may depend on it, 
+    so its current precedence @{text "cp (t@s) th'"} equals to its own precedence
+   @{text "preced th' (t@s)"}.  \label{arg_1}
+  \item Since @{text "th"} has the highest precedence in the system and 
+    precedences are distinct among threads, we have
+    @{text "preced th' (t@s) < preced th (t@s)"}. From this and item \ref{arg_1}, 
+    we have @{text "cp (t@s) th' < preced th (t@s)"}.
+  \item Since @{text "preced th (t@s)"} is already the highest in the system, 
+    @{text "cp (t@s) th"} can not be higher than this and can not be lower neither (by 
+    the definition of @{text "cp"}), we have @{text "preced th (t@s) = cp (t@s) th"}.
+  \item Finally we have @{text "cp (t@s) th' < cp (t@s) th"}.
+  \item By defintion of @{text "running"}, @{text "th'"} can not be runing at 
+    @{text "t@s"}.
+  \end{enumerate}
+  Since @{text "th'"} is not able to run at state @{text "t@s"}, it is not able to 
+  make either {text "P"} or @{text "V"} action, so if @{text "t@s"} is extended
+  one step further, @{text "th'"} still does not hold any resource. 
+  The situation will not unchanged in further extensions as long as 
+  @{text "th"} holds the highest precedence. Since this @{text "t"} is arbitarily chosen 
+  except being constrained by predicate @{text "extend_highest_gen"} and 
+  this predicate has the property that if it holds for @{text "t"}, it also holds
+  for any moment @{text "i"} inside @{text "t"}, as shown by lemma @{text "red_moment"}:
+@{thm [display] "extend_highest_gen.red_moment"}
+  so @{text "pv_blocked"} can be applied to any @{text "moment i t"}. 
+  From this, lemma @{text "moment_blocked"} follows.
+*}
+
+(*<*)
+end
+(*>*)
+
+
 section {* Properties for an Implementation\label{implement}*}
 
 text {*
diff -r 09281ccb31bd -r 3d154253d5fe prio/paper.pdf
Binary file prio/paper.pdf has changed