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 progressOur 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