diff -r f1d82f6c05a3 -r a8ceb68bfeb0 Journal/Paper.thy --- a/Journal/Paper.thy Tue Apr 25 14:05:57 2017 +0100 +++ b/Journal/Paper.thy Tue Apr 25 16:23:46 2017 +0100 @@ -909,7 +909,8 @@ (*<*) context valid_trace begin -(*>*) + (*>*) +(*<*) text {* \endnote{In this section we prove facts that immediately follow from @@ -951,6 +952,7 @@ \end{proof}} *} +(*>*) (*<*)end(*>*) section {* The Correctness Proof *} @@ -1184,105 +1186,103 @@ %then @{thm (concl) eq_pv_persist} %\end{lemma}} - \endnote{{\bf OUTLINE} +% \endnote{{\bf OUTLINE} - Since @{term "th"} is the most urgent thread, if it is somehow - blocked, people want to know why and wether this blocking is - reasonable. +% Since @{term "th"} is the most urgent thread, if it is somehow +% blocked, people want to know why and wether this blocking is +% reasonable. - @{thm [source] th_blockedE} @{thm th_blockedE} +% @{thm [source] th_blockedE} @{thm th_blockedE} - if @{term "th"} is blocked, then there is a path leading from - @{term "th"} to @{term "th'"}, which means: - there is a chain of demand leading from @{term th} to @{term th'}. +% if @{term "th"} is blocked, then there is a path leading from +% @{term "th"} to @{term "th'"}, which means: +% there is a chain of demand leading from @{term th} to @{term th'}. %%% in other words %%% th -> cs1 -> th1 -> cs2 -> th2 -> ... -> csn -> thn -> cs -> th'. %%% %%% We says that th is blocked by "th'". - THEN +% THEN - @{thm [source] vat_t.th_chain_to_ready} @{thm vat_t.th_chain_to_ready} +% @ {thm [source] vat_t.th_chain_to_ready} @ {thm vat_t.th_chain_to_ready} - It is basic propery with non-trival proof. +% It is basic propery with non-trival proof. - THEN +% THEN - @{thm [source] max_preced} @{thm max_preced} +% @ {thm [source] max_preced} @ {thm max_preced} - which says @{term "th"} holds the max precedence. +% which says @{term "th"} holds the max precedence. - THEN +% THEN - @{thm [source] th_cp_max th_cp_preced th_kept} - @{thm th_cp_max th_cp_preced th_kept} +% @ {thm [source] th_cp_max th_cp_preced th_kept} +% @ {thm th_cp_max th_cp_preced th_kept} + +% THENTHEN + + %@ {thm [source] running_inversion_4} @ {thm running_inversion_4} - THENTHEN + % which explains what the @{term "th'"} looks like. Now, we have found the + % @{term "th'"} which blocks @{term th}, we need to know more about it. + % To see what kind of thread can block @{term th}. - (here) %@ {thm [source] running_inversion_4} @ {thm running_inversion_4} + % From these two lemmas we can see the correctness of PIP, which is + % that: the blockage of th is reasonable and under control. + + % Lemmas we want to describe: - which explains what the @{term "th'"} looks like. Now, we have found the - @{term "th'"} which blocks @{term th}, we need to know more about it. - To see what kind of thread can block @{term th}. + % \begin{lemma} + % @ {thm running_cntP_cntV_inv} + % \end{lemma} - From these two lemmas we can see the correctness of PIP, which is - that: the blockage of th is reasonable and under control. +% \noindent +% Remember we do not have the well-nestedness restriction in our +% proof, which means the difference between the counters @{const cntV} +% and @{const cntP} can be larger than @{term 1}. - Lemmas we want to describe: +% \begin{lemma}\label{runninginversion} +% @ {thm running_inversion} +% \end{lemma} + +% explain tRAG +%} - - \begin{lemma} - @{thm running_cntP_cntV_inv} - \end{lemma} +% Suppose the thread @ {term th} is \emph{not} running in state @ {term +% "t @ s"}, meaning that it should be blocked by some other thread. +% It is first shown that there is a path in the RAG leading from node +% @ {term th} to another thread @ {text "th'"}, which is also in the +% @ {term readys}-set. Since @ {term readys}-set is non-empty, there +% must be one in it which holds the highest @ {term cp}-value, which, +% by definition, is currently the @ {term running}-thread. However, we +% are going to show in the next lemma slightly more: this running +% thread is exactly @ {term "th'"}. - \noindent - Remember we do not have the well-nestedness restriction in our - proof, which means the difference between the counters @{const cntV} - and @{const cntP} can be larger than @{term 1}. - - \begin{lemma}\label{runninginversion} - @{thm running_inversion} - \end{lemma} - - explain tRAG - \bigskip} +% \begin{lemma} +% There exists a thread @{text "th'"} +% such that @{thm (no_quants) th_blockedE_pretty}. +% \end{lemma} - - Suppose the thread @{term th} is \emph{not} running in state @{term - "t @ s"}, meaning that it should be blocked by some other thread. - It is first shown that there is a path in the RAG leading from node - @{term th} to another thread @{text "th'"}, which is also in the - @{term readys}-set. Since @{term readys}-set is non-empty, there - must be one in it which holds the highest @{term cp}-value, which, - by definition, is currently the @{term running}-thread. However, we - are going to show in the next lemma slightly more: this running - thread is exactly @{term "th'"}. - - \begin{lemma} - There exists a thread @{text "th'"} - such that @{thm (no_quants) th_blockedE_pretty}. - \end{lemma} +% \begin{proof} +% We know that @{term th} cannot be in @{term readys}, because it has +% the highest precedence and therefore must be running. This violates our +% assumption. So by ?? we have that there must be a @{term "th'"} such that +% @{term "th' \ readys (t @ s)"} and @{term "(Th th, Th th') \ (RAG (t @ s))\<^sup>+"}. +% We are going to first show that this @{term "th'"} must be running. For this we +% need to show that @{term th'} holds the highest @{term cp}-value. +% By ?? we know that the @{term "cp"}-value of @{term "th'"} must +% be the highest all precedences of all thread nodes in its @{term tRAG}-subtree. +% That is - \begin{proof} - We know that @{term th} cannot be in @{term readys}, because it has - the highest precedence and therefore must be running. This violates our - assumption. So by ?? we have that there must be a @{term "th'"} such that - @{term "th' \ readys (t @ s)"} and @{term "(Th th, Th th') \ (RAG (t @ s))\<^sup>+"}. - We are going to first show that this @{term "th'"} must be running. For this we - need to show that @{term th'} holds the highest @{term cp}-value. - By ?? we know that the @{term "cp"}-value of @{term "th'"} must - be the highest all precedences of all thread nodes in its @{term tRAG}-subtree. - That is +% \begin{center} +% @ {term "cp (t @ s) th' = Max (the_preced (t @ s) ` +% (the_thread ` subtree (tRAG (t @ s)) (Th th')))"} +% \end{center} - \begin{center} - @{term "cp (t @ s) th' = Max (the_preced (t @ s) ` - (the_thread ` subtree (tRAG (t @ s)) (Th th')))"} - \end{center} - - But since @{term th} is in this subtree the right-hand side is equal - to @{term "preced th (t @ s)"}. +% But since @{term th} is in this subtree the right-hand side is equal +% to @{term "preced th (t @ s)"}. %Let me distinguish between cp (current precedence) and assigned precedence (the precedence the %thread ``normally'' has). @@ -1295,126 +1295,126 @@ %is the Maximum of the threads in the subgraph starting from th' %this happens to be the precedence of th %th has the highest precedence of all threads - \end{proof} +% \end{proof} - \begin{corollary} - Using the lemma \ref{runninginversion} we can say more about the thread th' - \end{corollary} +% \begin{corollary} +% Using the lemma \ref{runninginversion} we can say more about the thread th' +% \end{corollary} - \endnote{\subsection*{END OUTLINE}} +% \endnote{\subsection*{END OUTLINE}} - In what follows we will describe properties of PIP that allow us to prove - Theorem~\ref{mainthm} and, when instructive, briefly describe our argument. - It is relatively easy to see that: +% In what follows we will describe properties of PIP that allow us to prove +% Theorem~\ref{mainthm} and, when instructive, briefly describe our argument. +% It is relatively easy to see that: - \begin{isabelle}\ \ \ \ \ %%% - \begin{tabular}{@ {}l} - @{text "running s \ ready s \ threads s"}\\ - @{thm[mode=IfThen] finite_threads} - \end{tabular} - \end{isabelle} +% \begin{isabelle}\ \ \ \ \ %%% +% \begin{tabular}{@ {}l} +% @ {text "running s \ ready s \ threads s"}\\ +% @ {thm[mode=IfThen] finite_threads} +% \end{tabular} +% \end{isabelle} - \noindent - The second property is by induction on @{term vt}. The next three - properties are: +% \noindent +% The second property is by induction on @{term vt}. The next three +% properties are: - \begin{isabelle}\ \ \ \ \ %%% - \begin{tabular}{@ {}l} - HERE?? +% \begin{isabelle}\ \ \ \ \ %%% +% \begin{tabular}{@ {}l} +% HERE?? %@ {thm[mode=IfThen] waiting_unique[of _ _ "cs1" "cs2"]}\\ %@ {thm[mode=IfThen] held_unique[of _ "th1" _ "th2"]}\\ %@ {thm[mode=IfThen] running_unique[of _ "th1" "th2"]} - \end{tabular} - \end{isabelle} +% \end{tabular} +% \end{isabelle} - \noindent - The first property states that every waiting thread can only wait for a single - resource (because it gets suspended after requesting that resource); the second - that every resource can only be held by a single thread; - the third property establishes that in every given valid state, there is - at most one running thread. We can also show the following properties - about the @{term RAG} in @{text "s"}. +% \noindent +% The first property states that every waiting thread can only wait for a single +% resource (because it gets suspended after requesting that resource); the second +% that every resource can only be held by a single thread; +% the third property establishes that in every given valid state, there is +% at most one running thread. We can also show the following properties +% about the @{term RAG} in @{text "s"}. - \begin{isabelle}\ \ \ \ \ %%% - \begin{tabular}{@ {}l} - HERE?? %@{text If}~@ {thm (prem 1) acyclic_RAG}~@{text "then"}:\\ - \hspace{5mm}@{thm (concl) acyclic_RAG}, - @{thm (concl) finite_RAG} and - %@ {thm (concl) wf_dep_converse},\\ - %\hspace{5mm}@{text "if"}~@ {thm (prem 2) dm_RAG_threads}~@{text "then"}~@{thm (concl) dm_RAG_threads} - and\\ - %\hspace{5mm}@{text "if"}~@ {thm (prem 2) range_in}~@{text "then"}~% @ {thm (concl) range_in}. - \end{tabular} - \end{isabelle} +% \begin{isabelle}\ \ \ \ \ %%% +% \begin{tabular}{@ {}l} +% HERE?? %@{text If}~@ {thm (prem 1) acyclic_RAG}~@{text "then"}:\\ +% \hspace{5mm}@{thm (concl) acyclic_RAG}, +% @{thm (concl) finite_RAG} and +% %@ {thm (concl) wf_dep_converse},\\ +% %\hspace{5mm}@{text "if"}~@ {thm (prem 2) dm_RAG_threads}~@{text "then"}~@{thm (concl) dm_RAG_threads} +% and\\ +% %\hspace{5mm}@{text "if"}~@ {thm (prem 2) range_in}~@{text "then"}~% @ {thm (concl) range_in}. +% \end{tabular} +% \end{isabelle} - \noindent - The acyclicity property follows from how we restricted the events in - @{text step}; similarly the finiteness and well-foundedness property. - The last two properties establish that every thread in a @{text "RAG"} - (either holding or waiting for a resource) is a live thread. +% \noindent +% The acyclicity property follows from how we restricted the events in +% @{text step}; similarly the finiteness and well-foundedness property. +% The last two properties establish that every thread in a @{text "RAG"} +% (either holding or waiting for a resource) is a live thread. - The key lemma in our proof of Theorem~\ref{mainthm} is as follows: +% The key lemma in our proof of Theorem~\ref{mainthm} is as follows: - \begin{lemma}\label{mainlem} - Given the assumptions about states @{text "s"} and @{text "s' @ s"}, - the thread @{text th} and the events in @{text "s'"}, - if @{term "th' \ threads (s' @ s)"}, @{text "th' \ th"} and @{text "detached (s' @ s) th'"}\\ - then @{text "th' \ running (s' @ s)"}. - \end{lemma} +% \begin{lemma}\label{mainlem} +% Given the assumptions about states @{text "s"} and @{text "s' @ s"}, +% the thread @{text th} and the events in @{text "s'"}, +% if @{term "th' \ threads (s' @ s)"}, @{text "th' \ th"} and @{text "detached (s' @ s) th'"}\\ +% then @{text "th' \ running (s' @ s)"}. +% \end{lemma} - \noindent - The point of this lemma is that a thread different from @{text th} (which has the highest - precedence in @{text s}) and not holding any resource, cannot be running - in the state @{text "s' @ s"}. +% \noindent +% The point of this lemma is that a thread different from @{text th} (which has the highest +% precedence in @{text s}) and not holding any resource, cannot be running +% in the state @{text "s' @ s"}. - \begin{proof} - Since thread @{text "th'"} does not hold any resource, no thread can depend on it. - Therefore its current precedence @{term "cp (s' @ s) th'"} equals its own precedence - @{term "prec th' (s' @ s)"}. Since @{text "th"} has the highest precedence in the - state @{text "(s' @ s)"} and precedences are distinct among threads, we have - @{term "prec th' (s' @s ) < prec th (s' @ s)"}. From this - we have @{term "cp (s' @ s) th' < prec th (s' @ s)"}. - Since @{text "prec th (s' @ s)"} is already the highest - @{term "cp (s' @ s) th"} can not be higher than this and can not be lower either (by - definition of @{term "cp"}). Consequently, we have @{term "prec th (s' @ s) = cp (s' @ s) th"}. - Finally we have @{term "cp (s' @ s) th' < cp (s' @ s) th"}. - By defintion of @{text "running"}, @{text "th'"} can not be running in state - @{text "s' @ s"}, as we had to show.\qed - \end{proof} +% \begin{proof} +% Since thread @{text "th'"} does not hold any resource, no thread can depend on it. +% Therefore its current precedence @{term "cp (s' @ s) th'"} equals its own precedence +% @{term "prec th' (s' @ s)"}. Since @{text "th"} has the highest precedence in the +% state @{text "(s' @ s)"} and precedences are distinct among threads, we have +% @{term "prec th' (s' @s ) < prec th (s' @ s)"}. From this +% we have @{term "cp (s' @ s) th' < prec th (s' @ s)"}. +% Since @{text "prec th (s' @ s)"} is already the highest +% @{term "cp (s' @ s) th"} can not be higher than this and can not be lower either (by +% definition of @{term "cp"}). Consequently, we have @{term "prec th (s' @ s) = cp (s' @ s) th"}. +% Finally we have @{term "cp (s' @ s) th' < cp (s' @ s) th"}. +% By defintion of @{text "running"}, @{text "th'"} can not be running in state +% @{text "s' @ s"}, as we had to show.\qed +% \end{proof} - \noindent - Since @{text "th'"} is not able to run in state @{text "s' @ s"}, it is not able to - issue a @{text "P"} or @{text "V"} event. Therefore if @{text "s' @ s"} is extended - one step further, @{text "th'"} still cannot hold any resource. The situation will - not change in further extensions as long as @{text "th"} holds the highest precedence. +% \noindent +% Since @{text "th'"} is not able to run in state @{text "s' @ s"}, it is not able to +% issue a @{text "P"} or @{text "V"} event. Therefore if @{text "s' @ s"} is extended +% one step further, @{text "th'"} still cannot hold any resource. The situation will +% not change in further extensions as long as @{text "th"} holds the highest precedence. - From this lemma we can deduce Theorem~\ref{mainthm}: that @{text th} can only be - blocked by a thread @{text th'} that - held some resource in state @{text s} (that is not @{text "detached"}). And furthermore - that the current precedence of @{text th'} in state @{text "(s' @ s)"} must be equal to the - precedence of @{text th} in @{text "s"}. - We show this theorem by induction on @{text "s'"} using Lemma~\ref{mainlem}. - This theorem gives a stricter bound on the threads that can block @{text th} than the - one obtained by Sha et al.~\cite{Sha90}: - only threads that were alive in state @{text s} and moreover held a resource. - This means our bound is in terms of both---alive threads in state @{text s} - and number of critical resources. Finally, the theorem establishes that the blocking threads have the - current precedence raised to the precedence of @{text th}. +% From this lemma we can deduce Theorem~\ref{mainthm}: that @{text th} can only be +% blocked by a thread @{text th'} that +% held some resource in state @{text s} (that is not @{text "detached"}). And furthermore +% that the current precedence of @{text th'} in state @{text "(s' @ s)"} must be equal to the +% precedence of @{text th} in @{text "s"}. +% We show this theorem by induction on @{text "s'"} using Lemma~\ref{mainlem}. +% This theorem gives a stricter bound on the threads that can block @{text th} than the +% one obtained by Sha et al.~\cite{Sha90}: +% only threads that were alive in state @{text s} and moreover held a resource. +% This means our bound is in terms of both---alive threads in state @{text s} +% and number of critical resources. Finally, the theorem establishes that the blocking threads have the +% current precedence raised to the precedence of @{text th}. - We can furthermore prove that under our assumptions no deadlock exists in the state @{text "s' @ s"} - by showing that @{text "running (s' @ s)"} is not empty. +% We can furthermore prove that under our assumptions no deadlock exists in the state @{text "s' @ s"} +% by showing that @{text "running (s' @ s)"} is not empty. - \begin{lemma} - Given the assumptions about states @{text "s"} and @{text "s' @ s"}, - the thread @{text th} and the events in @{text "s'"}, - @{term "running (s' @ s) \ {}"}. - \end{lemma} +% \begin{lemma} +% Given the assumptions about states @{text "s"} and @{text "s' @ s"}, +% the thread @{text th} and the events in @{text "s'"}, +% @{term "running (s' @ s) \ {}"}. +% \end{lemma} - \begin{proof} - If @{text th} is blocked, then by following its dependants graph, we can always - reach a ready thread @{text th'}, and that thread must have inherited the - precedence of @{text th}.\qed - \end{proof} +% \begin{proof} +% If @{text th} is blocked, then by following its dependants graph, we can always +% reach a ready thread @{text th'}, and that thread must have inherited the +% precedence of @{text th}.\qed +% \end{proof} %The following lemmas show how every node in RAG can be chased to ready threads: @@ -1523,28 +1523,28 @@ %duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen %then. - NOTE: about bounds in sha et al and ours: they prove a bound on the length of individual - blocages. We prove a bound for the overall-blockage. + % NOTE: about bounds in sha et al and ours: they prove a bound on the length of individual + % blocages. We prove a bound for the overall-blockage. - There are low priority threads, - which do not hold any resources, - such thread will not block th. - Their Theorem 3 does not exclude such threads. + % There are low priority threads, + % which do not hold any resources, + % such thread will not block th. + % Their Theorem 3 does not exclude such threads. - There are resources, which are not held by any low prioirty threads, - such resources can not cause blockage of th neither. And similiary, - theorem 6 does not exlude them. + % There are resources, which are not held by any low prioirty threads, + % such resources can not cause blockage of th neither. And similiary, + % theorem 6 does not exlude them. - Our one bound excudle them by using a different formaulation. " + % Our one bound excudle them by using a different formaulation. " *} (*<*) end (*>*) -text {* +(*text {* explan why Thm1 roughly corresponds to Sha's Thm 3 -*} +*}*) section {* A Finite Bound on Priority Inversion *}