In this paper we propose a method for the deductive verification of out-of-order scheduling algorithms. We use TLPVS, our PVS model of linear temporal logic LTL, to deductively verify the correctness of a model based on the Mips R10000 design. Our proofs use the predicted values method to verify a system including arithmetic and memory operations and speculation. In addition to the abstraction refinement traditionally used to verify safety properties, we also use fairness constraints to prove progress, allowing us to detect errors which may otherwise be overlooked.
16th International Conference on Computer Aided Verification
On this page are stored the PVS dump files for the proof of an advanced MIPS-type out-of-order execution algoritm. The verification uses PVS3.1 and files can be undumped using the PVS undump menu option.
The Mips system definitions and proofs are included in one dump. These files should be run with the April 2004 version of TLPVS. Lastly, we include the PVS status (run times etc) for the Mips proof, as run on my linux PC.
The dump mips.dump contains the proof of the mips system (top level file is mipsRefSeq.pvs). We note that many theories in TLPVS contain definitions and lemmas that were used in other proofs, but were not needed in this example. TLPVS is designed to contain reusable theories, and so we did not feel it desirable to tailor the theories to this proof. The Mips dump and TLPVS dump should not be undumped in the same directory as they contain different pvs-strategies files. Once tlpvs_for_mips has been undumped it should be included as a prelude in the mips directory (alt-x load-prelude-library your_tlpvs_directory).
File mipsRefSeq contains the proof of formulas (1), (2) and (4). Response property (3) is proved in mipsLive.pvs. The sequential system is in seq.pvs, and the invariants are in mipsInvs1, mipsInvs2, mipsInvs3, and mipsInvsPv.pvs (the last containing invariants about predicted values.)