Christoph Berg - Talks
 cb | cs | debian | bridge | irc | df7cb | projects | stuff  
[Ber04a]
Christoph Berg. Analyzing caches: Replacement strategies and persistence, July 2004. Ringvorlesung Graduiertenkolleg „Leistungsgarantien für Rechnersysteme“.
[ Slides | BibTeX | Link ]
The abstract interpretation framework used to analyze worst case cache behavior for real-time system works well for caches with least-recently-used (LRU) replacement. We give insights into why LRU is amenable to analysis and contrast this with a cache using FIFO (first-in, first-out) replacement, where no tight and at the same time safe upper bound on cache misses can be given.

The current approach evaluates each memory access in a program to decide its cache behavior. Another approach to cache analysis is to bound the total number of misses that can occur in parts of a given program. We outline research issues that will hopefully lead to better bounds on cache behavior in the future.

[Ber04b]
Christoph Berg. (K)ein Modell für den Cache des Motorola ColdFire, February 2004. Klausurtagung “Programming Systems and Compiler Design”, Dagstuhl.
[ Slides | BibTeX | Link ]
[Ber03a]
Christoph Berg. Discussion of a paper by Frank Mueller et al.: Virtual simple architecture (VISA): Exceeding the complexity limit in safe real-time systems, November 2003. Dagstuhl-Seminar 03471, ``Design of Systems with Predictable Behaviour''.
[ BibTeX | Dagstuhl Seminar | Link ]
[Ber03c]
Christoph Berg. Requirements for and design of a processor with predictable timing, June 2003. Ringvorlesung Informatik, Universität des Saarlandes. (Talk was also given at the Dagstuhl seminar ``Treffen von fünf Informatik-Graduiertenkollegs'', June 2003).
[ Slides | BibTeX | Link ]
Several processor features hinder precise prediction of program execution times on real-time systems. We show some examples where the processor behavior is hard to model for analysis due peculiarities in the processor's design. Upon that, we formulate principles that a processor designed for predictability must meet. Based on these principles, we give a design of a hard real-time processor with predictable timing, which is simultaneously capable of reaching respectable performance levels.
[Ber03b]
Christoph Berg. Prefetching-Techniken, February 2003. Oberseminar Compiler Design Lab, Saarbrücken.
[ Slides | BibTeX | Link ]
[Ber02b]
Christoph Berg. Formale Verifikation des VAMP-Mikroprozessors, August 2002. Graduiertenkolleg Leistungsgarantien für Rechnersysteme, Universität des Saarlandes.
[ Slides | BibTeX | Link ]
[Ber02a]
Christoph Berg. Formal verification of the VAMP microprocessor (project status), March 2002. Symposium on the Effectiveness of Logic in Computer Science (ELICS02), Max-Planck-Institut für Informatik.
[ Slides | BibTeX | Paper | Link ]
[Ber01b]
Christoph Berg. Verifikation der VAMP-Floating Point Unit, July 2001. Graduiertenkolleg Leistungsgarantien für Rechnersysteme, Universität des Saarlandes.
[ Slides | BibTeX | Link ]
Hardware zur Behandlung von Gleitkommazahlen ist sehr komplex und Korrektheit kann nicht alleine durch Tests sichergestellt werden. Mittels formaler Verifikation wird die Übereinstimmung der Hardware mit einer Spezifikation bewiesen.

Ich stelle das VAMP-Projekt vor, in dem am Lehrstuhl Paul der RISC-Prozessor VAMP (Verified Architecture MicroProcessor) verifiziert wird. Die Floating Point Unit (FPU) des VAMP unterstützt die Operationen Addition/Subtraktion, Multiplikation/Division, Vergleiche und Konversionen. Denormale Zahlen und Exceptions werden in Hardware behandelt.

Die Schaltkreise der VAMP-FPU werden auf Gatterebene (d.h. mit UND/ODER/NICHT-Gattern) in der Sprache des Theorembeweisers PVS implementiert. Gleichzeitig wird der IEEE Standard 754, in dem Gleitkomma-Arithmetik definiert wird, in PVS formalisiert. Die Spezifikation der FPU sagt nun aus, daß die von der FPU ausgeführten Rechnungen dem IEEE-Standard entsprechen. Die Übereinstimmung der Implementierung mit der Spezifikation wird mittels PVS bewiesen.

Der Vortrag gibt einen Überblick über das Verifikations-Projekt und skizziert den Beweisansatz. Als Ausblick wird auf die Implementierung des VAMP auf einem FPGA eingegangen.

[Ber01a]
Christoph Berg. Formal verification of a basic circuits library. February 2001. IASTED International Conference on Applied Informatics, Innsbruck (AI 2001).
[ Slides | BibTeX | Paper | Link ]
We describe the results and status of a project aiming to provide a provably correct library of basic circuits. We use the theorem proving system PVS in order to prove circuits such as incrementers, adders, arithmetic units, multipliers, leading zero counters, shifters, and decoders. All specifications and proofs are available on the web.
 
 Christoph Berg | Page last changed Fri Feb 13 19:45:13 2004 CET