--- a/prio/Paper/Paper.thy Tue Jan 24 00:34:52 2012 +0000
+++ b/prio/Paper/Paper.thy Fri Jan 27 13:50:02 2012 +0000
@@ -1,6 +1,6 @@
(*<*)
theory Paper
-imports CpsG ExtGG
+imports CpsG ExtGG LaTeXsugar
begin
(*>*)
@@ -113,11 +113,260 @@
*}
section {* General properties of Priority Inheritance \label{general} *}
+(*<*)
+ML {*
+ val () = show_question_marks_default := false;
+*}
+(*>*)
+
+text {*
+ The following are several very basic prioprites:
+ \begin{enumerate}
+ \item All runing threads must be ready (@{text "runing_ready"}):
+ @{thm[display] "runing_ready"}
+ \item All ready threads must be living (@{text "readys_threads"}):
+ @{thm[display] "readys_threads"}
+ \item There are finite many living threads at any moment (@{text "finite_threads"}):
+ @{thm[display] "finite_threads"}
+ \item Every waiting queue does not contain duplcated elements (@{text "wq_distinct"}):
+ @{thm[display] "wq_distinct"}
+ \item All threads in waiting queues are living threads (@{text "wq_threads"}):
+ @{thm[display] "wq_threads"}
+ \item The event which can get a thread into waiting queue must be @{term "P"}-events
+ (@{text "block_pre"}):
+ @{thm[display] "block_pre"}
+ \item A thread may never wait for two different critical resources
+ (@{text "waiting_unique"}):
+ @{thm[display] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}
+ \item Every resource can only be held by one thread
+ (@{text "held_unique"}):
+ @{thm[display] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}
+ \item Every living thread has an unique precedence
+ (@{text "preced_unique"}):
+ @{thm[display] preced_unique[of "th\<^isub>1" _ "th\<^isub>2"]}
+ \end{enumerate}
+*}
+
+text {* \noindent
+ The following lemmas show how RAG is changed with the execution of events:
+ \begin{enumerate}
+ \item Execution of @{term "Set"} does not change RAG (@{text "depend_set_unchanged"}):
+ @{thm[display] depend_set_unchanged}
+ \item Execution of @{term "Create"} does not change RAG (@{text "depend_create_unchanged"}):
+ @{thm[display] depend_create_unchanged}
+ \item Execution of @{term "Exit"} does not change RAG (@{text "depend_exit_unchanged"}):
+ @{thm[display] depend_exit_unchanged}
+ \item Execution of @{term "P"} (@{text "step_depend_p"}):
+ @{thm[display] step_depend_p}
+ \item Execution of @{term "V"} (@{text "step_depend_v"}):
+ @{thm[display] step_depend_v}
+ \end{enumerate}
+ *}
+
+text {* \noindent
+ These properties are used to derive the following important results about RAG:
+ \begin{enumerate}
+ \item RAG is loop free (@{text "acyclic_depend"}):
+ @{thm [display] acyclic_depend}
+ \item RAGs are finite (@{text "finite_depend"}):
+ @{thm [display] finite_depend}
+ \item Reverse paths in RAG are well founded (@{text "wf_dep_converse"}):
+ @{thm [display] wf_dep_converse}
+ \item The dependence relation represented by RAG has a tree structure (@{text "unique_depend"}):
+ @{thm [display] unique_depend[of _ _ "n\<^isub>1" "n\<^isub>2"]}
+ \item All threads in RAG are living threads
+ (@{text "dm_depend_threads"} and @{text "range_in"}):
+ @{thm [display] dm_depend_threads range_in}
+ \end{enumerate}
+ *}
+
+text {* \noindent
+ The following lemmas show how every node in RAG can be chased to ready threads:
+ \begin{enumerate}
+ \item Every node in RAG can be chased to a ready thread (@{text "chain_building"}):
+ @{thm [display] chain_building[rule_format]}
+ \item The ready thread chased to is unique (@{text "dchain_unique"}):
+ @{thm [display] dchain_unique[of _ _ "th\<^isub>1" "th\<^isub>2"]}
+ \end{enumerate}
+ *}
+
+text {* \noindent
+ Properties about @{term "next_th"}:
+ \begin{enumerate}
+ \item The thread taking over is different from the thread which is releasing
+ (@{text "next_th_neq"}):
+ @{thm [display] next_th_neq}
+ \item The thread taking over is unique
+ (@{text "next_th_unique"}):
+ @{thm [display] next_th_unique[of _ _ _ "th\<^isub>1" "th\<^isub>2"]}
+ \end{enumerate}
+ *}
+
+text {* \noindent
+ Some deeper results about the system:
+ \begin{enumerate}
+ \item There can only be one running thread (@{text "runing_unique"}):
+ @{thm [display] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}
+ \item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}):
+ @{thm [display] max_cp_eq}
+ \item There must be one ready thread having the max @{term "cp"}-value
+ (@{text "max_cp_readys_threads"}):
+ @{thm [display] max_cp_readys_threads}
+ \end{enumerate}
+ *}
+
+text {* \noindent
+ The relationship between the count of @{text "P"} and @{text "V"} and the number of
+ critical resources held by a thread is given as follows:
+ \begin{enumerate}
+ \item The @{term "V"}-operation decreases the number of critical resources
+ one thread holds (@{text "cntCS_v_dec"})
+ @{thm [display] cntCS_v_dec}
+ \item The number of @{text "V"} never exceeds the number of @{text "P"}
+ (@{text "cnp_cnv_cncs"}):
+ @{thm [display] cnp_cnv_cncs}
+ \item The number of @{text "V"} equals the number of @{text "P"} when
+ the relevant thread is not living:
+ (@{text "cnp_cnv_eq"}):
+ @{thm [display] cnp_cnv_eq}
+ \item When a thread is not living, it does not hold any critical resource
+ (@{text "not_thread_holdents"}):
+ @{thm [display] not_thread_holdents}
+ \item When the number of @{text "P"} equals the number of @{text "V"}, the relevant
+ thread does not hold any critical resource, therefore no thread can depend on it
+ (@{text "count_eq_dependents"}):
+ @{thm [display] count_eq_dependents}
+ \end{enumerate}
+ *}
section {* Key properties \label{extension} *}
+(*<*)
+context extend_highest_gen
+begin
+(*>*)
+
+text {*
+ The essential of {\em Priority Inheritance} is to avoid indefinite priority inversion. For this
+ purpose, we need to investigate what happens after one thread takes the highest precedence.
+ A locale is used to describe such a situation, which assumes:
+ \begin{enumerate}
+ \item @{term "s"} is a valid state (@{text "vt_s"}):
+ @{thm vt_s}.
+ \item @{term "th"} is a living thread in @{term "s"} (@{text "threads_s"}):
+ @{thm threads_s}.
+ \item @{term "th"} has the highest precedence in @{term "s"} (@{text "highest"}):
+ @{thm highest}.
+ \item The precedence of @{term "th"} is @{term "Prc prio tm"} (@{text "preced_th"}):
+ @{thm preced_th}.
+ \end{enumerate}
+ *}
+
+text {* \noindent
+ Under these assumptions, some basic priority can be derived for @{term "th"}:
+ \begin{enumerate}
+ \item The current precedence of @{term "th"} equals its own precedence (@{text "eq_cp_s_th"}):
+ @{thm [display] eq_cp_s_th}
+ \item The current precedence of @{term "th"} is the highest precedence in
+ the system (@{text "highest_cp_preced"}):
+ @{thm [display] highest_cp_preced}
+ \item The precedence of @{term "th"} is the highest precedence
+ in the system (@{text "highest_preced_thread"}):
+ @{thm [display] highest_preced_thread}
+ \item The current precedence of @{term "th"} is the highest current precedence
+ in the system (@{text "highest'"}):
+ @{thm [display] highest'}
+ \end{enumerate}
+ *}
+
+text {* \noindent
+ To analysis what happens after state @{term "s"} a sub-locale is defined, which
+ assumes:
+ \begin{enumerate}
+ \item @{term "t"} is a valid extension of @{term "s"} (@{text "vt_t"}): @{thm vt_t}.
+ \item Any thread created in @{term "t"} has priority no higher than @{term "prio"}, therefore
+ its precedence can not be higher than @{term "th"}, therefore
+ @{term "th"} remain to be the one with the highest precedence
+ (@{text "create_low"}):
+ @{thm [display] create_low}
+ \item Any adjustment of priority in
+ @{term "t"} does not happen to @{term "th"} and
+ the priority set is no higher than @{term "prio"}, therefore
+ @{term "th"} remain to be the one with the highest precedence (@{text "set_diff_low"}):
+ @{thm [display] set_diff_low}
+ \item Since we are investigating what happens to @{term "th"}, it is assumed
+ @{term "th"} does not exit during @{term "t"} (@{text "exit_diff"}):
+ @{thm [display] exit_diff}
+ \end{enumerate}
+*}
+
+text {* \noindent
+ All these assumptions are put into a predicate @{term "extend_highest_gen"}.
+ It can be proved that @{term "extend_highest_gen"} holds
+ for any moment @{text "i"} in it @{term "t"} (@{text "red_moment"}):
+ @{thm [display] red_moment}
+
+ From this, an induction principle can be derived for @{text "t"}, so that
+ properties already derived for @{term "t"} can be applied to any prefix
+ of @{text "t"} in the proof of new properties
+ about @{term "t"} (@{text "ind"}):
+ \begin{center}
+ @{thm[display] ind}
+ \end{center}
+
+ The following properties can be proved about @{term "th"} in @{term "t"}:
+ \begin{enumerate}
+ \item In @{term "t"}, thread @{term "th"} is kept live and its
+ precedence is preserved as well
+ (@{text "th_kept"}):
+ @{thm [display] th_kept}
+ \item In @{term "t"}, thread @{term "th"}'s precedence is always the maximum among
+ all living threads
+ (@{text "max_preced"}):
+ @{thm [display] max_preced}
+ \item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum precedence
+ among all living threads
+ (@{text "th_cp_max_preced"}):
+ @{thm [display] th_cp_max_preced}
+ \item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum current
+ precedence among all living threads
+ (@{text "th_cp_max"}):
+ @{thm [display] th_cp_max}
+ \item In @{term "t"}, thread @{term "th"}'s current precedence equals its precedence at moment
+ @{term "s"}
+ (@{text "th_cp_preced"}):
+ @{thm [display] th_cp_preced}
+ \end{enumerate}
+ *}
+
+text {* \noindent
+ The main theorem is to characterizing the running thread during @{term "t"}
+ (@{text "runing_inversion_2"}):
+ @{thm [display] runing_inversion_2}
+ According to this, if a thread is running, it is either @{term "th"} or was
+ already live and held some resource
+ at moment @{text "s"} (expressed by: @{text "cntV s th' < cntP s th'"}).
+
+ Since there are only finite many threads live and holding some resource at any moment,
+ if every such thread can release all its resources in finite duration, then after finite
+ duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen
+ then.
+ *}
+
+(*<*)
+end
+(*>*)
+
section {* Properties to guide implementation \label{implement} *}
+text {*
+ The properties (especially @{text "runing_inversion_2"}) convinced us that model defined
+ in section \ref{model} does prevent indefinite priority inversion and therefore fulfills
+ the fundamental requirement of Priority Inheritance protocol. Another purpose of this paper
+ is to show how this model can be used to guide a concrete implementation.
+ *}
+
+
section {* Related works \label{related} *}
text {*