# HG changeset patch # User urbanc # Date 1329735770 0 # Node ID 813e7257c7c356d0a7067c989943e4f53955cb8d # Parent 5faa1b59e870638ac571ce8221df13231742e840 some polishing of the repository diff -r 5faa1b59e870 -r 813e7257c7c3 IsaMakefile --- a/IsaMakefile Thu Feb 16 08:12:01 2012 +0000 +++ b/IsaMakefile Mon Feb 20 11:02:50 2012 +0000 @@ -14,78 +14,54 @@ USEDIR = $(ISABELLE_TOOL) usedir -v true -t true -## Slides +## Slides 1 session1: Slides/ROOT.ML \ Slides/document/root* \ Slides/Slides.thy @$(USEDIR) -D generated -f ROOT.ML HOL Slides -slides: session1 +slides1: session1 rm -f Slides/generated/*.aux # otherwise latex will fall over cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex cp Slides/generated/root.beamer.pdf Slides/slides.pdf -## Slides 1 +## Slides 2 -session11: Slides/ROOT.ML \ +session2: Slides/ROOT.ML \ Slides/document/root* \ Slides/Slides1.thy @$(USEDIR) -D generated -f ROOT1.ML HOL Slides -slides1: session11 +slides2: session2 rm -f Slides/generated/*.aux # otherwise latex will fall over cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex cp Slides/generated/root.beamer.pdf Slides/slides1.pdf -## Slides 2 +## Slides 3 -session22: Slides/ROOT.ML \ +session3: Slides/ROOT.ML \ Slides/document/root* \ Slides/Slides2.thy @$(USEDIR) -D generated -f ROOT2.ML HOL Slides -slides2: session22 +slides3: session3 rm -f Slides/generated/*.aux # otherwise latex will fall over cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex cp Slides/generated/root.beamer.pdf Slides/slides2.pdf -## long paper -session2: tphols-2011/ROOT.ML \ - tphols-2011/document/root* \ - *.thy - @$(USEDIR) -D generated -f ROOT.ML ListP tphols-2011 - -paper: session2 - rm -f tphols-2011/generated/*.aux # otherwise latex will fall over - cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex - cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex - cp tphols-2011/generated/root.pdf tphols-2011/myhill.pdf - -## full paper - -fullsession2: tphols-2011/ROOT.ML \ - tphols-2011/document/root* \ - *.thy - @$(USEDIR) -D generated -f ROOT.ML HOL tphols-2011 - -fullpaper: fullsession2 - rm -f tphols-2011/generated/*.aux # otherwise latex will fall over - cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex - cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex - cp tphols-2011/generated/root.pdf tphols-2011/myhill.pdf - +slides: slides1 slides2 slides3 ## ITP paper -session3: Paper/ROOT.ML \ +session_itp: Paper/ROOT.ML \ Paper/document/root* \ Paper/*.thy @$(USEDIR) -D generated -f ROOT.ML HOL Paper -itp: session3 +itp: session_itp rm -f Paper/generated/*.aux # otherwise latex will fall over cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex cd Paper/generated ; bibtex root @@ -94,12 +70,12 @@ ## Journal Version -session4: Journal/ROOT.ML \ +session_journal: Journal/ROOT.ML \ Journal/document/root* \ Journal/*.thy @$(USEDIR) -D generated -f ROOT.ML HOL Journal -journal: session4 +journal: session_journal rm -f Journal/generated/*.aux # otherwise latex will fall over cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex cd Journal/generated ; bibtex root @@ -110,5 +86,6 @@ ## clean clean: - rm -rf Slides/generated/* - rm -rf tphols-2011/generated/* + rm -rf Slides/generated* + rm -rf Paper/generated* + rm -rf Journal/generated* diff -r 5faa1b59e870 -r 813e7257c7c3 Slides/slides.pdf Binary file Slides/slides.pdf has changed diff -r 5faa1b59e870 -r 813e7257c7c3 Slides/slides1.pdf Binary file Slides/slides1.pdf has changed diff -r 5faa1b59e870 -r 813e7257c7c3 Slides/slides2.pdf Binary file Slides/slides2.pdf has changed diff -r 5faa1b59e870 -r 813e7257c7c3 prio/CpsG.thy --- a/prio/CpsG.thy Thu Feb 16 08:12:01 2012 +0000 +++ b/prio/CpsG.thy Mon Feb 20 11:02:50 2012 +0000 @@ -49,7 +49,7 @@ case (thread_P thread cs) assume eq_e: "e = P thread cs" and is_runing: "thread \ runing s" - from prems have vtp: "vt (P thread cs#s)" by auto + from assms thread_exit ih stp not_in vt eq_e have vtp: "vt (P thread cs#s)" by auto have neq_th: "th \ thread" proof - from not_in eq_e have "th \ threads s" by simp @@ -77,7 +77,7 @@ by (simp add:runing_def readys_def) ultimately show ?thesis by auto qed - from prems have vtv: "vt (V thread cs#s)" by auto + from assms thread_V eq_e ih stp not_in vt have vtv: "vt (V thread cs#s)" by auto from hold obtain rest where eq_wq: "wq s cs = thread # rest" by (case_tac "wq s cs", auto simp: wq_def s_holding_def) diff -r 5faa1b59e870 -r 813e7257c7c3 prio/Paper/Paper.thy --- a/prio/Paper/Paper.thy Thu Feb 16 08:12:01 2012 +0000 +++ b/prio/Paper/Paper.thy Mon Feb 20 11:02:50 2012 +0000 @@ -541,7 +541,7 @@ \end{center} \noindent - The first rule states that a thread can only be created, if it does not yet exists. + The first rule states that a thread can only be created, if it is not alive yet. Similarly, the second rule states that a thread can only be terminated if it was running and does not lock any resources anymore (this simplifies slightly our model; in practice we would expect the operating system releases all locks held by a @@ -559,7 +559,7 @@ the responsibility of the programmer. In our formal model we brush aside these problematic cases in order to be able to make some meaningful statements about PIP.\footnote{This situation is - similar to the infamous occurs check in Prolog: In order to say + similar to the infamous \emph{occurs check} in Prolog: In order to say anything meaningful about unification, one needs to perform an occurs check. But in practice the occurs check is omitted and the responsibility for avoiding problems rests with the programmer.} @@ -602,11 +602,11 @@ Sha et al.~state their first correctness criterion for PIP in terms of the number of low-priority threads \cite[Theorem 3]{Sha90}: if there are @{text n} low-priority threads, then a blocked job with - high priority can only be blocked @{text n} times. + high priority can only be blocked a maximum of @{text n} times. Their second correctness criterion is given in terms of the number of critical resources \cite[Theorem 6]{Sha90}: if there are @{text m} critical resources, then a blocked job with high priority - can only be blocked @{text m} times. Both results on their own, strictly speaking, do + can only be blocked a maximum of @{text m} times. Both results on their own, strictly speaking, do \emph{not} prevent indefinite, or unbounded, Priority Inversion, because if a low-priority thread does not give up its critical resource (the one the high-priority thread is waiting for), then the @@ -627,23 +627,26 @@ Even when fixed, their proof idea does not seem to go through for us, because of the way we have set up our formal model of PIP. One reason is that we allow that critical sections can intersect - (something Sha et al.~explicitly exclude). Therefore we have designed a - different correctness criterion for PIP. The idea behind our - criterion is as follows: for all states @{text - s}, we know the corresponding thread @{text th} with the highest - precedence; we show that in every future state (denoted by @{text - "s' @ s"}) in which @{text th} is still alive, either @{text th} is - running or it is blocked by a thread that was alive in the state - @{text s} and was in the possession of a lock in @{text s}. Since in @{text s}, as in every state, the set of alive - threads is finite, @{text th} can only be blocked a finite number of - times. We will actually prove a stronger statement where we also provide - the current precedence of the blocking thread. However, this - correctness criterion hinges upon a number of assumptions about the - states @{text s} and @{text "s' @ s"}, the thread @{text th} and the - events happening in @{text s'}. We list them next: + (something Sha et al.~explicitly exclude). Therefore we have + designed a different correctness criterion for PIP. The idea behind + our criterion is as follows: for all states @{text s}, we know the + corresponding thread @{text th} with the highest precedence; we show + that in every future state (denoted by @{text "s' @ s"}) in which + @{text th} is still alive, either @{text th} is running or it is + blocked by a thread that was alive in the state @{text s} and was in + the possession of a lock in @{text s}. Since in @{text s}, as in + every state, the set of alive threads is finite, @{text th} can only + be blocked a finite number of times. This is independent of how many + threads of lower priority are created in @{text "s'"}. We will actually prove a + stronger statement where we also provide the current precedence of + the blocking thread. However, this correctness criterion hinges upon + a number of assumptions about the states @{text s} and @{text "s' @ + s"}, the thread @{text th} and the events happening in @{text + s'}. We list them next: \begin{quote} - {\bf Assumptions on the states @{text s} and @{text "s' @ s"}:} In order to make + {\bf Assumptions on the states {\boldmath@{text s}} and + {\boldmath@{text "s' @ s"}:}} In order to make any meaningful statement, we need to require that @{text "s"} and @{text "s' @ s"} are valid states, namely \begin{isabelle}\ \ \ \ \ %%% @@ -655,7 +658,8 @@ \end{quote} \begin{quote} - {\bf Assumptions on the thread @{text "th"}:} The thread @{text th} must be alive in @{text s} and + {\bf Assumptions on the thread {\boldmath@{text "th"}:}} + The thread @{text th} must be alive in @{text s} and has the highest precedence of all alive threads in @{text s}. Furthermore the priority of @{text th} is @{text prio} (we need this in the next assumptions). \begin{isabelle}\ \ \ \ \ %%% @@ -668,7 +672,7 @@ \end{quote} \begin{quote} - {\bf Assumptions on the events in @{text "s'"}:} We want to prove that @{text th} cannot + {\bf Assumptions on the events in {\boldmath@{text "s'"}:}} We want to prove that @{text th} cannot be blocked indefinitely. Of course this can happen if threads with higher priority than @{text th} are continuously created in @{text s'}. Therefore we have to assume that events in @{text s'} can only create (respectively set) threads with equal or lower @@ -686,7 +690,7 @@ \noindent The locale mechanism of Isabelle helps us to manage conveniently such assumptions~\cite{Haftmann08}. - Under these assumptions we will prove the following correctness property: + Under these assumptions we shall prove the following correctness property: \begin{theorem}\label{mainthm} Given the assumptions about states @{text "s"} and @{text "s' @ s"}, @@ -808,7 +812,7 @@ that the current precedence of @{text th'} in state @{text "(s' @ s)"} must be equal to the precedence of @{text th} in @{text "s"}. We show this theorem by induction on @{text "s'"} using Lemma~\ref{mainlem}. - This theorem gives a stricter bound on the processes that can block @{text th} than the + This theorem gives a stricter bound on the threads that can block @{text th} than the one obtained by Sha et al.~\cite{Sha90}: only threads that were alive in state @{text s} and moreover held a resource. This means our bound is in terms of both---alive threads in state @{text s} @@ -1229,7 +1233,7 @@ to \cite{Steinberg10}, is that except for one unsatisfactory proposal nobody has a good idea for how PIP should be modified to work correctly on multi-processor systems. The difficulties become - clear when considering the fact that locking and releasing a resource always + clear when considering the fact that releasing and re-locking a resource always requires a small amount of time. If processes work independently, then a low priority process can ``steal'' in such an unguarded moment a lock for a resource that was supposed to allow a high-priority diff -r 5faa1b59e870 -r 813e7257c7c3 prio/Paper/document/root.bib --- a/prio/Paper/document/root.bib Thu Feb 16 08:12:01 2012 +0000 +++ b/prio/Paper/document/root.bib Mon Feb 20 11:02:50 2012 +0000 @@ -1,7 +1,7 @@ @inproceedings{Haftmann08, author = {F.~Haftmann and M.~Wenzel}, title = {{L}ocal {T}heory {S}pecifications in {I}sabelle/{I}sar}, - booktitle = {Proc.~of the International Conference on Types, Proofs and Programms (TYPES)}, + booktitle = {Proc.~of the International Conference on Types, Proofs and Programs (TYPES)}, year = {2008}, pages = {153-168}, series = {LNCS}, diff -r 5faa1b59e870 -r 813e7257c7c3 prio/PrioG.thy --- a/prio/PrioG.thy Thu Feb 16 08:12:01 2012 +0000 +++ b/prio/PrioG.thy Mon Feb 20 11:02:50 2012 +0000 @@ -361,7 +361,7 @@ and "waiting s th cs1" and "waiting s th cs2" shows "cs1 = cs2" -using waiting_unique_pre prems +using waiting_unique_pre assms unfolding wq_def s_waiting_def by auto @@ -371,7 +371,7 @@ assumes "holding s th1 cs" and "holding s th2 cs" shows "th1 = th2" -using prems +using assms unfolding s_holding_def by auto @@ -1204,7 +1204,7 @@ and not_in: "th \ set rest" shows "(th \ readys (V thread cs#s)) = (th \ readys s)" proof - - from prems show ?thesis + from assms show ?thesis apply (auto simp:readys_def) apply(simp add:s_waiting_def[folded wq_def]) apply (erule_tac x = csa in allE) @@ -1354,7 +1354,7 @@ and "wq s cs = []" shows "holdents (P th cs#s) th = holdents s th \ {cs}" proof - - from prems show ?thesis + from assms show ?thesis unfolding holdents_def step_depend_p[OF vt] by auto qed @@ -1364,7 +1364,7 @@ and "wq s cs \ []" shows "holdents (P th cs#s) th = holdents s th" proof - - from prems show ?thesis + from assms show ?thesis unfolding holdents_def step_depend_p[OF vt] by auto qed @@ -1545,7 +1545,7 @@ assume eq_e: "e = P thread cs" and is_runing: "thread \ runing s" and no_dep: "(Cs cs, Th thread) \ (depend s)\<^sup>+" - from prems have vtp: "vt (P thread cs#s)" by auto + from thread_P vt stp ih have vtp: "vt (P thread cs#s)" by auto show ?thesis proof - { have hh: "\ A B C. (B = C) \ (A \ B) = (A \ C)" by blast @@ -1650,7 +1650,7 @@ qed next case (thread_V thread cs) - from prems have vtv: "vt (V thread cs # s)" by auto + from assms vt stp ih thread_V have vtv: "vt (V thread cs # s)" by auto assume eq_e: "e = V thread cs" and is_runing: "thread \ runing s" and hold: "holding s thread cs" @@ -1983,7 +1983,7 @@ case (thread_P thread cs) assume eq_e: "e = P thread cs" and is_runing: "thread \ runing s" - from prems have vtp: "vt (P thread cs#s)" by auto + from assms thread_P ih vt stp thread_P have vtp: "vt (P thread cs#s)" by auto have neq_th: "th \ thread" proof - from not_in eq_e have "th \ threads s" by simp @@ -2011,7 +2011,7 @@ by (simp add:runing_def readys_def) ultimately show ?thesis by auto qed - from prems have vtv: "vt (V thread cs#s)" by auto + from assms thread_V vt stp ih have vtv: "vt (V thread cs#s)" by auto from hold obtain rest where eq_wq: "wq s cs = thread # rest" by (case_tac "wq s cs", auto simp: wq_def s_holding_def) diff -r 5faa1b59e870 -r 813e7257c7c3 prio/paper.pdf Binary file prio/paper.pdf has changed diff -r 5faa1b59e870 -r 813e7257c7c3 tphols-2011/myhill.pdf Binary file tphols-2011/myhill.pdf has changed