Progress of Concurrent Obiects with Partial methods Hongjin Liang and xinyu feng Nanjing University UStC
Progress of Concurrent Objects with Partial Methods Hongjin Liang and Xinyu Feng Nanjing University & USTC
acquire t What are good locks? as objects with partial methods? lock released Safety Functionality linearizability Progress Wait-freedom(wFy Lock-freedo LF) Starvation-freedom(SF) None applies! Deadhock-freedom(DF)
What are good locks? lock_acquire() { … } lock_release() { … } as objects with partial methods? None applies! Safety & Functionality: linearizability Progress: Wait-freedom (WF) Lock-freedom (LF) Starvation-freedom (SF) Deadlock-freedom (DF)
Not all locks are equally good
Not all locks are equally good!
Example: Test-and-Set (TAs)locks TAS locks acq i Tickets local succ. succ: false while(! succ i succ: =cas(L, 0, 1): re Unfair!
Example: Test-and-Set (TAS) locks acq() { local succ; succ := false; while( ! succ ) { succ := cas(L, 0, 1); } } rel() { L := 0; } TAS locks Tickets Unfair!
Example: Ticket locks acqot local i i: =getAndInc( next ) Fair! Whle(i!= serving)旮; relot serving: =serving+ 1;] Ticket locks serving next De 2 0 Queue management in banks
Example: Ticket locks Ticket locks Queue management in banks acq() { local i; i := getAndInc( next ); while( i != serving ) {} ; } rel() { serving := serving + 1; } next serving i Fair!
Not all locks are equally good Example: Test-and-Set (TAS) locks Example: Ticket locks TAS locks acq(( acqui i: getAndlnc( next ) Fair! succ:=false; while(! succ )i ICC: -cas(L, 0, 1); elI serving; serving 1; 1 Ticket locks= e Unfair! 上n Queue management in banks How to distinguish them? What are the progress-aware abstractions?
Not all locks are equally good! How to distinguish them? What are the progress-aware abstractions?
Abstractions contextual refinements Contextual Refinement(CR) o Ctx A iff VC. Obs Beh(c[o1)c Obs Beh(C[A]) void acq i Concrete Client c object o while(truer void relOt acq aca print(1) relo acq Is o as good as A, Abstract rel from Cs point of view? object a
Abstractions & Contextual Refinements O ctxt A iff C. ObsBeh(C[O]) ObsBeh(C[A]) Contextual Refinement (CR): Is O as good as A, from C’s point of view?
Abstractions contextual refinements Abstraction for linearizable objects atomic specs Filipovic et al. 2009] oin.Wr, atomic j分0 Similar equiv results hold for wf/LF/ SF/DF objects [Gotsman Yang 2011; Liang et al. 2013, 2016] oln.+ progress p分0 P∈ IWE, LF, SF, DF} progress-aware abstractions for progress P
Abstractions & Contextual Refinements Abstraction for linearizable objects: atomic specs O lin. w.r.t. atomic A O ctxt A Similar equiv. results hold for WF/LF/SF/DF objects: O lin. + progress P O ctxt AP P {WF, LF, SF, DF} progress-aware abstractions for progress P [Filipović et al. 2009] [Gotsman & Yang 2011; Liang et al. 2013, 2016]
Abstractions contextual refinements Abstraction for linearizable objects atomic specs Filipovic et al. 2009] o lin. w.rt. atomic 0 Cct Similar equiv results hold for WF/LF/SF/DF objects [ Gotsman Yang 2011; Liang et al. 2013, 2016 o lin. progress P< 0 Cctxt Ap no known results for locks! or, in general, objects with partial methods o lin, progress 0 Cctot ?
Abstractions & Contextual Refinements Abstraction for linearizable objects: atomic specs O lin. w.r.t. atomic A O ctxt A Similar equiv. results hold for WF/LF/SF/DF objects: No known results for locks! or, in general, objects with partial methods O lin. + progress P? O ctxt A??P [Filipović et al. 2009] O lin. + progress P O ctxt AP [Gotsman & Yang 2011; Liang et al. 2013, 2016]
Why is this bad? SF or DE? Depends on lock impl. Lock-based counter Compositional progress verification int cnt: of lock-based objects? inco t Redo the verification of acqu and relo ac in different obj [Liang & Feng 2016 cnt: cnt+1: No known results for locks! or, in general, objects with partial methods o lin. progress <>0 Cctxt ?
No known results for locks! or, in general, objects with partial methods O lin. + progress P? O ctxt A??P Why is this bad? • Compositional progress verification of lock-based objects? • Redo the verification of acq() and rel() in different obj. [Liang & Feng 2016] int cnt; inc() { acq(); cnt := cnt + 1; rel(); } Lock-based counter SF or DF? Depends on lock impl.!