pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:170e59f2d645
+:675416b1defd
 for machine instructions. Therefore we cannot characterise what are
 ``good'' programs that contain for every locking request for a
 resource also a corresponding unlocking request.  Second, we need to
 distinghish between a thread that ``just'' locks a resource for a
 finite amount of time (even if it is very long) and one that locks
-it forever (there might be a loop in between the locking and
+it forever (there might be an unbounded loop in between the locking and
 unlocking requests).
 Because of these problems, we decided in our earlier paper
 \cite{ZhangUrbanWu12} to leave out this property and let the
 programmer take on the responsibility to program threads in such a
 Sha et al.~in their paper.  However, in this paper we can make an
 improvement by establishing a finite bound on the duration of
 Priority Inversion measured by the number of events.  The events can
 be seen as a \textit{rough(!)} abstraction of the ``runtime
 behaviour'' of threads and also as an abstract notion of
-``time''---when a new event happened, some time must have passed.
+``time''---when a new event happens, some time must have passed.
 What we will establish in this section is that there can only be a
 finite number of states after state @{term s} in which the thread
-@{term th} is blocked.  For this finiteness bound to exist, Sha et
+@{term th} is blocked (recall for this that a state is a list of
-al.~informally make two assumtions: first, there is a finite pool of
+events).  For this finiteness bound to exist, Sha et al.~informally
-threads (active or hibernating) and second, each of them giving up
+make two assumtions: first, there is a finite pool of threads
-its resources after a finite amount of time.  However, we do not
+(active or hibernating) and second, each of them giving up its
-have this concept of active or hibernating threads in our model.  In
+resources after a finite amount of time.  However, we do not have
-fact we can dispence with the first assumption altogether and allow
+this concept of active or hibernating threads in our model.  In fact
-that in our model we can create or exit threads
+we can dispence with the first assumption altogether and allow that
+in our model we can create new threads or exit existing threads
 arbitrarily. Consequently, the avoidance of indefinite priority
 inversion we are trying to establish is in our model not true,
-unless we put up an upper bound on the number of threads that
+unless we stipulate an upper bound on the number of threads that
-have been created upto any valid future state after @{term
+have been created during the time leading to any future state
-s}. Otherwise our PIP scheduler could be ``swamped'' with @{text
+after @{term s}. Otherwise our PIP scheduler could be ``swamped''
-"Create"}-requests.  So our first assumption states:
+with @{text "Create"}-requests.  So our first assumption states:
 \begin{quote} {\bf Assumption on the number of threads created
 after the state {\boldmath@{text s}}:} Given the
 state @{text s}, in every ``future'' valid state @{text "es @ s"}, we
 require that the number of created threads is less than
 "s' @ s"} after @{text s}.  Instead, we need to put this bound on
 the @{text "Create"} events for all valid states after @{text s}.
 This ensures that no matter which ``future'' state is reached, the
 number of @{text "Create"}-events is finite. We use @{text "es @ s"}
 to stand for \emph{future states} after @{text s}---it is @{text s}
-extended with some list of events.
+extended with some list @{text es} of events.
 For our second assumption about giving up resources after a finite
 amount of ``time'', let us introduce the following definition about
 threads that can potentially block @{text th}:
 \end{isabelle}
 \noindent This set contains all treads that are not detached in
 state @{text s}. According to our definiton of @{text "detached"},
 this means a thread in @{text "blockers"} either holds or waits for
-some resource. Our Theorem~1 implies that they can all potentially
+some resource in state @{text s} . Our Them~1 implies that any of
-block @{text th} after state @{text s}. We need to make the
+those threads can all potentially block @{text th} after state
-following assumption about the threads in this set:
+@{text s}. We need to make the following assumption about the
+threads in the @{text "blockers"}-set:
 \begin{quote}
 {\bf Assumptions on the threads {\boldmath{@{term "th' \<in> blockers"}}}:}
 For each such @{text "th'"} there exists a finite bound @{text "BND(th')"}
 such that for all future
 anymore) after a finite number of events in @{text "es @ s"}. Again
 we have to state this bound to hold in all valid states after @{text
 s}. The bound reflects how each thread @{text "th'"} is programmed:
 Though we cannot express what instructions a thread is executing,
 the events in our model correspond to the system calls made by
-thread. Our @{text "BND(th')"} binds the number of these ``calls''.
+a thread. Our @{text "BND(th')"} binds the number of these ``calls''.
 The main reason for these two assumptions is that we can prove the
 following: The number of states after @{text s} in which the thread
 @{text th} is not running (that is where Priority Inversion occurs)
 can be bounded by the number of actions the threads in @{text
-blockers} perform and how many threads are newly created.  To state
+blockers} perform (i.e.~events) and how many threads are newly
-our bound formally, we need to make a definition of what we mean by
+created.  To state our bound formally, we need to make a definition
-intermediate states; it will be the list of states starting from
+of what we mean by intermediate states between a state @{text s} and
-@{text s} upto the state @{text "es @ s"}. For example, suppose
+a future state after @{text s}; they will be the list of states
-$\textit{es} = [\textit{e}_n, \textit{e}_{n-1}, \ldots, \textit{e}_2,
+starting from @{text s} upto the state \mbox{@{text "es @ s"}}. For
-\textit{e}_1]$, then the intermediate states from @{text s} upto
+example, suppose $\textit{es} = [\textit{e}_n, \textit{e}_{n-1},
-@{text "es @ s"} are
+\ldots, \textit{e}_2, \textit{e}_1]$, then the intermediate states
+from @{text s} upto @{text "es @ s"} are
 \begin{center}
 \begin{tabular}{l}
 $\textit{s}$\\
 $\textit{e}_1 :: \textit{s}$\\
 \noindent
 Our theorem can then be stated as follows:
 \begin{theorem}
 Given our assumptions about bounds, we have that
 \[
 @{text "len"}\,[@{text "s'"}
 \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}] \;\;\leq\;\;
 @{text "BC"} + \sum @{text "th'"} \in @{text "blockers"}.\;\; @{text "BND(th')"}\;.
 \]
 \end{theorem}
+\noindent This theorem uses Isabelle's list-comprehension notation,
+which lists all intermediate states between @{text s} and @{text "es
+@ s"}, and then filters this list according to states in which
+@{text th} is not running. By calculating the number of elements in
+the filtered list using the function @{text len}, we have the number
+of intermediate states in which @{text th} is not running and which
+by the theorem is bounded by the term on the right-hand side.
 \begin{proof} There are two characterisations for the number of
-events in @{text es}: First, for each corresponding state in @{text
+events in @{text es}: First, in each state in
-"s upto es"}, either @{text th} is running or not running. That
+@{text "s upto es"}, clearly either @{text th} is running or
-means
+not running. Together with @{text "len es = len (s upto es)"}, that
+implies %
-\begin{equation}\label{firsteq}
-@{text "len es"} =
+\begin{equation}
-@{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \in @{text "running s'"}] +
+\label{firsteq}
-@{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}]
+\begin{array}{lcl}
+@{text "len es"} & \;=\; &
+@{text len}\, [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \in @{text "running s'"}]\\
+& & +\;
+@{text len}\, [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}]
+\end{array}
 \end{equation}
 \noindent Second by Thm~\ref{mainthm}, the events are either the
 actions of @{text th} or @{text "Create"}-events or actions of the
 threads in blockers. That is
+%
 \begin{equation}\label{secondeq}
-@{text "len es"} = @{text "len (actions_of {th} es)"} +
+\begin{array}{lcl}
-@{text "len (filter isCreate es)"} +
+@{text "len es"} & \;=\; & @{text "len (actions_of {th} es)"}\\
-@{text "len (actions_of blockers es)"}
+& & +\; @{text "len (filter isCreate es)"}\\
+& & +\; @{text "len (actions_of blockers es)"}
+\end{array}
 \end{equation}
-\noindent
+\noindent Furthermore we know that an action of @{text th} in the
-Further we know that an action of @{text th} can only be taken when @{text th} is running. Therefore
+intermediate states @{text "s upto es"} can only be taken when
+@{text th} is running. Therefore
+%
 \[
-@{text "len (actions_of {th} es)"} \leq
+@{text "len (actions_of {th} es)"} \;\leq\;
-@{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \in @{text "running s'"}]
+@{text len}\,[@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \in @{text "running s'"}]
 \]
-\noindent Substituting this into \eqref{firsteq} gives
+\noindent holds. Substituting this into \eqref{firsteq} gives
+%
 \[
-@{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}]
+@{text len}\,[@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}]
-\leq @{text "len es"} - @{text "len (actions_of {th} es)"}
+\;\leq\; @{text "len es"} - @{text "len (actions_of {th} es)"}
 \]
+\noindent
 into which we can substitute \eqref{secondeq} yielding
+%
 \[
-@{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}] \leq
+\begin{array}{rcl}
-@{text "len (filter isCreate es)"} + @{text "len (actions_of blockers es)"}
+@{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}] & \;\;\leq\;\; &
+@{text "len (filter isCreate es)"}\\
+& & \quad + @{text "len (actions_of blockers es)"}
+\end{array}
 \]
-\noindent By our first assumption we know that the @{text
+\noindent By our first assumption we know that the number of @{text
 "Create"}-events are bounded by the bound @{text BC}.  By our second
 assumption we can prove that the actions of all blockers is bounded
 by the sum of bounds of the individual blocking threads, that is
 \[
 \noindent With this in place we can conclude our theorem.\hfill\qed
 \end{proof}
 \noindent This theorem is the main conclusion we obtain for the
-Priority Inheritance Protocol: it shows that the set of @{text blockers}
+Priority Inheritance Protocol. It is based on the fact that the set of
-is fixed at state @{text s} when @{text th} becomes the thread with
+@{text blockers} is fixed at state @{text s} when @{text th} becomes
-highest priority. Then no additional blocker of @{text th} can
+the thread with highest priority. Then no additional blocker of
-appear after the state @{text s}. And in this way we can bound the
+@{text th} can appear after the state @{text s}. And in this way we
-number of states where the thread @{text th} with the highest
+can bound the number of states where the thread @{text th} with the
-priority is prevented from running.
+highest priority is prevented from running.
-*}
+Our bound does not depend on the restriction of well-nested critical
-(*<*)
+sections in the Priority Inheritance Protocol as imposed by Sha et al.
-end
+*} (*<*) end (*>*)
-(*>*)
 section {* Properties for an Implementation\label{implement} *}
 text {*
 While our formalised proof gives us confidence about the correctness of our model of PIP,
 We can however improve upon this. For this let us define the notion
 of @{term children} of a thread @{text th} in a state @{text s} as
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
-HERE?? %%@ {thm children_def2}
+?? @{thm children_def}
 \end{tabular}
 \end{isabelle}
 \noindent
 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.
 \begin{lemma}\label{childrenlem}
-HERE %@{text "If"} @ {thm (prem 1) cp_rec} @{text "then"}
+HERE %@ {text "If"} @ {thm (prem 1) cp_rec} @{text "then"}
 \begin{center}
 %@ {thm (concl) cp_rec}.
 \end{center}
 \end{lemma}

changeset 176	675416b1defd
parent 175	170e59f2d645
child 177	abe117821c32