ࡱ> O( / 00DArialmi ||,00z[ 0"DComic Sans MS,00z[ 0B DEras Demi ITC,00z[ 0"0DSymbolmi ITC,00z[ 0 A .  @n?" dd@  @@`` p0 ,5  () 5 ()    21    >>//HG,,R5SUVW  `abcdefghijklnpqstuvwxyz{|}~ 0AA 3@8KL3R ʚ;ʚ;g4RdRdz[ 0Pppp@  <4dddd@< 0|80___PPT10 ?  %GFVerification of Multithreaded Object-Oriented Programs with InvariantsGG(0Bart Jacobs, K. Rustan M. Leino, Wolfram Schulte,9,Based On4Barnett, DeLine, Fhndrich, Leino, Schulte. Verification of object-oriented programs with invariants. Journal of Object Technology, 2004. Hoare. Monitors: an operating system structuring concept. CACM, 1974.n  Example in C#class Account { int balance; } Account act = & ; int b0 = act.balance; act.balance += 50; int b1 = act.balance; b1 == b0 + 50? Not necessarily!o  & t   "3& Example in C#qlock (act) { b0 = act.balance; act.balance += 50; b1 = act.balance; } b1 == b0 + 50? Not necessarily!>R N >   $Example in Spec#"class Account { int balance; } Account act = & ; int b0 = act.balance; act.balance += 50; int b1 = act.balance; Rejected by Spec# if act not ownedo# & t   %Example in Spec#oacquire act; int b0 = act.balance; act.balance += 50; int b1 = act.balance; release act; b1 == b0 + 50? Always!Y&b    &4' ObservationsnC# offers synchronization primitives But their correct usage is not enforced Spec# s primitives are very similar But their correct usage is enforced This is a must for local reasoningMdThe Bottom LineProgrammers want to reason locally about field accesses In C# this is unsound due to interference between threads In Spec# this is sound because Spec# enforces mutual exclusionWhat Will My Thread Do?A thread can be influenced by other threads only at inter-thread I/O operations Inter-thread I/O operations: In C#: field accesses (= everywhere) In Spec#: acquire and release operationsZmNm/ Spec#Spec#: conservative extension of C# Spec# compiler: Run-time checking Requires no method contracts Strictest mode guarantees safety, even in presence of malicious code Boogie: static verification for Spec# SoundTFZbZ&ZZFb&OverviewMethodology is introduced gradually Per-object exclusion Aggregate objects Object invariants Related work, future work, conclusion6$9&$9&Per-Object ExclusionIn each object, we introduce an owner field owner is either null or a thread Before thread t accesses field o.f, we check that o.owner == t *,l Per-Object ExclusionWe also introduce two new statements: acquire o; release o; owner field can be modified only by the acquire and release statements&G&#  Per-Object ExclusionWhen thread t creates an object o, we set o.owner = t; When thread t acquires an object o, we first wait until o.owner == null and then set o.owner = t; release o; checks that o.owner == t and then sets o.owner = null;>Z     b*>  Exampleclass Account { int balance; } Account act = new Account(); act.balance = 5; release act; & acquire act; act.balance++; release act; >) "  Aggregate ObjectsAn aggregate object is one that uses other objects for its representation We support treatment of aggregate objects with their representation as one entity We support exchange of rep objects Aggregate ObjectsWe introduce a rep field modifier to indicate fields that hold rep objects The owner field of a rep object points to its aggregate object (Thread objects have no rep fields; they denote the thread.)(Aggregate ObjectsBefore a thread can modify an aggregate object, it must unpack it unpacking causes the rep objects to become owned by the thread packing transfers ownership back to the aggregate objectT895Aggregate ObjectsWe introduce into each object a boolean field inv to indicate when it is being modified This field is set by pack and reset by unpack While !inv, rep modifiers are void.< Aggregate ObjectsR[[ o = new C; ]] o = new C; o.owner = t; o.inv = false; [[ x = o.f; ]] assert o.owner == t; x = o.f; [[ o.f = x; ]] assert o.owner == t; assert !o.inv; o.f = x; P     [[ acquire o; ]] lock (o) { while (o.owner != null) Monitor.Wait(o); o.owner = t; } [[ release o; ]] assert o.owner == t; assert o.inv; lock (o) { o.owner = null; Monitor.Pulse(o); // (*) }.P !  )#  Aggregate Objects[[ pack o; ]] assert o.owner == t; assert !o.inv; for each rep field o.f: if (o.f != null) { assert o.f.owner == t; assert o.f.inv; } for each rep field o.f: if (o.f != null) o.f.owner = o; o.inv = true;Z      [[ unpack o; ]] assert o.owner == t; assert o.inv; for each rep field o.f: if (o.f != null) o.f.owner = t; o.inv = false;bZt   Example Example"Example#Example$Example%Example&Example'Object InvariantsBehavior of thread is influenced externally only at acquire operations Full thread-local reasoning requires knowledge about incoming aggregates For this reason, we introduce object invariants(Object Invariants|Each class may declare an invariant Invariant can mention only fields this.f1.f2.& .fn.g where f1, f2, & , fn are rep fields pack statement checks invariant Therefore, invariant holds when invF <Sh)Object Invariantsrelease statement checks inv Therefore, free aggregates satisfy their invariant Cf. Hoare s monitor invariants6oR6+Example: Local Reasoningfclass A { int p, q; invariant q != 0; } class B { rep A a; invariant a != null; } B b = & ; acquire b; unpack b; unpack b.a; // OK, no NRE int n = b.a.p / b.a.q; // OK, no DBZE0    b j7)SummarySpec# ensures field accesses are thread-local operations Supports aggregate objects Object invariants are enforced Full dynamic enforcement Sound thread-local static checking*Some Related WorkJESC/Modula-3, ESC/Java Safe Concurrent Java Vault Calvin/R Atomizer Eraser,ESC/Modula-3, ESC/Java[Detlefs, Flanagan, Leino, Lillibridge, Nelson, Saxe, Stata 1998/2002] Performs static checking Each field is protected by a separately, freely chosen lock Not formalized; no soundness proofb   - Safe Concurrent Java[Boyapati, Lee, Rinard 2002] Type system that supports thread-local, aggregate, and read-only objects, and unique pointers Does not support object invariants Does not support ownership transfer,0#Vault[DeLine, Fhndrich 2002] Uses linear types for mutual exclusion Pack and unpack are implicit Does not support general invariants, o.!Calvin/R[Freund, Qadeer 2004] Specifies and verifies atomic transactions performed by a method User specifies per-field protection More flexible, but significantly more complex than Spec# 1$Atomizer[Flanagan, Freund 2004] Dynamically checks atomicity of unannotated methods Enables sequential reasoning We support sequential reasoning for non-atomic methods as well8 e/"Eraser[Savage, Burrows, Nelson, Sobalvarro, Anderson 1997] Finds data races in a running program Found to be effective in practice No guarantees about completeness or soundness +Current and Future WorkAssessing efficiency Adding support for conditions, multiple reader threads, immutable objects, & Liveness properties Inference of annotationsb%8* ConclusionSpec# ensures field accesses are thread-local operations Supports aggregate objects Object invariants are enforced Full dynamic enforcement Sound thread-local static checkingP1 ` fp=` f3` 33f` 3f33` 3f3f` fff3` f3` 3|f>?" dd@,|?" dd@   " @ ` n?" dd@   @@``PV    @ ` `p>> &-- 44P,(  P P BW CfDE,F6 W  Pn n /Hf  W W @`"" P S   "`P  T Click to edit Master title style! !  P C  "   RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S P C d "``  F*0 P C  "`   H*0 P C  "`8  H*0 P B_ CwDE,F6  12w  _  `@`"55^  P B C DE F*    FRj @`"%wT  i  P " iV  P BCDE`Fj3R3[J3d =xjXy.|7 sb"3324@`" Y:  P BCDEF"x@`" E  P B2C5DE0F: 3~25Fy+**. @`",X P BCDE F*ENEE@`"V P BCDE F*$ @`" lE P BCDEF"H@`"C P BCDE F*PWPP@`" P BC\DEF&j\+@`" P B8CDEFN8 @`"[mb  i P# " ib   P# "  P B9CDE(F2 kr $9[CJe kk@`"Z P BC DE$F. ( G((@`"|) P BWCDE$F. $],PWt.@`" _ P BCDEF"d4dd@`"L P BC(DE@FJ"BDF2Pk(x"""$@`". P BCDE(F2 [PjGaX9@`"5`Nb  iH P# " iH P BCDE F*n(BPgTnn@`"'` P "BCpDEhFr?4CfcCPp(Y**.:(sk6Pg_68@`"OH P BCODE$F. tj!:^OLtt@`"ja  P BCDE8FB|Q&9+Cca=wJL2 @`"  !P BCDE,F6 Lq>thc;?@`"BB> "P BC DE4F> )B@  tMY)) @`"H.  #P BCDE4F> _N95_}H9 @`" i $P BCDE@FJ~Bt*n Lp_55 n~~~"$@`"lT \5O %P "5\O &PB ZBC DEF!!T | ? s OOCi3[~d|YAdzu H  T T DH@`"\< ) 'PB ZBC DEF!!T | ? s OOCi3[~d|YAdzu H  T T DH@`"5O x T 9B (P "9B b 9B )P# "9B *P BC&DE F*{ V&Ox{ { @`"T\ 9B +P "9B ,P B\C]DE$F. *]\g @`"t9F -P B(CDEXFb`M;Bl (TDAkl`^tZ?v.0@`"d .P BC DEF" =@`"6zsn /P 0B CDElFv_  5  o } 6 +   N ? T iS/x9 h  r [  u _ _ 8<@`"B 0P BCVDE F*PjV!rPP@`"iC 1P BCDE F*NT~(rFNN@`"( 2P BCDE F*N<:W6NN@`"v 3P BCDE F*X425+XX@`"iy,hB 4P s *DԔ"T0B P s *޽h ? fp=80___PPT10.Uo Crayons K YQ0T(  T T BC#DEF" y#e  @`"  T <X\"3 Ԕ8c?"` P  " T Click to edit Master title style! ! T C _" " p  " W#Click to edit Master subtitle style$ $ T C a" "`` " F*0 T C f" "`  " H*0 T C `l" "`  " H*0T z N[  T " zN[  T zBCDE0F: >,GS:@`" E  T zB2C5DE0F: 3~25Fy+**. @`" 5  T zBCDE F*ENEE@`"  \ z N[  T "z N[  T zBCDE F*n(BPgTnn@`"zw  f T (zBCpDEhFr?4CfcCPp(Y**.:(sk6Pg_68@`" [  T zBCDEF"d4dd@`"Z!   T zBCODE$F. tj!:^OLtt@`"U N  T zBC(DE@FJ"BDF2Pk(x"""$@`"= L $ T C BCDELF$)+,04k|w@xy( @  E@      "p 8; F {8  T"{\ {  T "{   T BCDE0F: >,GS:@`"{   T B2C5DE0F: 3~25Fy+**. @`"j   T BCDE F*ENEE@`"X\ {   T "{   T BCDE F*n(BPgTnn@`"|f T (BCpDEhFr?4CfcCPp(Y**.:(sk6Pg_68@`"{  T BCDEF"d4dd@`"D T BCODE$F. tj!:^OLtt@`"| T BC(DE@FJ"BDF2Pk(x"""$@`"N T  B0CDE(F| fYc 0 @   " 8 B T s *޽h ? fp=80___PPT10.UoLK0 ` 0(   x  c $$x"T` P  " x  c $x"T p  " P  s *޽h ?"` 33___PPT10i.|+D=' = @B +$ K 0$(  0r 0 S P`P   r 0 S FP   H 0 0޽h ? fp=80___PPT10.X9} K pd$(  dr d S "P`P  " r d S "P   H d 0޽h ? fp=___PPT10i.dG+D=' = @B + K @0(  x  c $4"P`P  " x  c $"P  " H  0޽h ? fp=___PPT10i.dG+D=' = @B + K 0(  x  c $8"P`P  " x  c $ "P  " H  0޽h ? fp=___PPT10i.dG+D=' = @B + K 0(  x  c $("P`P  " x  c $"P  " H  0޽h ? fp=___PPT10i.dG+D=' = @B +$ K P$(  r  S "P`P  " r  S "P  " H  0޽h ? fp=80___PPT10.Xsr} K P\$(  \r \ S "P`P  " r \ S "P  " H \ 0޽h ? fp=___PPT10i.s`+D=' = @B +} K ``$(  `r ` S "P`P  " r ` S "P  " H ` 0޽h ? fp=___PPT10i.a?X+D=' = @B +} K 0$(  r  S *pP`P  p r  S 9pP  p H  0޽h ? fp=___PPT10i.E+D=' = @B + K  :(  r  S JpP`P  p   S #!P  p "p`PpH  0޽h ? fp=___PPT10i. +D=' = @B +} K @$(  r  S UpP`P  p r  S VpP  p H  0޽h ? fp=___PPT10i.c+D=' = @B +} K P$(  r  S X_pP`P  p r  S ]pP  p H  0޽h ? fp=___PPT10i. +D=' = @B +} K `$(  r  S gpP`P  p r  S hpP  p H  0޽h ? fp=___PPT10i.p8"+D=' = @B +} K p$(  r  S upP`P  p r  S TvpP  p H  0޽h ? fp=___PPT10i. +D=' = @B +} K $(  r  S T}pP`P  p r  S (~pP  p H  0޽h ? fp=___PPT10i.i3,+D=' = @B +} K $(  r  S pP`P  p r  S tpP  p H  0޽h ? fp=___PPT10i.@ +D=' = @B +} K $(  r  S |pP`P  p r  S PpP  p H  0޽h ? fp=___PPT10i.(+D=' = @B +} K $(  r  S hpP`P  p r  S (pP  p H  0޽h ? fp=___PPT10i. +D=' = @B + K  (  r  S pP`P  p x  c $xpP  p r  S LpPX   p H  0޽h ? fp=___PPT10i.`i +D=' = @B + K (  r  S DpP`P  p r  S pP  p r  S طpPX   p H  0޽h ? fp=___PPT10i.qq+D=' = @B + K (  X2  00 0 r  S \pP`P  p   0p` <Thread 1 (2   0tp   lclass Agg { rep Rep f; } class Rep {} Agg a = new Agg; Rep r = new Rep; pack r; a.f = r; pack a; release a;m 2  b X2  00X  0P  H  0޽h ? fp=___PPT10i. z̕+D=' = @B + K  (  X2  00 0 x  c $8pP`P  p   0p` <Thread 1 (2 X2  00X2  0   0Pp  3a 2X   0    0   lclass Agg { rep Rep f; } class Rep {} Agg a = new Agg; Rep r = new Rep; pack r; a.f = r; pack a; release a;m 2   b H  0޽h ? fp=___PPT10i. z̕+D=' = @B + K 0 n(  X2  00 0 x  c $P`P     0` <Thread 1 (2 X2  00X2  0   0p  3a 2X2   00    0 3r 2X   0 @ 0   0   lclass Agg { rep Rep f; } class Rep {} Agg a = new Agg; Rep r = new Rep; pack r; a.f = r; pack a; release a;m 2  " b H  0޽h ? fp=___PPT10i. z̕+D=' = @B + K 0(@ (  X2  00 0 x  c $$P`P     0&` <Thread 1 (2 X2  00X2  0   0*  3a 2X2   00    0. 3r 2X2   0  X   00    02   lclass Agg { rep Rep f; } class Rep {} Agg a = new Agg; Rep r = new Rep; pack r; a.f = r; pack a; release a;m 2  * b H  0޽h ? fp=___PPT10i. z̕+D=' = @B +i K xP (  X2  00 0 x  c $8CP`P     0D` <Thread 1 (2 X2  00X2  0   0PI  3a 2X2   00    0N 3r 2X2   0  X   0  RB  s *D0  0O   lclass Agg { rep Rep f; } class Rep {} Agg a = new Agg; Rep r = new Rep; pack r; a.f = r; pack a; release a;m 2  3b H  0޽h ? fp=___PPT10i. z̕+D=' = @B +W K nf` (  X2  00 0 X2  0 @ x  c $!P`P     0d`` <Thread 1 (2 X2  00X2  0   04e  3a 2X2   00    0.   --'--$>.?&D!--'--$K$G&F+I*J'M%K$--'--6$  ?-J+S-V*N%JGK%Q*I)A+B$FB >$=*     --'--$ F@  --'--$  --'--"$ '/4 / &"%,!5"6 2(  --'--*%X.Z/]0_1a1b1c1d/e.e.f-g-g.h.h/i1j3j4j5--'@BComic Sans MS-. 2 O}Verification of      . "System-@BComic Sans MS-. %2 iRMultithreaded Object    .-@BComic Sans MS-.  2 i8- .-@BComic Sans MS-. *2 NOriented Programs with      .-@BComic Sans MS-. 2 Invariants  .-@BComic Sans MS-. 2 O|Verification of      .. 2 N{Verification of      .-@BComic Sans MS-. %2 iQMultithreaded Object    .. %2 hPMultithreaded Object    .-@BComic Sans MS-.  2 i7- ..  2 h6- .-@BComic Sans MS-. *2 MOriented Programs with      .. *2 LOriented Programs with      .-@BComic Sans MS-. 2 Invariants  .. 2 Invariants  .-@BComic Sans MS-. 2 TBart Jacobs, K.    .. 2 SBart Jacobs, K.    .-@BComic Sans MS-. 2 Rustan .. 2 Rustan .-@BComic Sans MS-.  2 M. ..  2 M. .-@BComic Sans MS-. 2 Leinon .. 2 Leinon .-@BComic Sans MS-.  2 :, ..  2 9, .-@BComic Sans MS-. 2 Wolfram Schulte   .. 2 Wolfram Schulte   .-՜.+,D՜.+,D    Diavoorstellingiav)* /ArialComic Sans MSEras Demi ITCSymbolCrayonsGVerification of Multithreaded Object-Oriented Programs with Invariants Based OnExample in C#Example in C#Example in Spec#Example in Spec# ObservationsThe Bottom LineWhat Will My Thread Do?Spec# OverviewPer-Object ExclusionPer-Object ExclusionPer-Object ExclusionExampleAggregate ObjectsAggregate ObjectsAggregate ObjectsAggregate ObjectsAggregate ObjectsAggregate ObjectsExampleExampleExampleExampleExampleExampleExampleObject InvariantsObject InvariantsObject InvariantsExample: Local ReasoningSummarySome Related WorkESC/Modula-3, ESC/JavaSafe Concurrent JavaVault Calvin/R AtomizerEraserCurrent and Future Work Conclusion Gebruikte lettertypen Ontwerpsjabloon Diatitels*D 4<Version%_) yLieven DesmetLieven Desmet  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~Root EntrydO)Current UserSummaryInformation(XPowerPoint Document()DocumentSummaryInformation8Root EntrydO){AlCurrent UserMSummaryInformation(XPowerPoint Document()'_)Gary T. LeavensGary T. Leavens