--- a/Correctness.thy Thu Jun 02 13:15:03 2016 +0100
+++ b/Correctness.thy Tue Jun 07 13:51:39 2016 +0100
@@ -793,28 +793,29 @@
qed
lemma (* new proof of th_blockedE *)
- assumes "th \<notin> runing (t@s)"
+ assumes "th \<notin> runing (t @ s)"
obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
- "th' \<in> runing (t@s)"
+ "th' \<in> runing (t @ s)"
proof -
- -- {* According to @{thm vat_t.th_chain_to_ready}, either
- @{term "th"} is in @{term "readys"} or there is path leading from it to
- one thread in @{term "readys"}. *}
- have "th \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+)"
+
+ -- {* According to @{thm vat_t.th_chain_to_ready}, either @{term "th"} is
+ in @{term "readys"} or there is path in the @{term RAG} leading from
+ it to a thread that is in @{term "readys"}. However, @{term th} cannot
+ be in @{term readys}, because otherwise, since @{term th} holds the
+ highest @{term cp}-value, it must be @{term "runing"}. This would
+ violate our assumption. *}
+ have "th \<notin> readys (t @ s)"
+ using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto
+ then have "\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+"
using th_kept vat_t.th_chain_to_ready by auto
- -- {* However, @{term th} can not be in @{term readys}, because otherwise, since
- @{term th} holds the highest @{term cp}-value, it must be @{term "runing"}. *}
- moreover have "th \<notin> readys (t@s)"
- using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto
- -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in
- term @{term readys}: *}
- ultimately obtain th' where th'_in: "th' \<in> readys (t@s)"
- and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto
- -- {* We are going to show that this @{term th'} is running. *}
- have "th' \<in> runing (t@s)"
+ then obtain th' where th'_in: "th' \<in> readys (t@s)"
+ and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto
+
+ -- {* We are going to first show that this @{term th'} is running. *}
+ have "th' \<in> runing (t @ s)"
proof -
- -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *}
- have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R")
+ -- {* For this we need to show that @{term th'} holds the highest @{term cp}-value: *}
+ have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" (is "?L = ?R")
proof -
-- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}),
the @{term cp}-value of @{term th'} is the maximum of
@@ -828,7 +829,7 @@
qed
also have "... = (the_preced (t @ s) th)"
proof(rule image_Max_subset)
- show "finite (threads (t@s))" by (simp add: vat_t.finite_threads)
+ show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads)
next
show "the_thread ` subtree (tRAG (t @ s)) (Th th') \<subseteq> threads (t @ s)"
by (smt imageE mem_Collect_eq readys_def subsetCE subsetI th'_in
@@ -847,21 +848,25 @@
also have "... = ?R"
using th_cp_max th_cp_preced th_kept
the_preced_def vat_t.max_cp_readys_threads by auto
- thm th_cp_max th_cp_preced th_kept
- the_preced_def vat_t.max_cp_readys_threads
- finally show ?thesis .
+ finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" .
qed
- -- {* Now, since @{term th'} holds the highest @{term cp}
- and we have already show it is in @{term readys},
+
+ -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys,
it is @{term runing} by definition. *}
- with `th' \<in> readys (t@s)` show ?thesis by (simp add: runing_def)
+ with `th' \<in> readys (t @ s)` show "th' \<in> runing (t @ s)" by (simp add: runing_def)
qed
+
-- {* It is easy to show @{term th'} is an ancestor of @{term th}: *}
moreover have "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def)
ultimately show ?thesis using that by metis
qed
+lemma th_blockedE_pretty:
+ assumes "th \<notin> runing (t@s)"
+ shows "\<exists>th'. Th th' \<in> ancestors (RAG (t @ s)) (Th th) \<and> th' \<in> runing (t@s)"
+using th_blockedE assms by blast
+
text {*
Now it is easy to see there is always a thread to run by case analysis
on whether thread @{term th} is running: if the answer is Yes, the
--- a/Journal/Paper.thy Thu Jun 02 13:15:03 2016 +0100
+++ b/Journal/Paper.thy Tue Jun 07 13:51:39 2016 +0100
@@ -5,6 +5,26 @@
"~~/src/HOL/Library/LaTeXsugar"
begin
+ML {* Scan.succeed *}
+
+ML {*
+ fun strip_quants ctxt trm =
+ case trm of
+ Const("HOL.Trueprop", _) $ t => strip_quants ctxt t
+ | Const("Pure.imp", _) $ _ $ t => strip_quants ctxt t
+ | Const("Pure.all", _) $ Abs(n, T, t) =>
+ strip_quants ctxt (subst_bound (Free (n, T), t))
+ | Const("HOL.All", _) $ Abs(n, T, t) =>
+ strip_quants ctxt (subst_bound (Free (n, T), t))
+ | Const("HOL.Ex", _) $ Abs(n, T, t) =>
+ strip_quants ctxt (subst_bound (Free (n, T), t))
+ | _ => trm
+*}
+
+
+setup {* Term_Style.setup @{binding "no_quants"} (Scan.succeed strip_quants) *}
+
+
declare [[show_question_marks = false]]
notation (latex output)
@@ -26,6 +46,7 @@
DUMMY ("\<^raw:\mbox{$\_\!\_$}>") and
cntP ("c\<^bsub>P\<^esub>") and
cntV ("c\<^bsub>V\<^esub>")
+
(*>*)
@@ -1021,11 +1042,29 @@
thread is exactly @{term "th'"}.
\begin{lemma}
- If @{thm (prem 1) th_blockedE_pretty} then
- @{thm (concl) th_blockedE_pretty}.
+ If @{thm (prem 1) th_blockedE_pretty} then there exists a thread @{text "th'"}
+ such that @{thm (no_quants) th_blockedE_pretty}.
\end{lemma}
\begin{proof}
+ We know that @{term th} cannot be in @{term readys}, because it has
+ the highest precedence and therefore must be running. This violates our
+ assumption. So by ?? we have that there must be a @{term "th'"} such that
+ @{term "th' \<in> readys (t @ s)"} and @{term "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+"}.
+ We are going to first show that this @{term "th'"} must be running. For this we
+ need to show that @{term th'} holds the highest @{term cp}-value.
+ By ?? we know that the @{term "cp"}-value of @{term "th'"} must
+ be the highest all precedences of all thread nodes in its @{term tRAG}-subtree.
+ That is
+
+ \begin{center}
+ @{term "cp (t @ s) th' = Max (the_preced (t @ s) `
+ (the_thread ` subtree (tRAG (t @ s)) (Th th')))"}
+ \end{center}
+
+ But since @{term th} is in this subtree the right-hand side is equal
+ to @{term "preced th (t @ s)"}.
+
%Let me distinguish between cp (current precedence) and assigned precedence (the precedence the
%thread ``normally'' has).
%So we want to show what the cp of th' is in state t @ s.
--- a/PIPDefs.thy Thu Jun 02 13:15:03 2016 +0100
+++ b/PIPDefs.thy Tue Jun 07 13:51:39 2016 +0100
@@ -7,10 +7,10 @@
chapter {* Definitions *}
text {*
- In this section, the formal model of Priority Inheritance Protocol (PIP) is presented.
+ In this section, the formal model of Priority Inheritance Protocol (PIP) is presented.
The model is based on Paulson's inductive protocol verification method, where
- the state of the system is modelled as a list of events happened so far with the latest
- event put at the head.
+ the state of the system is modelled as a list of events (trace) happened so far with the
+ latest event put at the head.
*}
text {*
@@ -32,11 +32,11 @@
*}
datatype event =
- Create thread priority | -- {* Thread @{text "thread"} is created with priority @{text "priority"}. *}
- Exit thread | -- {* Thread @{text "thread"} finishing its execution. *}
- P thread cs | -- {* Thread @{text "thread"} requesting critical resource @{text "cs"}. *}
- V thread cs | -- {* Thread @{text "thread"} releasing critical resource @{text "cs"}. *}
- Set thread priority -- {* Thread @{text "thread"} resets its priority to @{text "priority"}. *}
+ Create thread priority -- {* Thread @{text "thread"} is created with priority @{text "priority"}. *}
+| Exit thread -- {* Thread @{text "thread"} finishing its execution. *}
+| P thread cs -- {* Thread @{text "thread"} requesting critical resource @{text "cs"}. *}
+| V thread cs -- {* Thread @{text "thread"} releasing critical resource @{text "cs"}. *}
+| Set thread priority -- {* Thread @{text "thread"} resets its priority to @{text "priority"}. *}
fun actor where
"actor (Exit th) = th" |
@@ -45,6 +45,7 @@
"actor (Set th pty) = th" |
"actor (Create th prio) = th"
+-- {* The actions of a set of threads *}
definition "actions_of ths s = filter (\<lambda> e. actor e \<in> ths) s"
fun isCreate :: "event \<Rightarrow> bool" where
@@ -60,27 +61,23 @@
"isV _ = False"
text {*
- As mentioned earlier, in Paulson's inductive method, the states of system are represented as lists of events,
- which is defined by the following type @{text "state"}:
- *}
+ As mentioned earlier, in Paulson's inductive method, the states of system are represented as lists
+ of events, which is defined by the following type @{text "state"}: *}
+
type_synonym state = "event list"
text {*
-\noindent
- Resource Allocation Graph (RAG for short) is used extensively in our formal analysis.
- The following type @{text "node"} is used to represent nodes in RAG.
- *}
+ Resource Allocation Graphs (RAG for short) are used extensively in our formal analysis.
+ The following type @{text "node"} is used to represent the two types of nodes in RAGs. *}
datatype node =
- Th "thread" | -- {* Node for thread. *}
- Cs "cs" -- {* Node for critical resource. *}
+ Th "thread" -- {* Node for a thread. *}
+| Cs "cs" -- {* Node for a critical resource. *}
text {*
- \noindent
- The following function
- @{text "threads"} is used to calculate the set of live threads (@{text "threads s"})
- in state @{text "s"}.
- *}
+ The function @{text "threads"} is used to calculate the set of live threads (@{text "threads s"})
+ in state @{text "s"}. *}
+
fun threads :: "state \<Rightarrow> thread set"
where
-- {* At the start of the system, the set of threads is empty: *}
@@ -93,28 +90,28 @@
"threads (e#s) = threads s"
text {*
- \noindent
- The function @{text "threads"} defined above is one of
- the so called {\em observation function}s which forms
- the very basis of Paulson's inductive protocol verification method.
- Each observation function {\em observes} one particular aspect (or attribute)
- of the system. For example, the attribute observed by @{text "threads s"}
- is the set of threads living in state @{text "s"}.
- The protocol being modelled
- The decision made the protocol being modelled is based on the {\em observation}s
- returned by {\em observation function}s. Since {\observation function}s forms
- the very basis on which Paulson's inductive method is based, there will be
- a lot of such observation functions introduced in the following. In fact, any function
- which takes event list as argument is a {\em observation function}.
- *}
-text {* \noindent
- Observation @{text "priority th s"} is
- the {\em original priority} of thread @{text "th"} in state @{text "s"}.
- The {\em original priority} is the priority
- assigned to a thread when it is created or when it is reset by system call
- (represented by event @{text "Set thread priority"}).
-*}
+ \noindent The function @{text "threads"} defined above is one of the
+ so called {\em observation function}s which forms the very basis of
+ Paulson's inductive protocol verification method. Each observation
+ function {\em observes} one particular aspect (or attribute) of the
+ system. For example, the attribute observed by @{text "threads s"}
+ is the set of threads living in state @{text "s"}. The protocol
+ being modelled The decision made the protocol being modelled is
+ based on the {\em observation}s returned by {\em observation
+ function}s. Since {\observation function}s forms the very basis on
+ which Paulson's inductive method is based, there will be a lot of
+ such observation functions introduced in the following. In fact, any
+ function which takes event list as argument is a {\em observation
+ function}. *}
+
+text {*
+
+ \noindent Observation @{text "priority th s"} is the {\em original
+ priority} of thread @{text "th"} in state @{text "s"}. The {\em
+ original priority} is the priority assigned to a thread when it is
+ created or when it is reset by system call (represented by event
+ @{text "Set thread priority"}). *}
fun priority :: "thread \<Rightarrow> state \<Rightarrow> priority"
where
@@ -127,11 +124,12 @@
"priority thread (e#s) = priority thread s"
text {*
- \noindent
- Observation @{text "last_set th s"} is the last time when the priority of thread @{text "th"} is set,
- observed from state @{text "s"}.
- The time in the system is measured by the number of events happened so far since the very beginning.
-*}
+
+ \noindent Observation @{text "last_set th s"} is the last time when
+ the priority of thread @{text "th"} is set, observed from state
+ @{text "s"}. The time in the system is measured by the number of
+ events happened so far since the very beginning. *}
+
fun last_set :: "thread \<Rightarrow> state \<Rightarrow> nat"
where
"last_set thread [] = 0" |
@@ -142,28 +140,31 @@
"last_set thread (_#s) = last_set thread s"
text {*
- \noindent
- The {\em precedence} is a notion derived from {\em priority}, where the {\em precedence} of
- a thread is the combination of its {\em original priority} and {\em time} the priority is set.
- The intention is to discriminate threads with the same priority by giving threads whose priority
- is assigned earlier higher precedences, becasue such threads are more urgent to finish.
- This explains the following definition:
- *}
+
+ \noindent The {\em precedence} is a notion derived from {\em
+ priority}, where the {\em precedence} of a thread is the combination
+ of its {\em original priority} and {\em time} the priority is set.
+ The intention is to discriminate threads with the same priority by
+ giving threads whose priority is assigned earlier higher
+ precedences, becasue such threads are more urgent to finish. This
+ explains the following definition: *}
+
definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"
where "preced thread s \<equiv> Prc (priority thread s) (last_set thread s)"
text {*
- \noindent
- A number of important notions in PIP are represented as the following functions,
- defined in terms of the waiting queues of the system, where the waiting queues
- , as a whole, is represented by the @{text "wq"} argument of every notion function.
- The @{text "wq"} argument is itself a functions which maps every critical resource
- @{text "cs"} to the list of threads which are holding or waiting for it.
- The thread at the head of this list is designated as the thread which is current
- holding the resrouce, which is slightly different from tradition where
- all threads in the waiting queue are considered as waiting for the resource.
- *}
+
+ \noindent A number of important notions in PIP are represented as
+ the following functions, defined in terms of the waiting queues of
+ the system, where the waiting queues , as a whole, is represented by
+ the @{text "wq"} argument of every notion function. The @{text
+ "wq"} argument is itself a functions which maps every critical
+ resource @{text "cs"} to the list of threads which are holding or
+ waiting for it. The thread at the head of this list is designated
+ as the thread which is current holding the resrouce, which is
+ slightly different from tradition where all threads in the waiting
+ queue are considered as waiting for the resource. *}
(*
consts
@@ -173,8 +174,7 @@
dependants :: "'b \<Rightarrow> thread \<Rightarrow> thread set"
*)
-definition
- -- {*
+-- {*
\begin{minipage}{0.9\textwidth}
This meaning of @{text "wq"} is reflected in the following definition of
@{text "holding wq th cs"}, where @{text "holding wq th cs"} means thread
@@ -183,6 +183,7 @@
\end{minipage}
*}
+definition
cs_holding_raw:
"holding_raw wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread = hd (wq cs))"
--- a/RTree.thy Thu Jun 02 13:15:03 2016 +0100
+++ b/RTree.thy Tue Jun 07 13:51:39 2016 +0100
@@ -45,40 +45,42 @@
definition "pred_of r = (\<lambda> x y. (x, y) \<in> r)"
text {*
- To reason about {\em Relational Graph}, a notion of path is
- needed, which is given by the following @{text "rpath"} (short
- for `relational path`).
- The path @{text "xs"} in proposition @{text "rpath r x xs y"} is
- a path leading from @{text "x"} to @{text "y"}, which serves as a
- witness of the fact @{text "(x, y) \<in> r^*"}.
- @{text "rpath"}
- is simply a wrapper of the @{text "rtrancl_path"} defined in the imported
- theory @{text "Transitive_Closure_Table"}, which defines
- a notion of path for the predicate form of binary relations.
-*}
+ To reason about {\em Relational Graph}, a notion of path is needed,
+ which is given by the following @{text "rpath"} (short for
+ `relational path`). The path @{text "xs"} in proposition @{text
+ "rpath r x xs y"} is a path leading from @{text "x"} to @{text "y"},
+ which serves as a witness of the fact @{text "(x, y) \<in> r^*"}.
+
+ @{text "rpath"} is simply a wrapper of the @{text "rtrancl_path"}
+ defined in the imported theory @{text "Transitive_Closure_Table"},
+ which defines a notion of path for the predicate form of binary
+ relations. *}
+
definition "rpath r x xs y = rtrancl_path (pred_of r) x xs y"
text {*
- Given a path @{text "ps"}, @{text "edges_on ps"} is the
- set of edges along the path, which is defined as follows:
-*}
+
+ Given a path @{text "ps"}, @{text "edges_on ps"} is the set of edges
+ along the path, which is defined as follows: *}
definition "edges_on ps = {(a,b) | a b. \<exists> xs ys. ps = xs@[a,b]@ys}"
text {*
- The following @{text "indep"} defines a notion of independence.
+
+ The following @{text "indep"} defines a notion of independence.
Two nodes @{text "x"} and @{text "y"} are said to be independent
- (expressed as @{text "indep x y"}), if neither one is reachable
- from the other in relational graph @{text "r"}.
-*}
+ (expressed as @{text "indep x y"}), if neither one is reachable
+ from the other in relational graph @{text "r"}. *}
+
definition "indep r x y = (((x, y) \<notin> r^*) \<and> ((y, x) \<notin> r^*))"
text {*
- In relational tree @{text "r"}, the sub tree of node @{text "x"} is written
- @{text "subtree r x"}, which is defined to be the set of nodes (including itself)
- which can reach @{text "x"} by following some path in @{text "r"}:
-*}
+
+ In relational tree @{text "r"}, the sub tree of node @{text "x"} is
+ written @{text "subtree r x"}, which is defined to be the set of
+ nodes (including itself) which can reach @{text "x"} by following
+ some path in @{text "r"}: *}
definition "subtree r x = {y . (y, x) \<in> r^*}"
@@ -87,17 +89,20 @@
definition "root r x = (ancestors r x = {})"
text {*
- The following @{text "edge_in r x"} is the set of edges
- contained in the sub-tree of @{text "x"}, with @{text "r"} as the underlying graph.
-*}
+
+ The following @{text "edge_in r x"} is the set of edges contained in
+ the sub-tree of @{text "x"}, with @{text "r"} as the underlying
+ graph. *}
definition "edges_in r x = {(a, b) | a b. (a, b) \<in> r \<and> b \<in> subtree r x}"
text {*
- The following lemma @{text "edges_in_meaning"} shows the intuitive meaning
- of `an edge @{text "(a, b)"} is in the sub-tree of @{text "x"}`,
- i.e., both @{text "a"} and @{text "b"} are in the sub-tree.
-*}
+
+ The following lemma @{text "edges_in_meaning"} shows the intuitive
+ meaning of `an edge @{text "(a, b)"} is in the sub-tree of @{text
+ "x"}`, i.e., both @{text "a"} and @{text "b"} are in the sub-tree.
+ *}
+
lemma edges_in_meaning:
"edges_in r x = {(a, b) | a b. (a, b) \<in> r \<and> a \<in> subtree r x \<and> b \<in> subtree r x}"
by (auto simp:edges_in_def subtree_def)
@@ -1735,12 +1740,6 @@
with h_b(2) and that show ?thesis by metis
qed
-(*
-lcrules crules
-
-declare crules(26,43,44,45,46,47)[rule del]
-*)
-
declare RTree.subtree_transfer[rule del]
Binary file journal.pdf has changed