--- 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*
Binary file Slides/slides.pdf has changed
Binary file Slides/slides1.pdf has changed
Binary file Slides/slides2.pdf has changed
--- 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 \<in> 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 \<noteq> thread"
proof -
from not_in eq_e have "th \<notin> 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)
--- 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
--- 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},
--- 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 \<notin> set rest"
shows "(th \<in> readys (V thread cs#s)) = (th \<in> 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 \<union> {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 \<noteq> []"
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 \<in> runing s"
and no_dep: "(Cs cs, Th thread) \<notin> (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: "\<And> A B C. (B = C) \<Longrightarrow> (A \<and> B) = (A \<and> 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 \<in> 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 \<in> 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 \<noteq> thread"
proof -
from not_in eq_e have "th \<notin> 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)
Binary file prio/paper.pdf has changed
Binary file tphols-2011/myhill.pdf has changed