ࡱ> FM.Kb|JFIFddDucky!Adobed0M   #%'%#//33//@@@@@@@@@@@@@@@&&0##0+.'''.+550055@@?@@@@@@@@@@@@"!1" 2A0P@`Bp#!1AQaq "02@P`BRb ]<@ L L L L @ @ @@0C110C111101h)1 &4C4`X B P&mP5Djcd!a@&PH&*mP`P&`Li0L*V! Rm`@ R0#d)AՒ0@ eC(Ę&H!(&Į@`b*D b(kQ= @8hCa4Bv@d)l%04&1*BT)`*BJ@P$ 0 0C@m4($`0t֡7"$66M6L܉M΂]!*bW4KCB&m Ar%l̤!ЧD" &h&)Uȝ` \'rTԀW:v413UMԌMT L%h)rM&4CVhhM56Jj@C)$s)"DPB!bI5M%Ы;T 5'LJ!#BD , )dڵJ 3*Ն{gdM*cD[ t*P9lv(RCW7;D)Km\4!;B%N&SijQi Gu6-sIuPJѐKe"+455)qM\h7$Աԣl9lTERb)#L;Sj7\j@b^*d&H)sR"$4qBֳr+!M⦚t4b؆! i,őYɋ:NTCF2RK-ES&5Ahȶ!V!CWpk EA2YuKFEѝX)D<MSL0n*i)g"gCYZMUHf)5,WΤLVYUQ)H$ܦFѪLQ-t 2 IH ŠԄ!n:R̩X芫U()&i2hpCDZ!M9CHLcBZk*)8.H, CT;Lk-QkNtC"Dᗖ UJTR (*E@IE)T8n;D]2ɍr5͢"vRR:J(BШ:άj8)= t"I$&-F쑃N:{N$r*`K#MmidTy5-y [tT &^ L $hIHґr15rRPHLGSB D5cYBi (bmɝ͔ I+p!M(T H].I(cyҒԖ-R%jjR, R43f:TR ֔Lji̹Ji2t#+:bi:I/;h9rf:+sV$VtW;! j ℨbB*CYZ)LТ`ZI.t%g TU@LT8M^T8,ILE%W%EMAJySIh:$bo!zhpgA4rȡ*!ŚgHGM YY t*D h*RB\i*M!!%T(-<ǦTY()K$hJ!Mt)b!҂BY$RWU8)46p+TFD%X&ZB ZZMaQ(B(qIRr4!qPE6Efm4YTHZ$ڦuB03F`Ӆ*hڌ i RUC@FU&PEPjei KΒVfX4HDH$b*,&\cj"ª ""*P:F "QF1 HAjGQCΓR-E0mYN(s,kJUz,-HV ӚL\`E;j=3@, \ZrJnΔʧ Rh-Rgm IJ)(Ph!֒HES;@#d"(K\VZf`S0*5JjƯ;cj@A1jPA"ZH%TPMf-& R7H4gT(%-ҳpQK96#U t"4iٛmf)zeE^VLQ*mHyI[B42j%˜Wg>.\xsυ/2Ĺ~>g?sW?m~|*%isDRyy_sQ?GfyuG'^|TK_c?om~3'q#̦J'!:%N!rT \J*ua8,W(+L31YNN%qA>Z* Lsu"JOnd/Njl'2JTcp#*S\C )1'+l*\ RJ\9~)`$FWPH `ms?*V|*%FTuQT娟sSCTvbZK\LJ*אn|:SGu_=Zf7#fuz2St 4>3AeJJ^\RyԼzQgU`r]8(b<˱_}M Ϋ x\E`ΪXҷQB6@jZ@WS+2;Z@\_:aΫ2sͺ~,3P9~@%bKY\F*c-2RfRa'\93댧ZߗsF3p53#A'~0^ Ԣ<tY>%q3&8qST.V%f̙ͦƉՅF8nYJψ ֝M|\PK$KA̋A4 Wg/]8xtus®TLNVݼT:rVRμhƁBΦLS^SK ZWeKY|vtu9.gֺ u gý:sS9j%zG%2h:Os+:s̪;>+!h3ƙԈǯZ־q} 稢[-gfiYh9L eW|gj=N.ZW3|fgը|m$s54LeZYEX \{z.kh&u]L~ʣ\Lj+4&3g2phhih:c /^P{uXI8 sܷ.㾲Bkئys +ռN>spr0r Ij [i٪m. zĩH}면S48f1q^+=g]LB1?Fj&EWePďZ,xJ{К=f3η3,&r&lZӠ f!QygW]KC8rfi(Z3膝j?bkZ~ѓ+4)=s!ӧY3tc,Uֱֳ'f ޻KkkٜaeYgi sZI99ήvr:֜ۏV֬zs>EVU]3>PukZRS\^Gp tt[}Y2h3zդp̡3F yMTrN&CFIRR!fv\glE=k &Fu02J52g>C r #Lg ;^Ck0r3DW_9WNPT;0zG9dkݪQlbkZS׉*Ԇۭfjy\ǯK|䅩{K2ag/\KA)5si2+w ϯZY׻Y&l3u]f#2L3Z26GZӦL뙑dΖk-_۬c&}yusf:uc= Y`WJMoks4\..u[dkM @k[@/E{TӠZ[LʇRkNoA&7ˬuɕ9E!T}3:F :u~7٫\nz }73f&~!v&i5+C=o_XL4\8,Q;t=E2N-smҫy]iofܖ>p }ۂ&8p]/3J:׊+j}AQ˧3)ۼ`HLgZ+0ˤpjۂ\h"֗|| t3EIi=khVӟ̌vc>#ޥqtr|gZYs:6͹ Y]R/%:Rs;\nS} kڱLk&=iXsp%[Y3s_ 4崪qmQnWU0C'mS`%g GZd\ ѫu dz'gn]&4Oa3Td3bWD3zgejd<!?TuWKLZ;๜gJYx#6@Y'q7h͝}yˬƒi}?!ZUjYukgzLoZ@dkG\qY9Y֡zkt0&Bj~EM =L̜kjtz\g{>fd9fw; J&?LtdQm޸[gXL_jQ֋&NzMmRoE3zz.z#u,u 1NiMkc}rL=SLќ8Z8Yz^&Z&4taUtEsxijy jAL 82'X V{WPaPs5aheHz^X۝}=ymtiɽvqƺ&W[L:0¨ ɝ+32>i7sLk][U HR.bG-huYփGLjz[YiE]y=e'p?X,Wح$S6)w`\wXָ3kFsMk&~sbܜDUh2L]\榶ndXOY\OSg:IPLgmu{Y kZBYY7cז&f4[=z=ecttEΐOgM3 g($|UfhYD iLg&W5rkZרɐ57=z_^讳Q8ɜx[muvf[w32{3f:jvj^ W׎ hӲ*f >d5ՎΧ+*Zl pT70߱ ׳A7:Fpw NçHӭ:ukv ւvcJ2+zSH.DJ2t:20h1C]Mju\:z{k^ n PlPM}{K5Z\Q-[tGPwM\܋Hp~V}}OWK9 ` p:S1kZ3Ȼ -.oٝls?&yVg-ރLtAߵrU%C[ӤzΤbjcguLiEU^1nU ћV ?]S4*zItg}Wι\W9'5m0S@Jjh*h&yR'l.z{oO9oPRaP=Gc*ՙ,KE,-*S}5ut' ٸ"Egf;]b~jf9,2`!ɕ9 p]n bQ{tNՓY`֖tSZ3! 3t6tRbgV]$p2F_^lk3GaDN3fspͨVrCSԳ&X2ٜkMT׳]jdvNC^ͺskַI1r^ӌE֞]u%u.3;9̴2bm}]_c e֮dkӭ%?4<W 9 -ֵN4G49 EhT@!A9aUtr$҆yFj=`ZsTӘ23us82,CT\ ?Wn-r:=}M[mr1jV3M=ӧQthƙ ˒sz֬X%-]gU|odZ9˿c2-s5gfD\2kSy/KFRq[7öuvoפJ=~1Ss?Q7ˑPH )fɕEۧ9=sWfTifɱYɜQ9!o fg,άond~t̄!,Ĭ*FCy v|)ueIAm٧YxԳWĖt&!C&d@ofUϮ\\붷t}:cZzjSNRtI&WAհ9Lg0ݲNֵyװ,=giPu iΗ`Mf}uޝ`yp{]=(c7K%Z3`umJf193zkyxk|s91F; v9]1J&d]]ۨt+1׬4Fg7=}M_ѝӭQW)LQC [cgf Kk+3cY5ԃ{?5ۜ^Z3e8ζh'[/ ڂQ_RfulpXaR7Y>5~3Uu-bNˢtX煶hhgדZӦdY]6N;jg$:g?/56ڹ;';A+,zKg YZ24`&Fz9E.:ւkLtֻ8ˤPem1֟f9÷gWBR-^ڜ(ٜn̦f*N{@YYQ4n J4@3y0K:;\x3ev3]9|`퐷RYvO-&F;gkjv3/Zz(u3&G~VvkQOS&uPʺgla29ʱҹj gZgʠ F\f{d@Cvd&}zZeZ֟bޔE+ KI7vO#isl3H+35;֊jd=4{49LwåhS:Mp8*-AoSN*g<&>nA m^g3Qδ\d͙U9RM.5̔vtd 'S.6N@H te\vV3#fvjC-roq]Lu>~>sMN)ӓ$WZui1Lpμ-34k)Fknu֮uDX2^3g zW:ڦz2^ەnmhuRd d:nnp8q=σ9f@>ަyuYΪlL(-\.&_~us3}MCfuh-0g2+gx=9g!9=: oP3Pѓ׭1iZ18MN\l-e6sS󬼺7ty֪ Zjioј fwkJss8~֚sWY678}9Ү3zd4teSmƲ/Zæ7c|\g6fhX 3gétֵ j8>'ΉVo+֕1< .@Z2ёMYᅝ!I=hC_֑Uq[_Yzޓ}cKX]o&GJP S흐/SFQJEo9W띌 :GUε7ZB![55i)3v+P֕dє]mg]F:iMɌX0j13{{wnڿ_g ~׫ޔ+H붳IOg8Yg7ւ=m_:I'n7zw=@e+mOcdmsײgRe,4 *uSzN`ʍ̖zdM t&@ڀڳ\vQ4esΕ:[GP3_mVz##uikkFC+9oƴ˃ \vӯ^S.I%#3]reKW3Y׌5UP"AXGk[\d7uk(5{h*9Ajgmi]fhDk[PfB:QZS5iuf9sUh/AZbdq}/Յκ.sS) 0PuNdɭOYj|ƃNګ+3Wm=FiN@"ȩ.3%;d@M+3dəR v*g_ml5d /&]fz5dg[@&2vӕtk_>kzk kFQ\%芭Abz.E]/RgMN9)C:U3am2s[⺉,Wx.z:3z5gy 8&1Ψ5 tYwZtʏ&M!9Ӥ 粘5٥ Qu0ڌjuc9ˤ5پawf ^IdPJϪ2aDlk}ugBhV;It-P{fjM+ 2̔W*ՆJfsd4?̦ic] vjsu d}9Ur|%;/|z[ +Q֣˚OdOol&{ہKIˠ/ZwYE9 2UE_KYQg;G2ڳy>83 }WM!jLd@NibWEku?!.h7qLy}jJRȰSvX*C 9+Ygrj9Kc :ӧ[.ig%{=vW)bGtzM'Q|> `)sQSPY_fR3Pscۭ?&N{hȻј3P Ӑͯ V S{u uu]A;?6Nt0a`}g yY{-q:X4vm)u:XV&n.OBB:MwwΧ3u3χ>4GZt%S/KKs|̴W Ӡ?[Zt[w "b:VᴎOjEVH{.Py\jK b8sDF-M73WUHk9 4|`V|&AYDl.ߕZxekHx*ȷ3\8ounRƧ*\9vbs4itLD&P˖KOQV\x%Mme;{2sρ?gUy3;Em0Yrw?μ2~'i\[K.f7>`*Oy/*W x'5iep:Xp\, -JKeiqcaK.XBY/,-KX>gυ ϋU֝?GN =B:_ͱ]p<|Apj[.៝kWpj-˗ -Qbߋ ϛ|οo7[O_c?ޙrXoڤAr,˩dXrb_Fܹ|A,] ܾ{rf.eh-T *Q*T(J(~u+J /#ZX<~^VX/ })~}1}^JZƱ6/Q1}S^FY௢>'n " ~ִ/H%^Z 蝉xD/Q财/m%au^N(R,Y_(͞e*ǯ2 +l"$2B<'9֛H=Iz۶1 w.4 (󤔨y#Y[v1>Hf촲/lI1 HX,-<"YegYEU!6'b",Ouܲ[,b#(&%pR6z",̶@ƊIt( 7?*R<>Y"4Mg$x87vLi G''B,셄7#,z # ^FpGܻ!*<|U4Ydl>=W/mlD$Hu^M^œx+؄.HWr$?sXۤ]'81G y$|"OR[#Y"~G^Im.Gӧ?&l(^#28{U"헅Y)GUD< U{ݎ?RVY%r$Qt!.}vD%A#dm3OQy-/<b'%܍4܈Ȃ̞ p*'+ԽϔQ;rJn:q@^r4/ Djv|Uuݍ&u^rEOcFK'b'<7ek;w,r&hOɩd>%*%XK!C?/s.ǩ䗤uT1z.R!Po뫇dR> a TY de^k _rs$y=>]} ^i3/ m K)d^cܓ>7Y2F0ps w>*xX$Z%-F|Z ^IL?r-% -i,eID~B!<'O$`]R1,FB fbEScKG-^M-r?o='粖G W$uSu\lKV^엃0>3i}oZUU2z A1 Tߦ)&2F^zc&YHj)i$d|DK'`!T^G̓2yYUeuC>}U4ݶ?, f F L}(ne +KaW+!}Dnɑ$MdɊ!)DĒJV)8^ 1֓"^ p5 زVv"::^Ic܏>='Otz"Ϗ_r.ߑ!Agl=OG/YJc+{ pF`Dg9!T)݋b1b1l͍% ampz[ N4%lKT^gGe Qx~‡5OKW'|S,>p<<[dNt='',m-%^I$=Kg>=p"XđKj/_"Gė WW2Q/G4|zgI^ļ uge#?r/ݐ@I#@Ң&OGv8^zp|J1u%`5nW>K"X>8FEz-o[%DrK<kKVؘ^v= T=4mPr~N=kK(q/Vyx%]pO <ɛ Ƹ+rbH ~;ݐقVH{\K-bIc!`RBPK,)Y/,HDlnB? ?")~o2>%ɉkCK/F~ڸɚ/',|BSLoE剡)Z%'Bx)$=_:Dr%=7&kOb1,ull@B#KE zL6F{24Y=-$py&,ɛ9") b%d2J )^p&g>;#/-lD% D<]q6ϊB\  %9>S|GS3$DuvCgw9JK11DdU)G]d䅒ƕ!{K,|'=pR>H5/cI߱[mDvB"`A%m&4Hn/Qd ,]QBs|b,n^Ii-%H|V7eř|mTV/,Ci$4l] U/$K<4sI+'ɼ0%q"%KDU]/HHވƊ9L UM񶞂HuN+rJ\ !ܡ1:ppLKj[?!uرq+#u|3ؘ0DR[dnG0K%f)99&) 2z-pHp!-/,7%M>+ܡ9eFKtX-VɊ'n,F[%BX'%%A$Lz cyvOgleIHV^KbV ~Dc^4$xG!:&e('^9{8I I}nm[nN[""u:R"F$Kؽ*+,#mS.3m Ƶ^>)%g0Xt]UKeBҥ~670(1GirrK?:.X )!a7%id!*X8Dr# Qc O'XJVBPUlN|؄_bt!{Hd,E[ݑd|)pxe[!+/) $22nF!\KfD_Y(L$ X)DbIcs.2~Tgq)'d ƖNǁ=82':{2Q϶:>J%.7)ANz^ Kvxܯv"VĞXK>}<.Zxbo?bd=zX[igNK$u%ĐdutCt~Jȧ#HD!-du=DQKLݒǨ#_BK!HP[܅YPBx<OjE[$ 얆߰TğQ-=! 0su*D4EI JD|Xۢ6-A =Q=)x䥍ė)$!"u:rd_Tʢ[hIzHH\\rd+|Bnbl)nV CnngQ,e=^⶗-wnFUB'}" {"2VD`Ky>=.ܐJع& ҒJ>)D T u@#d'/HYnζGU%K#cX)y.>]{׹Diz6Og1 #FɃ2V x'aP (^g/bom[-0f{1dnpILOkdrJ'ɒdnN`L8=-K,GZ>*KoO-u>+ܕD䬓="p[!/ $H$}uE G&i:!8!)6KKqZP;VGd#t"4yGSO'>]+C?q%@o}t?g9!nI IgstZ$l``F?|>O'ѷɋ9zB]3BtIz#t9# %$߁,$َu'_y:rx.1[[BҶ'Β/B":u//؅ȥ4)r_n$AC{! ،dq=6{a'ۅ*.ZrBҶK<#<*qMu\iVF#q>n?#Jz^7#m% C>tKΒelY(n(d!aoLQ*,s 6Uΐ41N%!|V!c{L!g}>]^䯹nX4ް^ &䄨%J-؞E^HP䎾Yw,/$ox<I$x2^4pz <DF|z{9 ,//JP~GȏېrmAI7S-%)?' ,N,)$\Kܼ"{Vy'7>[IjY/ܡ<^OQB i .9܅x$"/|-lN BDrU-yjO$NF$b Me< [ik؎9"HE{g Q`>ļQ%))Ye[zL(d"<*-ؖGT>ݯU,Wө e~4luoqN^9.׭u4%s /bȖUٞ Vy/%i.x!nI' ,m۷]" z[^'$".o'& (Q}<:Fd6Y/; r?(ΰFM$9%pY.7*ˡ.KrlbXJϗlLFcs&Y Oٵ bHTOpB-EđY)zɒbtVγ2ynJhY-/Ư=(d%//bYCycOb!K)/-Eg,bY RzK$} n3SQ cmcbLd-+$,/Y(xҰf bXoIu%x%VBy'd4%;'8H1&J#a;Ę"`BJ,^^璈TK%kk^#G)pY &OmH$*2%躱xc\P9rz]Bd'\唰>ݷ'>NbuR7N|bK& RDI"{R Y"~p>k}{9gb^ \;~J#/:K#9XM𱤒1oqU2Y%Гs sGK6~%2Iv1//rd/("hXųԷIX-ޓ;QB!;O{!u蟗ૂ۳6ȋ3 b^u[w*cmHYgedVmqY?'C< iFli\*9b[&rP^߱J]DFD>K~!amO:yx,ܷdp9r.O{֘_'PlϏU<YjķODh3d =#s0+92{ ,g5'Ǫydƒܻ̕lL^C% /}rVH_qy,[,^,m,]zlm,v)rBB,dux(D/=Ks#J pLI.ddǡ,vEh=M#m<ˡs#_џbй&HW$!Y'/ Ix!k%R "OK!-!{K|^N|fX3$bEi ܫD$%c$$6%/Q!Ξ~ڷf4dZI>KYkB]A?KoRx(n/^^I&~ >CԂ +=~ޱ} ~Tk o/^OV_G/QsdU'J[*k~?_ Hkk*,WԗWgE?ӯ;je<ܩ77777777777777777777777777777777Ŝ5( F/ 0|DArialew Roman|&| 0|DTahomaew Roman|&| 0| DWingdingsRoman|&| 0|0DTimes New Roman|&| 0|@DSymbolew Roman|&| 0| A .  @n?" dd@  @@`` XPt{ 5%.    0$A<C##GKMNOQRS"U XZ adeg,R$.Kb|M 0AAPf3f@38;<ʚ;ʚ;g42d2dc& 0ppp@ <4ddddk 0||& |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_0___PPT10 ?*+ SAVCBS 2004O  =q,7Encapsulating Concurrency as an Approach to Unification88(Santosh Kumar, Bruce W. Weide, Paolo A. G. Sivilotti The Ohio State University Nigamanth Sridhar Cleveland State University Jason O. Hallstrom Clemson University Scott M. Pike Texas A&M UniversityrP5B, :4Modular VerificationjProve the correctness of an implementation of a component using only the specification of its environment.bk  3-Framework ChoiceSequential Framework Assume a single thread of execution Collection of passive objects makes up the environment Think of the environment behavior in terms of Hoare-style pre- and post-conditions, weakest pre-conditions, etc. #H=3 Concurrent Framework Explicitly acknowledge the existence of multiple, concurrently executing threads Collection of active objects makes up the environment Think of the environment behavior in terms of Rely Guarantees, Hypothesis Conclusion, TLA, IOAutomata, etc.( G83 -'The Unification Problem)Major issues in sequential verification Contract style to use Impact of pointers, references, aliasing, etc. How to reason about inheritance? Major issues in concurrent verification Deadlock detection and avoidance Choice of synchronization primitives Scheduling of processes Protocol verification\(PfP(PtP(f(t4. Our ApproachXExtend a sequential verification framework (RESOLVE) to the domain of concurrent systemsYX360Example: Mutual ExclusionSeveral clients wanting mutually exclusive access to a resource The environment for clients is no longer passive Clients are aware of the existence of other concurrently executing clients in the system Clients negotiate with each other on mutually exclusive access to the resource. Clients can t use Sequential Verification FrameworkBqZZ4Zq471Facilitating a Solipsistic ViewNew description that simplifies semantics for the clients Each client  thinks it is the only thread of execution, and every change to the state of the environment is a result of its own actions. The state of the environment never changes spontaneously.N:v::v:5/Detailing Our Approach~Separation of a concurrent access component into a proxy component and a core component Proxy component presents a sequential interface to the clients of a concurrent access component How to abstract the inherent concurrency in a sequential spec (of Proxy)? Solution: Use relational specification How to ensure that the system behavior remains the same? Solution: A special relation between the Proxy and the Core   hides concurrency inherent in X`J'9^3J9   #)#Illustration of Our Approach 82Abstracting the ConcurrencyRelational Specification procedure Request() A counter, wait_index, is initialized to some natural number value that cannot be observed procedure Check_If_Available(ans) Every call results in a decrease of wait_index by a positive amount. The client gets access to the resource when wait_index hits 0. Clients can reason about their progress using a sequential verification framework.-Z\Z"ZZSZ           SP8 Q& C \*$Specifying Client ObligationsBWhat happens if some client does not relinquish the resource (by calling Release())? The progress of all waiting clients is jeopardized Solution Introduce a new  expects clause It encodes the obligations a client has towards its environment. The obligations are picked up while calling some operations. The mathematical structure for the  expects is a set of method calls that the client promises to make in future.^U3 !              C            -  93BIllustrating the  expects Clause$" NA client must release the resource. procedure Request() expects self.Release()f8$  @ 2,Summarizing the ContributionsTGoal : To present a sequential interface to the clients of a concurrent-access component Extract a sequential  proxy specification from a concurrent-access component Use relational specifications to abstract the effects of concurrency Introduce  expects clause to formalize the client obligationsYZZ3  (2 +=6Benefits of Our Approach&The effects of concurrency do not bleed through to the client Client verification can be carried out using a sequential verification framework Many client components are possible, all of whom benefit from this approach The effects of concurrency are limited to just one component, the proxy component Moreover, because of the  hides concurrency inherent in relation between the proxy and the core, the proof of proxy implementation is not too complicated either Illustrated by the proof for Mutex_Proxy implementation in the paper\>PPPEP>E 0*"Addressing the Unification Problem##(1+ Open IssuesHThe  expects clause Its mathematical structure  multi-set, string, or some other model instead of a set? Proof obligations for a non-terminating client Application of our approach to cooperative concurrent systems Proof system for verifying the correctness of core component implementations #1  3 More Questions and Comments? /    0` fy`ff3` Mj*333FV*` ffNNt^X` ffNL|>rL` +T3f3f` MMMff3f` Lx[he2` {$$>?" dd@,?nAd@    @ `  n?" dd@   @@``PR    @ ` ` p>> xp@(    6,' " `P ' T Click to edit Master title style! !$  0(& " ` ' RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  6+B#style.visibility<*d%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*d9%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*d9p%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*dp%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*d%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*df%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*df%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*d%(+s"  0 (  pD (  D D c $X% `P  %|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ B D c $Z%p `$@ 0 %|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ $B D s *D pp\ $@  0|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_$B D s *D\ p0 j $D  0|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_u D <i%  g$ 0|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ 7#(Sequential Verification Framework) D H@n% Opj $ 0|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ 7#(Concurrent Verification Framework)B D  br%E`FNQ&UVW}))? XX6381-D81^ DS &{'LO^ D+ YL^0L8]T+ YL7Gn2H+IJ7GI:9]T:I:Q= qR&QJ 7JJ >:*;9>:+$.+] x!+] 6381$ 3-D^ D %D^0L8]TH+ YL^0L8]T7G@8Cn2H+IJI:B,= qR&N7#Q7JK J 7J>:8*;9+ +$ x!+ ] x!+$(,`C0*0*ITNT0*0* BCCloud"pp $D   0|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ @Modern SystemsH D 0޽h ? ff[[ffRR|___PPT10.r0+hy~&D' ~%= @B D' = @BA?%,( < +O%,( < +Dd' =%(D ' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*D%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*D%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*D%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*D%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*D*%(D' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*D%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*D%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*D%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*D%(D' =%(D+' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*D%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*DD' =+4 8?dCB0-#ppt_h/2BCB#ppt_yB*Y3>B ppt_y<*D++0+D0 ++0+D0 ++0+D0 +  0 ll(  l l c $% `P  &|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_  l c $% ` %|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ H l 0޽h ? ff[[ffRR|___PPT10i.@+D=' = @B +   0 6 . 0 !t (  t t c $(% `P  &|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_  t c $%p ` %|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ < t <%"`P&=|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ Client 1B t s *DY  )|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_< t <%"`PR =|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ Client 2B t@ s *D@p|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_E t <$% ~ |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ 3Mutex6  t 6$%3@j |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ *? !t 6%3 |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ 3RH t 0޽h ? ff[[ffRR|___PPT10i.Q+D=' = @B +  0 P|l(  | | c $_ `P  _|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_  | c $_ ` _|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ H | 0޽h ? ff[[ffRR|___PPT10i.8+D=' = @B +   0  p(  p p c $% `P  &|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ B p c $`% `$D 0 %|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ H p 0޽h ? ff[[ffRR|J B ___PPT10" .0+YD ' = @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)%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*p)b%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*pb%(+nC  0 ,,;,0 ,,(  , , s *x!_ `P  _|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ < , <(_"`>}|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ Client 1B ,@ s *D8P|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_<  , <._"`~}|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ Client 2T  , <3_0T|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ BCheck_If_Available()B , s *D|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_/ , <:_XD|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_  Request()/ , <>_plPW|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_  Release()B , s *D  |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_B ,@ s *D ` 0 |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_T $, <F_04|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ BCheck_If_Available()/ %, <LL_||_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_  Request()/ &, <Q_pW|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_  Release()T (, <TV_ | |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ BCheck_If_Available()/ ), <[_p W |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_  Request()/ *, <`_0 |`  |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_  Release()T ,, <(f_ L  |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ BCheck_If_Available()/ -, <j_@ ' |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_  Request()/ ., <o_ @$ |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_  Release()J /, <tt_ t |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ 8 Mutex_Core K 0, <y_@p,' |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ 9 Mutex_Proxy K 1, <_I <0 |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ 9 Mutex_Proxy 6 4, 6_3 V |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ *? 5, 6<_3p .  `|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ 3R6 6, 6_ |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ *? 7, 6_0 |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ 3R6 8, 6(_@ |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ *? 9, 6_0 |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ 3R :, <_@$D 0|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ tprocedure Request (evaluates id: Integer) requires id is in self.all_proxies and not IS_REQUESTED(id, self.waiting_proxies) ensures self.all_proxies = #self.all_proxies and there exists ticket: NATURAL_NUMBER such that ((if #self.waiting_proxies = {} then (ticket = 0 and self.current_id = id) else (ticket > MIN_TICKET(self.waiting_proxies) and self.current_id = #self.current_id)) and self.waiting_proxies = #self.waiting_proxies union {(id, ticket)}) expects self.Release(id)r            =  ;   ;, <X_  ` $D 0|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ procedure Request () requires not self.requested ensures there exists i: NATURAL_NUMBER such that (self = (true, false, i)) expects self.Release()       ,#W H , 0޽h ? ff[[ffRR|f^___PPT10>.[p5m`+K@D2' _= @B D' = @BA?%,( < +O%,( < +D' =%(D' =%(DV' =A@BB5BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*:,%(D' =+4 8?RCBBCB#ppt_wB*Y3>B ppt_w<*:,D' =+4 8?RCBBCB#ppt_hB*Y3>B ppt_h<*:,D' =-g6B fade*<3<*:,D' =%(D' =%(DP' =A@BB5BB0B%(D' =+4 8?PCB ppt_wBCBB*Y3>B ppt_w<*:,D' =+4 8?PCB ppt_hBCBB*Y3>B ppt_h<*:,D' =-g6B fade*<3<*:,D' =1:Bhidden*o3>+B#style.visibility<*:,%(D' =%(D' =%(DV' =A@BB5BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*;,%(D' =+4 8?RCBBCB#ppt_wB*Y3>B ppt_w<*;,D' =+4 8?RCBBCB#ppt_hB*Y3>B ppt_h<*;,D' =-g6B fade*<3<*;,D' =%(D' =%(DP' =A@BB5BB0B%(D' =+4 8?PCB ppt_wBCBB*Y3>B ppt_w<*;,D' =+4 8?PCB ppt_hBCBB*Y3>B ppt_h<*;,D' =-g6B fade*<3<*;,D' =1:Bhidden*o3>+B#style.visibility<*;,%(++0+:,0 ++0+:,0 ++0+;,0 ++0+;,0 +B   0 Y Q (    c $ Z ``  &|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_   c $ Z   Z|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ u  <HHZ `|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ cprocedure Request () requires not self.requested ensures there exists i: NATURAL_NUMBER such that (self = (true, false, i)) expects self.Release() procedure Check_If_Available (replaces b: Boolean) requires self.requested Ensures self.requested and (if #self.wait_index /= 0 then self.wait_index < #self.wait_index else #self.wait_index = self.wait_index) and b = self.available = (self.wait_index = 0)z              #Y + H  0޽h ? ff[[ffRR|___PPT10i.p+D=' = @B +,   0 0"4(  4 4 s *XZ `P  Z|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ B "4 c $tZ `$@ 0 Z|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ H 4 0޽h ? ff[[ffRR|  ___PPT10 .[p5m`+wDr ' = @B D- ' = @BA?%,( < +O%,( < +Dd' =%(D ' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*"4%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*"4%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*"4%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*"40%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*"40%(+  0 l(    c $Z `P  Z|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_   c $ Z ` Z|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ H  0޽h ? ff[[ffRR|___PPT10i.uz+D=' = @B +n   0 `(  ` ` c $Z `P  Z|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ B ` c $Z `$D 0 Z|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ H ` 0޽h ? ff[[ffRR|___PPT10.+YD' = @B Du' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*`Y%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*`%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*`+%(+  0 p`(    S Z `P  Z|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_   S `Z ` Z|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ H  0޽h ? +T3f3f___PPT10i.cp+D=' = @B +  0 UM T(  T T c $Z `P  *|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ B T s *Dppr |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_B T s *Dr pP |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_B  T  b`ZE`FNQ&UVW))? XX6381-D81^ DS &{'LO^ D+ YL^0L8]T+ YL7Gn2H+IJ7GI:9]T:I:Q= qR&QJ 7JJ >:*;9>:+$.+] x!+] 6381$ 3-D^ D %D^0L8]TH+ YL^0L8]T7G@8Cn2H+IJI:B,= qR&N7#Q7JK J 7J>:8*;9+ +$ x!+ ] x!+$(,`C0*0*ITNT0*0* BCCloud" v$@  0|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ :Our Goal  5  T 6Zf"` } |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ RESOLVE< T 6Zf"`s ` |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ "Model Checking9 T <Zf"`|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ UNITY9 T <Zf"`TA|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ Seuss*B T 0D $D 0|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_I T <Z  g|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ 7#(Sequential Verification Framework)U T HTEPq |_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ 7#(Concurrent Verification Framework)H T 0޽h ? ff[[ffRR|ld___PPT10D.:0+|98D' RE= @B D' = @BA?%,( < +O%,( < +D' =%(Dz' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* T%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<* TD' =+4 8?dCB0-#ppt_h/2BCB#ppt_yB*Y3>B ppt_y<* TDG' =4@BBB B%(D' =1:Bvisible*o3>+B#style.visibility<*T%(D' =-6B'blinds(horizontal)*<3<*T+8+0+ T0 +  0 \l(  \ \ c $P_E `P  E|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_  \ c $DaE ` E|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ H \ 0޽h ? ff[[ffRR|___PPT10i.+D=' = @B +  0 N(    c $0*` `0   '|_INSTRUCTOR VIEW19C14C36-AC8E-43BC-9DB6-C2AAF774C7DC|PANE__TAG_ H  0޽h ? ff[[ffRR|___PPT10i.&W+D=' = @B +  0 H(  HX H C D   % H S %D 0  %  H H 0޽h ? 3380___PPT10.p rtcK aEf<9) Ѯ-j05 R^+RG *O5?z>>1Oh+'0T hp   , 8DL8Encapsulating Concurrency as an Approach to UnificationSantosh Kumar TexturedGary T. Leavens149Microsoft PowerPoint@`ރm@@:YY[@@R}6GSg  )'    """)))UUUMMMBBB999|PP3f333f3333f3ffffff3f̙3ff333f333333333f33333333f33f3ff3f3f3f3333f33̙33333f333333f3333f3ffffff3f33ff3f3f3f3fff3ffffffffff3ffff̙fff3fffff3fff333f3f3ff3ff33f̙̙3̙ff̙̙̙3f̙3f333f3333f3ffffff3f̙3f3f3f333f3333f3ffffff3f̙3f3ffffffffff!___www``4'A x(xKʦ """)))UUUMMMBBB999|PP3f3333f333ff3fffff3f3f̙f3333f3333333333f3333333f3f33ff3f3f3f3333f3333333f3̙33333f333ff3ffffff3f33f3ff3f3f3ffff3fffffffff3fffffff3f̙ffff3ff333f3ff33fff33f3ff̙3f3f3333f333ff3fffff̙̙3̙f̙̙̙3f̙3f3f3333f333ff3fffff3f3f̙3ffffffffff!___wwwllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllll՜.+,0    $ On-screen ShowThe Ohio State University ArialTahoma WingdingsTimes New RomanSymbol Textured8Encapsulating Concurrency as an Approach to UnificationModular VerificationFramework ChoiceThe Unification Problem Our ApproachExample: Mutual Exclusion Facilitating a Solipsistic ViewDetailing Our ApproachIllustration of Our ApproachAbstracting the ConcurrencySpecifying Client Obligations"Illustrating the expects ClauseSummarizing the ContributionsBenefits of Our Approach#Addressing the Unification Problem Open IssuesMore Questions and Comments?  Fonts UsedDesign Template Slide Titles'_>Gary T. LeavensGary T. Leavens