# HG changeset patch # User Christian Urban # Date 1465303899 -3600 # Node ID a88af0e4731ffd796ee3c84b51da1ea012036ce0 # Parent 95e7933968f8cfff3bb29e6aee6b0bfae4185afc minor update diff -r 95e7933968f8 -r a88af0e4731f Correctness.thy --- 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 \ runing (t@s)" + assumes "th \ runing (t @ s)" obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" - "th' \ runing (t@s)" + "th' \ 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 \ readys (t @ s) \ (\th'. th' \ readys (t @ s) \ (Th th, Th th') \ (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 \ readys (t @ s)" + using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto + then have "\th'. th' \ readys (t @ s) \ (Th th, Th th') \ (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 \ 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' \ readys (t@s)" - and dp: "(Th th, Th th') \ (RAG (t @ s))\<^sup>+" by auto - -- {* We are going to show that this @{term th'} is running. *} - have "th' \ runing (t@s)" + then obtain th' where th'_in: "th' \ readys (t@s)" + and dp: "(Th th, Th th') \ (RAG (t @ s))\<^sup>+" by auto + + -- {* We are going to first show that this @{term th'} is running. *} + have "th' \ 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') \ 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' \ readys (t@s)` show ?thesis by (simp add: runing_def) + with `th' \ readys (t @ s)` show "th' \ 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' \ ancestors (RAG (t @ s)) (Th th)" using `(Th th, Th th') \ (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def) ultimately show ?thesis using that by metis qed +lemma th_blockedE_pretty: + assumes "th \ runing (t@s)" + shows "\th'. Th th' \ ancestors (RAG (t @ s)) (Th th) \ th' \ 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 diff -r 95e7933968f8 -r a88af0e4731f Journal/Paper.thy --- 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' \ readys (t @ s)"} and @{term "(Th th, Th th') \ (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. diff -r 95e7933968f8 -r a88af0e4731f PIPDefs.thy --- 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 (\ e. actor e \ ths) s" fun isCreate :: "event \ 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 \ 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 \ state \ 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 \ state \ 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 \ state \ precedence" where "preced thread s \ 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 \ thread \ 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 \ (thread \ set (wq cs) \ thread = hd (wq cs))" diff -r 95e7933968f8 -r a88af0e4731f RTree.thy --- 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 = (\ x y. (x, y) \ 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) \ 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) \ 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. \ 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) \ r^*) \ ((y, x) \ 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) \ 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) \ r \ b \ 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) \ r \ a \ subtree r x \ b \ 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] diff -r 95e7933968f8 -r a88af0e4731f journal.pdf Binary file journal.pdf has changed