Long-Standing problems in verifying Linearizability Objects with Non-Fixed Linearization Points(LPs) Future-dependent Lps(e.g. lazy set, pair snapshot) Helping (e.g. HSY elimination-backoff stack) Most existing work: either not supports them, or lacks formal soundnessLong-Standing Problems in Verifying Linearizability • Objects with Non-Fixed Linearization Points (LPs) – Future-dependent LPs (e.g. lazy set, pair snapshot) – Helping (e.g. HSY elimination-backoff stack) Most existing work : either not supports them, or lacks formal soundness