
diff -r 312497c6d6b9 -r fdba35b422a0 Journal/Paper.thy
--- a/Journal/Paper.thy	Wed Aug 02 14:56:47 2017 +0100
+++ b/Journal/Paper.thy	Fri Aug 11 16:09:02 2017 +0100
@@ -78,10 +78,11 @@
   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
-  indefinitely. Since $H$ is blocked by threads with lower priorities,
-  the problem is called Priority Inversion. It was first described in
-  \cite{Lampson80} in the context of the Mesa programming language
-  designed for concurrent programming.
+  indefinitely (consider the case where threads with propority $M$
+  continously need to be processed). Since $H$ is blocked by threads
+  with lower priorities, the problem is called Priority Inversion. It
+  was first described in \cite{Lampson80} in the context of the Mesa
+  programming language designed for concurrent programming.
  
   If the problem of Priority Inversion is ignored, real-time systems
   can become unpredictable and resulting bugs can be hard to diagnose.
@@ -321,7 +322,8 @@
   \isacommand{datatype} event 
   & @{text "="} & @{term "Create thread priority\<iota>"}\\
   & @{text "|"} & @{term "Exit thread"} \\
-  & @{text "|"} & @{term "Set thread priority\<iota>"} & {\rm reset of the priority for} @{text thread}\\
+  & @{text "|"} & @{term "Set thread priority\<iota>"} & 
+  @{text thread} {\rm resets its own priority} \\
   & @{text "|"} & @{term "P thread cs"} & {\rm request of resource} @{text "cs"} {\rm by} @{text "thread"}\\
   & @{text "|"} & @{term "V thread cs"} & {\rm release of resource} @{text "cs"} {\rm by} @{text "thread"}
   \end{tabular}}
@@ -412,7 +414,7 @@
   \end{isabelle}
 
   \noindent
-  This allows us to define what actions a set of threads @{text ths} might
+  This allows us to filter out the actions a set of threads @{text ths} 
   perform in a list of events @{text s}, namely
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -437,7 +439,7 @@
   \end{isabelle}
 
   \noindent
-  for the set of precedences of threads @{text ths} in state @{text s}.
+  for the precedences of a set of threads @{text ths} in state @{text s}.
   The point of precedences is to schedule threads not according to priorities (because what should
   we do in case two threads have the same priority), but according to precedences. 
   Precedences allow us to always discriminate between two threads with equal priority by 
@@ -484,7 +486,7 @@
   \end{isabelle}
 
   \noindent
-  In this definition we assume @{text "set"} converts a list into a set.
+  In this definition we assume that @{text "set"} converts a list into a set.
   Note that in the first definition the condition about @{text "th \<in> set (wq cs)"} does not follow
   from @{text "th = hd (set (wq cs))"}, since the head of an empty list is undefined in Isabelle/HOL. 
   At the beginning, that is in the state where no thread is created yet, 
@@ -623,7 +625,8 @@
   only have at most one outgoing holding edge---indicating that the
   resource is locked. So if the @{text "RAG"} is well-founded and
   finite, we can always start at a thread waiting for a resource and
-  ``chase'' outgoing arrows leading to a single root of a tree.
+  ``chase'' outgoing arrows leading to a single root of a tree,
+  which must be a ready thread.
   
   The use of relations for representing @{text RAG}s allows us to
   conveniently define the \emph{Thread Dependants Graph} (TDG):
@@ -633,12 +636,12 @@
   \mbox{}\hfill\numbered{dependants}
   \end{isabelle}
 
-  \noindent This definition represents all threads in a @{text RAG} that wait
-  for a thread to release a resource, but the corresponding 
+  \noindent This definition is the relation that one thread is waiting for
+  another to release a resource, but the corresponding 
   resource is ``hidden''. 
-  In Figure~\ref{RAGgraph} this means the @{text TDG} connects @{text "th\<^sub>0"} with
-  @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which both wait for
-  resource @{text "cs\<^sub>1"}; and @{text "th\<^sub>2"} with @{text "th\<^sub>3"}, which
+  In Figure~\ref{RAGgraph} this means the @{text TDG} connects 
+  @{text "th\<^sub>1"} and @{text "th\<^sub>2"} to @{text "th\<^sub>0"}, which both wait for
+  resource @{text "cs\<^sub>1"} to be released; and @{text "th\<^sub>3"} to @{text "th\<^sub>2"}, which
   cannot make any progress unless @{text "th\<^sub>2"} makes progress. 
   Similarly for the other threads.
   If
@@ -646,7 +649,8 @@
   deadlock. Therefore when a thread requests a resource, we must
   ensure that the resulting @{text RAG} and @{text TDG} are not circular. In practice, the
   programmer has to ensure this. Our model will enforce that critical 
-  resources can only be requested provided no circularity can arise.
+  resources can only be requested provided no circularity can arise (but 
+  they can overlap, see Fig~\ref{overlap}).
 
   Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a 
   state @{text s}. It is defined as
@@ -662,7 +666,8 @@
   created), the point of the current precedence is to dynamically
   increase this precedence, if needed according to PIP. Therefore the
   current precedence of @{text th} is given as the maximum of the
-  precedence of @{text th} \emph{and} all threads in its subtree. Since the notion of current precedence is defined as the 
+  precedences of all threads in its subtree (which includes by definition 
+  @{text th} itself). Since the notion of current precedence is defined as the 
   transitive closure of the dependent
   threads in the @{text TDG}, we deal correctly with the problem in the informal
   algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
@@ -874,7 +879,10 @@
   @{thm[mode=Rule] thread_set[where thread=th]}
   \end{center}
 
-  \noindent If a thread wants to lock a resource, then the thread
+  \noindent This is because the @{text Set} event is for a thread to change
+  its \emph{own} priority---therefore it must be running.
+
+  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 does not lead to a cycle in the RAG (the prurpose of the second
   premise in the rule below). In practice, ensuring the latter is the
@@ -918,7 +926,7 @@
 
   \noindent
   This completes our formal model of PIP. In the next section we present
-  a series of desirable properties derived from our model of PIP. This can
+  a series of desirable properties derived from this model of PIP. This can
   be regarded as a validation of the correctness of our model.
 *}
 
@@ -1023,7 +1031,7 @@
   th} is running or it is blocked by a thread that was alive in the
   state @{text s} and was waiting for or in the possession of a lock
   in @{text s}. Since in @{text s}, as in every state, the set of
-  alive threads is finite, @{text th} can only be blocked a finite
+  alive threads is finite, @{text th} can only be blocked by a finite
   number of threads.  We will actually prove a
   stronger statement where we also provide the current precedence of
   the blocking thread. 
@@ -1059,11 +1067,13 @@
   \end{quote}
   
   \begin{quote}
-  {\bf Assumptions on the events in {\boldmath@{text "s'"}:}} We want to prove that @{text th} cannot
-  be blocked indefinitely. Of course this can happen if threads with higher priority
-  than @{text th} are continuously created in @{text s'}. Therefore we have to assume that  
+  {\bf Assumptions on the events in {\boldmath@{text "s'"}:}} 
+  %We want to prove that @{text th} cannot
+  %be blocked indefinitely. Of course this can happen if threads with higher priority
+  %than @{text th} are continuously created in @{text s'}. 
+  To make sure @{text th} has the highest precedence we have to assume that  
   events in @{text s'} can only create (respectively set) threads with equal or lower 
-  priority than @{text prio} of @{text th}. We also need to assume that the
+  priority than @{text prio} of @{text th}. For the same reason, we also need to assume that the
   priority of @{text "th"} does not get reset and all other reset priorities are either
   less or equal. Moreover, we assume  that @{text th} does
   not get ``exited'' in @{text "s'"}. This can be ensured by assuming the following three implications. 
@@ -1151,7 +1161,7 @@
   If @{term "th' \<in> running (s' @ s)"} and @{term "th \<noteq> th'"} then @{term "\<not>detached s th'"}.
   \end{lemma}
 
-  \begin{proof} Let us assume @{text "th'"} is detached in state
+  \begin{proof} Let us assume otherwise, that is @{text "th'"} is detached in state
   @{text "s"}, then, according to the definition of detached, @{text
   "th’"} does not hold or wait for any resource. Hence the @{text
   cp}-value of @{text "th'"} in @{text s} is not boosted, that is
@@ -1591,7 +1601,7 @@
   further need the property that every thread gives up its resources
   after a finite amount of time. We found that this property is not so
   straightforward to formalise in our model. There are mainly two
-  reasons for this: First, we do not specify what ``running'' the code
+  reasons for this: First, we do not specify what ``running the code''
   of a thread means, for example by giving an operational semantics
   for machine instructions. Therefore we cannot characterise what are
   ``good'' programs that contain for every locking request for a
@@ -1618,7 +1628,7 @@
   finite number of states after state @{term s} in which the thread
   @{term th} is blocked (recall for this that a state is a list of
   events).  For this finiteness bound to exist, Sha et al.~informally
-  make two assumtions: first, there is a finite pool of threads
+  make two assumptions: first, there is a finite pool of threads
   (active or hibernating) and second, each of them giving up its
   resources after a finite amount of time.  However, we do not have
   this concept of active or hibernating threads in our model.  In fact




