A comparison of two verification methods for speculative instruction execution

T. Arons and A. Pnueli

In this paper we describe and compare two methodologies for verifying the correctness of a speculative out-of-order execution system with interrupts. Both methods are deductive (we use PVS) and are based on refinement. The first proof is by direct refinement to a sequential system; the second proof combines refinement with induction over the number of retirement buffer slots.

TACAS00: Tools and Algorithms for the Construction and Analysis of Systems

Gzipped PostScript PDF

PVS dump files

We provide the PVS dump files for the direct proof and for the inductive proof. Both include a file called "allTheories" which includes all the necessary files and gives a brief explanation of the different files. Notes:
  1. We used PVS version 2.2
  2. The speculative design, called DES in the paper, is referred to as "Spec" in the proofs.
  3. The proof of "liveness" and that the split transition relation does not exclude any behaviours of the joint transition relation is identical for the two systems (modulo auxiliary variables) and is included in the dump file for the direct proof (as live.pvs and SplitEqual.pvs, respectively).
  4. When running the indirect proof, one may get "extra" type-checks not included in the given proofs. This occurs if RefB or RefMapB is in the context when one is running other theories (Ref1 etc). It is therefore suggested that these files be left for last (the logical order).
    If such typechecks do occur, exit PVS, erase the .pvscontext file, and start the troubled proof again.
Please refer any queries to Tamarah.