pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:5697bb5b6b2b
+:def87c589516
 alive threads is finite, @{text th} can only be blocked a finite
 number of threads.  We will actually prove a
 stronger statement where we also provide the current precedence of
 the blocking thread.
-However, this correctness criterion hinges upon a number of
+However, the theorem we are going to prove hinges upon a number of
 natural assumptions about the states @{text s} and @{text "s' @ s"}, the
 thread @{text th} and the events happening in @{text s'}. We list
 them next:
 \begin{quote}
 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
 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 also a
+``good'' programs that contain for every locking request for a
-corresponding unlocking request for a resource.  Second, we need to
+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 lookp in between the locking and
+it forever (there might be a 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 assume the responsibility to program threads in such a
+programmer take on the responsibility to program threads in such a
 benign manner (in addition to causing no circularity in the
 RAG). This leave-it-to-the-programmer was also the approach taken by
 Sha et al.~in their paper.  However, in this paper we can make an
-improvement: we can look at the \emph{events} that are happening
+improvement by establishing a finite bound on the duration of
-after a Priority Inversion occurs. The events can be seen as a
+Priority Inversion measured by the number of events.  The events can
-\textbf{rough} abstraction of the ``runtime behaviour'' of threads
+be seen as a \textit{rough(!)} abstraction of the ``runtime
-and also as an abstract notion of ``time''---when a new event
+behaviour'' of threads and also as an abstract notion of
-happened, some time must have passed.  In this setting we can prove
+``time''---when a new event happened, some time must have passed.
-a more direct bound for the absence of indefinite Priority
+In this setting we can prove a more direct bound for the absence of
-Inversion. This is what we shall show below.
+indefinite Priority Inversion. This is what we shall show below.
 What we will establish in this section is that there can only be a
-finite amount of states after state @{term s} in which the thread
+finite number of states after state @{term s} in which the thread
 @{term th} is blocked.  For this finiteness bound to exist, Sha et
-al.~assume in their work that there is a finite pool of threads
+al.~informally make two assumtions: first, there is a finite pool of
-(active or hibernating). However, we do not have this concept of
+threads (active or hibernating) and second, each of them giving up
-active or hibernating threads in our model. Rather, in our model we
+its resources after a finite amount of time.  However, we do not
-can create or exit threads arbitrarily. Consequently, the avoidance
+have this concept of active or hibernating threads in our model.  In
-of indefinite priority inversion we are trying to establish is in
+fact we can dispence with the first assumption altogether and allow
-our model not true, unless we require that the number of threads
+that in our model we can create or exit threads
-created is bounded in every valid future state after @{term s}. So
+arbitrarily. Consequently, the avoidance of indefinite priority
-our first assumption states:
+inversion we are trying to establish is in our model not true,
+unless we require that the number of threads created is bounded in
+every valid future state after @{term s}. So our first assumption
+states:
 \begin{quote} {\bf Assumption on the number of threads created in
 every valid state after the state {\boldmath@{text s}}:} Given the
 state @{text s}, in every ``future'' valid state @{text "t @ s"}, we
 require that the number of created threads is less than
 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}:
 \begin{isabelle}\ \ \ \ \ %%%
-@{thm blockers_def}
+@{thm blockers_def[THEN eq_reflection]}
 \end{isabelle}
 \noindent This set contains all treads that are not detached in
 state @{text s} (i.e.~they have a lock on a resource) and therefore
 can potentially block @{text th} after state @{text s}. We need to
 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.
-The main reason for these two assumptions is that we can prove: the
+The main reason for these two assumptions is that we can prove the
-number of states after @{text s} in which the thread @{text th} is
+following: The number of states after @{text s} in which the thread
-is not running (that is where Priority Inversion occurs) can be
+@{text th} is not running (that is where Priority Inversion occurs)
-bounded by the number of actions the threads in @{text blockers}
+can be bounded by the number of actions the threads in @{text
-perform and how many threads are newly created. This bound can be
+blockers} perform and how many threads are newly created. This bound
-stated for all valid states @{term "t @ s"} that can happen after
+can be stated for all valid intermediate states @{term "t @ s"} that
-@{text s}. To state our bound we need to make a definition of what we
+can happen after @{text s}. To state our bound we need to make a
-mean by intermediate states: it will be the list of traces/states starting
+definition of what we mean by intermediate states; it will be the
-from @{text s} ending in @{text "t @ s"}
+list of states starting from @{text s} upto the state @{text "t @
+s"}. For example, suppose $\textit{t} =
+[\textit{e}_n, \textit{e}_{n-1}, \ldots, \textit{e}_2, \textit{e}_1]$, then
+the intermediate states from @{text s} upto @{text "t @ s"} are
 \begin{center}
-@{text "t @ s"},\; \ldots,\; @{text "e2 :: e1 :: s"},\;@{text "e1 :: s"},\;@{text "s"}
+\begin{tabular}{l}
+$\textit{s}$\\
+$\textit{e}_1 :: \textit{s}$\\
+$\textit{e}_2 :: \textit{e}_1 :: \textit{s}$\\
+\ldots\\
+$\textit{e}_{n - 1} :: \ldots :: \textit{e}_2 :: \textit{e}_1 :: \textit{s}$\\
+\end{tabular}
 \end{center}
-\noindent This can be defined by the following recursive functions
+\noindent This can be defined by the following recursive function
 \begin{center}
-\begin{tabular}{rcl}
+\begin{tabular}{lcl}
-@{text "s upto t"} & $\equiv$ & @{text "if (t = []) then [s]"} \\
+@{text "s upto []"} & $\dn$ & $[]$\\
-& & @{text "else (t @ s) :: s upto (tail t)"}
+@{text "s upto (e::es)"} & $\dn$ & @{text "(es @ s) :: s upto es"}
 \end{tabular}
 \end{center}
 \noindent Assume you have an extension @{text t}, this essentially

changeset 170	def87c589516
parent 169	5697bb5b6b2b
child 171	daf75d6ebc89