Mechanizing Proofs of Computation Equivalence

A proof-theoretic mechanized verification environment that allows taking advantage of the “convenient computations” method is presented. The PV S theories encapsulating this method reduce the conceptual difficulty of proving a safety or liveness property for all the possible interleavings of a parallel computation by separating two different concerns: proving that certain convenient computations satisfy the property, and proving that every computation is related to a convenient one by a relation which preserves the property. We define one such relation, the equivalence of computations which differ only in the order of independent operations. We also introduce the computation as an explicit semantic object. The application of the method requires the definition of a “measure” function from computations into a well-founded set. We supply two possible default measures, which can be applied in many cases, together with examples of their use. The work is done in PV S, and a clear separation is made between “infrastructural” theories to be supplied as a proof environment library to users, and the specification and proof of particular examples.