# HG changeset patch # User urbanc # Date 1328873447 0 # Node ID 6a6d0bd16035731d1e57e2b0c8a8bd10c130bf09 # Parent a5dd2c966cbe1b7986ba5916ff045588b1a4ccd7 more on paper diff -r a5dd2c966cbe -r 6a6d0bd16035 prio/CpsG.thy --- a/prio/CpsG.thy Thu Feb 09 16:34:18 2012 +0000 +++ b/prio/CpsG.thy Fri Feb 10 11:30:47 2012 +0000 @@ -276,13 +276,13 @@ qed -lemma cp_eq_cpreced_f: "cp s = cpreced s (wq s)" +lemma cp_eq_cpreced_f: "cp s = cpreced (wq s) s" proof - from fun_eq_iff have h:"\f g. (\ x. f x = g x) \ f = g" by auto show ?thesis proof(rule h) - from cp_eq_cpreced show "\x. cp s x = cpreced s (wq s) x" by auto + from cp_eq_cpreced show "\x. cp s x = cpreced (wq s) s x" by auto qed qed diff -r a5dd2c966cbe -r 6a6d0bd16035 prio/ExtGG.thy --- a/prio/ExtGG.thy Thu Feb 09 16:34:18 2012 +0000 +++ b/prio/ExtGG.thy Fri Feb 10 11:30:47 2012 +0000 @@ -461,7 +461,7 @@ lemma th_cp_max_preced: "cp (t@s) th = Max ((\ th'. preced th' (t @ s)) ` (threads (t@s)))" (is "?L = ?R") proof - - have "?L = cpreced (t@s) (wq (t@s)) th" + have "?L = cpreced (wq (t@s)) (t@s) th" by (unfold cp_eq_cpreced, simp) also have "\ = ?R" proof(unfold cpreced_def) diff -r a5dd2c966cbe -r 6a6d0bd16035 prio/Paper/Paper.thy --- a/prio/Paper/Paper.thy Thu Feb 09 16:34:18 2012 +0000 +++ b/prio/Paper/Paper.thy Fri Feb 10 11:30:47 2012 +0000 @@ -16,9 +16,12 @@ Prc ("'(_, _')") and holding ("holds") and waiting ("waits") and - Th ("_") and - Cs ("_") and + Th ("T") and + Cs ("C") and readys ("ready") and + depend ("RAG") and + preced ("prec") and + cpreced ("cprec") and DUMMY ("\<^raw:\mbox{$\_\!\_$}>") (*>*) @@ -162,7 +165,7 @@ PIP is based on Paulson's inductive approach to protocol verification \cite{Paulson98}, where the \emph{state} of a system is given by a list of events that happened so far. \emph{Events} in PIP fall - into five categories defined as the datatype + into five categories defined as the datatype: \begin{isabelle}\ \ \ \ \ %%% \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l} @@ -197,7 +200,8 @@ \end{isabelle} \noindent - Another function calculates the priority for a thread @{text "th"}, defined as + Another function calculates the priority for a thread @{text "th"}, which is + defined as \begin{isabelle}\ \ \ \ \ %%% \mbox{\begin{tabular}{lcl} @@ -215,7 +219,7 @@ In this definition we set @{text 0} as the default priority for threads that have not (yet) been created. The last function we need calculates the ``time'', or index, at which time a process had its - priority set. + priority last set. \begin{isabelle}\ \ \ \ \ %%% \mbox{\begin{tabular}{lcl} @@ -233,40 +237,91 @@ In this definition @{term "length s"} stands for the length of the list of events @{text s}. Again the default value in this function is @{text 0} for threads that have not been created yet. A \emph{precedence} of a thread @{text th} in a - state @{text s} is a pair of natural numbers defined as + state @{text s} is the pair of natural numbers defined as \begin{isabelle}\ \ \ \ \ %%% - @{thm (rhs) preced_def[where thread="th"]} + @{thm preced_def[where thread="th"]} \end{isabelle} \noindent The point of precedences is to schedule threads not according to priorities (because what should we do in case two threads have the same priority), but according to precedences. - Precedences allow us to always discriminate two threads with equal priority by + Precedences allow us to always discriminate between two threads with equal priority by tacking into account the time when the priority was last set. We order precedences so that threads with the same priority get a higher precedence if their priority has been - set earlier, since for such threads it is more urgent to finish. In an impementation + set earlier, since for such threads it is more urgent to finish their work. In an impementation this choice would translate to a quite natural a FIFO-scheduling of processes with the same priority. Next, we introduce the concept of \emph{waiting queues}. They are lists of threads associated with every resource. The first thread in - this list is chosen to be in the one that is in possession of the + this list (the head, or short @{term hd}) is chosen to be in 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 argument and returning a list of threads. This allows us to define - when a thread \emph{holds}, respectively \emph{waits}, for a + when a thread \emph{holds}, respectively \emph{waits} for, a resource @{text cs} given a waiting queue function. \begin{isabelle}\ \ \ \ \ %%% \begin{tabular}{@ {}l} - @{thm s_holding_def[where thread="th"]}\\ - @{thm s_waiting_def[where thread="th"]} + @{thm cs_holding_def[where thread="th"]}\\ + @{thm cs_waiting_def[where thread="th"]} \end{tabular} \end{isabelle} \noindent In this definition we assume @{text "set"} converts a list into a set. + 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 + + \begin{isabelle}\ \ \ \ \ %%% + @{term "(Th th, Cs cs)"} \hspace{5mm}{\rm and}\hspace{5mm} + @{term "(Cs cs, Th th)"} + \end{isabelle} + + \noindent + where the first stands for a \emph{waiting edge} and the second for a + \emph{holding edge} (@{term Cs} and @{term Th} are constructors of a + datatype for vertices). Given a waiting queue function, a RAG is defined + as + + \begin{isabelle}\ \ \ \ \ %%% + @{thm cs_depend_def} + \end{isabelle} + + \noindent + An instance of a RAG is as follows: + + \begin{center} + Picture + \end{center} + + \noindent + The use or relations for representing RAGs allows us to conveninetly define + the notion of the \emph{dependants} of a thread. This is defined as + + \begin{isabelle}\ \ \ \ \ %%% + @{thm cs_dependents_def} + \end{isabelle} + + \noindent + This definition needs to account for all threads that wait for tread to + release a resource. This means we need to include threads that transitively + 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}. + + \begin{isabelle}\ \ \ \ \ %%% + @{thm cpreced_def2}\\ + \end{isabelle} + + + \begin{isabelle}\ \ \ \ \ %%% \begin{tabular}{@ {}l} diff -r a5dd2c966cbe -r 6a6d0bd16035 prio/PrioG.thy --- a/prio/PrioG.thy Thu Feb 09 16:34:18 2012 +0000 +++ b/prio/PrioG.thy Fri Feb 10 11:30:47 2012 +0000 @@ -2071,7 +2071,7 @@ from wq_threads [OF vt this] show ?thesis . qed -lemma cp_eq_cpreced: "cp s th = cpreced s (wq s) th" +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 diff -r a5dd2c966cbe -r 6a6d0bd16035 prio/PrioGDef.thy --- a/prio/PrioGDef.thy Thu Feb 09 16:34:18 2012 +0000 +++ b/prio/PrioGDef.thy Fri Feb 10 11:30:47 2012 +0000 @@ -110,7 +110,7 @@ This explains the following definition: *} definition preced :: "thread \ state \ precedence" - where "preced thread s = Prc (original_priority thread s) (birthtime thread s)" + where "preced thread s \ Prc (original_priority thread s) (birthtime thread s)" text {* @@ -189,15 +189,25 @@ @{text "th"}'s {\em current precedence} equals its original precedence, i.e. @{text "preced th s"}. *} -definition cpreced :: "state \ (cs \ thread list) \ thread \ precedence" - where "cpreced s wq = (\ th. Max ((\ th. preced th s) ` ({th} \ dependents wq th)))" +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})" + unfolding cpreced_def image_def + apply(rule arg_cong) + back + by (auto) text {* \noindent The following function @{text "schs"} is used to calculate the schedule state @{text "schs s"}. It is the key function to model Priority Inheritance: *} fun schs :: "state \ schedule_state" - where "schs [] = \waiting_queue = \ cs. [], cur_preced = cpreced [] (\ cs. [])\" | + where + "schs [] = (| waiting_queue = \ cs. [], cur_preced = cpreced (\ cs. []) [] |)" | + -- {* \begin{minipage}{0.9\textwidth} \begin{enumerate} @@ -227,13 +237,13 @@ let pwq = waiting_queue ps in let pcp = cur_preced ps in let nwq = case e of - P thread cs \ pwq(cs:=(pwq cs @ [thread])) | - V thread cs \ let nq = case (pwq cs) of + P th cs \ pwq(cs:=(pwq cs @ [th])) | + V th cs \ let nq = case (pwq cs) of [] \ [] | - (th'#qs) \ (SOME q. distinct q \ set q = set qs) + (_#qs) \ (SOME q. distinct q \ set q = set qs) in pwq(cs:=nq) | _ \ pwq - in let ncp = cpreced (e#s) nwq in + in let ncp = cpreced nwq (e#s) in \waiting_queue = nwq, cur_preced = ncp\ )" diff -r a5dd2c966cbe -r 6a6d0bd16035 prio/paper.pdf Binary file prio/paper.pdf has changed