טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
Ph.D Thesis
Ph.D StudentGlusman Marcelo
SubjectMechanizing Proofs of Computation Equivalence
DepartmentDepartment of Computer Science
Supervisor Professor Shmuel Katz


Abstract

   In the Convenient Computations proof method, one first analyzes a subset of the possible computations, which are more `convenient' to verify, and then shows that every computation can be reduced to some convenient one, by a relation that preserves the properties of interest. A common reduction is based on the notion that in concurrent systems one may consider two computations as equivalent if they differ only in the order in which independent operations occur.

In many cases, the equivalence to convenient computations is an interesting property by itself, as in the property of serializability of a distributed database, or sequential consistency of distributed implementations of shared memory.

   Proofs based on showing equivalence to convenient computations have been carried out manually in previous work. However, it is today possible to avoid many subtle errors by carrying out proofs within a mechanized environment.

   In this work, a proof environment is built based on the mechanized theorem prover PVS, in which the proof method is formalized in a generic way, and support is provided for inductive proofs of swap-equivalence - a reduction based on finitely many operation interchanges and a state-dependent operation independence notion. The idea of extending swap-equivalence to cover infinitely many swaps arises naturally, but it poses several challenges related to convergence, fairness, and the preservation of non-safety properties by such a reduction.

This is exemplified by the case of sequential consistency, where we show what is involved in extending a proof for finite computation prefixes to infinite computations. The last contribution is a technique based on finite-state transducers, which can be used to model check the equivalence of infinite computations. The system state is extended with a bounded history within which independent operations can be reordered and convenient prefixes recognized. An original technique based on prediction is given, that can in many cases solve the problem of unbounded out-of-order of operations with respect to the convenient computation. These techniques are implemented in a prototype tool based on the model checker Cadence SMV.