43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
44 \mode<presentation>{ |
44 \mode<presentation>{ |
45 \begin{frame} |
45 \begin{frame} |
46 \frametitle{% |
46 \frametitle{% |
47 \begin{tabular}{@ {}c@ {}} |
47 \begin{tabular}{@ {}c@ {}} |
48 \\[8mm] |
48 \\[-3mm] |
49 \Large A Provably Correct Implementation\\[-3mm] |
49 \Large Priority Inheritance Protocol \\[-3mm] |
50 \Large of the Priority Inheritance Protocol\\[0mm] |
50 \Large Proved Correct \\[0mm] |
51 \end{tabular}} |
51 \end{tabular}} |
52 |
52 |
53 \begin{center} |
53 \begin{center} |
54 \small Christian Urban\\ |
54 \small Xingyuan Zhang \\ |
55 \end{center} |
55 \small \mbox{PLA University of Science and Technology} \\ |
56 |
56 \small \mbox{Nanjing, China} |
57 \begin{center} |
57 \end{center} |
58 \small joint work with Xingyuan Zhang and Chunhan Wu\medskip \\ |
58 |
59 \small \mbox{from the PLA University of Science and Technology in Nanjing} |
59 \begin{center} |
60 \end{center} |
60 \small joint work with \\ |
61 |
61 Christian Urban \\ |
62 \end{frame}} |
62 Kings College, University of London, U.K.\\ |
63 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
63 Chunhan Wu \\ |
64 |
64 My Ph.D. student now working for Christian\\ |
65 *} |
65 \end{center} |
66 |
66 |
67 text_raw {* |
67 \end{frame}} |
68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
69 \mode<presentation>{ |
69 *} |
70 \begin{frame}[c] |
70 |
71 \frametitle{Isabelle Theorem Prover} |
71 text_raw {* |
72 My background: |
72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
73 |
73 \mode<presentation>{ |
74 \begin{itemize} |
74 \begin{frame}[c] |
75 \item mechanical reasoning about languages with binders (Nominal)\medskip |
75 \frametitle{\large Prioirty Inheritance Protocol (PIP)} |
76 \item Barendregt's variable convention can lead to \alert{false}\medskip |
|
77 \item found a bug in a proof by Bob Harper and Frank Pfenning (CMU) on |
|
78 LF (ACM TOCL, 2005) |
|
79 \end{itemize} |
|
80 |
|
81 \begin{textblock}{6}(6.5,12.5) |
|
82 \includegraphics[scale=0.28]{isabelle1.png} |
|
83 \end{textblock} |
|
84 |
|
85 \end{frame}} |
|
86 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
87 |
|
88 *} |
|
89 |
|
90 text_raw {* |
|
91 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
92 \mode<presentation>{ |
|
93 \begin{frame}[c] |
|
94 \frametitle{Real-Time OSes} |
|
95 \large |
76 \large |
96 |
77 |
97 \begin{itemize} |
78 \begin{itemize} \large |
98 \item Processes have priorities\\[5mm] |
79 \item Widely used in Real-Time OSs \pause |
99 \item Resources can be locked and unlocked |
80 \item One solution of \textcolor{red}{`Priority Inversion'} problem \pause |
100 \end{itemize} |
81 \item A flawed manual correctness proof (1990) \pause |
101 |
82 \begin{itemize} \large |
102 \end{frame}} |
83 \item {Notations with no precise definition} |
103 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
84 \item {Resorts to intuitions} |
104 |
85 \end{itemize} \pause |
105 *} |
86 \item Formal treatments using model-checking \pause |
106 |
87 \begin{itemize} \large |
107 text_raw {* |
88 \item {Applicable to small size system models} |
108 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
89 \item { Unhelpful for human understanding } |
109 \mode<presentation>{ |
90 \end{itemize} \pause |
110 \begin{frame}[c] |
91 \item Verification of PCP in PVS (2000) \pause |
111 \frametitle{Problem} |
92 \begin{itemize} \large |
112 \Large |
93 \item {A related protocol} |
113 |
94 \item {Priority Ceiling Protocol} |
114 \begin{center} |
95 \end{itemize} |
115 \begin{tabular}{l} |
96 \end{itemize} |
116 \alert{H}igh-priority process\\[4mm] |
97 |
117 \onslide<2->{\alert{M}edium-priority process}\\[4mm] |
98 \end{frame}} |
118 \alert{L}ow-priority process\\[4mm] |
99 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
119 \end{tabular} |
100 |
120 \end{center} |
101 *} |
121 |
102 |
122 \onslide<3->{ |
103 text_raw {* |
123 \begin{itemize} |
104 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
124 \item \alert{Priority Inversion} @{text "\<equiv>"} \alert{H $<$ L} |
105 \mode<presentation>{ |
125 \item<4> avoid indefinite priority inversion |
106 \begin{frame}[c] |
126 \end{itemize}} |
107 \frametitle{Our Motivation} |
127 |
108 \large |
128 \end{frame}} |
109 |
129 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
110 \begin{itemize} |
130 |
111 \item Undergraduate OS course in our university \pause |
131 *} |
112 \begin{itemize} |
132 |
113 \item {\large Experiments using intrutional OSs } |
133 text_raw {* |
114 \item {\large PINTOS (Stanford) is choosen } |
134 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
115 \item {\large Core project: Implementing PIP in it} |
135 \mode<presentation>{ |
116 \end{itemize} \pause |
136 \begin{frame}[c] |
117 \item Understanding is crucial to implemention \pause |
137 \frametitle{Mars Pathfinder Mission 1997} |
118 \item Little help was found in the literature \pause |
138 \Large |
119 \item Some mentioning the complication |
139 |
120 \end{itemize} |
140 \begin{center} |
121 |
141 \includegraphics[scale=0.26]{pathfinder.jpg} |
122 \end{frame}} |
142 \end{center} |
123 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
143 |
124 |
144 \end{frame}} |
125 *} |
145 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
126 |
146 *} |
127 |
147 |
128 text_raw {* |
148 text_raw {* |
129 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
149 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
130 \mode<presentation>{ |
150 \mode<presentation>{ |
131 \begin{frame}[c] |
151 \begin{frame}[c] |
132 \frametitle{\mbox{Some excerpts}} |
152 \frametitle{Solution} |
|
153 \Large |
|
154 |
|
155 \alert{Priority Inheritance Protocol (PIP):} |
|
156 |
|
157 \begin{center} |
|
158 \begin{tabular}{l} |
|
159 \alert{H}igh-priority process\\[4mm] |
|
160 \textcolor{gray}{Medium-priority process}\\[4mm] |
|
161 \alert{L}ow-priority process\\[21mm] |
|
162 {\normalsize (temporarily raise its priority)} |
|
163 \end{tabular} |
|
164 \end{center} |
|
165 |
|
166 \end{frame}} |
|
167 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
168 *} |
|
169 |
|
170 |
|
171 text_raw {* |
|
172 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
173 \mode<presentation>{ |
|
174 \begin{frame}[c] |
|
175 \frametitle{\mbox{}} |
|
176 |
133 |
177 \begin{quote} |
134 \begin{quote} |
178 ``Priority inheritance is neither ef$\!$ficient nor reliable. |
135 ``Priority inheritance is neither ef$\!$ficient nor reliable. |
179 Implementations are either incomplete (and unreliable) |
136 Implementations are either incomplete (and unreliable) |
180 or surprisingly complex and intrusive.'' |
137 or surprisingly complex and intrusive.'' |
181 \end{quote}\medskip |
138 \end{quote}\medskip |
|
139 |
|
140 \pause |
182 |
141 |
183 \begin{quote} |
142 \begin{quote} |
184 ``I observed in the kernel code (to my disgust), the Linux |
143 ``I observed in the kernel code (to my disgust), the Linux |
185 PIP implementation is a nightmare: extremely heavy weight, |
144 PIP implementation is a nightmare: extremely heavy weight, |
186 involving maintenance of a full wait-for graph, and requiring |
145 involving maintenance of a full wait-for graph, and requiring |
195 |
154 |
196 text_raw {* |
155 text_raw {* |
197 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
156 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
198 \mode<presentation>{ |
157 \mode<presentation>{ |
199 \begin{frame}[c] |
158 \begin{frame}[c] |
|
159 \frametitle{Our Aims} |
|
160 \large |
|
161 |
|
162 \begin{itemize} |
|
163 \item Formal specification at appropriate abstract level, |
|
164 convenient for: |
|
165 \begin{itemize} \large |
|
166 \item Constructing interactive proofs |
|
167 \item Clarifying the underlying ideas |
|
168 \end{itemize} \pause |
|
169 \item Theorems usable to guide implementation, critical point: |
|
170 \begin{itemize} \large |
|
171 \item Understanding the relationship with real OS code \pause |
|
172 \item Not yet formalized |
|
173 \end{itemize} |
|
174 \end{itemize} |
|
175 |
|
176 \end{frame}} |
|
177 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
178 |
|
179 *} |
|
180 |
|
181 |
|
182 |
|
183 |
|
184 text_raw {* |
|
185 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
186 \mode<presentation>{ |
|
187 \begin{frame}[c] |
|
188 \frametitle{Real-Time OSes} |
|
189 \large |
|
190 |
|
191 \begin{itemize} |
|
192 \item Purpose: gurantee the most urgent task be processed in time |
|
193 \item Processes have priorities\\ |
|
194 \item Resources can be locked and unlocked |
|
195 \end{itemize} |
|
196 |
|
197 \end{frame}} |
|
198 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
199 |
|
200 *} |
|
201 |
|
202 |
|
203 text_raw {* |
|
204 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
205 \mode<presentation>{ |
|
206 \begin{frame}[c] |
|
207 \frametitle{Problem} |
|
208 \Large |
|
209 |
|
210 \begin{center} |
|
211 \begin{tabular}{l} |
|
212 \alert{H}igh-priority process\\[4mm] |
|
213 \onslide<2->{\alert{M}edium-priority process}\\[4mm] |
|
214 \alert{L}ow-priority process\\[4mm] |
|
215 \end{tabular} |
|
216 \end{center} |
|
217 |
|
218 \onslide<3->{ |
|
219 \begin{itemize} |
|
220 \item \alert{Priority Inversion} @{text "\<equiv>"} \alert{H $<$ L} |
|
221 \item<4> avoid indefinite priority inversion |
|
222 \end{itemize}} |
|
223 |
|
224 \end{frame}} |
|
225 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
226 |
|
227 *} |
|
228 |
|
229 |
|
230 text_raw {* |
|
231 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
232 \mode<presentation>{ |
|
233 \begin{frame}[c] |
|
234 \frametitle{Priority Inversion} |
|
235 |
|
236 \begin{center} |
|
237 \includegraphics[scale=0.4]{PriorityInversion.png} |
|
238 \end{center} |
|
239 |
|
240 \end{frame}} |
|
241 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
242 |
|
243 *} |
|
244 |
|
245 |
|
246 text_raw {* |
|
247 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
248 \mode<presentation>{ |
|
249 \begin{frame}[c] |
|
250 \frametitle{Mars Pathfinder Mission 1997} |
|
251 \Large |
|
252 |
|
253 \begin{center} |
|
254 \includegraphics[scale=0.2]{marspath1.png} |
|
255 \includegraphics[scale=0.22]{marspath3.png} |
|
256 \includegraphics[scale=0.4]{marsrover.png} |
|
257 \end{center} |
|
258 |
|
259 \end{frame}} |
|
260 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
261 *} |
|
262 |
|
263 text_raw {* |
|
264 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
265 \mode<presentation>{ |
|
266 \begin{frame}[c] |
|
267 \frametitle{Solution} |
|
268 \Large |
|
269 |
|
270 \alert{Priority Inheritance Protocol (PIP):} |
|
271 |
|
272 \begin{center} |
|
273 \begin{tabular}{l} |
|
274 \alert{H}igh-priority process\\[4mm] |
|
275 \textcolor{gray}{Medium-priority process}\\[4mm] |
|
276 \alert{L}ow-priority process\\[21mm] |
|
277 {\normalsize (temporarily raise its priority)} |
|
278 \end{tabular} |
|
279 \end{center} |
|
280 |
|
281 \end{frame}} |
|
282 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
283 *} |
|
284 |
|
285 |
|
286 |
|
287 |
|
288 text_raw {* |
|
289 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
290 \mode<presentation>{ |
|
291 \begin{frame}[c] |
200 \frametitle{A Correctness ``Proof'' in 1990} |
292 \frametitle{A Correctness ``Proof'' in 1990} |
201 \Large |
293 \Large |
202 |
294 |
203 \begin{itemize} |
295 \begin{itemize} |
204 \item a paper$^\star$ |
296 \item a paper$^\star$ |
366 |
478 |
367 |
479 |
368 \end{frame}} |
480 \end{frame}} |
369 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
481 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
370 *} |
482 *} |
371 |
483 (*<*) |
372 text_raw {* |
484 context extend_highest_gen |
373 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
485 begin |
374 \mode<presentation>{ |
486 (*>*) |
375 \begin{frame}[c] |
487 text_raw {* |
376 \frametitle{Theorem} |
488 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
377 |
489 \mode<presentation>{ |
378 \textcolor{gray}{``No indefinite priority inversion''}\bigskip |
490 \begin{frame}[c] |
379 |
491 \frametitle{\mbox{\large Theorem: ``No indefinite priority inversion''}} |
380 Theorem:$^\star$ If th is the thread with the highest precedence in state s, |
492 |
381 then in every future state @{text "s'"} in which th is still |
493 \pause |
382 alive\smallskip |
494 |
383 |
495 Theorem $^\star$: If th is the thread with the highest precedence in state |
384 |
496 @{text "s"}: \pause |
385 \begin{itemize} |
497 \begin{center} |
386 \item th is blocked by a thread @{text "th'"} that was alive in s |
498 \textcolor{red}{@{thm highest})} |
387 \item @{text "th'"} held a resource in s, and |
499 \end{center} |
388 \item @{text "th'"} is running with the precedence of th.\bigskip |
500 \pause |
389 \end{itemize} |
501 and @{text "th"} is blocked by a thread @{text "th'"} in |
390 |
502 a future state @{text "s'"} (with @{text "s' = t@s"}): \pause |
|
503 \begin{center} |
|
504 \textcolor{red}{@{text "th' \<in> running (t@s)"} and @{text "th' \<noteq> th"}} \pause |
|
505 \end{center} |
|
506 \fbox{ \hspace{1em} \pause |
|
507 \begin{minipage}{0.95\textwidth} |
|
508 \begin{itemize} |
|
509 \item @{text "th'"} did not hold or wait for a resource in s: |
|
510 \begin{center} |
|
511 \textcolor{red}{@{text "\<not>detached s th'"}} |
|
512 \end{center} \pause |
|
513 \item @{text "th'"} is running with the precedence of @{text "th"}: |
|
514 \begin{center} |
|
515 \textcolor{red}{@{text "cp (t@s) th' = preced th s"}} |
|
516 \end{center} |
|
517 \end{itemize} |
|
518 \end{minipage}} |
|
519 \pause |
391 \small |
520 \small |
392 $^\star$ modulo some further assumptions\bigskip\pause |
521 $^\star$ modulo some further assumptions\bigskip\pause |
393 |
522 |
394 It does not matter which process gets a released lock. |
523 It does not matter which process gets a released lock. |
395 |
524 |
438 text_raw {* |
568 text_raw {* |
439 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
569 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
440 \mode<presentation>{ |
570 \mode<presentation>{ |
441 \begin{frame}[t] |
571 \begin{frame}[t] |
442 \frametitle{Implementation} |
572 \frametitle{Implementation} |
443 |
573 |
444 s $=$ current state; @{text "s'"} $=$ next state\bigskip |
574 s $=$ current state; @{text "s'"} $=$ next state $=$ @{text "e#s"}\bigskip\bigskip |
445 |
575 |
446 \alert{Unlock th cs} where there is a thread to take over |
576 When @{text "e"} = \alert{Unlock th cs} where there is a thread to take over |
447 |
577 |
448 \begin{itemize} |
578 \begin{itemize} |
449 \item @{text "RAG s' = RAG s - {(C cs, T th), (T th', C cs)} \<union> {(C cs, T th')}"} |
579 \item @{text "RAG s' = RAG s - {(C cs, T th), (T th', C cs)} \<union> {(C cs, T th')}"} |
450 \item we have to recalculate the precedence of the direct descendants |
580 \item we have to recalculate the precedence of the direct descendants |
451 \end{itemize}\bigskip |
581 \end{itemize}\bigskip |
452 |
582 |
453 \alert{Unlock th cs} where no thread takes over |
583 \pause |
|
584 |
|
585 When @{text "e"} = \alert{Unlock th cs} where no thread takes over |
454 |
586 |
455 \begin{itemize} |
587 \begin{itemize} |
456 \item @{text "RAG s' = RAG s - {(C cs, T th)}"} |
588 \item @{text "RAG s' = RAG s - {(C cs, T th)}"} |
457 \item no recalculation of precedences |
589 \item no recalculation of precedences |
458 \end{itemize} |
590 \end{itemize} |
465 text_raw {* |
597 text_raw {* |
466 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
598 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
467 \mode<presentation>{ |
599 \mode<presentation>{ |
468 \begin{frame}[t] |
600 \begin{frame}[t] |
469 \frametitle{Implementation} |
601 \frametitle{Implementation} |
470 |
602 |
471 s $=$ current state; @{text "s'"} $=$ next state\bigskip\bigskip |
603 s $=$ current state; @{text "s'"} $=$ next state $=$ @{text "e#s"}\bigskip\bigskip |
472 |
604 |
473 \alert{Lock th cs} where cs is not locked |
605 When @{text "e"} = \alert{Lock th cs} where cs is not locked |
474 |
606 |
475 \begin{itemize} |
607 \begin{itemize} |
476 \item @{text "RAG s' = RAG s \<union> {(C cs, T th')}"} |
608 \item @{text "RAG s' = RAG s \<union> {(C cs, T th')}"} |
477 \item no recalculation of precedences |
609 \item no recalculation of precedences |
478 \end{itemize}\bigskip |
610 \end{itemize}\bigskip |
479 |
611 |
480 \alert{Lock th cs} where cs is locked |
612 \pause |
|
613 |
|
614 When @{text "e"} = \alert{Lock th cs} where cs is locked |
481 |
615 |
482 \begin{itemize} |
616 \begin{itemize} |
483 \item @{text "RAG s' = RAG s - {(T th, C cs)}"} |
617 \item @{text "RAG s' = RAG s - {(T th, C cs)}"} |
484 \item we have to recalculate the precedence of the descendants |
618 \item we have to recalculate the precedence of the descendants |
485 \end{itemize} |
619 \end{itemize} |
487 |
621 |
488 \end{frame}} |
622 \end{frame}} |
489 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
623 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
490 *} |
624 *} |
491 |
625 |
492 text_raw {* |
|
493 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
494 \mode<presentation>{ |
|
495 \begin{frame}[c] |
|
496 \frametitle{PINTOS} |
|
497 |
|
498 \begin{itemize} |
|
499 \item \ldots{}small operating system developed at Stanford for teaching; |
|
500 written in C\bigskip |
|
501 \end{itemize} |
|
502 |
|
503 \begin{center} |
|
504 \begin{tabular}{|l@ {\hspace{2mm}}|l@ {\hspace{2mm}}|} |
|
505 \hline |
|
506 {\bf Event} & {\bf PINTOS function} \\ |
|
507 \hline |
|
508 @{text Create} & @{text "thread_create"}\\ |
|
509 @{text Exit} & @{text "thread_exit"}\\ |
|
510 @{text Set} & @{text "thread_set_priority"}\\ |
|
511 @{text Lock} & @{text "lock_acquire"}\\ |
|
512 @{text Unlock} & @{text "lock_release"}\\ |
|
513 \hline |
|
514 \end{tabular} |
|
515 \end{center} |
|
516 |
|
517 |
|
518 \end{frame}} |
|
519 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
520 *} |
|
521 |
626 |
522 text_raw {* |
627 text_raw {* |
523 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
628 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
524 \mode<presentation>{ |
629 \mode<presentation>{ |
525 \begin{frame}[c] |
630 \begin{frame}[c] |
526 \frametitle{Conclusion} |
631 \frametitle{Conclusion} |
527 |
632 |
528 \begin{itemize} |
633 \begin{itemize} \large |
529 \item surprised how pleasant the experience was\medskip |
634 \item Aims fulfilled \medskip \pause |
530 |
635 \item Alternative way \pause |
531 \item no real specification existed for PIP\medskip |
636 \begin{itemize} |
532 |
637 \item using Isabelle/HOL in OS code development \medskip |
533 \item general technique (a ``hammer''):\\[2mm] |
638 \item through the Inductive Approach |
534 events, separation of good and bad configurations\medskip |
639 \end{itemize} \pause |
535 |
640 \item Future researches \pause |
536 \item scheduler in RT-Linux\medskip |
641 \begin{itemize} \large |
537 |
642 \item scheduler in RT-Linux\medskip |
538 \item multiprocessor case\medskip |
643 \item multiprocessor case\medskip |
539 |
644 \item other ``nails'' ? (networks, \ldots) \pause |
540 \item other ``nails'' ? (networks, \ldots) |
645 \item Refinement to real code and relation between implemenations |
541 \end{itemize} |
646 \end{itemize} |
542 |
647 \end{itemize} |
543 |
648 \end{frame}} |
544 \end{frame}} |
649 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
545 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
650 *} |
546 *} |
651 |
547 |
652 |
548 (*<*) |
653 (*<*) |
549 end |
654 end |
|
655 end |
550 (*>*) |
656 (*>*) |