# HG changeset patch # User Christian Urban # Date 1481287889 0 # Node ID 10c16b85a839a26ea2c2b1cc93b898a82552dc83 # Parent f70344294e9932e28ee93419a1c8e14ab18ff2f8 updated diff -r f70344294e99 -r 10c16b85a839 Correctness.thy --- a/Correctness.thy Fri Oct 21 14:47:01 2016 +0100 +++ b/Correctness.thy Fri Dec 09 12:51:29 2016 +0000 @@ -736,87 +736,6 @@ running thread is exactly @{term "th'"}. *} -(* -lemma th_blockedE: (* ddd, the other main lemma to be presented: *) - assumes "th \ running (t @ s)" - obtains th' where "th' \ ancestors (tG (t @ s)) th" - "th' \ running (t @ s)" -proof - - -- {* According to @{thm vat_t.th_chain_to_ready_tG}, either - @{term "th"} is in @{term "readys"} or there is path leading from it to - one thread in @{term "readys"}. *} - have "th \ readys (t @ s) \ (\th'. th' \ readys (t @ s) \ (th, th') \ (tG (t @ s))\<^sup>+)" - using th_kept vat_t.th_chain_to_ready_tG by blast - - -- {* However, @{term th} can not be in @{term readys}, because otherwise, since - @{term th} holds the highest @{term cp}-value, it would be @{term "running"}. *} - moreover have "th \ readys (t @ s)" - using assms running_def th_cp_max vat_t.max_cp_readys_threads by auto - - -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in - term @{term readys}: *} - ultimately obtain th' where th'_readys: "th' \ readys (t @ s)" - and dp: "(th, th') \ (tG (t @ s))\<^sup>+" by auto - - -- {* @{text "th'"} is an ancestor of @{term "th"} *} - have "th' \ ancestors (tG (t @ s)) th" using dp - unfolding ancestors_def by simp - - moreover - -- {* We are going to show that this @{term th'} is running. *} - have "th' \ running (t @ s)" - proof - - -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *} - have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t@s))" (is "?L = ?R") - proof - - -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}), - the @{term cp}-value of @{term th'} is the maximum of - all precedences of all thread nodes in its @{term tRAG}-subtree: *} - - have "?L = Max (preceds (subtree (tG (t @ s)) th') (t @ s))" - unfolding cp_alt_def2 image_def the_preced_def by meson - also have "... = (preced th (t @ s))" - thm subset_Max - thm preced_unique - proof(rule subset_Max[where ?A="preceds (threads (t @ s)) (t @ s)"]) - show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads) - next - have "subtree (tG (t @ s)) th' \ threads (t @ s)" - using readys_def th'_readys vat_t.subtree_tG_thread by auto - then show "preceds (subtree (tG (t @ s)) th') (t @ s) \ preceds (threads (t @ s)) (t @ s)" - by auto - next - have "th \ subtree (tG (t @ s)) th'" - by (simp add: dp subtree_def trancl_into_rtrancl) - then show " preced th (t @ s) \ preceds (subtree (tG (t @ s)) th') (t @ s)" - by blast - next - have "Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th" - apply(simp only: the_preced_def) - by simp - show "Max (preceds (threads (t @ s)) (t @ s)) = preced th (t @ s)" - thm th_kept max_kept - apply(simp del: th_kept) - apply(simp only: the_preced_def image_def) - apply(simp add: Bex_def_raw) - - qed - also have "... = ?R" - using th_cp_max th_cp_preced th_kept - the_preced_def vat_t.max_cp_readys_threads by auto - finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" . - qed - - -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, - it is @{term running} by definition. *} - then show "th' \ running (t @ s)" using th'_readys - unfolding running_def by simp - qed - - ultimately show ?thesis using that by metis -qed -*) - lemma th_blockedE: (* ddd, the other main lemma to be presented: *) obtains th' where "th' \ nancestors (tG (t @ s)) th" "th' \ running (t @ s)" diff -r f70344294e99 -r 10c16b85a839 Journal/Paper.thy --- a/Journal/Paper.thy Fri Oct 21 14:47:01 2016 +0100 +++ b/Journal/Paper.thy Fri Dec 09 12:51:29 2016 +0000 @@ -424,7 +424,7 @@ tasks involved in the inheritance process and thus minimises the number of potentially expensive thread-switches. - {\bf NEEDED?} We will also need counters for @{term P} and @{term V} events of a thread @{term th} + \endnote{{\bf NEEDED?} We will also need counters for @{term P} and @{term V} events of a thread @{term th} in a state @{term s}. This can be straightforwardly defined in Isabelle as \begin{isabelle}\ \ \ \ \ %%% @@ -434,7 +434,7 @@ \end{tabular}} \end{isabelle} - \noindent using the predefined function @{const count} for lists. + \noindent using the predefined function @{const count} for lists.} Next, we introduce the concept of \emph{waiting queues}. They are lists of threads associated with every resource. The first thread in @@ -569,16 +569,17 @@ forrest} is a forest which is well-founded and every node has finitely many children (is only finitely branching). + \endnote{ \begin{isabelle}\ \ \ \ \ %%% @{thm rtrancl_path.intros} \end{isabelle} \begin{isabelle}\ \ \ \ \ %%% @{thm rpath_def} - \end{isabelle} + \end{isabelle}} - {\bf Lemma about overlapping paths} + \endnote{{\bf Lemma about overlapping paths}} We will design our PIP-scheduler @@ -619,9 +620,10 @@ @{thm cpreced_def}\hfill\numbered{cpreced} \end{isabelle} + \endnote{ \begin{isabelle}\ \ \ \ \ %%% @{thm cp_alt_def cp_alt_def1} - \end{isabelle} + \end{isabelle}} \noindent where the dependants of @{text th} are given by the waiting queue function. @@ -881,7 +883,7 @@ (*>*) text {* - In this section we prove facts that immediately follow from + \endnote{In this section we prove facts that immediately follow from our definitions of valid traces. \begin{lemma}??\label{precedunique} @@ -917,7 +919,7 @@ infer by Lemma~\ref{precedunique} that @{text "th'\<^sub>1"} and @{text "th'\<^sub>2"} are the same threads. However, this also means the roots @{text "th\<^sub>1"} and @{text "th\<^sub>2"} must be the same.\qed - \end{proof} + \end{proof}} *} (*<*)end(*>*) @@ -1030,9 +1032,9 @@ Given the assumptions about states @{text "s"} and @{text "s' @ s"}, the thread @{text th} and the events in @{text "s'"}, then either \begin{itemize} - \item @{term "th \ running (s' @ s)"} or\medskip + \item[$\bullet$] @{term "th \ running (s' @ s)"} or\medskip - \item there exists a thread @{term "th'"} with @{term "th' \ th"} + \item[$\bullet$] there exists a thread @{term "th'"} with @{term "th' \ th"} and @{term "th' \ running (s' @ s)"} such that @{text "th' \ threads s"}, @{text "\ detached s th'"} and @{term "cp (s' @ s) th' = prec th s"}. @@ -1074,14 +1076,14 @@ Given our assumptions (on @{text th}), the first property we can show is that any running thread, say @{text "th'"}, has the same - precedence of @{text th}: + precedence as @{text th}: \begin{lemma}\label{runningpreced} @{thm [mode=IfThen] running_preced_inversion} \end{lemma} \begin{proof} - By definition the running thread has as current precedence the maximum of + By definition, the running thread has as current precedence the maximum of all ready threads, that is \begin{center} @@ -1089,53 +1091,71 @@ \end{center} \noindent - We also know that this is equal to all threads, that is + We also know that this is equal to the current precedences of all threads, + that is \begin{center} @{term "cp (t @ s) th' = Max (cp (t @ s) ` treads (t @ s))"} \end{center} \noindent + This is because each ready thread, say @{text "th\<^sub>r"}, has the maximum + current precedence of the subtree located at @{text "th\<^sub>r"}. All these + subtrees together form the set of threads. But the maximum of all threads is the @{term "cp"} of @{text "th"}, - which is the @{term preced} of @{text th}. + which is equal to the @{term preced} of @{text th}.\qed \end{proof} + \endnote{ @{thm "th_blockedE_pretty"} -- thm-blockedE?? + @{text "th_kept"} shows that th is a thread in s'-s + } - @{text "th_kept"} shows that th is a thread in s'-s + Next we show that a running thread @{text "th'"} must either wait for or + hold a resource in state @{text s}. + + \begin{lemma}\label{notdetached} + If @{term "th' \ running (s' @ s)"} then @{term "\detached s th'"}. + \end{lemma} - + \begin{proof} Let us assume @{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 + @{term "cp s th' = prec th s"}, and is therefore lower than the + precedence (as well as the @{text "cp"}-value) of @{term "th"}. This + means @{text "th'"} will not run as long as @{text "th"} is a + live thread. In turn this means @{text "th'"} cannot acquire a reseource + and is still detached in state @{text "s' @ s"}. Consequently + @{text "th'"} is also not boosted in state @{text "s' @ s"} and + would not run. This contradicts our assumption.\qed + \end{proof} - \begin{proof}[of Theorem 1] - If @{term "th \ running (s' @ s)"}, then there is nothing to show. So let us - assume otherwise. By Lem.~\ref{thblockedE} we know there exists a thread - @{text "th'"} that is an acestor of @{text th} in the @{text "RAG"} - and @{text "th'"} is running, that is we know - - \begin{center} - @{term "th' \ nancestors (tG (s' @ s)) th"} \quad and \quad - @{term "th' \ running (s' @ s)"} - \end{center} - - \noindent We have that @{term "th \ th'"} since we assumed - @{text th} is not running. By Lem.~\ref{thkept}, we know that - @{text "th'"} is also running in state @{text s} and by - Lem.~\ref{detached} that @{term "\detached s th'"}. - By Lem.~\ref{runningpreced} we have + \begin{proof}[of Theorem 1] If @{term "th \ running (s' @ s)"}, + then there is nothing to show. So let us assume otherwise. Since the + @{text "RAG"} is well-founded, we know there exists an ancestor of + @{text "th"} that is the root of the corrsponding subtree and + therefore is ready. Let us call this thread @{text "th'"}. We know + that @{text "th'"} has the highest precedence of all ready threads. + Therefore it is running. We have that @{term "th \ th'"} + since we assumed @{text th} is not running. By + Lem.~\ref{notdetached} we have that @{term "\detached s th'"}. + If @{text "th'"} is not detached in @{text s}, that is either + holding or waiting for a resource, it must be that @{term "th' \ + threads s"}. By Lem.~\ref{runningpreced} we have \begin{center} @{term "cp (t @ s) th' = preced th s"} \end{center} \noindent - This concludes the proof of Theorem 1. + This concludes the proof of Theorem 1.\qed \end{proof} - - + \endnote{ In what follows we will describe properties of PIP that allow us to prove Theorem~\ref{mainthm} and, when instructive, briefly describe our argument. Recall we want to prove that in state @{term "s' @ s"} @@ -1143,7 +1163,6 @@ "th'"} (@{term "th \ th'"}) which was alive in state @{term s}. We can show that - \begin{lemma} If @{thm (prem 2) eq_pv_blocked} @@ -1153,9 +1172,9 @@ \begin{lemma} If @{thm (prem 2) eq_pv_persist} then @{thm (concl) eq_pv_persist} - \end{lemma} + \end{lemma}} - \subsection*{\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 @@ -1218,7 +1237,7 @@ \end{lemma} explain tRAG - \bigskip + \bigskip} Suppose the thread @{term th} is \emph{not} running in state @{term @@ -1272,10 +1291,7 @@ Using the lemma \ref{runninginversion} we can say more about the thread th' \end{corollary} - \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. @@ -2009,6 +2025,8 @@ \bibliographystyle{plain} \bibliography{root} + + \theendnotes *} diff -r f70344294e99 -r 10c16b85a839 Journal/document/root.tex --- a/Journal/document/root.tex Fri Oct 21 14:47:01 2016 +0100 +++ b/Journal/document/root.tex Fri Dec 09 12:51:29 2016 +0000 @@ -18,6 +18,7 @@ \usepackage{url} \usepackage{color} \usepackage{courier} +\usepackage{endnotes} \usetikzlibrary{patterns} \usepackage{listings} \lstset{language=C, diff -r f70344294e99 -r 10c16b85a839 PIPBasics.thy --- a/PIPBasics.thy Fri Oct 21 14:47:01 2016 +0100 +++ b/PIPBasics.thy Fri Dec 09 12:51:29 2016 +0000 @@ -3784,14 +3784,14 @@ unfolding threads_alt_def1 by simp also have "... = Max {Max (preceds (subtree (tG s) th) s) | th. th \ readys s}" apply(subst Max_Segments[symmetric]) - prefer 5 + apply (simp add: finite_readys) + apply (simp add: fsbttGs.finite_subtree) + apply blast + using False apply blast apply(rule arg_cong) back apply(blast) - apply (simp add: finite_readys) - apply (simp add: fsbttGs.finite_subtree) - apply blast - using False by blast + done also have "... = Max {cp s th | th. th \ readys s}" unfolding cp_alt_def3 .. finally show "Max (cp s ` readys s) = Max (preceds (threads s) s)" diff -r f70344294e99 -r 10c16b85a839 journal.pdf Binary file journal.pdf has changed