Formal Verification of Processors and of Low Level Software

"LEISTUNGSGARANTIEN FÜR COMPUTERSYSTEME"

Am Freitag, den 23.05.2002, spricht um 16 c. t. im Gebäude 45, HS 003,

Prof. Dr. W. Paul

zum Thema:

Formal Verification of Processors and of Low Level Software

Abstract

Modern interactive theorem provers permit the formal verification of
mathematical proofs which are on paper many hundred
pages long. On several hundred pages one can prove the correctness of
remarkably complex computer systems, provided the
construction of the system is well structured and well documented.
Unfortunately such constructions and/or their
documentations are today extremely rare. We view this presently as the
main obstacle for the formal verification of real
systems.

In this talk we present bottom up a structured construction of a
powerful parallel processor. With the construction steps we state the
associated correctness assertions, and we make some remarks on the
proofs. We proceed in the folowing order:
1) arithmetic circuits
2) sequential fixed point core
3) pipelining
4) forwarding and stalling
5) speculation
6) interrupts
7) out of order execution
8) caches
9) memory management units
10) virtual shared memory.

It will turn out that in some situations the correctness assertions
concerning the hardware are so complex that it is by no means clear,
that they are 'right'. If
however one considers the hardware together with some interrupt service
routines of
the operating system, then one gets back to beautiful simple correctness
assertions which are 'right' in a completely obvious way.

This is partially joint work with IBM Böblingen.


Alle InteressentInnen sind zu dem Vortrag herzlich eingeladen.

Die Veranstaltung wird gemeinsam von der Fachrichtung Informatik und der
International Max Planck Research School getragen.