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]