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))"