# HG changeset patch # User urbanc # Date 1328792751 0 # Node ID 440382eb642743bc40c3231ecfc821eef115afd4 # Parent 572f202659ff21ea32c173348a6ecf8a6951b758 more on the specification section diff -r 572f202659ff -r 440382eb6427 prio/Paper/Paper.thy --- a/prio/Paper/Paper.thy Wed Feb 08 16:35:49 2012 +0000 +++ b/prio/Paper/Paper.thy Thu Feb 09 13:05:51 2012 +0000 @@ -14,6 +14,11 @@ birthtime ("last'_set") and If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and Prc ("'(_, _')") and + holding ("holds") and + waiting ("waits") and + Th ("_") and + Cs ("_") and + readys ("ready") and DUMMY ("\<^raw:\mbox{$\_\!\_$}>") (*>*) @@ -156,7 +161,7 @@ later to the case of PIP on multi-processor systems.} Our model of 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} fall + given by a list of events that happened so far. \emph{Events} in PIP fall into five categories defined as the datatype \begin{isabelle}\ \ \ \ \ %%% @@ -192,7 +197,7 @@ \end{isabelle} \noindent - Another calculates the priority for a thread @{text "th"}, defined as + Another function calculates the priority for a thread @{text "th"}, defined as \begin{isabelle}\ \ \ \ \ %%% \mbox{\begin{tabular}{lcl} @@ -224,18 +229,18 @@ \end{tabular}} \end{isabelle} - \footnote{Can Precedence be the real birth-time / or must be time precedence last set?} - \noindent - A \emph{precedence} of a thread @{text th} in a state @{text s} is a pair of - natural numbers defined as + 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 \begin{isabelle}\ \ \ \ \ %%% @{thm (rhs) preced_def[where thread="th"]} \end{isabelle} \noindent - The point of precedences is to schedule threads not according to priorities (what should + 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 tacking into account the time when the priority was last set. We order precedences so @@ -251,18 +256,40 @@ 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 - resource @{text cs}. + 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"]} + \end{tabular} + \end{isabelle} + + \noindent + In this definition we assume @{text "set"} converts a list into a set. \begin{isabelle}\ \ \ \ \ %%% \begin{tabular}{@ {}l} - @{thm cs_holding_def[where thread="th"]}\\ - @{thm cs_waiting_def[where thread="th"]} + @{thm s_depend_def}\\ + \end{tabular} + \end{isabelle} + + \begin{isabelle}\ \ \ \ \ %%% + \begin{tabular}{@ {}l} + @{thm readys_def}\\ + \end{tabular} + \end{isabelle} + + \begin{isabelle}\ \ \ \ \ %%% + \begin{tabular}{@ {}l} + @{thm runing_def}\\ \end{tabular} \end{isabelle} + resources - resources + done: threads not done: running step relation: @@ -271,6 +298,7 @@ @{thm[mode=Rule] thread_create[where thread=th]}\hspace{1cm} @{thm[mode=Rule] thread_exit[where thread=th]}\medskip\\ + @{thm[mode=Rule] thread_set[where thread=th]}\medskip\\ @{thm[mode=Rule] thread_P[where thread=th]}\medskip\\ @{thm[mode=Rule] thread_V[where thread=th]}\\ \end{tabular} diff -r 572f202659ff -r 440382eb6427 prio/PrioG.thy --- a/prio/PrioG.thy Wed Feb 08 16:35:49 2012 +0000 +++ b/prio/PrioG.thy Thu Feb 09 13:05:51 2012 +0000 @@ -791,11 +791,12 @@ else depend s \ {(Th th, Cs cs)})" apply(unfold s_depend_def wq_def) apply (auto split:list.splits prod.splits simp:Let_def cs_waiting_def cs_holding_def) - apply(case_tac "c = cs", auto) + apply(case_tac "csa = cs", auto) apply(fold wq_def) apply(drule_tac step_back_step) - by (ind_cases " step s (P (hd (wq s cs)) cs)", - auto simp:s_depend_def wq_def cs_holding_def) + apply(ind_cases " step s (P (hd (wq s cs)) cs)") + apply(auto simp:s_depend_def wq_def cs_holding_def) + done lemma simple_A: fixes A diff -r 572f202659ff -r 440382eb6427 prio/PrioGDef.thy --- a/prio/PrioGDef.thy Wed Feb 08 16:35:49 2012 +0000 +++ b/prio/PrioGDef.thy Thu Feb 09 13:05:51 2012 +0000 @@ -159,7 +159,7 @@ *} cs_depend_def: "depend (wq::cs \ thread list) \ - {(Th t, Cs c) | t c. waiting wq t c} \ {(Cs c, Th t) | c t. holding wq t c}" + {(Th th, Cs cs) | th cs. waiting wq th cs} \ {(Cs cs, Th th) | cs th. holding wq th cs}" -- {* \begin{minipage}{0.9\textwidth} The following @{text "dependents wq th"} represents the set of threads which are depending on @@ -264,7 +264,7 @@ "waiting (s::state) thread cs \ (thread \ set (wq s cs) \ thread \ hd (wq s cs))" s_depend_def: "depend (s::state) \ - {(Th t, Cs c) | t c. waiting (wq s) t c} \ {(Cs c, Th t) | c t. holding (wq s) t c}" + {(Th th, Cs cs) | th cs. waiting (wq s) th cs} \ {(Cs cs, Th th) | cs th. holding (wq s) th cs}" s_dependents_def: "dependents (s::state) th \ {th' . (Th th', Th th) \ (depend (wq s))^+}" @@ -273,7 +273,7 @@ for running if it is a live thread and it is not waiting for any critical resource. *} definition readys :: "state \ thread set" - where "readys s = {thread . thread \ threads s \ (\ cs. \ waiting s thread cs)}" + where "readys s \ {th . th \ threads s \ (\ cs. \ waiting s th cs)}" text {* \noindent The following function @{text "runing"} calculates the set of running thread, which is the ready diff -r 572f202659ff -r 440382eb6427 prio/paper.pdf Binary file prio/paper.pdf has changed