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 PAbstractions & 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]