ࡱ> x(@   Jhttp://research.micsoft.com/specsharpJhttp://research.micsoft.com/specsharpF/ 0|DArialngsode MS``0 T0"DArial Unicode MS`0 T0" DCalibriicode MS`0 T0"0DSymbolicode MS`0 T0@DWingdingsode MS`0 T0 B . @n?" dd@  @@``  #         - D1H         &1H1 *"           ) 1<    0 3f3@ʚ;ʚ;<4dddd,#0,g4\d\d0 T0ppp@  <42d2d,O$0`)___PPT12 %0___PPT10 ``6___PPT9{?  O  Wa9Lecture 5 Towards a Verifying Compiler: Multithreading: :$ : Z Wolfram Schulte Microsoft Research Formal Methods 2006 Race Conditions, Locks, Deadlocks, Invariants, Locklevels Access Sets _____________ Joint work with Rustan Leino, Mike Barnett, Manuel Fhndrich, Herman Venter, Rob DeLine, Wolfram Schulte (all MSR), and Peter Mller (ETH), Bart Jacobs (KU Leuven) and Bor-Yuh Evan Chung (Berkley) . : PGPP P P)I4"J " H$  2   R     '  $   %Review: Pure Methods and Model Fields&&$ & 3Data abstraction is crucial to express functional correctness properties Verification methodology for model fields Model fields are reduced to ordinary fields with automatic updates Verification challenges for model fields and pure methods Consistency Weak purity Heap dependence (and frame properties) J*D:AJ*D3:A3 4 Multi-threading  JData race prevention Invariants and ownership trees Deadlock prevention (J5 K Multithreading  Multiple threads running in parallel, reading and writing shared data A data race occurs when a shared variable is written by one thread and concurrently read or written by another thread How to guarantee that there are no data races? TFI 3l0    class Counter { int dangerous; void Inc() { int tmp = dangerous; dangerous = tmp + 1; } } Counter ct = new Counter(); new Thread(ct.Inc).Start(); new Thread(ct.Inc).Start(); // What is the value of // ct.dangerous after both // threads have terminated?|  UV        2   #   + Mutexes: Avoiding Races  Mutual exclusion for shared objects is provided via locks Locks can be obtained using a lock block. A thread may enter a lock (o) block only if no other thread is executing inside a lock (o) block; else, the thread waits When a thread holds a lock on object o, C#/Java do prevent other threads from locking o but do not prevent other threads from accessing o s fieldsc3f 3f3f 3f!3f3f,63f&g   !Program Method for Avoiding Races""$ " Our program rules enforce that a thread t can only access a field of object o if o is either thread local or t has locked o We model accessibility using access sets: A thread s access set consists of all objects it has created but not shared yet or whose lock it holds. Threads are only allowed to access fields of objects in their corresponding access set Our program rules prevent data races by ensuring that access sets of different threads never intersect.h 3f3f#3f3f3f3f3f3f 3f3f3f 3f03f  !Annotations Needed to Avoid Races""$ " FThreads have access sets t.A is a new ghost field in each thread t describing the set of accessible objects Objects can be shared o.shared is a new boolean ghost field in each object o share(o) is a new operation that shares an unshared o Fields can be declared to be shared Shared fields can only be assigned shared objects. Sm$4N..#3f -  t  f        Object Life Cycle  Verification via Access Sets  Tr[[o = new C();]] = & o.shared:= false; tid.A[o]:= true Tr[[x = o.f;]] = & assert tid.A[o]; x :=o.f; Tr[[o.f = x;]] = & assert tid.A[o]; if (f is declared shared) assert x.shared; o.f :=x;  ZZ3                     *      Tr[[share(o)]] = & assert tid.A[o]; assert ! o.shared; o.shared :=true; tid.A[o] :=false; Tr[[lock (o) S ]] = & assert ! tid.A[o]; assert o.shared; havoc o.*; tid.A[o]:=true; Tr[[S]]; tid.A[o]:= false2Z 8  3f                            A Note on havoc in the Lock Rule&!  ! When a thread (re) acquires o, o might have been changed by another thread. int x; lock (o) { x = o.f; } lock (o) { assert x == o.f; // fails } So we have to  forget all knowledge about o s fields . We do so by assigning an arbitrary value to all of o s field, expressed as havoc o.* MJM   M      :  =  @ Example for Data Race Freedom   Counter ct = new Counter(); share(ct); new Thread(delegate () { lock (ct) ct.Inc(); }).Start(); new Thread(delegate () { lock (ct) ct.Inc(); }).Start();  3f333fC           Example for Data Race Freedom  4class Session { shared Counter ct ; int id; Session(Counter ct , int id) requires ct.shared; ensures tid.A[this] '" ! this.shared; { this.ct=ct; this.id=id; } void Run() requires tid.A[this]; { for (; ; ) lock (this.ct) this.ct.Inc(); } }2Z 3>3f 3f3f 3f% 3f3f**(                    !             // thread t0 Counter ct = new Counter(); share(ct); Session s1 =new Session(ct,1); Session s2 =new Session(ct,2); // transfers s1 to t1 t1 = new Thread(s1.Run); // transfers s2 to t2 t2 = new Thread(s2.Run); t1.Start(); t2.Start(); PZZZ  3f -Cx                   Soundness  Theorem " threads t1,t2 :: t1t2 t1.A t2.A = " object o, thread t :: o.shared && o " t.A t holds o s lock Proof sketch for Theorem new share (o) Entry into lock (o) Exit from lock (o) Corollary Valid programs don t have data races  ZZ5ZZZ Z&Z ( " 1  ZM        Multi-threading  JData race prevention Invariants and ownership trees Deadlock prevention 0J  K Invariants and Concurrency  Invariants, whether over a single object or over an ownership tree, can be protected via a single lock (coarse grained locking) For sharing and locking require an object o to be valid when o becomes free ensures o s invariant on entry to its locked state For owned objects require that commited objects are unaccessable, but unpack(o) adds o s owned objects to the thread s access set pack(o) deletes o s owned objects from the thread s access set i4| 3A33"354 39  I          *     - $Verifying Multi-threaded Pack/Unpack%%$ % Tr[[ pack o;]] = assert tid.A[o]; assert ! o.inv; assert "c: c.owner = o tid.A[c] '" c.inv; foreach (c | c.owner = o) { tid.A[c] := false; } assert Inv( o ); o.inv := true; ZZ   3f3f3f3f3f"3f;3f3f 3f3f                   +     Tr[[unpack o;]] = assert tid.A[o]; assert o.inv; foreach (c | c.owner = o) { tid.A[c] := true; } o.inv := false; ZZ 33f3f                  Ownership: Verifying Lock Blocks!!$ ! Finally, when locking we also have to  forget the knowledge about owned objects Tr[[lock (o) S; ]] = assert o.shared; assert ! tid.A[o]; foreach (p | !tid.A[p]) havoc p.*; tid.A[o]:=true; Tr[[S]] ; tid.A[o]:= false; hQ  &3f3fR                    Outline of the talk  GData race prevention Invariants and ownership trees Deadlock preventionH4 H Multi-threading  JData race prevention Invariants and ownership trees Deadlock prevention 0J  K Concurrency: Deadlocks  A deadlock occurs when a set of threads each wait for a mutex (i.e shared object) that another thread holds Methodology: partial order over all shared objects in each thread, acquire shared objects in descending order lZZ ZaZZ3fp&3+3@8       Dining Philosophers L1 has F1, waits for F2 L2 has F2, waits for F3 L3 has F3, waits for F1 &iZM i %Annotations Needed to Avoid Deadlocks&&$ & xWe construct a partial order on shared objects, denoted by z". When o is shared, we add edges to the partial order as specified in the share command s where clause. (Specified lower bounds have to be less than specified upper bounds) Each thread has a new ghost field lockstack, holding the set of acquired locks@fGP;3f$3f3fK P" 3#&   $ -Verification via Lock Ordering and Lockstacks..$&#    RTr[[share o where p z" o && o z" q;]] = assert o tid.A; assert ! o.shared; tid.A[o] := false; o.shared := true; assert p z" q; assume p z" o && o z" q; ~+ ~    8 3$3 $33$3  3$$$3((3((3f((   /         7  Tr[[lock (o) S ]] = assert o.shared; assert tid.lockstack != empty o z" tid.lockstack.top(); tid.lockStack.push(o); foreach (p | !tid.A[p]) havoc p.*; tid.A[o]:=true; Tr[[S]] ; tid.A[o]:= false; tid.lockstack.pop(o);" 3f3f3f$3/3f3f                          %Example: Deadlock Avoidance (contd.) &&$ &  f1 = new Fork(); share f1; f2 = new Fork(); share f2 where f1 z" f2; f3 = new Fork(); share f3 where f2 z" f3 ; P1 = new Thread( delegate() { lock (f2) { lock (f1) { /*eat*/ }}}); P1.Start(); P2 = new Thread( delegate() { lock (f3) { lock (f2) {/*eat*/ }}}); P2.Start(); P3 = new Thread( delegate() { lock (f3) { lock (f1) {/*eat*/ }}}); P3.Start(); `g        3f 3f3f  3f 3f3f  3f 3f3f g  Conclusion  Clients can reason entirely as if world was single-threaded for non-shared objects Supports caller-side locking and callee-side locking Deadlocks are prevented by partially ordering shared objects&t  K The End (for now) 4     Thank you! $  h 0` 33` Sf3f` 33g` f` www3PP` ZXdbmo` \ғ3y`Ӣ` 3f3ff` 3f3FKf` hk]wwwfܹ` ff>>\`Y{ff` R>&- {p_/̴>?" dd(3fx?" dd  " @ ` n?" dd@   @@``@n?" dd@  @@``PR    @ ` `p>>aN0  (     T0 ?Rectangle 3073" `} 0  X Click to edit Master title style!! F  NP0 ?Rectangle 3074" ` 0  RClick to edit Master text styles Second level Third level Fourth level Fifth level!    S   N0 ?Rectangle 3075"^ ` 0  Z F     N3 ?Rectangle 3076"^  0  |* C   _   Nh0 ?Rectangle 1029#"A5PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!$K drs/shapexml.xmlVn6}/Zx-ɗ* ;m70eH'EgHIE~G&9sf̡>92 c+2|Y$TJ33bu\\j%24r/m"Uvdl\3vm5t#Jmjh+qjMxuk^)v gjln0QULk9@8n32ֶ* DajPjbj~^X\Bl"ݮF՞3' C>ܼdm}zSwN*|r(M}~NIeҳ v08(dž4!ǎ0tB;cW?WD2fZ-ϭJVR_T;36rQARrn@Y,rQʝY>8{&sZVE~]$ꌍbt7hy0bע`Ax%d'J+wY堎1p.( uЈsFlyFJniP P~u?H`^^pUƨgneXtOЙqS ^&4فjf^`Jse-!"-v*Ggm(Eu3fuZw()Ӝ]IA8$Vy_J(. %'Z^ia'H GKhGq N6w3n:m^\$_i{IV5IraЕjWIȘPopB^EH3Rz-mtG'YidE5~ma.&TA(O}7>Q GE5UۈPk;E"&I8Si*pПt=/ jfr|{/PK!Bn" drs/downrev.xmlD]K0CdZ!ls]޾6&I xy8<3_Z4unD NND΃PhC9$t:(0K}Pr Ԩw6VTX[Ut،TAÄ_%c8Ig4>xv}]6yxsoaZU ˆ_&AeKh9a.~PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!$K drs/shapexml.xmlPK-!Bn" drs/downrev.xmlPK*^ ` 3  *  G   H  0޽h ? 3380___PPT10..f#PK!(b[Content_Types].xmln0 EAkP }l} m $_tI$svs^챐KkH$Q -G$oo1# ɩ5 J# \Qg0?0omRo?Y8 Jm i|TX+N3tr@9>?4 ΠMfrAsѺo_p?yjŝ & Xg3PK!*8 _rels/.rels 0DnzЃXmlo0of5OIw AN{cݠv=m 838yG 6U} ShLq`L)d=Ҍ\@.;3, ;$e͂): vq}j:zɥ'k茜(f,ƁXA6\m>PK!`.Xޏ$!drs/slideMasters/slideMaster1.xmlMr0 cV1oz`iYq+9Qkl  %Tpo\H EhB7 !IH` ݋4=>Ox7BZ{IR+"˷J@kWX]Mi"I~뮞^wa/ sBug\djV{a7UZp>!_5|e~sM ҠSo}WՂCN| <p{/L]V`=n; ʝJҤj>Wn+ orAr]hM1ѝbg-_:G, ޲xHT1@el+b-R2td۩w 2YjŹ1l`MM; [#kQ\H %}񲵗U.dEG_h PK-!(b[Content_Types].xmlPK-!*8 *_rels/.relsPK-!`.Xޏ$!drs/slideMasters/slideMaster1.xmlPK.PK![Content_Types].xmlj0Eжr(΢Iw},-j4 wP-t#bΙ{UTU^hd}㨫)*1P' ^W0)T9<l#$yi};~@(Hu* Dנz/0ǰ $ X3aZ,D0j~3߶b~i>3\`?/[G\!-Rk.sԻ..a濭?PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK!ŖL=7theme/theme/theme1.xml[[6~L{c ÙdiL;9YcCﻺadlɡIڞIdyZIZq^|(iUї/ ]Kˤ~ZrL7zY%kj=kb$Ѝ1-]Up b[OP,LpRJ|QV&ߗ .`mHGRD}z7ڒj~Idzݠ/}qr@}q9.}oE;s Q$0Ae{B9m$~k`47 j /YO5|Q${wfdF/Siť;]UzQ | VQ:9wU@|(pZޚu bKqu%Y/;嬺O`TL$3E~):ɦ*-N;C1&In_cڿ6{arpF;V |Q7eȵlpڲnN 1ELZ?o%S[RӨHS {8tv aDTb$HdYBY6eC&/Ñ93G\VGIἯn.%v:9΢>mtZ|uޔ{]im?iŇ ͷ!Ӏ5ey8fC,"<n I?\4eGC6oڍ]c0%Y&[b=2d}Hkmn 1TCڢk`\ g rQ|_knLZ}:i:MetcZ[F cz7GkK}!pHhY6~LZ/[x"xܷdxܓܥ$)8t$4=B!qBF3&d4"lly ]`4"(rft'T/qtyxN=BMQ@qi`NSbzĸQ_4!Ɗcdel v`AhQft9L8jNքo}r}i?)=;~t3II5ȤXfYO'cKȬDJآRN^=ъH16F-΂C {` XacRdC|ƗF~ʊO(!yw(eo_$CQ"Yv};k݆U2gZ@%\>4XL4I bzC77K`2)"6K =D9@ <_ x=6[CqYw`dճaw d6 %l(t:a5lGR!&lrvO5W2|YsI.nQ~6lGlجXFZ };Gb<66ͤ6fDf* dC-K `o;66o|gywϟਐ)z6OW)6NP6p |졔tm|?p%lY+I\z6aC$@$@$'P4`kwWac*Z.M"H^/ E ^{oI~/MlT&L֯:-48l"7ʦ%i[ظWacUf ;Qڻ9bYҥd#l|#eTV!kӭ8lƒLjlg*lKܜ#?H8y93mb+z%[S ;'qU GOmל JXh#l g%{ |q\'#- 2=B7t^ۄ, N~ gE&t-" nPK!M[Content_Types].xml|N0 EHC-jaj; +,Kq:=ig ,?ϵYD&oDzCwO-gkcg$./XQ{jsԈHt䒦AFP0skfx(壓8?.C(ũ{R(Mb˳7{-IF#{_R'dK0FFjr'"&@_'PK!p8ܾ8 _rels/.rels 0Dnz x%ٶ6 (тqLݾQ(NAU ioo'tGHL m^W16 AJMȅ8a22~`Or[;,lij@搛}YMGBh ]pϔ{J Loc!"rPK!};7!drs/slideLayouts/slideLayout1.xmlݎ +OUUVv{@1b@@\{vM# 101aq֊4yiN'M)nI7W_()ŒjCoV?,lUyf$ْV!<,M59Xn]Z(HCq(nVyx&WDgCTpL붝vfbVUpOhA,z"=6!ރiگ,&j F|vj,&F; U4NW%D5'O06eL1 YTnSjb|YqSI7^p5%fB5O#>LؽDOV5}lRxd,c)-_PK-!M[Content_Types].xmlPK-!p8ܾ8 ._rels/.relsPK-!};7!drs/slideLayouts/slideLayout1.xmlPKUPK!M[Content_Types].xml|N0 EHC-jaj; +,Kq:=ig ,?ϵYD&oDzCwO-gkcg$./XQ{jsԈHt䒦AFP0skfx(壓8?.C(ũ{R(Mb˳7{-IF#{_R'dK0FFjr'"&@_'PK!p8ܾ8 _rels/.rels 0Dnz x%ٶ6 (тqLݾQ(NAU ioo'tGHL m^W16 AJMȅ8a22~`Or[;,lij@搛}YMGBh ]pϔ{J Loc!"rPK!M/"N!drs/slideLayouts/slideLayout1.xmlXr6}L׎#Swk,gbn38- ,{v td/,g/]464>qJ4~{6^ k9 u~bbj& DLõsŤӱZf~ &桳2 Йtχ^'=9!O4&ڕ0F*᠀]Њc #-`xs4߅ -& 01Oc12xJ:݄elqo$ibnxvntEP"/Ưbt?THbKLvu)&I3=ILq9׳+W;P(5Qnb- D{JQ<~Ρ'_m+0ҙuPߥNI/W.=*y6.D4vǠ.4 af0zc>B!%t1q|L&]3N-tA%me=+㭊p@!d%o/{yk l*Aq)EyQi<_ul6..Ca1]+J[{mv`@崓܊ gEӜ;Ѡ4EoQD &\Bđ0x2,la>k; /~sx1͕ekG8p. fzQ^+d̘f^!Iѐx!3Q^Kd1 K(/.| ^xq,[xQoQwA= xAp,p xa tCBϞ;AeB8 ^4щN!fbVÖ 79q} @{\ uE y3}my}⤻]kdPt (Is[[֐ɡ,e%>%Hm܆_]nnqD/7_Arf]# Γz5FPydimT@%PP{a2LF 4b)%z)J_ߩEůduRks Y:M36W&X>JQ%&Bkk$qfZ I&]eL{cn(?fzp-gQbA%(b{[ju\lb#[loS:k_ws/1JM)Tu>U+jS5e*{l9Z 鸦-L IFrCɡPVyN,]@FTZh-χ4/PK-!M[Content_Types].xmlPK-!p8ܾ8 ._rels/.relsPK-!M/"N!drs/slideLayouts/slideLayout1.xmlPKvPK!M[Content_Types].xml|N0 EHC-jaj; +,Kq:=ig ,?ϵYD&oDzCwO-gkcg$./XQ{jsԈHt䒦AFP0skfx(壓8?.C(ũ{R(Mb˳7{-IF#{_R'dK0FFjr'"&@_'PK!p8ܾ8 _rels/.rels 0Dnz x%ٶ6 (тqLݾQ(NAU ioo'tGHL m^W16 AJMȅ8a22~`Or[;,lij@搛}YMGBh ]pϔ{J Loc!"rPK!%,% N !drs/slideLayouts/slideLayout1.xmlWݎ8_i} ! 0@LU>I$[ǎ}=c&2J{s|;';RELx\>TKi;zOB4)]u:5Y*ڼ5x(W+>Q4h)A am2{ЎF1N5hn<[=V]7Jj8,7<bj0Xls"hG bA1fbe(R憪Ff 0?z&Z1!Ehdn2{͊gY z7My;κ5#+Xz' ~{Γ }]~]jZ{i񍍩78l8&hb(b"IzTDt_$NiFڍ 9oZ82NS!l#?8ꁦ9~T"u0ocp#wxl"$x`)-xm/DKROL5-1҂c"+ ]>Uչl9{aV5?C68!'MIc/^ Whyg.DTs /BPK-!M[Content_Types].xmlPK-!p8ܾ8 ._rels/.relsPK-!%,% N !drs/slideLayouts/slideLayout1.xmlPKpzPK!M[Content_Types].xml|N0 EHC-jaj; +,Kq:=ig ,?ϵYD&oDzCwO-gkcg$./XQ{jsԈHt䒦AFP0skfx(壓8?.C(ũ{R(Mb˳7{-IF#{_R'dK0FFjr'"&@_'PK!p8ܾ8 _rels/.rels 0Dnz x%ٶ6 (тqLݾQ(NAU ioo'tGHL m^W16 AJMȅ8a22~`Or[;,lij@搛}YMGBh ]pϔ{J Loc!"rPK!"G~!drs/slideLayouts/slideLayout1.xmlRj0BFI ؁>/mH[YMbw r1ٙюEk k4ڻ&SδS&_7θ|__̓x&F.JxRBDUi qv+=ZHtč(q;ދ;av|pK|YJ?{ڥ jĪqt ԑlzPi(YOĆ)Z9< *׼aXf.:bh F8oF'm6G`miYK"MLAuDU:RL=4?NPK-!M[Content_Types].xmlPK-!p8ܾ8 ._rels/.relsPK-!"G~!drs/slideLayouts/slideLayout1.xmlPK`PK!M[Content_Types].xml|N0 EHC-jaj; +,Kq:=ig ,?ϵYD&oDzCwO-gkcg$./XQ{jsԈHt䒦AFP0skfx(壓8?.C(ũ{R(Mb˳7{-IF#{_R'dK0FFjr'"&@_'PK!p8ܾ8 _rels/.rels 0Dnz x%ٶ6 (тqLݾQ(NAU ioo'tGHL m^W16 AJMȅ8a22~`Or[;,lij@搛}YMGBh ]pϔ{J Loc!"rPK! !drs/slideLayouts/slideLayout1.xmlSN0}٥RUE u })L7C}Dyŗ3g|`4eيo/7I+\OۋEۂvVV:~]eQXB;D_E4/r' mùh%j{0,g餄ċ' 5 qaaAF'P˃#gz nyMF̂1XL eZw  L`.Ŝayk F]yar8S$7Pq1T)(^;|bi@'X&U\-rdU*s92Hg?B4'z߱7ϸ)XG ~ƽymg/V>ՙq#+)Ko~;:_5*=d:s)mkEvESv$U޵hчR\( E`5G_$\XĤ[Շ+.R K8ٲ-#)x:R,p>0ݲ幣`<-nB B"i'٪ao`hţ\X2 k%%hX[m,kۉڊZ`mub-v:XS@(6gC=#Uv0FɔDI&RW),$wʍSЌ EGD\!Y>1laHRw&IvM;O&~uDop-iQW2yDHiïKn*/fceFsY/ԙed?*'L͒3 "1$6Ǚ8ډhl'OHܐk Sإ@eo Ʃ A,˯ڤnZձ#JAS>Ur;~2'i[-vN$ZbS)uz%Sn »ph'2xnS6ͰtP_`u`;:[b=سC{~usDƸ 3clvDpV1~;VgYtI_R>+Ĩ>h{?Vwͺguʳ1ugz[wlƒYx*Qxܽi/R5-o+w9uwyzPK-!M[Content_Types].xmlPK-!p8ܾ8 ._rels/.relsPK-!MQ~ !drs/slideLayouts/slideLayout1.xmlPKZ0PK!M[Content_Types].xml|N0 EHC-jaj; +,Kq:=ig ,?ϵYD&oDzCwO-gkcg$./XQ{jsԈHt䒦AFP0skfx(壓8?.C(ũ{R(Mb˳7{-IF#{_R'dK0FFjr'"&@_'PK!p8ܾ8 _rels/.rels 0Dnz x%ٶ6 (тqLݾQ(NAU ioo'tGHL m^W16 AJMȅ8a22~`Or[;,lij@搛}YMGBh ]pϔ{J Loc!"rPK!;bE !drs/slideLayouts/slideLayout1.xmlVn0?'z![i$%:BQɸvd;i 89]{v$[ mZM4 Py]a]f,W@&32@(IKQqsZ7BamQ[|ꇰ7+&Q4 {aKz(sΟ*Br̲lLhav$e7 6"!x0gW)g`W32ڭN Avj]7VM׫[ʂ@A.fS g녮g<l= bڲO|ymu9SN҅3[Fx7zU珆qR>zՁQ,ޖV/:=:{4nH~4G/DI4c4qoD9C7] I:?2|Yd-m4vf7)x%cc\>PI )g;] bp)[Nd9"t@$); YLe?B3' /hu@υL?P-vt{WIû򜌣a?+yDQ<Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!,S1 drs/shapexml.xmlVo0~M!*TЕu8ؑ0}wvR*I<$Nﻻ.\rL1omq&TLmirfVb̕7ϟ *cuMoE.B[MͦYarO.Vk6saj*V~iXy39|12H:YaB;[Q᝱`J M.GMI!#r[l;H(qN]8CjM!igwtv,1oYLw,F[oo# ,Y~Fs BuY1䡈a#!x\R1-2j™qV׌HV 1{r2lMD Ռ][)*j/@M}X̂/Щg*~˚6CO^!Q#Ҙ6P3#ET+7B4gVUfܲVY*>RBEnѯ[L5ـadʺ.oy:>Xx}x!A V(={Aӹ5:a7޴fy>8'\y)Q0X]g`\ u(4`k+l' h/pPU";Zq VȌ6VL:5)]gReKtSa.bߢDb -JxITk/b$%W g3Cl+!aZ߇) (~W~:Td h}ۅߙ/)PdqPK!drs/downrev.xmlD]K0Cx\b [W EЮ M1eݿ9ͨ$ngЕn(&ӜIm`XA/B&)І`S} X6N0E`0!sc:=]̊m+(| x\j/|qNKC{sYdSOO xPK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!,S1 drs/shapexml.xmlPK-!Ndrs/downrev.xmlPK_ ?%  p* C    @ V1? Rectangle 82947"@XK   @ Hܲ?Rectangle 4"PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!E\ndrs/shapexml.xmlXMo0 tZۉ1NhwicˉY$9KGIN6 R+٤'>dÔ.HitRD&R,Szw{y4D9p)XJϟND )]S'A@˚ RU`V-Z1̈́q*p JA'뙲z3SS:D@1oXwD1ZP_ ~bzP!ñ$ [h! (E۔۹~.vA-Tu8 $(pTR0 ,H֐ a8 paz,ֵV\1]* 7 L|>qz6lϑJi)}u6b-#T(/$Oi,dzȢl!6:fnvX`wq@n_ &`7n7.#R_x9%9+na1qӐ`*7)0gn pTh8eZC}㎋yYLf!e~\#DK^v\yַ/ܧ^(P{Zhik2odK%i{ 20L2d-6rowmpo{V^qoliK:u*J{"wRy^;wx0λ1Q kK;t/C1zDxdN2d>do??pPד_PK!_jjdrs/downrev.xmlDKK0!\8΃N b:e$N7pn=9V nfTY|+{Ұ۞mx$<&ޡl4 lPr;*UH|45-{z+:_4|K2V1CꪗǮ[`bprcZ/·bDvWbx@/xg`   PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!E\ndrs/shapexml.xmlPK-!_jjydrs/downrev.xmlPK )  RClick to edit Master text styles Second level Third level Fourth level Fifth level!    S  @ V ? Rectangle 82949z   X C    @ N?Rectangle 6"PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!JGeJ drs/shapexml.xmlVMo0 tMtv~cˍY$9K;Iۡa@v\,R#H xvęP.*u/w׃9g֑*Hj%24yچᬲisM:|'jou#d659|acʑZFpf]w:lci^S˒x1ǨCtPP*^a4OrhL( #o1}bT JRJuY$7fIq:`3y8yeAkR92S*۸pdA&/#y62!B$IwХvRF]e<j:! dV!~,nNûR:2,{ hE2x`PRK J܇)Ns&֪͊[*$$CM{L׹cd}.~Xu6j8,P?um{)1T}n-8FR+رJKYc9_ftp5 &d9Uru$Q!ބAUm]k |e\M).XlUbg=Fқl/܁a9auMN*?e(>-Y!+?Q(Fү=0SJtܱZV02q`B(KL>JuynnXTR@oj5.vAQvAZ=>߅99kX!? 6 d=⟄m.~PK!1drs/downrev.xmlDQK0Co.ˆL2|Ve-6IMpzRкh3uedk>I8/AX./"f;_.RW5u*C5V:161UAш7 V q[?|(DQ'ί; '?@0l62>Q$;%a[Yr`@W?PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!JGeJ drs/shapexml.xmlPK-!1gdrs/downrev.xmlPKx ?  p* C   < @ 0.k ?"PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!7drs/shapexml.xmlAn1 EHC=$S$Fa #'J7Ă;_zϿމ+<Ь1r "d.0icvlSNV=PK!Bdrs/downrev.xmlLAK@B2ovb4R<(m{fM4;viwK|0Ǜh;1hZng͵S- #uv,'WxM4"epIBc#іNoPy:l]-^4F׿<h +{3R^ODcLmvn*NBZgNIJ?PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!7drs/shapexml.xmlPK-!Bdrs/downrev.xmlPK I}OPM80___PPT10.q PK![Content_Types].xmlj0Eжr(΢Iw},-j4 wP-t#bΙ{UTU^hd}㨫)*1P' ^W0)T9<l#$yi};~@(Hu* Dנz/0ǰ $ X3aZ,D0j~3߶b~i>3\`?/[G\!-Rk.sԻ..a濭?PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK!,߼etheme/theme/theme1.xmlYKo7 Hȁ%Kq81,%E.˘\ߊX@Ѵ@o=m$@/qM]ֵ!~fr~4.DG4I3nֻ\*!)A0=$J囵 aK<'|rb"Emjkz֬fp S4֤VI?`)B&Fx3 6:lh<}&f$ExLu7 S@ X=:\3")90 Acg8 +l e~]oxFkoXR%z^d%|w<Y|g ?ixJu 9dn%|@籣ELy΋b dX Lq1njN&;ʥ!- P\ur {컗Ϟ>xzӇO`8݉/>B?ţϫ?Y5P_<_~۷*O\Dl3 kN&'3X k)x' \+xG@}^%b {]OR9qQ ׵,YW 3wQ><f9FZEO>Ù1ɈB?$bR |]zV.ɘNhZLڥ)JA6{wP*wȑB1a2^3*1N7J ODŽq4Usn qunc'Vq~OpWaG4K\B}{~ٹCm{*-D K^Ni"\L3u<"⻃g>x_ށ޷7xkyj]Yϱ is)elN!M,aÈ0癓 b$dFIbYP\vxhؕ=pSg9vbs,55š R0U5R+KkLM.ՄNA܁ Hn¥[^d#b2 iK+ v`\#Gz;iei8JVR /ij279YA:@!λ"xJspԽf1\Jب0M/ypcqNye R`0Hdd_kC̼&mZRL$Tr|%186\Z+8(KN[1l}\Vx 7uu.Ҽ9ڀ)[VѼ%J])B#L2eem/\ poFz}Cz\C=rDž@p_1Y.,hF%} 3Q&h.$+)L8 ˼u01u\/+{cw}Ɣ46¯9%#cdhn PK! ѐ'theme/theme/_rels/themeManager.xml.relsM 0wooӺ&݈Э5 6?$Q ,.aic21h:qm@RN;d`o7gK(M&$R(.1r'JЊT8V"AȻHu}|$b{P8g/]QAsم(#L[PK-![Content_Types].xmlPK-!֧6 +_rels/.relsPK-!TGtheme/theme/themeManager.xmlPK-!,߼etheme/theme/theme1.xmlPK-! ѐ'j theme/theme/_rels/themeManager.xml.relsPK]e ; |   D (  D D P ? Rectangle 83969z%   V B    D P? Rectangle 83970 ?%  X B    D V? Rectangle 83971z   V B   q  D V? Rectangle 71684"QKPK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!9{:c  drs/shapexml.xmlVn6?e`'t70PeH'E璲' b]M%^9X)v֕F'ÙԙKIׇք3΅2Z&\>3W3nV'|}=k]pL-5 c+h7J'q*u:v]R+8Ӈu+;ܖJ]ކPҗ;b {$Jx,uzÙP)6T l*H*+LC5W7` ؕ9S1h<{Q. 41҃H\BPG'dk3ʷrGB3 RNˇpÃ}:jz]g  BsquP]bvt0>Rd,U#:0W]!I~ZQ寕K'$/myl EUoE|=#9M>y JZ *6PxĜ™%q49' %A镰K*as\Cay r{ @"h-R/.oB6Md*yKw@DAwPF>(b'EHbV<M&ݛho 7֠?&y5-:^5X׸ɅTvep[_PM>7HfVϕ!g[x$>_SКjx>BsDd7},Df<--^J7kS$B?hR jJXAhozv &WPK!8g drs/downrev.xmlDN@E&3qc`F(H&[ PƄ;[tJ#Z`4 .ht {@Zpi42ˋ9_ޡ]޷Qq74-+UVTX~J ;xX7 \?t"Y1v}=>!$;EkIW\3 &qx\lm#R3\`?/[G\!-Rk.sԻ..a濭?PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK!aYKtheme/theme/theme1.xmlYMo5#d4uS%ڴQv[ԣw;3ޤ( 7J\ʯ AxmYlKPթۏ_{/_3tHDK"EZpI3^NTƻ\*#9A0eJ덆5xI 6" EH>9k,7V#ǴPs{s<1AC-4ڨ<J1-T# *9XߤHG]&!fiq+SmsU ,'ǭ5<q 7 \wl|B ^{1s@ve۞=dsromPhq0n6pU)dNnw:3dZ3ZŘʫ [s\l@?0hqI8bFGj{:*s.$cAKՉ>(1Lދ߽xx? 7!͉D79f[NFF 3LE*qQD DcH VALm|"H0pcVflUO-ܔTyrW_6ԕP +Ui$TKYr}Uoze+U`^'Beh-И+.0|qT{9OS$(0*0e\aS1l%] e [Nʞ!aCA)RW" q -1Ju$K-qͣfkvpuk@!ߖ,.Ԥ4[,_sKs w/c$U=]Ehh,MNV~*bf$|S2 oc¬707`~Fr᣻g܃c7d`\Yk5PK! ѐ'theme/theme/_rels/themeManager.xml.relsM 0wooӺ&݈Э5 6?$Q ,.aic21h:qm@RN;d`o7gK(M&$R(.1r'JЊT8V"AȻHu}|$b{P8g/]QAsم(#L[PK-![Content_Types].xmlPK-!֧6 +_rels/.relsPK-!TGtheme/theme/themeManager.xmlPK-!aYKtheme/theme/theme1.xmlPK-! ѐ'P theme/theme/_rels/themeManager.xml.relsPK]K ;   0aN0   !t (  tX t 3 9 0e0e ?Shape 121859"b\PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK! $..drs/shapexml.xmlT]O0}u6"E6Bgt84Ա3-~N M$^!^~s?N϶6Z ,V::R%IDƔfgϟNԶ|Mی-k8|) J!nB9rxq2GqCb3S]/Du 0pr<x_ԨGF9J wcM tOp̯K-3#RQC-nZrs Һ=K$Gd0`!39@ tIժuL+:Enw=[! \i΃SAAT.1 x`E0/ؖ/6Á BTmf՞WvX_Js |"^!5R0qṰ "ظY~00Z7uTd1r,8NEPv&kȲԫ h% =M[•[O;-=߲3F*ȶqRP!JJ_Rv t7V˺7aIvIPX<&*ݞ\S$82<H竏B:"xO7#" B 2cMKmg?PK!/ drs/downrev.xmlD[K@C8/b7i5mb[Q om4{EO{FNhE!qUi&TM᭜_f9a4L''c̙>wk_G\MN. *x[m% mMC`˖ 8%#"Q0Ѡ voIl/c.Ն=Sz~ a }9JD'V7f\>//$K򸱂<b PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-! $..drs/shapexml.xmlPK-!/ 8drs/downrev.xmlPKQ`  9  @ t 3 9 0e0e ?Shape 78849D `  9  @H t 0޽h ? 33___PPT10i.Ck+D=' : = @B + 0aN0 P!\(  x  c $ }     c $  <$D0  H  0޽h ? 33 ~ ___PPT10^ .P+YD2 ' : = @B D ' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*t%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* 3%(+ 0aN0 @!0(  x  c $X  `}   x  c $0 Lo  H  0޽h ? 33___PPT10i.nP+D=' : = @B + 0aN0 .(  ~  s *9   `}  9    s *<9    <$D0 9   @   09   S"   9  H  0޽h ? ffNL|>rL___PPT10.uJWK+YD~' : = @B D9' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*G%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(+ 0aN0 0(  x  c $\4  `}   x  c $H    H  0޽h ? 33___PPT10i.(+D=' : = @B +<  0aN0 r(  x  c $๚  `}     c $š  <$@0  "P@0PpH  0޽h ? 33___PPT10.0+ED' : = @B DQ' = @BA?%,( < +O%,( < +DL' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*i%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*j%(+ 0aN0  0(   x   c $E  `}   x   c $F    H   0޽h ? 33___PPT10i.i+D=' : = @B +  0aN0   $y (  $x $ c $4  `}    $ < J  <   2 $ <̙ w  @  2 $ Bo{  @  2 $ B   Lfree   2 $ Bp 2  Nlocked   XB $ 0DWYXB  $ 0Dqv XB  $ 0DL lXB  $ 0D* L l,   $ Bty  Lnew T()      $ B謮v ] Kacquire    $ B*   Krelease    $ BH,   Lshared    $ B 4  Nunshared     $ <4uy y Kshare   H $ 0޽h ? 33___PPT10i.p+D=' : = @B +X 0aN0 (F(  (x ( c $   `}    (  6  S"      (  0  S"  <$@0  H ( 0޽h ? 332*___PPT10 .K+AGD' : = @B D' = @BA?%,( < +O%,( < +D' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*(&%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*(&;%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*(;O%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*(Oc%(D ' =%(D ' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*(}%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*(%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*(%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*(%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*(%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*(%(+ 0aN0 ,(  ,x , c $T  `}   x , c $U  `  X , 0Q H , 0޽h ? 33___PPT10i.K0+D=' : = @B + 0aN0  4h(  4x 4 c $  `}    4  6t  S"  `  H 4 0޽h ? 33___PPT10i. Ed+D=' : = @B + 0aN0  8(  8x 8 c $x\  `}    8  6<]  S" 0 }   8  0^  S" 0   H 8 0޽h ? 33___PPT10i. Ed+D=' : = @B +a 0aN0 `X 0(  0x 0 c $  `}   x 0 c $  `  X 0 058x~X 0 0/j#H 0 0޽h ? 33___PPT10i. d+D=' : = @B + 0aN0  l0(  lx l c $  `}   x l c $h Lo  H l 0޽h ? 33___PPT10i.nP+D=' : = @B + 0aN0 0 <0(  <x < c $  `}   x < c $Խ   H < 0޽h ? 33___PPT10i.0⡈+D=' : = @B +f  0aN0 @ @L(  @~ @ s *X }    @  6X  S"  @ y <$@0   @  00  S"   @ y   H @ 0޽h ? ̙33:2___PPT10.*?`+ED' : = @B D' = @BA?%,( < +O%,( < +D' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*@2Q%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*@Qp%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*@p%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*@%(+2 0aN0 ,$P D(  Dx D c $l  `}    D c $l   <$D0  X D 0T 3H D 0޽h ? 33___PPT10n.bN^+YDB' : = @B D' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*D%(+ 0aN0 !p0(  px p c $P  `}   x p c $(  `  H p 0޽h ? 33___PPT10i.nP+D=' : = @B + 0aN0 0!|0(  |x | c $  `}   x | c $ Lo  H | 0޽h ? 33___PPT10i.nP+D=' : = @B +> 0aN0   ` HH(  H~ H s *L   `}    H s *8   <$@0  x H c $ p `  2 H < XL3$   2 H <,0   XL2$   2 H <40   XL1$   ^R H 6GHdIh a ^b  H@ 6ZGv/HIE XH XR  H 0G HI ha   H <8  a d Fork 1&     H <L!@ 7p:  XFork 2"     H <T% 9 XFork 3"   X H 0@ `H H 0޽h ??`HHHHH HHH H ffNL|>rL___PPT10.uJ+EDZ' : = @B D' = @BA?%,( < +O%,( < +DL' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*Hmz%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*Hz%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*H%(+ 0aN0 p L0(  Lx L c $(F }   x L c $F    H L 0޽h ? 33___PPT10i.i+D=' : = @B + 0aN0 z P(  Px P c $dN }    P  0dO  S"  <$@0   P  0dP  S"  <$D0   P s *Q? D0 Z H P 0޽h ? 33&  ___PPT10 .K+MpD ' : = @B D ' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*P}%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*P%(DL' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*P'b%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*Pb{%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*P%(+ 0aN0  T (  Tx T c $`l  `}    T  6$m  S" {    T s *n?`P  } Dining Philosophers . P   T <dtwvq @  X T 0L 2 T < wv XJ3$   2 T <{ 6  XJ2$   2  T < 6  XJ1$   Xr  T@ 0G}H!4I: ^b  T@ 6ZGv/HIE6 H87 ^r  T 6GH!4It   T < Q d Fork 1&    T <̉ '`  XFork 2"    T <()  XFork 3"    T B/` '0  Jleft    T B@    Mright    T By̚@   Jleft    T B   Mright    T B"ъ Mright    T B@` Jleft   H T 0޽h ??`T T T TT TTT T 33___PPT10i.˓+D=' = @B + 0aN0  X0(  Xx X c $ P  `}   x X c $I  `  H X 0޽h ? 33___PPT10i.|gN+D=' = @B +0aN0  `L(  `x ` c $ Q   ` <eys &http://research.micsoft.com/specsharp ' '%  J0%x ` c $Ln  `    H ` 0޽h ? 33___PPT10i.0GwW+D=' = @B +r0~\x PH8QS%_am,5dҠ^MmJ` +E6X1Oh+'0 hp    (00Towards a Verifying Compiler The Spec# Approachschulteschulte201Microsoft Office PowerPoint@PȻ @r2@a(Gg   T  y--$xx--'"Arial Unicode MS-.  2 q1u."System-"Arial Unicode MS-. 3f2 ? Lecture 5.-"Arial Unicode MS-. 3f42 "Towards a Verifying Compiler: .-"Arial Unicode MS-. 3f2 ,9Multithreading.-"Arial Unicode MS-. 2 6@Wolfram Schulte.-"Arial Unicode MS-. "2 ;>Microsoft Research.-"Arial Unicode MS-. $2 A;Formal Methods 2006).-"Arial Unicode MS-. +2 N;Race Conditions, Locks, .-"Arial Unicode MS-. *2 R6Deadlocks, Invariants, .-"Arial Unicode MS-. 2 R^ Locklevels.-"Arial Unicode MS-. 2 VH Access Setsu.-"Arial Unicode MS-. 2 e _____________t.-"Arial Unicode MS-. T2 i3Joint work with Rustan Leino, Mike Barnett, Manuel .-"Arial Unicode MS-.  2 icFu.-"Arial Unicode MS-.  2 ieau.-"Arial Unicode MS-. 2 ighndrich.-"Arial Unicode MS-. '2 is, Herman Venter, Rob ,.-"Arial Unicode MS-. 2 lDeLine.-"Arial Unicode MS-. B2 l', Wolfram Schulte (all MSR), and Peter .-"Arial Unicode MS-.  2 lZMu.-"Arial Unicode MS-.  2 l]uu.-"Arial Unicode MS-.  2 l_ller.-"Arial Unicode MS-. *2 le(ETH), Bart Jacobs (KU .-"Arial Unicode MS-. 2 p Leuven) and .-"Arial Unicode MS-.  2 p%Bor.-"Arial Unicode MS-.  2 p+-u.-"Arial Unicode MS-.  2 p,Yuh.-"Arial Unicode MS-. *2 p3Evan Chung (Berkley) . .-PropertiesWEBPE4CXRRYA==2 0fkEY0fkEYItem  Properties13QCENBGHBYZ4A==2 0fkEY0fkEYItem (Properties* <_Hschulteschulte  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~xsd:element ref="dcterms:created" minOccurs="0" maxOccurs="1"/> This value indicates the number of saves or revisions. The application is responsible for updati  !"#$%&')+,- DocumentLibraryFormDocumentLibraryFormDocumentLibraryFormRoot EntrydO)0fkEY Current UserSummaryInformation(PowerPoint Document(l      !"ng this value after each revision. ltithreading ata Race Freedom SoundnessMulti-threadingInvariants and Concurrency%Verifying Multi-threaded Pack/Unpack!Ownership: Verifying Lock BlocksOutline of the talkMulti-threadingConcurrency: Deadlocks&Annotations Needed to Avoid Deadlocks.Verification via Lock Ordering and Lockstacks&Example: Deadlock Avoidance (contd.) ConclusionThe End (for now)  Fonts UsedDesign Template Slide Titles 8@ _PID_HLINKSA&http://research.micsoft.com/specsharpDocumentSummaryInformation8 MsoDataStore0fkEY0fkEYGFWF4MBNEZWQDY4HC==2 0fkEY0fkEYItem  ՜.+,D՜.+,@    On-screen ShowMicrosoft Corporationl*d ArialArial Unicode MSCalibriSymbol WingdingsDefault Design:Lecture 5 Towards a Verifying Compiler: Multithreading&Review: Pure Methods and Model FieldsMulti-threadingMultithreadingMutexes: Avoiding Races"Program Method for Avoiding Races"Annotations Needed to Avoid RacesObject Life CycleVerification via Access Sets!A Note on havoc in the Lock RuleExample for Data Race FreedomExample for Data Race Freedom SoundnessMulti-threadingInvariants and Concurrency%Verifying Multi-threaded Pack/Unpack!Ownership: Verifying Lock BlocksOutline of the talkMulti-threadingConcurrency: Deadlocks&Annotations Needed to Avoid Deadlocks.Verification via Lock Ordering and Lockstacks&Example: Deadlock Avoidance (contd.) ConclusionThe End (for now)  Fonts UsedDesign Template Slide Titles0P _PID_HLINKSPublishingExpirationDatePublishingStartDateA&http://research.micsoft.com/specsharp2018-12-08T06:59:54Z2000-01-01T00:00:00Z