109 {\bf Long, long proof} \ldots\\ |
200 {\bf Long, long proof} \ldots\\ |
110 \end{bubble}\bigskip\medskip |
201 \end{bubble}\bigskip\medskip |
111 |
202 |
112 \small This can be a gigantic proof. The only hope is to have |
203 \small This can be a gigantic proof. The only hope is to have |
113 help from the computer. `Program' is here to be understood to be |
204 help from the computer. `Program' is here to be understood to be |
114 quite general (protocols, OS, \ldots). |
205 quite general (compiler, OS, \ldots). |
115 |
206 |
116 \end{frame} |
207 \end{frame} |
117 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
208 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
118 |
209 |
119 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
210 |
120 \begin{frame}[c] |
211 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
121 \frametitle{\Large{}Mars Pathfinder Mission 1997} |
212 |
122 |
213 \begin{frame}[c] |
123 \begin{center} |
214 \frametitle{Can This Be Done?} |
124 \includegraphics[scale=0.15]{../pics/marspath1.png} |
215 |
125 \includegraphics[scale=0.16]{../pics/marspath3.png} |
216 \begin{itemize} |
126 \includegraphics[scale=0.3]{../pics/marsrover.png} |
217 \item in 2008, verification of a small C-compiler |
127 \end{center} |
|
128 |
|
129 \begin{itemize} |
|
130 \item despite NASA's famous testing procedures, the lander crashed frequently on Mars |
|
131 \item a scheduling algorithm was not used in the OS |
|
132 \end{itemize} |
|
133 |
|
134 \end{frame} |
|
135 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
136 |
|
137 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
138 \begin{frame}[c] |
|
139 |
|
140 |
|
141 \begin{textblock}{11}(1,3) |
|
142 \begin{tabular}{@{\hspace{-10mm}}l} |
|
143 \begin{tikzpicture}[scale=1.1] |
|
144 \node at (-2.5,-1.5) {\textcolor{white}{a}}; |
|
145 \node at (8,4) {\textcolor{white}{a}}; |
|
146 |
|
147 |
|
148 |
|
149 \only<1>{ |
|
150 \draw[fill, blue!50] (1,0) rectangle (3,0.6); |
|
151 } |
|
152 \only<2>{ |
|
153 \draw[fill, blue!50] (1,0) rectangle (2,0.6); |
|
154 \draw[fill, blue!50] (3,0) rectangle (5,0.6); |
|
155 \draw[fill, blue!100] (2,3) rectangle (3,3.6); |
|
156 } |
|
157 \only<3>{ |
|
158 \draw[fill, blue!50] (1,0) rectangle (2,0.6); |
|
159 \draw[fill, blue!50] (3,0) rectangle (4.5,0.6); |
|
160 \draw[fill, blue!50] (5.5,0) rectangle (6,0.6); |
|
161 \draw[fill, blue!100] (2,3) rectangle (3,3.6); |
|
162 \draw[fill, blue!100] (4.5,3) rectangle (5.5,3.6); |
|
163 } |
|
164 \only<4>{ |
|
165 \node at (2.5,0.9) {\small locked a resource}; |
|
166 \draw[fill, blue!50] (1,0) rectangle (2,0.6); |
|
167 \draw[blue!50, very thick] (2,0) rectangle (4,0.6); |
|
168 \draw[blue!100, very thick] (2,3) rectangle (3, 3.6); |
|
169 \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1); |
|
170 } |
|
171 \only<5>{ |
|
172 \node at (2.5,0.9) {\small locked a resource}; |
|
173 \draw[fill, blue!50] (1,0) rectangle (4,0.6); |
|
174 \draw[blue!100, fill] (4,3) rectangle (5, 3.6); |
|
175 } |
|
176 \only<6>{ |
|
177 \node at (2.5,0.9) {\small locked a resource}; |
|
178 \draw[fill, blue!50] (1,0) rectangle (2,0.6); |
|
179 \draw[blue!50, very thick] (2,0) rectangle (4,0.6); |
|
180 \draw[blue!100, very thick] (2,3) rectangle (3, 3.6); |
|
181 \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1); |
|
182 } |
|
183 \only<7>{ |
|
184 \node at (2.5,0.9) {\small locked a resource}; |
|
185 \draw[fill, blue!50] (1,0) rectangle (2.5,0.6); |
|
186 \draw[blue!50, very thick] (2.5,0) rectangle (4,0.6); |
|
187 \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6); |
|
188 \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1); |
|
189 } |
|
190 \only<8>{ |
|
191 \node at (2.5,0.9) {\small locked a resource}; |
|
192 \draw[fill, blue!50] (1,0) rectangle (2.5,0.6); |
|
193 \draw[blue!50, very thick] (2.5,0) rectangle (4,0.6); |
|
194 \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6); |
|
195 \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6); |
|
196 \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1); |
|
197 \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1); |
|
198 } |
|
199 \only<9>{ |
|
200 \node at (2.5,0.9) {\small locked a resource}; |
|
201 \draw[fill, blue!50] (1,0) rectangle (2.5,0.6); |
|
202 \draw[blue!50, very thick] (3.5,0) rectangle (5,0.6); |
|
203 \draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6); |
|
204 \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1); |
|
205 \draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1); |
|
206 } |
|
207 \only<10>{ |
|
208 \node at (2.5,0.9) {\small locked a resource}; |
|
209 \draw[fill, blue!50] (1,0) rectangle (2.5,0.6); |
|
210 \draw[blue!50, very thick] (3.5,0) rectangle (5,0.6); |
|
211 \draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6); |
|
212 \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1); |
|
213 \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1); |
|
214 \draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1); |
|
215 } |
|
216 \only<11>{ |
|
217 \node at (2.5,0.9) {\small locked a resource}; |
|
218 \draw[fill, blue!50] (1,0) rectangle (2.5,0.6); |
|
219 \draw[blue!50, very thick] (4.5,0) rectangle (6,0.6); |
|
220 \draw[blue!100, very thick] (4.5,3) rectangle (5.5, 3.6); |
|
221 \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1); |
|
222 \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1); |
|
223 \draw[red, <-, line width = 2mm] (4.5,-0.1) -- (4.5, -1); |
|
224 } |
|
225 \only<12>{ |
|
226 \node at (2.5,0.9) {\small locked a resource}; |
|
227 \draw[fill, blue!50] (1,0) rectangle (2.5,0.6); |
|
228 \draw[blue!50, very thick] (5.5,0) rectangle (7,0.6); |
|
229 \draw[blue!100, very thick] (5.5,3) rectangle (6.5, 3.6); |
|
230 \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1); |
|
231 \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1); |
|
232 \draw[red, fill] (4.55,1.5) rectangle (5.5,2.1); |
|
233 \draw[red, <-, line width = 2mm] (5.5,-0.1) -- (5.5, -1); |
|
234 \node [anchor=base] at (6.3, 1.8) {\Large\ldots}; |
|
235 } |
|
236 \only<13>{ |
|
237 \node at (2.5,0.9) {\small locked a resource}; |
|
238 \draw[fill, blue!50] (1,0) rectangle (2,0.6); |
|
239 \draw[blue!50, very thick] (2,0) rectangle (4,0.6); |
|
240 \draw[blue!100, very thick] (2,3) rectangle (3, 3.6); |
|
241 \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1); |
|
242 } |
|
243 \only<14>{ |
|
244 \node at (2.5,3.9) {\small locked a resource}; |
|
245 \draw[fill, blue!50] (1,0) rectangle (2,0.6); |
|
246 \draw[blue!50, fill] (2,3) rectangle (4,3.6); |
|
247 \draw[blue!100, very thick] (4,3) rectangle (5, 3.6); |
|
248 \draw[blue!50, ->, line width = 2mm] (2,1) -- (2, 2.5); |
|
249 \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1); |
|
250 } |
|
251 \only<15>{ |
|
252 \node at (2.5,3.9) {\small locked a resource}; |
|
253 \draw[fill, blue!50] (1,0) rectangle (2,0.6); |
|
254 \draw[blue!50, fill] (2,3) rectangle (4,3.6); |
|
255 \draw[blue!100, very thick] (4,3) rectangle (5, 3.6); |
|
256 \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1); |
|
257 \draw[red, very thick] (2.5,1.5) rectangle (3.5,2.1); |
|
258 } |
|
259 |
|
260 |
|
261 \draw[very thick,->](0,0) -- (8,0); |
|
262 \node [anchor=base] at (8, -0.3) {\scriptsize time}; |
|
263 \node [anchor=base] at (0, -0.3) {\scriptsize 0}; |
|
264 \node [anchor=base] at (-1.2, 0.2) {\small low priority}; |
|
265 \only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};} |
|
266 \only<8->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};} |
|
267 |
|
268 \end{tikzpicture} |
|
269 \end{tabular} |
|
270 \end{textblock} |
|
271 |
|
272 \begin{textblock}{0}(2.5,13)% |
|
273 \small |
|
274 \onslide<3->{ |
|
275 \begin{bubble}[8cm]% |
|
276 Scheduling: You want to avoid that a high |
|
277 priority process is starved indefinitely. |
|
278 \end{bubble}} |
|
279 \end{textblock} |
|
280 |
|
281 \end{frame} |
|
282 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
283 |
|
284 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
285 \begin{frame}[c] |
|
286 \frametitle{\Large Priority Inheritance Scheduling} |
|
287 |
|
288 \begin{itemize} |
|
289 \item Let a low priority process $L$ temporarily inherit |
|
290 the high priority of $H$ until $L$ leaves the critical |
|
291 section unlocking the resource.\bigskip |
|
292 \item Once the resource is unlocked $L$ returns to its original |
|
293 priority level. |
|
294 \end{itemize} |
|
295 |
|
296 \end{frame} |
|
297 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
298 |
|
299 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
300 \begin{frame}[c] |
|
301 |
|
302 \begin{textblock}{11}(1,3) |
|
303 \begin{tabular}{@{\hspace{-10mm}}l} |
|
304 \begin{tikzpicture}[scale=1.1] |
|
305 \node at (-2.5,-1.5) {\textcolor{white}{a}}; |
|
306 \node at (8,4) {\textcolor{white}{a}}; |
|
307 |
|
308 \only<1>{ |
|
309 \draw[fill, blue!50] (1,0) rectangle (6,0.6); |
|
310 \node at (1.5,0.9) {\small $A_L$}; |
|
311 \node at (2.0,0.9) {\small $B_L$}; |
|
312 \node at (3.5,0.9) {\small $A_R$}; |
|
313 \node at (5.7,0.9) {\small $B_R$}; |
|
314 \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); |
|
315 \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); |
|
316 \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6); |
|
317 \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6); |
|
318 } |
|
319 \only<2>{ |
|
320 \draw[fill, blue!50] (1,0) rectangle (3,0.6); |
|
321 \draw[very thick, blue!50] (3,0) rectangle (6,0.6); |
|
322 \node at (1.5,0.9) {\small $A_L$}; |
|
323 \node at (2.0,0.9) {\small $B_L$}; |
|
324 \node at (3.5,0.9) {\small $A_R$}; |
|
325 \node at (5.7,0.9) {\small $B_R$}; |
|
326 \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); |
|
327 \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); |
|
328 \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6); |
|
329 \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6); |
|
330 } |
|
331 \only<3>{ |
|
332 \draw[fill, blue!50] (1,0) rectangle (3,0.6); |
|
333 \draw[very thick, blue!50] (3,0) rectangle (6,0.6); |
|
334 \node at (1.5,0.9) {\small $A_L$}; |
|
335 \node at (2.0,0.9) {\small $B_L$}; |
|
336 \node at (3.5,0.9) {\small $A_R$}; |
|
337 \node at (5.7,0.9) {\small $B_R$}; |
|
338 \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); |
|
339 \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); |
|
340 \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6); |
|
341 \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6); |
|
342 \draw[very thick,blue!100] (3,3) rectangle (4,3.6); |
|
343 \node at (3.5,3.3) {\small $A$}; |
|
344 } |
|
345 \only<4>{ |
|
346 \draw[fill, blue!50] (1,0) rectangle (3,0.6); |
|
347 \draw[very thick, blue!50] (3,0) rectangle (6,0.6); |
|
348 \node at (1.5,0.9) {\small $A_L$}; |
|
349 \node at (2.0,0.9) {\small $B_L$}; |
|
350 \node at (3.5,0.9) {\small $A_R$}; |
|
351 \node at (5.7,0.9) {\small $B_R$}; |
|
352 \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); |
|
353 \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); |
|
354 \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6); |
|
355 \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6); |
|
356 \draw[very thick,blue!100] (3,3) rectangle (4,3.6); |
|
357 \node at (3.5,3.3) {\small $A$}; |
|
358 \draw[very thick,blue!100] (4,3) rectangle (5,3.6); |
|
359 \node at (4.5,3.3) {\small $B$}; |
|
360 } |
|
361 \only<5>{ |
|
362 \draw[fill, blue!50] (1,0) rectangle (3,0.6); |
|
363 \draw[very thick, blue!50] (3,3) rectangle (6,3.6); |
|
364 \node at (1.5,0.9) {\small $A_L$}; |
|
365 \node at (2.0,0.9) {\small $B_L$}; |
|
366 \node at (3.5,3.9) {\small $A_R$}; |
|
367 \node at (5.7,3.9) {\small $B_R$}; |
|
368 \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); |
|
369 \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); |
|
370 \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6); |
|
371 \draw[very thick,blue!100] (5.7,3) -- (5.7,3.6); |
|
372 \draw[very thick,blue!100] (6,3) rectangle (7,3.6); |
|
373 \node at (6.5,3.3) {\small $A$}; |
|
374 \draw[very thick,blue!100] (7,3) rectangle (8,3.6); |
|
375 \node at (7.5,3.3) {\small $B$}; |
|
376 \draw[blue!50, ->, line width = 2mm] (3,1) -- (3, 2.5); |
|
377 } |
|
378 \only<6>{ |
|
379 \draw[fill, blue!50] (1,0) rectangle (3,0.6); |
|
380 \draw[fill, blue!50] (3,3) rectangle (3.5,3.6); |
|
381 \draw[very thick, blue!50] (3.5,3) rectangle (6,3.6); |
|
382 \node at (1.5,0.9) {\small $A_L$}; |
|
383 \node at (2.0,0.9) {\small $B_L$}; |
|
384 \node at (3.5,3.9) {\small $A_R$}; |
|
385 \node at (5.7,3.9) {\small $B_R$}; |
|
386 \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); |
|
387 \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); |
|
388 \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6); |
|
389 \draw[very thick,blue!100] (5.7,3) -- (5.7,3.6); |
|
390 \draw[very thick,blue!100] (6,3) rectangle (7,3.6); |
|
391 \node at (6.5,3.3) {\small $A$}; |
|
392 \draw[very thick,blue!100] (7,3) rectangle (8,3.6); |
|
393 \node at (7.5,3.3) {\small $B$}; |
|
394 } |
|
395 \only<7>{ |
|
396 \draw[fill, blue!50] (1,0) rectangle (3,0.6); |
|
397 \draw[fill, blue!50] (3,3) rectangle (3.5,3.6); |
|
398 \draw[very thick, blue!50] (3.5,0) rectangle (6,0.6); |
|
399 \node at (1.5,0.9) {\small $A_L$}; |
|
400 \node at (2.0,0.9) {\small $B_L$}; |
|
401 \node at (3.5,3.9) {\small $A_R$}; |
|
402 \node at (5.7,0.9) {\small $B_R$}; |
|
403 \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); |
|
404 \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); |
|
405 \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6); |
|
406 \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6); |
|
407 \draw[very thick,blue!100] (6,3) rectangle (7,3.6); |
|
408 \node at (6.5,3.3) {\small $A$}; |
|
409 \draw[very thick,blue!100] (7,3) rectangle (8,3.6); |
|
410 \node at (7.5,3.3) {\small $B$}; |
|
411 \draw[blue!50, <-, line width = 2mm] (3.5,1) -- (3.5, 2.5); |
|
412 \draw[blue!50, <-, line width = 2mm] (4,3.3) -- (5.5,3.3); |
|
413 } |
|
414 \only<8>{ |
|
415 \draw[fill, blue!50] (1,0) rectangle (3,0.6); |
|
416 \draw[fill, blue!50] (3,3) rectangle (3.5,3.6); |
|
417 \draw[very thick, blue!50] (4.5,0) rectangle (7,0.6); |
|
418 \node at (1.5,0.9) {\small $A_L$}; |
|
419 \node at (2.0,0.9) {\small $B_L$}; |
|
420 \node at (3.5,3.9) {\small $A_R$}; |
|
421 \node at (6.7,0.9) {\small $B_R$}; |
|
422 \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); |
|
423 \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); |
|
424 \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6); |
|
425 \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6); |
|
426 \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6); |
|
427 \node at (4,3.3) {\small $A$}; |
|
428 \draw[very thick,blue!100] (7,3) rectangle (8,3.6); |
|
429 \node at (7.5,3.3) {\small $B$}; |
|
430 } |
|
431 \only<9>{ |
|
432 \draw[fill, blue!50] (1,0) rectangle (3,0.6); |
|
433 \draw[fill, blue!50] (3,3) rectangle (3.5,3.6); |
|
434 \draw[fill, blue!50] (4.5,0) rectangle (5,0.6); |
|
435 \draw[very thick, blue!50] (5,0) rectangle (7,0.6); |
|
436 \node at (1.5,0.9) {\small $A_L$}; |
|
437 \node at (2.0,0.9) {\small $B_L$}; |
|
438 \node at (3.5,3.9) {\small $A_R$}; |
|
439 \node at (6.7,0.9) {\small $B_R$}; |
|
440 \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); |
|
441 \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); |
|
442 \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6); |
|
443 \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6); |
|
444 \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6); |
|
445 \node at (4,3.3) {\small $A$}; |
|
446 \draw[very thick,blue!100] (7,3) rectangle (8,3.6); |
|
447 \node at (7.5,3.3) {\small $B$}; |
|
448 } |
|
449 \only<10>{ |
|
450 \draw[fill, blue!50] (1,0) rectangle (3,0.6); |
|
451 \draw[fill, blue!50] (3,3) rectangle (3.5,3.6); |
|
452 \draw[fill, blue!50] (4.5,0) rectangle (5,0.6); |
|
453 \draw[very thick, blue!50] (5,0) rectangle (7,0.6); |
|
454 \node at (1.5,0.9) {\small $A_L$}; |
|
455 \node at (2.0,0.9) {\small $B_L$}; |
|
456 \node at (3.5,3.9) {\small $A_R$}; |
|
457 \node at (6.7,0.9) {\small $B_R$}; |
|
458 \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); |
|
459 \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); |
|
460 \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6); |
|
461 \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6); |
|
462 \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6); |
|
463 \node at (4,3.3) {\small $A$}; |
|
464 \draw[very thick,blue!100] (7,3) rectangle (8,3.6); |
|
465 \node at (7.5,3.3) {\small $B$}; |
|
466 \draw[red, fill] (5,1.5) rectangle (6,2.1); |
|
467 \draw[red, fill] (6.05,1.5) rectangle (7,2.1); |
|
468 } |
|
469 \only<11>{ |
|
470 \draw[fill, blue!50] (1,0) rectangle (3,0.6); |
|
471 \draw[fill, blue!50] (3,3) rectangle (3.5,3.6); |
|
472 \draw[fill, blue!50] (4.5,0) rectangle (5,0.6); |
|
473 \draw[very thick, blue!50] (5,0) rectangle (7,0.6); |
|
474 \node at (1.5,0.9) {\small $A_L$}; |
|
475 \node at (2.0,0.9) {\small $B_L$}; |
|
476 \node at (3.5,3.9) {\small $A_R$}; |
|
477 \node at (6.7,0.9) {\small $B_R$}; |
|
478 \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); |
|
479 \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); |
|
480 \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6); |
|
481 \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6); |
|
482 \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6); |
|
483 \node at (4,3.3) {\small $A$}; |
|
484 \draw[very thick,blue!100] (7,3) rectangle (8,3.6); |
|
485 \node at (7.5,3.3) {\small $B$}; |
|
486 \draw[red, fill] (5,1.5) rectangle (6,2.1); |
|
487 \draw[red, fill] (6.05,1.5) rectangle (7,2.1); |
|
488 \draw[blue!50, ->, line width = 2mm] (7.1,0.4) -- (8, 0.4); |
|
489 \draw[blue!50, ->, line width = 2mm] (7.1,4) -- (8,4); |
|
490 } |
|
491 |
|
492 \draw[very thick,->](0,0) -- (8,0); |
|
493 \node [anchor=base] at (8, -0.3) {\scriptsize time}; |
|
494 \node [anchor=base] at (0, -0.3) {\scriptsize 0}; |
|
495 \node [anchor=base] at (-1.2, 0.2) {\small low priority}; |
|
496 \only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};} |
|
497 \only<10->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};} |
|
498 |
|
499 \end{tikzpicture} |
|
500 \end{tabular} |
|
501 \end{textblock} |
|
502 |
|
503 \begin{textblock}{0}(2.5,13)% |
|
504 \small |
|
505 \onslide<11>{ |
|
506 \begin{bubble}[8cm]% |
|
507 Scheduling: You want to avoid that a high |
|
508 priority process is staved indefinitely. |
|
509 \end{bubble}} |
|
510 \end{textblock} |
|
511 |
|
512 |
|
513 \end{frame} |
|
514 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
515 |
|
516 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
517 \begin{frame}[c] |
|
518 \frametitle{\Large Priority Inheritance Scheduling} |
|
519 |
|
520 \begin{itemize} |
|
521 \item Let a low priority process $L$ temporarily inherit |
|
522 the high priority of $H$ until $L$ leaves the critical |
|
523 section unlocking the resource.\bigskip |
|
524 \item Once the resource is unlocked $L$ returns to its original |
|
525 priority level. \alert{\bf BOGUS}\pause\bigskip |
|
526 \item \ldots $L$ needs to switch to the highest |
|
527 \alert{remaining} priority of the threads that it blocks. |
|
528 \end{itemize}\bigskip |
|
529 |
|
530 \small this error is already known since around 1999 |
|
531 |
|
532 \end{frame} |
|
533 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
534 |
|
535 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
536 \begin{frame}[c] |
|
537 |
|
538 \begin{center} |
|
539 \includegraphics[scale=0.25]{../pics/p3.jpg} |
|
540 \end{center} |
|
541 |
|
542 \begin{itemize} |
|
543 \item by Rajkumar, 1991 |
|
544 \item \it ``it resumes the priority it had at the point of entry into the critical |
|
545 section'' |
|
546 \end{itemize} |
|
547 |
|
548 \end{frame} |
|
549 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
550 |
|
551 |
|
552 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
553 \begin{frame}[c] |
|
554 |
|
555 \begin{center} |
|
556 \includegraphics[scale=0.25]{../pics/p2.jpg} |
|
557 \end{center} |
|
558 |
|
559 \begin{itemize} |
|
560 \item by Jane Liu, 2000 |
|
561 \item {\it ``The job $J_l$ executes at its inherited |
|
562 priority until it releases $R$; at that time, the |
|
563 priority of $J_l$ returns to its priority |
|
564 at the time when it acquires the resource $R$.''}\medskip |
|
565 \item \small gives pseudo code and totally bogus data structures |
|
566 \item \small interesting part ``{\it left as an exercise}'' |
|
567 \end{itemize} |
|
568 |
|
569 \end{frame} |
|
570 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
571 |
|
572 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
573 \begin{frame}[c] |
|
574 |
|
575 \begin{center} |
|
576 \includegraphics[scale=0.15]{../pics/p1.pdf} |
|
577 \end{center} |
|
578 |
|
579 \begin{itemize} |
|
580 \item by Laplante and Ovaska, 2011 (\$113.76) |
|
581 \item \it ``when $[$the task$]$ exits the critical section that |
|
582 caused the block, it reverts to the priority it had |
|
583 when it entered that section'' |
|
584 \end{itemize} |
|
585 |
|
586 \end{frame} |
|
587 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
588 |
|
589 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
590 \begin{frame}[c] |
|
591 |
|
592 \begin{center} |
|
593 \includegraphics[scale=0.25]{../pics/p4.jpg} |
|
594 \end{center} |
|
595 |
|
596 \begin{itemize} |
|
597 \item by Silberschatz, Galvin, and Gagne, 2013 (OS-bible) |
|
598 \item \it ``Upon releasing the lock, the |
|
599 $[$low-priority$]$ thread will revert to |
|
600 its original priority.'' |
|
601 \end{itemize} |
|
602 |
|
603 \end{frame} |
|
604 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
605 |
|
606 |
|
607 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
608 \begin{frame}[c] |
|
609 \frametitle{Priority Scheduling} |
|
610 |
|
611 \begin{itemize} |
|
612 \item a scheduling algorithm that is widely used in real-time operating systems |
|
613 \item has been ``proved'' correct by hand in a paper in 1983 |
|
614 \item but this algorithm turned out to be incorrect, despite its ``proof''\bigskip\pause |
|
615 |
|
616 \item we used the corrected algorithm and then {\bf really} proved |
|
617 that it is correct |
|
618 |
|
619 \item we implemented this algorithm in a small OS called PINTOS |
|
620 (used for teaching at Stanford) |
|
621 |
|
622 \item our implementation was much more efficient than their |
|
623 reference implementation |
|
624 |
|
625 \end{itemize} |
|
626 |
|
627 \end{frame} |
|
628 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
629 |
|
630 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
631 |
|
632 \begin{frame}[c] |
|
633 \frametitle{Big Proofs in CS (1)} |
|
634 |
|
635 Formal proofs in CS sound like science fiction? |
|
636 |
|
637 \begin{itemize} |
|
638 \item in 2008, verification of a C-compiler |
|
639 \begin{itemize} |
218 \begin{itemize} |
640 \item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour'' |
219 \item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour'' |
641 \item is as good as \texttt{gcc -O1}, but much less buggy |
220 \item is as good as \texttt{gcc -O1}, but much, much less buggy |
642 \end{itemize} |
221 \end{itemize} |
643 \end{itemize} |
222 \end{itemize} |
644 |
223 |
645 \begin{center} |
224 \begin{center} |
646 \includegraphics[scale=0.12]{../pics/compcert.png} |
225 \includegraphics[scale=0.12]{../pics/compcert.png} |
648 |
227 |
649 \end{frame} |
228 \end{frame} |
650 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
229 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
651 |
230 |
652 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
231 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
653 % \begin{frame}[c] |
232 \begin{frame}[c] |
654 % \frametitle{Fuzzy Testing C-Compilers} |
233 \frametitle{Fuzzy Testing C-Compilers} |
655 |
234 |
656 % \begin{itemize} |
235 \begin{itemize} |
657 % \item tested GCC, LLVM and others by randomly generating |
236 \item tested GCC, LLVM and others by randomly generating |
658 % C-programs |
237 C-programs |
659 % \item found more than 300 bugs in GCC and also |
238 \item found more than 300 bugs in GCC and also |
660 % many in LLVM (some of them highest-level critical)\bigskip |
239 many in LLVM (some of them highest-level critical)\bigskip |
661 % \item about CompCert: |
240 \item about CompCert: |
662 |
241 |
663 % \begin{bubble}[10cm]\small ``The striking thing about our CompCert |
242 \begin{bubble}[10cm]\small ``The striking thing about our CompCert |
664 % results is that the middle-end bugs we found in all other |
243 results is that the middle-end bugs we found in all other |
665 % compilers are absent. As of early 2011, the under-development |
244 compilers are absent. As of early 2011, the under-development |
666 % version of CompCert is the only compiler we have tested for |
245 version of CompCert is the only compiler we have tested for |
667 % which Csmith cannot find wrong-code errors. This is not for |
246 which Csmith cannot find wrong-code errors. This is not for |
668 % lack of trying: we have devoted about six CPU-years to the |
247 lack of trying: we have devoted about six CPU-years to the |
669 % task.'' |
248 task.'' |
670 % \end{bubble} |
249 \end{bubble} |
671 % \end{itemize} |
|
672 |
|
673 % \end{frame} |
|
674 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
675 |
|
676 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
677 \begin{frame}[c] |
|
678 \frametitle{Big Proofs in CS (2)} |
|
679 |
|
680 \begin{itemize} |
|
681 \item in 2010, verification of a micro-kernel operating system (approximately 8700 loc) |
|
682 \begin{itemize} |
|
683 \item used in helicopters and mobile phones |
|
684 \item 200k loc of proof |
|
685 \item 25 - 30 person years |
|
686 \item found 160 bugs in the C code (144 by the proof) |
|
687 \end{itemize} |
|
688 \end{itemize} |
250 \end{itemize} |
689 |
251 |
690 \begin{bubble}[10cm]\small |
252 \end{frame} |
691 ``Real-world operating-system kernel with an end-to-end proof |
253 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
692 of implementation correctness and security enforcement'' |
|
693 \end{bubble}\bigskip\pause |
|
694 |
|
695 unhackable kernel (New Scientists, September 2015) |
|
696 \end{frame} |
|
697 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
698 |
|
699 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
700 \begin{frame}[c] |
|
701 \frametitle{Big Proofs in CS (3)} |
|
702 |
|
703 \begin{itemize} |
|
704 \item verified TLS implementation\medskip |
|
705 \item verified compilers (CompCert, CakeML)\medskip |
|
706 \item verified distributed systems (Verdi)\medskip |
|
707 \item verified OSes or OS components\\ |
|
708 (seL4, CertiKOS, \ldots)\bigskip\pause |
|
709 \item Infer static analyser developed by Facebook |
|
710 \end{itemize} |
|
711 |
|
712 \end{frame} |
|
713 |
|
714 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
715 \begin{frame}[c] |
|
716 \frametitle{How Did This Happen?} |
|
717 |
|
718 Lots of ways! |
|
719 |
|
720 \begin{itemize} |
|
721 \item better programming languages |
|
722 \begin{itemize} |
|
723 \item basic safety guarantees built in |
|
724 \item powerful mechanisms for abstraction and modularity |
|
725 \end{itemize} |
|
726 \item better software development methodology |
|
727 \item stable platforms and frameworks |
|
728 \item better use of specifications\medskip\\ |
|
729 \small If you want to build software that works or is secure, |
|
730 it is helpful to know what you mean by ``works'' and by ``is secure''! |
|
731 \end{itemize} |
|
732 |
|
733 \end{frame} |
|
734 |
|
735 |
|
736 |
|
737 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
738 \begin{frame}[c] |
|
739 \frametitle{Goal} |
|
740 |
|
741 Remember the Bridges example? |
|
742 |
|
743 \begin{itemize} |
|
744 \item Can we look at our programs and somehow ensure |
|
745 they are bug free/correct?\pause\bigskip |
|
746 |
|
747 \item Very hard: Anything interesting about programs is equivalent |
|
748 to the Halting Problem, which is undecidable.\pause\bigskip |
|
749 |
|
750 \item \alert{Solution:} We avoid this ``minor'' obstacle by |
|
751 being as close as possible of deciding the halting |
|
752 problem, without actually deciding the halting problem. |
|
753 \small$\quad\Rightarrow$ yes, no, don't know (static analysis) |
|
754 \end{itemize} |
|
755 |
|
756 \end{frame} |
|
757 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
758 |
|
759 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
760 \begin{frame}[c] |
|
761 \frametitle{What is Static Analysis?} |
|
762 |
|
763 \begin{center} |
|
764 \includegraphics[scale=0.4]{../pics/state.png} |
|
765 \end{center} |
|
766 |
|
767 \begin{itemize} |
|
768 \item depending on some initial input, a program |
|
769 (behaviour) will ``develop'' over time. |
|
770 \end{itemize} |
|
771 |
|
772 \end{frame} |
|
773 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
774 |
|
775 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
776 \begin{frame}[c] |
|
777 \frametitle{What is Static Analysis?} |
|
778 |
|
779 \begin{center} |
|
780 \includegraphics[scale=0.4]{../pics/state2.png} |
|
781 \end{center} |
|
782 |
|
783 \end{frame} |
|
784 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
785 |
|
786 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
787 \begin{frame}[c] |
|
788 \frametitle{What is Static Analysis?} |
|
789 |
|
790 \begin{center} |
|
791 \includegraphics[scale=0.4]{../pics/state3.jpg} |
|
792 \end{center} |
|
793 |
|
794 \end{frame} |
|
795 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
796 |
|
797 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
798 \begin{frame}[c] |
|
799 \frametitle{What is Static Analysis?} |
|
800 |
|
801 \begin{center} |
|
802 \includegraphics[scale=0.4]{../pics/state4.jpg} |
|
803 \end{center} |
|
804 |
|
805 \begin{itemize} |
|
806 \item to be avoided |
|
807 \end{itemize} |
|
808 |
|
809 \end{frame} |
|
810 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
811 |
|
812 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
813 \begin{frame}[c] |
|
814 \frametitle{What is Static Analysis?} |
|
815 |
|
816 \begin{center} |
|
817 \includegraphics[scale=0.4]{../pics/state5.png} |
|
818 \end{center} |
|
819 |
|
820 \begin{itemize} |
|
821 \item this needs more work |
|
822 \end{itemize} |
|
823 |
|
824 \end{frame} |
|
825 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
826 |
|
827 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
828 \begin{frame}[c] |
|
829 \frametitle{What is Static Analysis?} |
|
830 |
|
831 \begin{center} |
|
832 \includegraphics[scale=0.4]{../pics/state6.png} |
|
833 \end{center} |
|
834 |
|
835 \end{frame} |
|
836 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
837 |
|
838 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
839 \begin{frame}[c,fragile] |
|
840 \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm] |
|
841 Are Vars Definitely Initialised?\end{tabular}} |
|
842 |
|
843 Assuming \texttt{x} is initialised, what about \texttt{y}?\bigskip |
|
844 |
|
845 Prog.~1:\\ |
|
846 \begin{lstlisting}[numbers=none, |
|
847 basicstyle=\ttfamily, |
|
848 language=While,xleftmargin=3mm] |
|
849 if x < 1 then y := x else y := x + 1; |
|
850 y := y + 1 |
|
851 \end{lstlisting}\medskip |
|
852 |
|
853 Prog.~2:\\ |
|
854 \begin{lstlisting}[numbers=none, |
|
855 basicstyle=\ttfamily, |
|
856 language=While,xleftmargin=3mm] |
|
857 if x < x then y := y + 1 else y := x; |
|
858 y := y + 1 |
|
859 \end{lstlisting} |
|
860 |
|
861 \end{frame} |
|
862 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
863 |
|
864 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
865 \begin{frame}[c,fragile] |
|
866 \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm] |
|
867 Are Vars Definitely Initialised?\end{tabular}} |
|
868 |
|
869 What should the rules be for deciding when a |
|
870 variable is initialised?\bigskip\pause |
|
871 |
|
872 \begin{itemize} |
|
873 \item variable \texttt{x} is definitely initialized after |
|
874 \texttt{skip}\\ |
|
875 iff \texttt{x} is definitely initialized before \texttt{skip}. |
|
876 \end{itemize} |
|
877 |
|
878 \end{frame} |
|
879 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
880 |
|
881 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
882 \begin{frame}[c,fragile] |
|
883 % \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm] |
|
884 % Are Vars Definitely Initialised?\end{tabular}} |
|
885 |
|
886 $\bl{A}$ is the set of definitely defined variables: |
|
887 |
|
888 \begin{center} |
|
889 \begin{tabular}{c} |
|
890 \bl{\infer{\mbox{}}{A\;\texttt{skip}\;A}}\qquad |
|
891 \bl{\infer{vars(a) \subseteq A}{A\;\;(\texttt{x\,:=\,a})\;\;\{x\}\cup A}} |
|
892 \medskip\\\pause |
|
893 |
|
894 \bl{\infer{A_1\;s_1\;A_2\quad A_2\;s_2\;A_3}{A_1\;(s_1 ; s_2)\;A_3}} |
|
895 \medskip\\\pause |
|
896 |
|
897 \bl{\infer{vars(b)\subseteq A\quad A\;s_1\;A_1\quad A\;s_2\;A_2} |
|
898 {A\;(\texttt{if}\;b\;\texttt{then}\;s_1\;\texttt{else}\;s_2)\;A_1\cap A_2}} |
|
899 \medskip\\\pause |
|
900 |
|
901 \bl{\infer{vars(b)\subseteq A\quad A\;s\;A'} |
|
902 {A\;(\texttt{while}\;b\;\texttt{do}\;s)\;A}}\pause |
|
903 \end{tabular} |
|
904 \end{center} |
|
905 |
|
906 \hfill we start with $\bl{A = \{\}}$ |
|
907 \end{frame} |
|
908 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
909 |
|
910 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
911 \begin{frame}[fragile] |
|
912 \frametitle{\large Concrete Example: Sign-Analysis} |
|
913 \mbox{}\\[-20mm]\mbox{} |
|
914 |
|
915 \bl{\begin{plstx}[rhs style=,one per line] |
|
916 : \meta{Exp} ::= \meta{Exp} + \meta{Exp} |
|
917 | \meta{Exp} * \meta{Exp} |
|
918 | \meta{Exp} = \meta{Exp} |
|
919 | \meta{num} |
|
920 | \meta{var}\\ |
|
921 : \meta{Stmt} ::= \meta{label} : |
|
922 | \meta{var} := \meta{Exp} |
|
923 | \pcode{jmp?} \meta{Exp} \meta{label} |
|
924 | \pcode{goto} \meta{label}\\ |
|
925 : \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\ |
|
926 \end{plstx}} |
|
927 |
|
928 \begin{textblock}{0}(7.8,2.5) |
|
929 \small |
|
930 \begin{bubble}[5.6cm] |
|
931 \begin{lstlisting}[numbers=none, |
|
932 basicstyle=\ttfamily, |
|
933 language={},xleftmargin=3mm] |
|
934 a := 1 |
|
935 n := 5 |
|
936 top: jmp? n = 0 done |
|
937 a := a * n |
|
938 n := n + -1 |
|
939 goto top |
|
940 done: |
|
941 \end{lstlisting} |
|
942 \end{bubble} |
|
943 \end{textblock} |
|
944 |
|
945 \end{frame} |
|
946 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
947 |
|
948 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
949 \begin{frame}[fragile] |
|
950 \frametitle{\large Concrete Example: Sign-Analysis} |
|
951 \mbox{}\\[-20mm]\mbox{} |
|
952 |
|
953 \bl{\begin{plstx}[rhs style=,one per line] |
|
954 : \meta{Exp} ::= \meta{Exp} + \meta{Exp} |
|
955 | \meta{Exp} * \meta{Exp} |
|
956 | \meta{Exp} = \meta{Exp} |
|
957 | \meta{num} |
|
958 | \meta{var}\\ |
|
959 : \meta{Stmt} ::= \meta{label} : |
|
960 | \meta{var} := \meta{Exp} |
|
961 | \pcode{jmp?} \meta{Exp} \meta{label} |
|
962 | \pcode{goto} \meta{label}\\ |
|
963 : \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\ |
|
964 \end{plstx}} |
|
965 |
|
966 \begin{textblock}{0}(7.8,3.5) |
|
967 \small |
|
968 \begin{bubble}[5.6cm] |
|
969 \begin{lstlisting}[numbers=none, |
|
970 basicstyle=\ttfamily, |
|
971 language={},xleftmargin=3mm] |
|
972 n := 6 |
|
973 m1 := 0 |
|
974 m2 := 1 |
|
975 top: jmp? n = 0 done |
|
976 tmp := m2 |
|
977 m2 := m1 + m2 |
|
978 m1 := tmp |
|
979 n := n + -1 |
|
980 goto top |
|
981 done: |
|
982 \end{lstlisting} |
|
983 \end{bubble} |
|
984 \end{textblock} |
|
985 |
|
986 \end{frame} |
|
987 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
988 |
|
989 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
990 \begin{frame}[fragile] |
|
991 \frametitle{\large Concrete Example: Sign-Analysis} |
|
992 \mbox{}\\[-20mm]\mbox{} |
|
993 |
|
994 \bl{\begin{plstx}[rhs style=,one per line] |
|
995 : \meta{Exp} ::= \meta{Exp} + \meta{Exp} |
|
996 | \meta{Exp} * \meta{Exp} |
|
997 | \meta{Exp} = \meta{Exp} |
|
998 | \meta{num} |
|
999 | \meta{var}\\ |
|
1000 : \meta{Stmt} ::= \meta{label} : |
|
1001 | \meta{var} := \meta{Exp} |
|
1002 | \pcode{jmp?} \meta{Exp} \meta{label} |
|
1003 | \pcode{goto} \meta{label}\\ |
|
1004 : \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\ |
|
1005 \end{plstx}} |
|
1006 |
|
1007 \end{frame} |
|
1008 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1009 |
|
1010 |
|
1011 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1012 \begin{frame}[fragile] |
|
1013 \frametitle{Eval: An Interpreter} |
|
1014 \mbox{}\\[-14mm]\mbox{} |
|
1015 |
|
1016 \small |
|
1017 \begin{center} |
|
1018 \bl{\begin{tabular}{lcl} |
|
1019 $[n]_{env}$ & $\dn$ & $n$\\ |
|
1020 $[x]_{env}$ & $\dn$ & $env(x)$\\ |
|
1021 $[e_1 + e_2]_{env}$ & $\dn$ & $[e_1]_{env} + [e_2]_{env}$\\ |
|
1022 $[e_1 * e_2]_{env}$ & $\dn$ & $[e_1]_{env} * [e_2]_{env}$\\ |
|
1023 $[e_1 = e_2]_{env}$ & $\dn$ & |
|
1024 $\begin{cases} |
|
1025 1 & \text{if}\quad[e_1]_{env} = [e_2]_{env}\\ |
|
1026 0 & \text{otherwise} |
|
1027 \end{cases}$\\ |
|
1028 \end{tabular}} |
|
1029 \end{center} |
|
1030 |
|
1031 \footnotesize |
|
1032 \begin{lstlisting}[numbers=none,xleftmargin=-5mm] |
|
1033 def eval_exp(e: Exp, env: Env) : Int = e match { |
|
1034 case Num(n) => n |
|
1035 case Var(x) => env(x) |
|
1036 case Plus(e1, e2) => eval_exp(e1, env) + eval_exp(e2, env) |
|
1037 case Times(e1, e2) => eval_exp(e1, env) * eval_exp(e2, env) |
|
1038 case Equ(e1, e2) => |
|
1039 if (eval_exp(e1, env) == eval_exp(e2, env)) 1 else 0 |
|
1040 } |
|
1041 \end{lstlisting} |
|
1042 |
|
1043 \end{frame} |
|
1044 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1045 |
|
1046 |
|
1047 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1048 \begin{frame}[fragile] |
|
1049 \small |
|
1050 A program |
|
1051 \begin{bubble}[6cm]\footnotesize |
|
1052 \begin{lstlisting}[numbers=none, |
|
1053 language={}, |
|
1054 basicstyle=\ttfamily, |
|
1055 xleftmargin=1mm] |
|
1056 a := 1 |
|
1057 n := 5 |
|
1058 top: jmp? n = 0 done |
|
1059 a := a * n |
|
1060 n := n + -1 |
|
1061 goto top |
|
1062 done: |
|
1063 \end{lstlisting} |
|
1064 \end{bubble} |
|
1065 |
|
1066 The \emph{snippets} of the program: |
|
1067 |
|
1068 \footnotesize |
|
1069 \begin{columns} |
|
1070 \begin{column}[t]{5cm} |
|
1071 \begin{bubble}[4.5cm] |
|
1072 \begin{lstlisting}[numbers=none, |
|
1073 basicstyle=\ttfamily, |
|
1074 language={},xleftmargin=1mm] |
|
1075 "" a := 1 |
|
1076 n := 5 |
|
1077 top: jmp? n = 0 done |
|
1078 a := a * n |
|
1079 n := n + -1 |
|
1080 goto top |
|
1081 done: |
|
1082 \end{lstlisting} |
|
1083 \end{bubble} |
|
1084 \end{column} |
|
1085 \begin{column}[t]{5cm} |
|
1086 \begin{bubble}[4.5cm] |
|
1087 \begin{lstlisting}[numbers=none, |
|
1088 basicstyle=\ttfamily, |
|
1089 language={},xleftmargin=1mm] |
|
1090 top: jmp? n = 0 done |
|
1091 a := a * n |
|
1092 n := n + -1 |
|
1093 goto top |
|
1094 done: |
|
1095 \end{lstlisting} |
|
1096 \end{bubble} |
|
1097 \end{column} |
|
1098 \begin{column}[t]{2cm} |
|
1099 \begin{bubble}[1.1cm] |
|
1100 \begin{lstlisting}[numbers=none, |
|
1101 basicstyle=\ttfamily, |
|
1102 language={},xleftmargin=1mm] |
|
1103 done: |
|
1104 \end{lstlisting} |
|
1105 \end{bubble} |
|
1106 \end{column} |
|
1107 \end{columns} |
|
1108 |
|
1109 \end{frame} |
|
1110 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1111 |
|
1112 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1113 \begin{frame}[fragile] |
|
1114 \frametitle{Eval for Stmts} |
|
1115 \mbox{}\\[-12mm]\mbox{} |
|
1116 |
|
1117 Let \bl{$sn$} be the snippets of a program |
|
1118 |
|
1119 \small |
|
1120 \begin{center} |
|
1121 \bl{\begin{tabular}{lcl} |
|
1122 $[\texttt{nil}]_{env}$ & $\dn$ & $env$\medskip\\ |
|
1123 $[\texttt{Label}(l:)::rest]_{env}$ & $\dn$ & $[rest]_{env}$\medskip\\ |
|
1124 $[x \,\texttt{:=}\, a::rest]_{env}$ & $\dn$ & |
|
1125 $[rest]_{(env[x:= [a]_{env}])}$\medskip\\ |
|
1126 $[\texttt{jmp?}\;b\;l::rest]_{env}$ & $\dn$ & |
|
1127 $\begin{cases} |
|
1128 [sn(l)]_{env} & \text{if}\quad[b]_{env} = true\\ |
|
1129 [rest]_{env} & \text{otherwise} |
|
1130 \end{cases}$\medskip\\ |
|
1131 $[\texttt{goto}\;l::rest]_{env}$ & $\dn$ & $[sn(l)]_{env}$\\ |
|
1132 \end{tabular}} |
|
1133 \end{center}\bigskip |
|
1134 |
|
1135 Start with \bl{$[sn(\mbox{\code{""}})]_{\varnothing}$} |
|
1136 |
|
1137 \end{frame} |
|
1138 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1139 |
|
1140 |
|
1141 |
|
1142 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1143 \begin{frame}[fragile] |
|
1144 \frametitle{Eval in Code} |
|
1145 |
|
1146 \footnotesize |
|
1147 \begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm] |
|
1148 def eval(sn: Snips) : Env = { |
|
1149 def eval_stmts(sts: Stmts, env: Env) : Env = sts match { |
|
1150 case Nil => env |
|
1151 |
|
1152 case Label(l)::rest => eval_stmts(rest, env) |
|
1153 |
|
1154 case Assign(x, e)::rest => |
|
1155 eval_stmts(rest, env + (x -> eval_exp(e, env))) |
|
1156 |
|
1157 case Jmp(b, l)::rest => |
|
1158 if (eval_exp(b, env) == 1) eval_stmts(sn(l), env) |
|
1159 else eval_stmts(rest, env) |
|
1160 |
|
1161 case Goto(l)::rest => eval_stmts(sn(l), env) |
|
1162 } |
|
1163 |
|
1164 eval_stmts(sn(""), Map()) |
|
1165 } |
|
1166 \end{lstlisting} |
|
1167 |
|
1168 \end{frame} |
|
1169 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1170 |
|
1171 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1172 \begin{frame}[fragile] |
|
1173 \frametitle{The Idea of Static Analysis} |
|
1174 \small |
|
1175 \mbox{}\bigskip\\ |
|
1176 |
|
1177 \begin{columns} |
|
1178 \begin{column}{5cm} |
|
1179 \begin{bubble}[4.5cm]\footnotesize |
|
1180 \begin{lstlisting}[numbers=none, |
|
1181 language={}, |
|
1182 basicstyle=\ttfamily, |
|
1183 xleftmargin=1mm] |
|
1184 a := 1 |
|
1185 n := 5 |
|
1186 top: jmp? n = 0 done |
|
1187 a := a * n |
|
1188 n := n + -1 |
|
1189 goto top |
|
1190 done: |
|
1191 \end{lstlisting} |
|
1192 \end{bubble} |
|
1193 \end{column} |
|
1194 |
|
1195 \begin{column}{1cm} |
|
1196 \raisebox{-20mm}{\LARGE\bf$\Rightarrow$} |
|
1197 \end{column} |
|
1198 \begin{column}{6cm} |
|
1199 \begin{bubble}[4.7cm]\footnotesize |
|
1200 \begin{lstlisting}[numbers=none, |
|
1201 language={}, |
|
1202 basicstyle=\ttfamily, |
|
1203 xleftmargin=1mm, |
|
1204 escapeinside={(*}{*)}] |
|
1205 a := (*\hl{'+'}*) |
|
1206 n := (*\hl{'+'}*) |
|
1207 top: jmp? n = (*\hl{'0'}*) done |
|
1208 a := a * n |
|
1209 n := n + (*\hl{'-'}*) |
|
1210 goto top |
|
1211 done: |
|
1212 \end{lstlisting} |
|
1213 \end{bubble} |
|
1214 \end{column} |
|
1215 \end{columns}\bigskip\bigskip |
|
1216 |
|
1217 Replace all constants and variables by either |
|
1218 \pcode{+}, \pcode{-} or \pcode{0}. What we want to find out |
|
1219 is what the sign of \texttt{a} and \texttt{n} is (they should |
|
1220 always positive). |
|
1221 |
|
1222 \end{frame} |
|
1223 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1224 |
|
1225 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1226 \begin{frame}[c] |
|
1227 \frametitle{Sign Analysis?} |
|
1228 |
|
1229 |
|
1230 \begin{columns} |
|
1231 \begin{column}{3cm} |
|
1232 \begin{tabular}{cc|l} |
|
1233 $e_1$ & $e_2$ & $e_1 + e_2$\\\hline{} |
|
1234 - & - & -\\ |
|
1235 - & 0 & -\\ |
|
1236 - & + & -, 0, +\\ |
|
1237 0 & $x$ & $x$\\ |
|
1238 + & - & -, 0, +\\ |
|
1239 + & 0 & +\\ |
|
1240 + & + & +\\ |
|
1241 \end{tabular} |
|
1242 \end{column} |
|
1243 |
|
1244 \begin{column}{3cm} |
|
1245 \begin{tabular}{cc|l} |
|
1246 $e_1$ & $e_2$ & $e_1 * e_2$\\\hline{} |
|
1247 - & - & +\\ |
|
1248 - & 0 & 0\\ |
|
1249 - & + & -\\ |
|
1250 0 & $x$ & 0\\ |
|
1251 + & - & -\\ |
|
1252 + & 0 & 0\\ |
|
1253 + & + & +\\ |
|
1254 \end{tabular} |
|
1255 \end{column} |
|
1256 \end{columns} |
|
1257 |
|
1258 \end{frame} |
|
1259 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1260 |
|
1261 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1262 \begin{frame}[fragile] |
|
1263 \mbox{}\\[-13mm]\mbox{} |
|
1264 |
|
1265 \small |
|
1266 \begin{center} |
|
1267 \bl{\begin{tabular}{lcl} |
|
1268 $[n]_{aenv}$ & $\dn$ & |
|
1269 $\begin{cases} |
|
1270 \{+\} & \text{if}\; n > 0\\ |
|
1271 \{-\} & \text{if}\; n < 0\\ |
|
1272 \{0\} & \text{if}\; n = 0 |
|
1273 \end{cases}$\\ |
|
1274 $[x]_{aenv}$ & $\dn$ & $aenv(x)$\\ |
|
1275 $[e_1 + e_2]_{aenv}$ & $\dn$ & $[e_1]_{aenv} \oplus [e_2]_{aenv}$\\ |
|
1276 $[e_1 * e_2]_{aenv}$ & $\dn$ & $[e_1]_{aenv} \otimes [e_2]_{aenv}$\\ |
|
1277 $[e_1 = e_2]_{aenv}$ & $\dn$ & $\{0, +\}$\\ |
|
1278 \end{tabular}} |
|
1279 \end{center} |
|
1280 |
|
1281 \scriptsize |
|
1282 \begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm] |
|
1283 def aeval_exp(e: Exp, aenv: AEnv) : Set[Abst] = e match { |
|
1284 case Num(0) => Set(Zero) |
|
1285 case Num(n) if (n < 0) => Set(Neg) |
|
1286 case Num(n) if (n > 0) => Set(Pos) |
|
1287 case Var(x) => aenv(x) |
|
1288 case Plus(e1, e2) => |
|
1289 aplus(aeval_exp(e1, aenv), aeval_exp(e2, aenv)) |
|
1290 case Times(e1, e2) => |
|
1291 atimes(aeval_exp(e1, aenv), aeval_exp(e2, aenv)) |
|
1292 case Equ(e1, e2) => Set(Zero, Pos) |
|
1293 } |
|
1294 \end{lstlisting} |
|
1295 |
|
1296 \end{frame} |
|
1297 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1298 |
|
1299 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1300 \begin{frame}[fragile] |
|
1301 \frametitle{AEval for Stmts} |
|
1302 \mbox{}\\[-12mm]\mbox{} |
|
1303 |
|
1304 Let \bl{$sn$} be the snippets of a program |
|
1305 |
|
1306 \small |
|
1307 \begin{center} |
|
1308 \bl{\begin{tabular}{lcl} |
|
1309 $[\texttt{nil}]_{aenv}$ & $\to$ & $(\texttt{nil},aenv)$\medskip\\ |
|
1310 $[\texttt{Label}(l:)::rest]_{aenv}$ & $\to$ & $(rest, aenv)$\medskip\\ |
|
1311 $[x \,\texttt{:=}\, e::rest]_{aenv}$ & $\to$ & |
|
1312 $(rest, aenv[x:= [e]_{aenv}])$\medskip\\ |
|
1313 $[\texttt{jmp?}\;e\;l::rest]_{aenv}$ & $\to$ & |
|
1314 $(sn(l),aenv)$ \textcolor{black}{and} $(rest, aenv)$\medskip\\ |
|
1315 $[\texttt{goto}\;l::rest]_{aenv}$ & $\to$ & $(sn(l), aenv)$\\ |
|
1316 \end{tabular}} |
|
1317 \end{center}\bigskip |
|
1318 |
|
1319 Start with \bl{$[sn(\mbox{\code{""}})]_{\varnothing}$}, try to |
|
1320 reach all \emph{states} you can find (until a fix point is reached). |
|
1321 |
|
1322 Check whether there are only $aenv$ in the final states that have |
|
1323 your property. |
|
1324 \end{frame} |
|
1325 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1326 |
|
1327 |
|
1328 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1329 \begin{frame}[c] |
|
1330 \frametitle{Sign Analysis} |
|
1331 |
|
1332 \begin{itemize} |
|
1333 \item We want to find out whether \texttt{a} and \texttt{n} |
|
1334 are always positive?\medskip |
|
1335 \item After a few optimisations, we can indeed find this out. |
|
1336 \begin{itemize} |
|
1337 \item equal signs return only \texttt{+} or \texttt{0} |
|
1338 \item branch into only one direction if you know |
|
1339 \item if $x$ is \texttt{+}, then $x + \texttt{-1}$ |
|
1340 cannot be negative |
|
1341 \end{itemize}\bigskip |
|
1342 |
|
1343 \item What is this good for? Well, you do not need |
|
1344 underflow checks (in order to prevent buffer-overflow |
|
1345 attacks). In general this technique is used to make sure |
|
1346 keys stay secret. |
|
1347 \end{itemize} |
|
1348 |
|
1349 \end{frame} |
|
1350 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1351 |
|
1352 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1353 \begin{frame}[c] |
|
1354 \frametitle{Take Home Points} |
|
1355 |
|
1356 \begin{itemize} |
|
1357 \item While testing is important, it does not show the |
|
1358 absence of bugs/vulnerabilities.\medskip |
|
1359 \item More and more we need (formal) proofs that show |
|
1360 a program is bug free.\medskip |
|
1361 |
|
1362 \item Static analysis is more and more employed nowadays |
|
1363 in order to automatically hunt for bugs. |
|
1364 \end{itemize} |
|
1365 |
|
1366 \end{frame} |
|
1367 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1368 |
|
1369 |
|
1370 |
254 |
1371 \end{document} |
255 \end{document} |
1372 |
|
1373 |
256 |
1374 %%% Local Variables: |
257 %%% Local Variables: |
1375 %%% mode: latex |
258 %%% mode: latex |
1376 %%% TeX-master: t |
259 %%% TeX-master: t |
1377 %%% End: |
260 %%% End: |