Verification of Linearizability as Refinement using Possibilities, Local Proof Obligations and their application to the Lazy Set Algorithm

This page describes KIV proofs that connect refinement theory with linearizability and possibilities as defined in [HeWi90]. Completeness of backward simulations is shown. As a special case, local proof obligations are derived and applied to verify the lazy set algorithm of [Helleretal05], which uses fine-grained locking. The local proof obligations and their application to the lazy set algorithm is described in [DSW11]. The global theory, that shows that backward simulation for possibilities is complete together with an application to the particularly intricate queue example of [HeWi90] is explained in [CAV12]. The projects described here contain the following results: The development is organized into six projects. The first two define data refinement, and data refinement with invariants. The third defines linearizability and possibilities.The fourth project gives connections between linearizabilty and refinement. It defines a set of proof obligations based on backward simulation with possibilities. It is proved that these proof obligations are complete. The fifth project derives local proof obligations from the global ones. These are suitable to verify linearizability for lazy sets..