|
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: |