Welcome to the MIPS-Why3k Development
The
MIPS 32-bit architecture is used worldwide in teaching Computer Engineering due to its clean and simple design. This project aims to extend on the traditional view of the Hardware/Software interface to include aspects of
modelling, code
verification, code
analysis, and
certified programming.
To this end we undertake the approach of deductive program verification as provided by the
Why3 platform.
The development is ongoing (started September 2015), in parallel with teaching Micro-Computer Engineering (D0013E) at Luleå University of Technology (LTU). Hence the material will be subject to continuous updates and changes. The documentation roughly follows the presented material during classes as follows:
- Section A provides a gentle introduction to formal methods, without requiring prior knowledge, covering:
- get started by downloading the Why3 platform and at least one SMT solver,
- first-order logic,
- contract based verification and Hoare-logic,
- the Why3 tool and the WhyML language (functional and imperative constructs), and
- Why3 and SMT solvers.
- Section B presents a simple model of the MIPS-3k architecture, including:
- register-file model, (read/write operations and predicates for content and preservation),
- arithmetic instructions (already here you will be able to verify your first Why3k assembly program),
- the stack memory model and data memory operations (load/store operations with predicates for alignment, content and preservation.
- MIPS ABI (calling convention) and predicates for well-formedness and stack access separation
- Section C present a simple program verification example:
- from logic specification to verified (WhyML) implementation(s), recursive and imperative solutions for sum, and
- verifying Why3k assembly to its logic specification.
Planned content (currently not implemented/demonstrated)
- Refinements of the Why3k verification model:
- heap memory model, labels and predicates for separation of memory regions,
- data types, word-, half-word-, and byte-wise memory operations
- logic operations
- Performance 1:
- modeling of execution time,
- modeling of pipelining, and predicates to safe reordering.
- Concurrency:
- modelling of CP0, (kernel/user modes), and
- verification under concurrency-
- Performance 2:
- modeling of cache memory, cachelocking_, implications of concurrency.
- Certified Programming:
- the Why3 driver architecture, and
- extraction of Why3k models to MIPS-3k assembly format, instructions, labels , and data.