pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:914288aec495
+:312497c6d6b9
 In the second case we know that resource @{text cs} is locked. We can show that
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm (concl) valid_trace_p_w.RAG_es}\\
-@{text "If"} @{thm (prem 2) valid_trace_p_w.cp_kept} @{text "then"}
+@{text "If"} @{thm (prem 2) valid_trace_p_w.cp_kept_tG} @{text "then"}
 @{thm (concl) valid_trace_p_w.cp_kept_tG}
 \end{tabular}
 \end{isabelle}
-\noindent
+\noindent That means we have to add a waiting edge to the @{text
-That means we have to add a waiting edge to the @{text RAG}. Furthermore
+RAG}. Furthermore the current precedence for all threads that are
-the current precedence for all threads that are not dependants of @{text "th'"}
+not ancestors of @{text "th"} are unchanged. For the others we need
-are unchanged. For the others we need to follow the edges
+to follow the edges in the @{text TDG} and recompute the @{term
-in the @{text RAG} and recompute the @{term "cp"}. To do this we can start from @{term "th"}
+"cp"}. To do this we can start from @{term "th"} and follow the
-and follow the @{term "depend"}-edges to recompute  using Lemma~\ref{childrenlem}
+@{term "children"}-edges to recompute the @{term "cp"} of every
-the @{term "cp"} of every
+thread encountered on the way using Lemma~\ref{childrenlem}. Since
-thread encountered on the way. Since the @{term "depend"}
+the @{text RAG}, and thus @{text "TDG"}, are loop free, this
-is loop free, this procedure will always stop. The following lemma shows, however,
+procedure will always stop. The following lemma shows, however, that
-that this procedure can actually stop often earlier without having to consider all
+this procedure can actually stop often earlier without having to
-dependants.
+consider all ancestors.
 \begin{isabelle}\ \ \ \ \ %%%
-\begin{tabular}{@ {}l}
+\begin{tabular}{@ {}ll}
-%%@ {t hm[mode=IfThen] eq_up_self}\\
+@{text If} & @{thm (prem 2) valid_trace_p_w.cp_up_tG}\\
-HERE
+& @{thm (prem 4) valid_trace_p_w.cp_up_tG} and \\
-%@{text "If"} @ {thm (prem 1) eq_up}, @ {thm (prem 2) eq_up} and @ {thm (prem 3) eq_up}\\
+& @{thm (prem 3) valid_trace_p_w.cp_up_tG}\\
-%@{text "then"} @ {thm (concl) eq_up}.
+& @{text then} @{thm (concl) valid_trace_p_w.cp_up_tG}\\
 \end{tabular}
 \end{isabelle}
-\noindent
+\noindent This lemma states that if an intermediate @{term cp}-value
-This lemma states that if an intermediate @{term cp}-value does not change, then
+does not change (in this case the @{text cprec}-value of @{text "th'"}), then the procedure can
-the procedure can also stop, because none of its dependent threads will
+also stop, because none of @{text "th'"} ancestor-threads will have their
-have their current precedence changed.
+current precedence changed.
-*}
+*}
 text {*
 As can be seen, a pleasing byproduct of our formalisation is that the properties in
 this section closely inform an implementation of PIP, namely whether the
-RAG needs to be reconfigured or current precedences need to
+@{text RAG} needs to be reconfigured or current precedences need to
 be recalculated for an event. This information is provided by the lemmas we proved.
 We confirmed that our observations translate into practice by implementing
 our version of PIP on top of PINTOS, a small operating system written in C and used for teaching at
 Stanford University \cite{PINTOS}. An alternative would have been the small Xv6 operating
 system used for teaching at MIT \cite{Xv6link,Xv6}. However this operating system implements
 The waiting queue is referenced in the usual C-way as @{ML_text "&lock->wq"}.
 Next, we record that the current thread is waiting for the lock (Line 10).
 Thus we established two pointers: one in the waiting queue of the lock pointing to the
 current thread, and the other from the currend thread pointing to the lock.
 According to our specification in Section~\ref{model} and the properties we were able
-to prove for @{text P}, we need to ``chase'' all the dependants
+to prove for @{text P}, we need to ``chase'' all the ancestor threads
-in the RAG (Resource Allocation Graph) and update their
+in the @{text RAG} and update their
 current precedence; however we only have to do this as long as there is change in the
 current precedence.
 The ``chase'' is implemented in the while-loop in Lines 13 to 24.
 To initialise the loop, we
 Inside the loop, we first update the precedence of the lock held by @{ML_text pt} (Line 14).
 Next, we check whether there is a change in the current precedence of @{ML_text pt}. If not,
 then we leave the loop, since nothing else needs to be updated (Lines 15 and 16).
 If there is a change, then we have to continue our ``chase''. We check what lock the
 thread @{ML_text pt} is waiting for (Lines 17 and 18). If there is none, then
-the thread @{ML_text pt} is ready (the ``chase'' is finished with finding a root in the RAG). In this
+the thread @{ML_text pt} is ready (the ``chase'' is finished with finding a root in the @{text RAG}).
+In this
 case we update the ready-queue accordingly (Lines 19 and 20). If there is a lock  @{ML_text pt} is
 waiting for, we update the waiting queue for this lock and we continue the loop with
 the holder of that lock
 (Lines 22 and 23). After all current precedences have been updated, we finally need
 to block the current thread, because the lock it asked for was taken (Line 25).
 %referees.
 \bibliographystyle{plain}
 \bibliography{root}
-\theendnotes
+%%\theendnotes
 *}
 (*<*)
 end

changeset 190	312497c6d6b9
parent 189	914288aec495
child 191	fdba35b422a0