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