# HG changeset patch # User urbanc # Date 1328907663 0 # Node ID 5ef9f6ebe827a70c7a3aaac10932b25b751a7164 # Parent 6a6d0bd16035731d1e57e2b0c8a8bd10c130bf09 more on paper; modified schs functions; it is still compatible with the old definition diff -r 6a6d0bd16035 -r 5ef9f6ebe827 prio/Paper/Paper.thy --- a/prio/Paper/Paper.thy Fri Feb 10 11:30:47 2012 +0000 +++ b/prio/Paper/Paper.thy Fri Feb 10 21:01:03 2012 +0000 @@ -22,6 +22,9 @@ depend ("RAG") and preced ("prec") and cpreced ("cprec") and + dependents ("dependants") and + waiting_queue ("wq_fun") and + cur_preced ("cprec_fun") and DUMMY ("\<^raw:\mbox{$\_\!\_$}>") (*>*) @@ -255,7 +258,7 @@ Next, we introduce the concept of \emph{waiting queues}. They are lists of threads associated with every resource. The first thread in - this list (the head, or short @{term hd}) is chosen to be in the one + this list (the head, or short @{term hd}) is chosen to be the one that is in possession of the ``lock'' of the corresponding resource. We model waiting queues as functions, below abbreviated as @{text wq}, taking a resource as @@ -272,6 +275,15 @@ \noindent In this definition we assume @{text "set"} converts a list into a set. + At the beginning, that is in the state where no process is created yet, + the waiting queue function will be just the function that returns the + empty list. + + \begin{isabelle}\ \ \ \ \ %%% + @{abbrev all_unlocked} + \end{isabelle} + + \noindent Using @{term "holding"} and @{term waiting}, we can introduce \emph{Resource Allocation Graphs} (RAG), which represent the dependencies between threads and resources. We represent RAGs as relations using pairs of the form @@ -295,7 +307,15 @@ An instance of a RAG is as follows: \begin{center} - Picture + \begin{tikzpicture}[scale=1] + \draw[step=2mm] (0,0) grid (3,2); + + \draw[rounded corners=1mm, very thick] (0,0) rectangle (0.6,0.6); + \draw[rounded corners=1mm, very thick] (3,0) rectangle (3.6,0.6); + + \draw (0.3,0.3) node {\small$th_0$}; + \draw (3.3,0.3) node {\small$th_1$}; + \end{tikzpicture} \end{center} \noindent @@ -312,16 +332,99 @@ wait for a resource being realeased (in the picture this means also @{text "th\<^isub>3"}, which cannot make any progress unless @{text "th\<^isub>2"} makes progress which in turn waits for @{text "th\<^isub>1"}). If there is a cirle in a RAG, then clearly - we have a deadlock. Therefore when we state our correctness property for PIP - we must ensure that RAGs are not circular. This allows us to define the notion - of the \emph{current precedence} of a thread @{text th} in a state @{text s}. + we have a deadlock. Therefore when a thread requests a resource, + we must ensure that the resulting RAG is not not circular. + + Next we introduce the notion of \emph{current precedence} for a thread @{text th} in a + state @{text s}, which is defined as + + \begin{isabelle}\ \ \ \ \ %%% + @{thm cpreced_def2} + \end{isabelle} + + \noindent + While the precedence of a thread is determined by the programmer (for example when the thread is + created), the point of the current precedence is to let scheduler increase this + priority, if needed according to PIP. Therefore the current precedence of @{text th} is + given as the maximum of the precedence @{text th} has in state @{text s} \emph{and} all + processes that are dependants of @{text th}. Since the notion @{term "dependents"} is + defined as the transitive closure of all dependent threads, we deal correctly with the + problem in the algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is + lowered prematurely. + + The next function, called @{term schs}, defines the behaviour of the scheduler. It is defined + by recursion on the state (a list of events); @{term "schs"} takes a state as argument + and returns a \emph{schedule state}, which we defined as a record consisting of ... + + In the initial state, the scheduler starts with all resources unlocked and the + precedence of every thread is initialised with @{term "Prc 0 0"}. + + \begin{isabelle}\ \ \ \ \ %%% + \begin{tabular}{@ {}l} + @{thm (lhs) schs.simps(1)} @{text "\"}\\ + \hspace{5mm}@{term "(|waiting_queue = all_unlocked, cur_preced = (\_::thread. Prc 0 0)|)"} + \end{tabular} + \end{isabelle} + + \noindent + The cases for @{term Create}, @{term Exit} and @{term Set} are straightforward: + we calculuate the waiting queue function of the (previous) state @{text s}; + this waiting queue function @{text wq} is unchanged in the next schedule state; for calculuating + the next @{term "cprec_fun"} we use @{text wq} and the function @{term cpreced}. + This gives the following clauses: \begin{isabelle}\ \ \ \ \ %%% - @{thm cpreced_def2}\\ + \begin{tabular}{@ {}l} + @{thm (lhs) schs.simps(2)} @{text "\"}\\ + \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\ + \hspace{8mm}@{term "(|waiting_queue = wq\, cur_preced = cpreced wq\ (Create th prio # s)|)"}\\ + @{thm (lhs) schs.simps(3)} @{text "\"}\\ + \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\ + \hspace{8mm}@{term "(|waiting_queue = wq\, cur_preced = cpreced wq\ (Exit th # s)|)"}\smallskip\\ + @{thm (lhs) schs.simps(4)} @{text "\"}\\ + \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\ + \hspace{8mm}@{term "(|waiting_queue = wq\, cur_preced = cpreced wq\ (Set th prio # s)|)"} + \end{tabular} + \end{isabelle} + + \noindent + More interesting are the cases when a resource, say @{text cs}, is locked or relaesed. In this case + we need to calculate a new waiting queue function. In case of @{term P} we update + the function so that the new thread list for @{text cs} is old thread list with the waiting + thread appended to the end (remember the head of this list is in the possession of the + resource). + + \begin{isabelle}\ \ \ \ \ %%% + \begin{tabular}{@ {}l} + @{thm (lhs) schs.simps(5)} @{text "\"}\\ + \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\ + \hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := (wq cs @ [th]))"} @{text "in"}\\ + \hspace{8mm}@{term "(|waiting_queue = new_wq, cur_preced = cpreced new_wq (P th cs # s)|)"} + \end{tabular} + \end{isabelle} + + \noindent + The case for @{term V} is similarly, except that we update the waiting queue function + using the auxiliary definition + + \begin{isabelle}\ \ \ \ \ %%% + @{abbrev release} + \end{isabelle} + + \noindent + This gives for @{term schs} the clause: + + \begin{isabelle}\ \ \ \ \ %%% + \begin{tabular}{@ {}l} + @{thm (lhs) schs.simps(6)} @{text "\"}\\ + \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\ + \hspace{5mm}@{text "let"} @{text "new_wq = release (wq cs)"} @{text "in"}\\ + \hspace{8mm}@{term "(|waiting_queue = new_wq, cur_preced = cpreced new_wq (V th cs # s)|)"} + \end{tabular} \end{isabelle} - + TODO \begin{isabelle}\ \ \ \ \ %%% \begin{tabular}{@ {}l} diff -r 6a6d0bd16035 -r 5ef9f6ebe827 prio/Paper/document/root.tex --- a/prio/Paper/document/root.tex Fri Feb 10 11:30:47 2012 +0000 +++ b/prio/Paper/document/root.tex Fri Feb 10 21:01:03 2012 +0000 @@ -4,8 +4,8 @@ \usepackage{amsmath} \usepackage{amssymb} \usepackage{mathpartir} -%\usepackage{tikz} -%\usepackage{pgf} +\usepackage{tikz} +\usepackage{pgf} %\usetikzlibrary{arrows,automata,decorations,fit,calc} %\usetikzlibrary{shapes,shapes.arrows,snakes,positioning} %\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf @@ -34,6 +34,7 @@ \newcommand{\isasymcalL}{\ensuremath{\cal{L}}} \newcommand{\isasymbigplus}{\ensuremath{\bigplus}} +\renewcommand{\isasymiota}{} \newcommand{\bigplus}{\mbox{\Large\bf$+$}} \begin{document} diff -r 6a6d0bd16035 -r 5ef9f6ebe827 prio/PrioG.thy --- a/prio/PrioG.thy Fri Feb 10 11:30:47 2012 +0000 +++ b/prio/PrioG.thy Fri Feb 10 21:01:03 2012 +0000 @@ -2072,14 +2072,17 @@ qed lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th" -proof(unfold cp_def wq_def, induct s) - case (Cons e s') - show ?case - by (auto simp:Let_def) -next - case Nil - show ?case by (auto simp:Let_def) -qed +unfolding cp_def wq_def +apply(induct s rule: schs.induct) +apply(simp add: Let_def cpreced_initial) +apply(simp add: Let_def) +apply(simp add: Let_def) +apply(simp add: Let_def) +apply(subst (2) schs.simps) +apply(simp add: Let_def) +apply(subst (2) schs.simps) +apply(simp add: Let_def) +done lemma runing_unique: diff -r 6a6d0bd16035 -r 5ef9f6ebe827 prio/PrioGDef.thy --- a/prio/PrioGDef.thy Fri Feb 10 11:30:47 2012 +0000 +++ b/prio/PrioGDef.thy Fri Feb 10 21:01:03 2012 +0000 @@ -192,13 +192,27 @@ definition cpreced :: "(cs \ thread list) \ state \ thread \ precedence" where "cpreced wq s = (\ th. Max ((\ th. preced th s) ` ({th} \ dependents wq th)))" +(*<*) lemma cpreced_def2: - "cpreced wq s th = Max ({preced th s} \ {preced th' s | th'. th' \ dependents wq th})" + "cpreced wq s th \ Max ({preced th s} \ {preced th' s | th'. th' \ dependents wq th})" unfolding cpreced_def image_def + apply(rule eq_reflection) apply(rule arg_cong) back by (auto) +(*>*) + +abbreviation + "all_unlocked \ \_::cs. ([]::thread list)" + +abbreviation + "initial_cprec \ \_::thread. Prc 0 0" + +abbreviation + "release qs \ case qs of + [] => [] + | (_#qs) => (SOME q. distinct q \ set q = set qs)" text {* \noindent The following function @{text "schs"} is used to calculate the schedule state @{text "schs s"}. @@ -206,14 +220,14 @@ *} fun schs :: "state \ schedule_state" where - "schs [] = (| waiting_queue = \ cs. [], cur_preced = cpreced (\ cs. []) [] |)" | + "schs [] = (| waiting_queue = \ cs. [], cur_preced = (\_. Prc 0 0) |)" | -- {* \begin{minipage}{0.9\textwidth} \begin{enumerate} \item @{text "ps"} is the schedule state of last moment. \item @{text "pwq"} is the waiting queue function of last moment. - \item @{text "pcp"} is the precedence function of last moment. + \item @{text "pcp"} is the precedence function of last moment (NOT USED). \item @{text "nwq"} is the new waiting queue function. It is calculated using a @{text "case"} statement: \begin{enumerate} \item If the happening event is @{text "P thread cs"}, @{text "thread"} is added to @@ -233,9 +247,34 @@ \end{enumerate} \end{minipage} *} - "schs (e#s) = (let ps = schs s in + "schs (Create th prio # s) = + (let wq = waiting_queue (schs s) in + (|waiting_queue = wq, cur_preced = cpreced wq (Create th prio # s)|))" +| "schs (Exit th # s) = + (let wq = waiting_queue (schs s) in + (|waiting_queue = wq, cur_preced = cpreced wq (Exit th # s)|))" +| "schs (Set th prio # s) = + (let wq = waiting_queue (schs s) in + (|waiting_queue = wq, cur_preced = cpreced wq (Set th prio # s)|))" +| "schs (P th cs # s) = + (let wq = waiting_queue (schs s) in + let new_wq = wq(cs := (wq cs @ [th])) in + (|waiting_queue = new_wq, cur_preced = cpreced new_wq (P th cs # s)|))" +| "schs (V th cs # s) = + (let wq = waiting_queue (schs s) in + let new_wq = wq(cs := release (wq cs)) in + (|waiting_queue = new_wq, cur_preced = cpreced new_wq (V th cs # s)|))" + +lemma cpreced_initial: + "cpreced (\ cs. []) [] = (\_. (Prc 0 0))" +apply(simp add: cpreced_def) +apply(simp add: cs_dependents_def cs_depend_def cs_waiting_def cs_holding_def) +apply(simp add: preced_def) +done + +lemma sch_old_def: + "schs (e#s) = (let ps = schs s in let pwq = waiting_queue ps in - let pcp = cur_preced ps in let nwq = case e of P th cs \ pwq(cs:=(pwq cs @ [th])) | V th cs \ let nq = case (pwq cs) of @@ -246,6 +285,10 @@ in let ncp = cpreced nwq (e#s) in \waiting_queue = nwq, cur_preced = ncp\ )" +apply(cases e) +apply(simp_all) +done + text {* \noindent diff -r 6a6d0bd16035 -r 5ef9f6ebe827 prio/paper.pdf Binary file prio/paper.pdf has changed