# HG changeset patch # User Christian Urban # Date 1494597335 -3600 # Node ID def87c589516bbaa57759950351c3055a81432e4 # Parent 5697bb5b6b2bf8d63bc23374f3e1e0c4fc0ff0b3 updated diff -r 5697bb5b6b2b -r def87c589516 Correctness.thy --- a/Correctness.thy Fri May 05 15:03:30 2017 +0100 +++ b/Correctness.thy Fri May 12 14:55:35 2017 +0100 @@ -1283,11 +1283,21 @@ fun postfixes where "postfixes [] = []" | - "postfixes (x#xs) = (xs)#postfixes xs" + "postfixes (x#xs) = xs # postfixes xs" definition "up_to s t = map (\ t'. t'@s) (postfixes t)" +fun upto where + "upto s [] = []" | + "upto s (e # es) = (es @ s) # upto s es" +value "up_to [s3, s2, s1] [e5, e4, e3, e2, e1] " +value "upto [s3, s2, s1] [e5, e4, e3, e2, e1] " + +lemma "upto s t = up_to s t" +apply(induct t arbitrary: s) +apply(auto simp add: up_to_def) +done definition "occs' Q tt = length (filter Q (postfixes tt))" diff -r 5697bb5b6b2b -r def87c589516 Journal/Paper.thy --- a/Journal/Paper.thy Fri May 05 15:03:30 2017 +0100 +++ b/Journal/Paper.thy Fri May 12 14:55:35 2017 +0100 @@ -1018,7 +1018,7 @@ 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: @@ -1583,38 +1583,41 @@ 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 - corresponding unlocking request for a resource. Second, we need to + ``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 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 - after a Priority Inversion occurs. The events can be seen as a - \textbf{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. In this setting we can prove - a more direct bound for the absence of indefinite Priority - Inversion. This is what we shall show below. + 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. + In this setting we can prove a more direct bound for the absence of + 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 - (active or hibernating). However, we do not have this concept of - active or hibernating threads in our model. Rather, in our model we - can create or exit threads arbitrarily. Consequently, the avoidance - of indefinite priority 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: + al.~informally make two assumtions: 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 we can dispence with the first assumption altogether and allow + that in our model we can create or exit threads + arbitrarily. Consequently, the avoidance of indefinite priority + 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 @@ -1635,7 +1638,7 @@ 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 @@ -1661,26 +1664,36 @@ 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 - number of states after @{text s} in which the thread @{text th} is - 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. This bound can be - stated for all valid states @{term "t @ s"} that can happen after - @{text s}. To state our bound we need to make a definition of what we - mean by intermediate states: it will be the list of traces/states starting - from @{text s} ending in @{text "t @ s"} + 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. This bound + can be stated for all valid intermediate states @{term "t @ s"} that + can happen after @{text s}. To state our bound we need to make a + definition of what we mean by intermediate states; it will be the + 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} - @{text "s upto t"} & $\equiv$ & @{text "if (t = []) then [s]"} \\ - & & @{text "else (t @ s) :: s upto (tail t)"} + \begin{tabular}{lcl} + @{text "s upto []"} & $\dn$ & $[]$\\ + @{text "s upto (e::es)"} & $\dn$ & @{text "(es @ s) :: s upto es"} \end{tabular} \end{center} diff -r 5697bb5b6b2b -r def87c589516 journal.pdf Binary file journal.pdf has changed