262
+ − 1 %
+ − 2 \begin{isabellebody}%
+ − 3 \def\isabellecontext{PrioGDef}%
+ − 4 %
+ − 5 \isadelimtheory
+ − 6 %
+ − 7 \endisadelimtheory
+ − 8 %
+ − 9 \isatagtheory
+ − 10 %
+ − 11 \endisatagtheory
+ − 12 {\isafoldtheory}%
+ − 13 %
+ − 14 \isadelimtheory
+ − 15 %
+ − 16 \endisadelimtheory
+ − 17 %
+ − 18 \begin{isamarkuptext}%
+ − 19 In this section, the formal model of Priority Inheritance is presented. First, the identifiers of {\em threads},
+ − 20 {\em priority} and {\em critical resources } (abbreviated as \isa{cs}) are all represented as natural numbers,
+ − 21 i.e. standard Isabelle/HOL type \isa{nat}.%
+ − 22 \end{isamarkuptext}%
+ − 23 \isamarkuptrue%
+ − 24 \isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
+ − 25 \ thread\ {\isaliteral{3D}{\isacharequal}}\ nat\ %
+ − 26 \isamarkupcmt{Type for thread identifiers.%
+ − 27 }
+ − 28 \isanewline
+ − 29 \isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
+ − 30 \ priority\ {\isaliteral{3D}{\isacharequal}}\ nat\ \ %
+ − 31 \isamarkupcmt{Type for priorities.%
+ − 32 }
+ − 33 \isanewline
+ − 34 \isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
+ − 35 \ cs\ {\isaliteral{3D}{\isacharequal}}\ nat\ %
+ − 36 \isamarkupcmt{Type for critical sections (or critical resources).%
+ − 37 }
+ − 38 %
+ − 39 \begin{isamarkuptext}%
+ − 40 Priority Inheritance protocol is modeled as an event driven system, where every event represents an
+ − 41 system call. Event format is given by the following type definition:%
+ − 42 \end{isamarkuptext}%
+ − 43 \isamarkuptrue%
+ − 44 \isacommand{datatype}\isamarkupfalse%
+ − 45 \ event\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
+ − 46 \ \ Create\ thread\ priority\ {\isaliteral{7C}{\isacharbar}}\ %
+ − 47 \isamarkupcmt{Thread \isa{thread} is created with priority \isa{priority}.%
+ − 48 }
+ − 49 \isanewline
+ − 50 \ \ Exit\ thread\ {\isaliteral{7C}{\isacharbar}}\ %
+ − 51 \isamarkupcmt{Thread \isa{thread} finishing its execution.%
+ − 52 }
+ − 53 \isanewline
+ − 54 \ \ P\ thread\ cs\ {\isaliteral{7C}{\isacharbar}}\ %
+ − 55 \isamarkupcmt{Thread \isa{thread} requesting critical resource \isa{cs}.%
+ − 56 }
+ − 57 \isanewline
+ − 58 \ \ V\ thread\ cs\ {\isaliteral{7C}{\isacharbar}}\ %
+ − 59 \isamarkupcmt{Thread \isa{thread} releasing critical resource \isa{cs}.%
+ − 60 }
+ − 61 \isanewline
+ − 62 \ \ Set\ thread\ priority\ %
+ − 63 \isamarkupcmt{Thread \isa{thread} resets its priority to \isa{priority}.%
+ − 64 }
+ − 65 %
+ − 66 \begin{isamarkuptext}%
+ − 67 Resource Allocation Graph (RAG for short) is used extensively in the analysis of Priority Inheritance.
+ − 68 The following type \isa{node} is used to model nodes in RAG.%
+ − 69 \end{isamarkuptext}%
+ − 70 \isamarkuptrue%
+ − 71 \isacommand{datatype}\isamarkupfalse%
+ − 72 \ node\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
+ − 73 \ \ \ Th\ {\isaliteral{22}{\isachardoublequoteopen}}thread{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ %
+ − 74 \isamarkupcmt{Node for thread.%
+ − 75 }
+ − 76 \isanewline
+ − 77 \ \ \ Cs\ {\isaliteral{22}{\isachardoublequoteopen}}cs{\isaliteral{22}{\isachardoublequoteclose}}\ %
+ − 78 \isamarkupcmt{Node for critical resource.%
+ − 79 }
+ − 80 %
+ − 81 \begin{isamarkuptext}%
+ − 82 The protocol is analyzed using Paulson's inductive protocol verification method, where
+ − 83 the state of the system is modelled as the list of events happened so far with the latest
+ − 84 event at the head. Therefore, the state of the system is represented by the following
+ − 85 type \isa{state}.%
+ − 86 \end{isamarkuptext}%
+ − 87 \isamarkuptrue%
+ − 88 \isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
+ − 89 \ state\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}event\ list{\isaliteral{22}{\isachardoublequoteclose}}%
+ − 90 \begin{isamarkuptext}%
+ − 91 The following \isa{threads} is used to calculate the set of live threads (\isa{threads\ s})
+ − 92 in state \isa{s}.%
+ − 93 \end{isamarkuptext}%
+ − 94 \isamarkuptrue%
+ − 95 \isacommand{fun}\isamarkupfalse%
+ − 96 \ threads\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 97 \isakeyword{where}\ \isanewline
+ − 98 \ \ {\isaliteral{22}{\isachardoublequoteopen}}threads\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ %
+ − 99 \isamarkupcmt{At the start of the system, the set of threads is empty.%
+ − 100 }
+ − 101 \isanewline
+ − 102 \ \ {\isaliteral{22}{\isachardoublequoteopen}}threads\ {\isaliteral{28}{\isacharparenleft}}Create\ thread\ prio{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}thread{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ threads\ s{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ %
+ − 103 \isamarkupcmt{New thread is added to the \isa{threads}.%
+ − 104 }
+ − 105 \isanewline
+ − 106 \ \ {\isaliteral{22}{\isachardoublequoteopen}}threads\ {\isaliteral{28}{\isacharparenleft}}Exit\ thread\ {\isaliteral{23}{\isacharhash}}\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}threads\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{7B}{\isacharbraceleft}}thread{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ %
+ − 107 \isamarkupcmt{Finished thread is removed.%
+ − 108 }
+ − 109 \isanewline
+ − 110 \ \ {\isaliteral{22}{\isachardoublequoteopen}}threads\ {\isaliteral{28}{\isacharparenleft}}e{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ threads\ s{\isaliteral{22}{\isachardoublequoteclose}}\ %
+ − 111 \isamarkupcmt{other kind of events does not affect the value of \isa{threads}.%
+ − 112 }
+ − 113 %
+ − 114 \begin{isamarkuptext}%
+ − 115 Functions such as \isa{threads}, which extract information out of system states, are called
+ − 116 {\em observing functions}. A series of observing functions will be defined in the sequel in order to
+ − 117 model the protocol.
+ − 118 Observing function \isa{original{\isaliteral{5F}{\isacharunderscore}}priority} calculates
+ − 119 the {\em original priority} of thread \isa{th} in state \isa{s}, expressed as
+ − 120 : \isa{original{\isaliteral{5F}{\isacharunderscore}}priority\ th\ s}. The {\em original priority} is the priority
+ − 121 assigned to a thread when it is created or when it is reset by system call \isa{Set\ thread\ priority}.%
+ − 122 \end{isamarkuptext}%
+ − 123 \isamarkuptrue%
+ − 124 \isacommand{fun}\isamarkupfalse%
+ − 125 \ original{\isaliteral{5F}{\isacharunderscore}}priority\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ priority{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 126 \isakeyword{where}\isanewline
+ − 127 \ \ {\isaliteral{22}{\isachardoublequoteopen}}original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ %
+ − 128 \isamarkupcmt{\isa{{\isadigit{0}}} is assigned to threads which have never been created.%
+ − 129 }
+ − 130 \isanewline
+ − 131 \ \ {\isaliteral{22}{\isachardoublequoteopen}}original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ {\isaliteral{28}{\isacharparenleft}}Create\ thread{\isaliteral{27}{\isacharprime}}\ prio{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
+ − 132 \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ thread{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ thread\ then\ prio\ else\ original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+ − 133 \ \ {\isaliteral{22}{\isachardoublequoteopen}}original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ {\isaliteral{28}{\isacharparenleft}}Set\ thread{\isaliteral{27}{\isacharprime}}\ prio{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
+ − 134 \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ thread{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ thread\ then\ prio\ else\ original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+ − 135 \ \ {\isaliteral{22}{\isachardoublequoteopen}}original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ {\isaliteral{28}{\isacharparenleft}}e{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ s{\isaliteral{22}{\isachardoublequoteclose}}%
+ − 136 \begin{isamarkuptext}%
+ − 137 \isa{birthtime\ th\ s} is the time when thread \isa{th} is created, observed from state \isa{s}.
+ − 138 The time in the system is measured by the number of events happened so far since the very beginning.%
+ − 139 \end{isamarkuptext}%
+ − 140 \isamarkuptrue%
+ − 141 \isacommand{fun}\isamarkupfalse%
+ − 142 \ birthtime\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 143 \isakeyword{where}\isanewline
+ − 144 \ \ {\isaliteral{22}{\isachardoublequoteopen}}birthtime\ thread\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+ − 145 \ \ {\isaliteral{22}{\isachardoublequoteopen}}birthtime\ thread\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Create\ thread{\isaliteral{27}{\isacharprime}}\ prio{\isaliteral{29}{\isacharparenright}}{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}thread\ {\isaliteral{3D}{\isacharequal}}\ thread{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ then\ length\ s\ \isanewline
+ − 146 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ birthtime\ thread\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+ − 147 \ \ {\isaliteral{22}{\isachardoublequoteopen}}birthtime\ thread\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Set\ thread{\isaliteral{27}{\isacharprime}}\ prio{\isaliteral{29}{\isacharparenright}}{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}thread\ {\isaliteral{3D}{\isacharequal}}\ thread{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ then\ length\ s\ \isanewline
+ − 148 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ birthtime\ thread\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+ − 149 \ \ {\isaliteral{22}{\isachardoublequoteopen}}birthtime\ thread\ {\isaliteral{28}{\isacharparenleft}}e{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ birthtime\ thread\ s{\isaliteral{22}{\isachardoublequoteclose}}%
+ − 150 \begin{isamarkuptext}%
+ − 151 The {\em precedence} is a notion derived from {\em priority}, where the {\em precedence} of
+ − 152 a thread is the combination of its {\em original priority} and {\em birth time}. The intention is
+ − 153 to discriminate threads with the same priority by giving threads with the earlier assigned priority
+ − 154 higher precedence in scheduling. This explains the following definition:%
+ − 155 \end{isamarkuptext}%
+ − 156 \isamarkuptrue%
+ − 157 \isacommand{definition}\isamarkupfalse%
+ − 158 \ preced\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ precedence{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 159 \ \ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}preced\ thread\ s\ {\isaliteral{3D}{\isacharequal}}\ Prc\ {\isaliteral{28}{\isacharparenleft}}original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}birthtime\ thread\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+ − 160 \begin{isamarkuptext}%
+ − 161 A number of important notions are defined here:%
+ − 162 \end{isamarkuptext}%
+ − 163 \isamarkuptrue%
+ − 164 \isacommand{consts}\isamarkupfalse%
+ − 165 \ \isanewline
+ − 166 \ \ holding\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isanewline
+ − 167 \ \ \ \ \ \ \ waiting\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 168 \ \ \ \ \ \ \ depend\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}node\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ node{\isaliteral{29}{\isacharparenright}}\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 169 \ \ \ \ \ \ \ dependents\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ set{\isaliteral{22}{\isachardoublequoteclose}}%
+ − 170 \begin{isamarkuptext}%
+ − 171 The definition of the following several functions, it is supposed that
+ − 172 the waiting queue of every critical resource is given by a waiting queue
+ − 173 function \isa{wq}, which servers as arguments of these functions.%
+ − 174 \end{isamarkuptext}%
+ − 175 \isamarkuptrue%
+ − 176 \isacommand{defs}\isamarkupfalse%
+ − 177 \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{overloaded}{\isaliteral{29}{\isacharparenright}}\ \isanewline
+ − 178 \ \ %
+ − 179 \isamarkupcmt{\begin{minipage}{0.8\textwidth}
+ − 180 We define that the thread which is at the head of waiting queue of resource \isa{cs}
+ − 181 is holding the resource. This definition is slightly different from tradition where
+ − 182 all threads in the waiting queue are considered as waiting for the resource.
+ − 183 This notion is reflected in the definition of \isa{holding\ wq\ th\ cs} as follows:
+ − 184 \end{minipage}%
+ − 185 }
+ − 186 \isanewline
+ − 187 \ \ cs{\isaliteral{5F}{\isacharunderscore}}holding{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}holding\ wq\ thread\ cs\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ {\isaliteral{28}{\isacharparenleft}}wq\ cs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ thread\ {\isaliteral{3D}{\isacharequal}}\ hd\ {\isaliteral{28}{\isacharparenleft}}wq\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 188 \ \ %
+ − 189 \isamarkupcmt{\begin{minipage}{0.8\textwidth}
+ − 190 In accordance with the definition of \isa{holding\ wq\ th\ cs},
+ − 191 a thread \isa{th} is considered waiting for \isa{cs} if
+ − 192 it is in the {\em waiting queue} of critical resource \isa{cs}, but not at the head.
+ − 193 This is reflected in the definition of \isa{waiting\ wq\ th\ cs} as follows:
+ − 194 \end{minipage}%
+ − 195 }
+ − 196 \isanewline
+ − 197 \ \ cs{\isaliteral{5F}{\isacharunderscore}}waiting{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}waiting\ wq\ thread\ cs\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ {\isaliteral{28}{\isacharparenleft}}wq\ cs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ thread\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ hd\ {\isaliteral{28}{\isacharparenleft}}wq\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 198 \ \ %
+ − 199 \isamarkupcmt{\begin{minipage}{0.8\textwidth}
+ − 200 \isa{depend\ wq} represents the Resource Allocation Graph of the system under the waiting
+ − 201 queue function \isa{wq}.
+ − 202 \end{minipage}%
+ − 203 }
+ − 204 \isanewline
+ − 205 \ \ cs{\isaliteral{5F}{\isacharunderscore}}depend{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}depend\ {\isaliteral{28}{\isacharparenleft}}wq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ list{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}Th\ t{\isaliteral{2C}{\isacharcomma}}\ Cs\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ t\ c{\isaliteral{2E}{\isachardot}}\ waiting\ wq\ t\ c{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ \isanewline
+ − 206 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}Cs\ c{\isaliteral{2C}{\isacharcomma}}\ Th\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ c\ t{\isaliteral{2E}{\isachardot}}\ holding\ wq\ t\ c{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 207 \ \ %
+ − 208 \isamarkupcmt{\begin{minipage}{0.8\textwidth}
+ − 209 \isa{dependents\ wq\ th} represents the set of threads which are depending on
+ − 210 thread \isa{th} in Resource Allocation Graph \isa{depend\ wq}:
+ − 211 \end{minipage}%
+ − 212 }
+ − 213 \isanewline
+ − 214 \ \ cs{\isaliteral{5F}{\isacharunderscore}}dependents{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}dependents\ {\isaliteral{28}{\isacharparenleft}}wq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ list{\isaliteral{29}{\isacharparenright}}\ th\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}th{\isaliteral{27}{\isacharprime}}\ {\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}Th\ th{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ Th\ th{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{28}{\isacharparenleft}}depend\ wq{\isaliteral{29}{\isacharparenright}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+ − 215 \begin{isamarkuptext}%
+ − 216 The data structure used by the operating system for scheduling is referred to as
+ − 217 {\em schedule state}. It is represented as a record consisting of
+ − 218 a function assigning waiting queue to resources and a function assigning precedence to
+ − 219 threads:%
+ − 220 \end{isamarkuptext}%
+ − 221 \isamarkuptrue%
+ − 222 \isacommand{record}\isamarkupfalse%
+ − 223 \ schedule{\isaliteral{5F}{\isacharunderscore}}state\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
+ − 224 \ \ \ \ waiting{\isaliteral{5F}{\isacharunderscore}}queue\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ list{\isaliteral{22}{\isachardoublequoteclose}}\ %
+ − 225 \isamarkupcmt{The function assigning waiting queue.%
+ − 226 }
+ − 227 \isanewline
+ − 228 \ \ \ \ cur{\isaliteral{5F}{\isacharunderscore}}preced\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ precedence{\isaliteral{22}{\isachardoublequoteclose}}\ %
+ − 229 \isamarkupcmt{The function assigning precedence.%
+ − 230 }
+ − 231 %
+ − 232 \begin{isamarkuptext}%
+ − 233 \isa{cpreced\ s\ th} gives the {\em current precedence} of thread \isa{th} under
+ − 234 state \isa{s}. The definition of \isa{cpreced} reflects the basic idea of
+ − 235 Priority Inheritance that the {\em current precedence} of a thread is the precedence
+ − 236 inherited from the maximum of all its dependents, i.e. the threads which are waiting
+ − 237 directly or indirectly waiting for some resources from it. If no such thread exits,
+ − 238 \isa{th}'s {\em current precedence} equals its original precedence, i.e.
+ − 239 \isa{preced\ th\ s}.%
+ − 240 \end{isamarkuptext}%
+ − 241 \isamarkuptrue%
+ − 242 \isacommand{definition}\isamarkupfalse%
+ − 243 \ cpreced\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ list{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ precedence{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 244 \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}cpreced\ s\ wq\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\ th{\isaliteral{2E}{\isachardot}}\ Max\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\ th{\isaliteral{2E}{\isachardot}}\ preced\ th\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{7B}{\isacharbraceleft}}th{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ dependents\ wq\ th{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+ − 245 \begin{isamarkuptext}%
+ − 246 The following function \isa{schs} is used to calculate the schedule state \isa{schs\ s}.
+ − 247 It is the key function to model Priority Inheritance:%
+ − 248 \end{isamarkuptext}%
+ − 249 \isamarkuptrue%
+ − 250 \isacommand{fun}\isamarkupfalse%
+ − 251 \ schs\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ schedule{\isaliteral{5F}{\isacharunderscore}}state{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 252 \isakeyword{where}\isanewline
+ − 253 \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}schs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}waiting{\isaliteral{5F}{\isacharunderscore}}queue\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\ cs{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
+ − 254 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ cur{\isaliteral{5F}{\isacharunderscore}}preced\ {\isaliteral{3D}{\isacharequal}}\ cpreced\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\ cs{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+ − 255 \ \ %
+ − 256 \isamarkupcmt{\begin{minipage}{0.8\textwidth}
+ − 257 \begin{enumerate}
+ − 258 \item \isa{ps} is the schedule state of last moment.
+ − 259 \item \isa{pwq} is the waiting queue function of last moment.
+ − 260 \item \isa{pcp} is the precedence function of last moment.
+ − 261 \item \isa{nwq} is the new waiting queue function. It is calculated using a \isa{case} statement:
+ − 262 \begin{enumerate}
+ − 263 \item If the happening event is \isa{P\ thread\ cs}, \isa{thread} is added to
+ − 264 the end of \isa{cs}'s waiting queue.
+ − 265 \item If the happening event is \isa{V\ thread\ cs} and \isa{s} is a legal state,
+ − 266 \isa{th{\isaliteral{27}{\isacharprime}}} must equal to \isa{thread},
+ − 267 because \isa{thread} is the one currently holding \isa{cs}.
+ − 268 The case \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} may never be executed in a legal state.
+ − 269 the \isa{{\isaliteral{28}{\isacharparenleft}}SOME\ q{\isaliteral{2E}{\isachardot}}\ distinct\ q\ {\isaliteral{5C3C616E643E}{\isasymand}}\ set\ q\ {\isaliteral{3D}{\isacharequal}}\ set\ qs{\isaliteral{29}{\isacharparenright}}} is used to choose arbitrarily one
+ − 270 thread in waiting to take over the released resource \isa{cs}. In our representation,
+ − 271 this amounts to rearrange elements in waiting queue, so that one of them is put at the head.
+ − 272 \item For other happening event, the schedule state just does not change.
+ − 273 \end{enumerate}
+ − 274 \item \isa{ncp} is new precedence function, it is calculated from the newly updated waiting queue
+ − 275 function. The dependency of precedence function on waiting queue function is the reason to
+ − 276 put them in the same record so that they can evolve together.
+ − 277 \end{enumerate}
+ − 278 \end{minipage}%
+ − 279 }
+ − 280 \isanewline
+ − 281 \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}schs\ {\isaliteral{28}{\isacharparenleft}}e{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}let\ ps\ {\isaliteral{3D}{\isacharequal}}\ schs\ s\ in\ \isanewline
+ − 282 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ let\ pwq\ {\isaliteral{3D}{\isacharequal}}\ waiting{\isaliteral{5F}{\isacharunderscore}}queue\ ps\ in\ \isanewline
+ − 283 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ let\ pcp\ {\isaliteral{3D}{\isacharequal}}\ cur{\isaliteral{5F}{\isacharunderscore}}preced\ ps\ in\isanewline
+ − 284 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ let\ nwq\ {\isaliteral{3D}{\isacharequal}}\ case\ e\ of\isanewline
+ − 285 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ P\ thread\ cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ \ pwq{\isaliteral{28}{\isacharparenleft}}cs{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{28}{\isacharparenleft}}pwq\ cs\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{5B}{\isacharbrackleft}}thread{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+ − 286 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ V\ thread\ cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ let\ nq\ {\isaliteral{3D}{\isacharequal}}\ case\ {\isaliteral{28}{\isacharparenleft}}pwq\ cs{\isaliteral{29}{\isacharparenright}}\ of\isanewline
+ − 287 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7C}{\isacharbar}}\ \isanewline
+ − 288 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}th{\isaliteral{27}{\isacharprime}}{\isaliteral{23}{\isacharhash}}qs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}SOME\ q{\isaliteral{2E}{\isachardot}}\ distinct\ q\ {\isaliteral{5C3C616E643E}{\isasymand}}\ set\ q\ {\isaliteral{3D}{\isacharequal}}\ set\ qs{\isaliteral{29}{\isacharparenright}}\isanewline
+ − 289 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ in\ pwq{\isaliteral{28}{\isacharparenleft}}cs{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}nq{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\isanewline
+ − 290 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ pwq\isanewline
+ − 291 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ in\ let\ ncp\ {\isaliteral{3D}{\isacharequal}}\ cpreced\ {\isaliteral{28}{\isacharparenleft}}e{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ nwq\ in\ \isanewline
+ − 292 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}waiting{\isaliteral{5F}{\isacharunderscore}}queue\ {\isaliteral{3D}{\isacharequal}}\ nwq{\isaliteral{2C}{\isacharcomma}}\ cur{\isaliteral{5F}{\isacharunderscore}}preced\ {\isaliteral{3D}{\isacharequal}}\ ncp{\isaliteral{5C3C72706172723E}{\isasymrparr}}\isanewline
+ − 293 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+ − 294 \begin{isamarkuptext}%
+ − 295 \isa{wq} is a shorthand for \isa{waiting{\isaliteral{5F}{\isacharunderscore}}queue}.%
+ − 296 \end{isamarkuptext}%
+ − 297 \isamarkuptrue%
+ − 298 \isacommand{definition}\isamarkupfalse%
+ − 299 \ wq\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isanewline
+ − 300 \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}wq\ s\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ waiting{\isaliteral{5F}{\isacharunderscore}}queue\ {\isaliteral{28}{\isacharparenleft}}schs\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+ − 301 \begin{isamarkuptext}%
+ − 302 \isa{cp} is a shorthand for \isa{cur{\isaliteral{5F}{\isacharunderscore}}preced}.%
+ − 303 \end{isamarkuptext}%
+ − 304 \isamarkuptrue%
+ − 305 \isacommand{definition}\isamarkupfalse%
+ − 306 \ cp\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ precedence{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 307 \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}cp\ s\ {\isaliteral{3D}{\isacharequal}}\ cur{\isaliteral{5F}{\isacharunderscore}}preced\ {\isaliteral{28}{\isacharparenleft}}schs\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+ − 308 \begin{isamarkuptext}%
+ − 309 Functions \isa{holding}, \isa{waiting}, \isa{depend} and \isa{dependents} still have the
+ − 310 same meaning, but redefined so that they no longer depend on the fictitious {\em waiting queue function}
+ − 311 \isa{wq}, but on system state \isa{s}.%
+ − 312 \end{isamarkuptext}%
+ − 313 \isamarkuptrue%
+ − 314 \isacommand{defs}\isamarkupfalse%
+ − 315 \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{overloaded}{\isaliteral{29}{\isacharparenright}}\ \isanewline
+ − 316 \ \ s{\isaliteral{5F}{\isacharunderscore}}holding{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}holding\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}state{\isaliteral{29}{\isacharparenright}}\ thread\ cs\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ {\isaliteral{28}{\isacharparenleft}}wq\ s\ cs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ thread\ {\isaliteral{3D}{\isacharequal}}\ hd\ {\isaliteral{28}{\isacharparenleft}}wq\ s\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 317 \ \ s{\isaliteral{5F}{\isacharunderscore}}waiting{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}waiting\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}state{\isaliteral{29}{\isacharparenright}}\ thread\ cs\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ {\isaliteral{28}{\isacharparenleft}}wq\ s\ cs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ thread\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ hd\ {\isaliteral{28}{\isacharparenleft}}wq\ s\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 318 \ \ s{\isaliteral{5F}{\isacharunderscore}}depend{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}depend\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}Th\ t{\isaliteral{2C}{\isacharcomma}}\ Cs\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ t\ c{\isaliteral{2E}{\isachardot}}\ waiting\ {\isaliteral{28}{\isacharparenleft}}wq\ s{\isaliteral{29}{\isacharparenright}}\ t\ c{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ \isanewline
+ − 319 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}Cs\ c{\isaliteral{2C}{\isacharcomma}}\ Th\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ c\ t{\isaliteral{2E}{\isachardot}}\ holding\ {\isaliteral{28}{\isacharparenleft}}wq\ s{\isaliteral{29}{\isacharparenright}}\ t\ c{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 320 \ \ s{\isaliteral{5F}{\isacharunderscore}}dependents{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}dependents\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}state{\isaliteral{29}{\isacharparenright}}\ th\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}th{\isaliteral{27}{\isacharprime}}\ {\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}Th\ th{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ Th\ th{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{28}{\isacharparenleft}}depend\ {\isaliteral{28}{\isacharparenleft}}wq\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+ − 321 \begin{isamarkuptext}%
+ − 322 The following function \isa{readys} calculates the set of ready threads. A thread is {\em ready}
+ − 323 for running if it is a live thread and it is not waiting for any critical resource.%
+ − 324 \end{isamarkuptext}%
+ − 325 \isamarkuptrue%
+ − 326 \isacommand{definition}\isamarkupfalse%
+ − 327 \ readys\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 328 \isakeyword{where}\isanewline
+ − 329 \ \ {\isaliteral{22}{\isachardoublequoteopen}}readys\ s\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
+ − 330 \ \ \ \ \ {\isaliteral{7B}{\isacharbraceleft}}thread\ {\isaliteral{2E}{\isachardot}}\ thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ threads\ s\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}\ cs{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ waiting\ s\ thread\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+ − 331 \begin{isamarkuptext}%
+ − 332 The following function \isa{runing} calculates the set of running thread, which is the ready
+ − 333 thread with the highest precedence.%
+ − 334 \end{isamarkuptext}%
+ − 335 \isamarkuptrue%
+ − 336 \isacommand{definition}\isamarkupfalse%
+ − 337 \ runing\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 338 \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}runing\ s\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}th\ {\isaliteral{2E}{\isachardot}}\ th\ {\isaliteral{5C3C696E3E}{\isasymin}}\ readys\ s\ {\isaliteral{5C3C616E643E}{\isasymand}}\ cp\ s\ th\ {\isaliteral{3D}{\isacharequal}}\ Max\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}cp\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{28}{\isacharparenleft}}readys\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+ − 339 \begin{isamarkuptext}%
+ − 340 The following function \isa{holdents\ s\ th} returns the set of resources held by thread
+ − 341 \isa{th} in state \isa{s}.%
+ − 342 \end{isamarkuptext}%
+ − 343 \isamarkuptrue%
+ − 344 \isacommand{definition}\isamarkupfalse%
+ − 345 \ holdents\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ cs\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 346 \ \ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}holdents\ s\ th\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}cs\ {\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}Cs\ cs{\isaliteral{2C}{\isacharcomma}}\ Th\ th{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ depend\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+ − 347 \begin{isamarkuptext}%
+ − 348 \isa{cntCS\ s\ th} returns the number of resources held by thread \isa{th} in
+ − 349 state \isa{s}:%
+ − 350 \end{isamarkuptext}%
+ − 351 \isamarkuptrue%
+ − 352 \isacommand{definition}\isamarkupfalse%
+ − 353 \ cntCS\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 354 \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}cntCS\ s\ th\ {\isaliteral{3D}{\isacharequal}}\ card\ {\isaliteral{28}{\isacharparenleft}}holdents\ s\ th{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+ − 355 \begin{isamarkuptext}%
+ − 356 The fact that event \isa{e} is eligible to happen next in state \isa{s}
+ − 357 is expressed as \isa{step\ s\ e}. The predicate \isa{step} is inductively defined as
+ − 358 follows:%
+ − 359 \end{isamarkuptext}%
+ − 360 \isamarkuptrue%
+ − 361 \isacommand{inductive}\isamarkupfalse%
+ − 362 \ step\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ event\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 363 \isakeyword{where}\isanewline
+ − 364 \ \ %
+ − 365 \isamarkupcmt{A thread can be created if it is not a live thread:%
+ − 366 }
+ − 367 \isanewline
+ − 368 \ \ thread{\isaliteral{5F}{\isacharunderscore}}create{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}thread\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ threads\ s{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ step\ s\ {\isaliteral{28}{\isacharparenleft}}Create\ thread\ prio{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+ − 369 \ \ %
+ − 370 \isamarkupcmt{A thread can exit if it no longer hold any resource:%
+ − 371 }
+ − 372 \isanewline
+ − 373 \ \ thread{\isaliteral{5F}{\isacharunderscore}}exit{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ runing\ s{\isaliteral{3B}{\isacharsemicolon}}\ holdents\ s\ thread\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ step\ s\ {\isaliteral{28}{\isacharparenleft}}Exit\ thread{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+ − 374 \ \ %
+ − 375 \isamarkupcmt{A thread can request for an critical resource \isa{cs}, if it is running and
+ − 376 the request does not form a loop in the current RAG. The latter condition
+ − 377 is set up to avoid deadlock. The condition also reflects our assumption all threads are
+ − 378 carefully programmed so that deadlock can not happen.%
+ − 379 }
+ − 380 \isanewline
+ − 381 \ \ thread{\isaliteral{5F}{\isacharunderscore}}P{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ runing\ s{\isaliteral{3B}{\isacharsemicolon}}\ \ {\isaliteral{28}{\isacharparenleft}}Cs\ cs{\isaliteral{2C}{\isacharcomma}}\ Th\ thread{\isaliteral{29}{\isacharparenright}}\ \ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{28}{\isacharparenleft}}depend\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ step\ s\ {\isaliteral{28}{\isacharparenleft}}P\ thread\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+ − 382 \ \ %
+ − 383 \isamarkupcmt{A thread can release a critical resource \isa{cs} if it is running and holding that resource.%
+ − 384 }
+ − 385 \isanewline
+ − 386 \ \ thread{\isaliteral{5F}{\isacharunderscore}}V{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ runing\ s{\isaliteral{3B}{\isacharsemicolon}}\ \ holding\ s\ thread\ cs{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ step\ s\ {\isaliteral{28}{\isacharparenleft}}V\ thread\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+ − 387 \ \ %
+ − 388 \isamarkupcmt{A thread can adjust its own priority as long as it is current running.%
+ − 389 }
+ − 390 \ \ \isanewline
+ − 391 \ \ thread{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ runing\ s{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ step\ s\ {\isaliteral{28}{\isacharparenleft}}Set\ thread\ prio{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+ − 392 \begin{isamarkuptext}%
+ − 393 With predicate \isa{step}, the fact that \isa{s} is a legal state in
+ − 394 Priority Inheritance protocol can be expressed as: \isa{vt\ step\ s}, where
+ − 395 the predicate \isa{vt} can be defined as the following:%
+ − 396 \end{isamarkuptext}%
+ − 397 \isamarkuptrue%
+ − 398 \isacommand{inductive}\isamarkupfalse%
+ − 399 \ vt\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ event\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 400 \ \isakeyword{for}\ cs\ %
+ − 401 \isamarkupcmt{\isa{cs} is an argument representing any step predicate.%
+ − 402 }
+ − 403 \isanewline
+ − 404 \isakeyword{where}\isanewline
+ − 405 \ \ %
+ − 406 \isamarkupcmt{Empty list \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is a legal state in any protocol:%
+ − 407 }
+ − 408 \isanewline
+ − 409 \ \ vt{\isaliteral{5F}{\isacharunderscore}}nil{\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}vt\ cs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+ − 410 \ \ %
+ − 411 \isamarkupcmt{If \isa{s} a legal state, and event \isa{e} is eligible to happen
+ − 412 in state \isa{s}, then \isa{e{\isaliteral{23}{\isacharhash}}{\isaliteral{23}{\isacharhash}}s} is a legal state as well:%
+ − 413 }
+ − 414 \isanewline
+ − 415 \ \ vt{\isaliteral{5F}{\isacharunderscore}}cons{\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}vt\ cs\ s{\isaliteral{3B}{\isacharsemicolon}}\ cs\ s\ e{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ vt\ cs\ {\isaliteral{28}{\isacharparenleft}}e{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+ − 416 \begin{isamarkuptext}%
+ − 417 It is easy to see that the definition of \isa{vt} is generic. It can be applied to
+ − 418 any step predicate to get the set of legal states.%
+ − 419 \end{isamarkuptext}%
+ − 420 \isamarkuptrue%
+ − 421 %
+ − 422 \begin{isamarkuptext}%
+ − 423 The following two functions \isa{the{\isaliteral{5F}{\isacharunderscore}}cs} and \isa{the{\isaliteral{5F}{\isacharunderscore}}th} are used to extract
+ − 424 critical resource and thread respectively out of RAG nodes.%
+ − 425 \end{isamarkuptext}%
+ − 426 \isamarkuptrue%
+ − 427 \isacommand{fun}\isamarkupfalse%
+ − 428 \ the{\isaliteral{5F}{\isacharunderscore}}cs\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}node\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ cs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 429 \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}the{\isaliteral{5F}{\isacharunderscore}}cs\ {\isaliteral{28}{\isacharparenleft}}Cs\ cs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ cs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 430 \isanewline
+ − 431 \isacommand{fun}\isamarkupfalse%
+ − 432 \ the{\isaliteral{5F}{\isacharunderscore}}th\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}node\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 433 \ \ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}the{\isaliteral{5F}{\isacharunderscore}}th\ {\isaliteral{28}{\isacharparenleft}}Th\ th{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ th{\isaliteral{22}{\isachardoublequoteclose}}%
+ − 434 \begin{isamarkuptext}%
+ − 435 The following predicate \isa{next{\isaliteral{5F}{\isacharunderscore}}th} describe the next thread to
+ − 436 take over when a critical resource is released. In \isa{next{\isaliteral{5F}{\isacharunderscore}}th\ s\ th\ cs\ t},
+ − 437 \isa{th} is the thread to release, \isa{t} is the one to take over.%
+ − 438 \end{isamarkuptext}%
+ − 439 \isamarkuptrue%
+ − 440 \isacommand{definition}\isamarkupfalse%
+ − 441 \ next{\isaliteral{5F}{\isacharunderscore}}th{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 442 \ \ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}next{\isaliteral{5F}{\isacharunderscore}}th\ s\ th\ cs\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}\ rest{\isaliteral{2E}{\isachardot}}\ wq\ s\ cs\ {\isaliteral{3D}{\isacharequal}}\ th{\isaliteral{23}{\isacharhash}}rest\ {\isaliteral{5C3C616E643E}{\isasymand}}\ rest\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ \isanewline
+ − 443 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ t\ {\isaliteral{3D}{\isacharequal}}\ hd\ {\isaliteral{28}{\isacharparenleft}}SOME\ q{\isaliteral{2E}{\isachardot}}\ distinct\ q\ {\isaliteral{5C3C616E643E}{\isasymand}}\ set\ q\ {\isaliteral{3D}{\isacharequal}}\ set\ rest{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+ − 444 \begin{isamarkuptext}%
+ − 445 The function \isa{count\ Q\ l} is used to count the occurrence of situation \isa{Q}
+ − 446 in list \isa{l}:%
+ − 447 \end{isamarkuptext}%
+ − 448 \isamarkuptrue%
+ − 449 \isacommand{definition}\isamarkupfalse%
+ − 450 \ count\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 451 \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}count\ Q\ l\ {\isaliteral{3D}{\isacharequal}}\ length\ {\isaliteral{28}{\isacharparenleft}}filter\ Q\ l{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+ − 452 \begin{isamarkuptext}%
+ − 453 \isa{cntP\ s} returns the number of operation \isa{P} happened
+ − 454 before reaching state \isa{s}.%
+ − 455 \end{isamarkuptext}%
+ − 456 \isamarkuptrue%
+ − 457 \isacommand{definition}\isamarkupfalse%
+ − 458 \ cntP\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 459 \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}cntP\ s\ th\ {\isaliteral{3D}{\isacharequal}}\ count\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\ e{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}\ cs{\isaliteral{2E}{\isachardot}}\ e\ {\isaliteral{3D}{\isacharequal}}\ P\ th\ cs{\isaliteral{29}{\isacharparenright}}\ s{\isaliteral{22}{\isachardoublequoteclose}}%
+ − 460 \begin{isamarkuptext}%
+ − 461 \isa{cntV\ s} returns the number of operation \isa{V} happened
+ − 462 before reaching state \isa{s}.%
+ − 463 \end{isamarkuptext}%
+ − 464 \isamarkuptrue%
+ − 465 \isacommand{definition}\isamarkupfalse%
+ − 466 \ cntV\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 467 \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}cntV\ s\ th\ {\isaliteral{3D}{\isacharequal}}\ count\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\ e{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}\ cs{\isaliteral{2E}{\isachardot}}\ e\ {\isaliteral{3D}{\isacharequal}}\ V\ th\ cs{\isaliteral{29}{\isacharparenright}}\ s{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+ − 468 %
+ − 469 \isadelimtheory
+ − 470 %
+ − 471 \endisadelimtheory
+ − 472 %
+ − 473 \isatagtheory
+ − 474 \isacommand{end}\isamarkupfalse%
+ − 475 %
+ − 476 \endisatagtheory
+ − 477 {\isafoldtheory}%
+ − 478 %
+ − 479 \isadelimtheory
+ − 480 \isanewline
+ − 481 %
+ − 482 \endisadelimtheory
+ − 483 \isanewline
+ − 484 \end{isabellebody}%
+ − 485 %%% Local Variables:
+ − 486 %%% mode: latex
+ − 487 %%% TeX-master: "root"
+ − 488 %%% End: