Progress of Concurrent Objects with Partial Methods

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.!