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 soundness
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 soundness
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 impl
Refinement 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
Our Contributions(Part 1) RGSim Rely/Guarantee Simulation Compositional w.r.t. parallel composition Flexible applicable optimizations in concurrent contexts concurrent gc fine-grained concurrent obj
Our Contributions (Part 1) • RGSim = Rely/Guarantee + Simulation – Compositional w.r.t. parallel composition – Flexible & applicable • optimizations in concurrent contexts • concurrent GC • fine-grained concurrent obj. • …
Our Contributions(Part 2) RGSim= Rely/ Guarantee+ Simulation A program logic for linearizability Support non-fixed LPs Verified 12 well-known algorithms(some are used in iava.util concurrent ight instrumentation mechanism to help verification Formal meta-theory: simulation ( extends rgsim) Establish a contextual refinement
Our Contributions (Part 2) • RGSim = Rely/Guarantee + Simulation • A program logic for linearizability – Support non-fixed LPs – Verified 12 well-known algorithms (some are used in java.util.concurrent) – Light instrumentation mechanism to help verification – Formal meta-theory: simulation (extends RGSim) • Establish a contextual refinement
Our Contributions(Part 3) RGSim Rely/Guarantee Simulation A program logic for linearizability A framework to characterize progress properties via contextual refinement( CR) Propose different termination-sensitive CR Equivalent to linearizability+ progress Unify all five progress properties Lf, WE, OF, DE, SF) lake modular verification of whole program C[O] easier Potential to have a generic verification framework for linearizability progress
Our Contributions (Part 3) • RGSim = Rely/Guarantee + Simulation • A program logic for linearizability • A framework to characterize progress properties via contextual refinement(CR) – Propose different termination-sensitive CR • Equivalent to linearizability + progress • Unify all five progress properties (LF, WF, OF, DF, SF) – Make modular verification of whole program C[O] easier – Potential to have a generic verification framework for linearizability + progress