Refinement vs Progress Properties · Linearizability Correctness w.rt. functionality Not talk about termination /liveness properties Progress properties Lock-freedom(LF Wait-freedom(WF) Non-blocking impl. Obstruction-freedom(OF) Deadlock-freedom(DF) Starvation-freedom(SF Lock-based implRefinement vs. Progress Properties ? • Linearizability – Correctness w.r.t. functionality – Not talk about termination/liveness properties • Progress properties – Lock-freedom (LF) – Wait-freedom (WF) – Obstruction-freedom (OF) – Deadlock-freedom (DF) – Starvation-freedom (SF) Non-blocking impl. Lock-based impl