From a specification to an equivalence proof in object-oriented parallelism

Abstract

We investigate the use of a TLA specification for modeling and proving parallelization within an object-oriented language. Our model is based on Eiffel// a parallel extension of Eiffel, where sequential programs can be reused for parallel or concurrent programming with very minor changes. We want to prove that both versions of a given program (sequential and parallel) axe equivalent with respect to some properties. This article presents a description in TLA+ that captures the general Eiffel// execution model, and, as a case-study, specifies a program (a binary search tree) in both its sequential and parallel form. We then prove a property that demonstrates a behavioral equivalence for the two versions.