Computer Science & Engineering Distinguished Lecture SMU School of Engineering Department of Computer Science and Engineering

Making Operating Systems Fault Free

Presented by

Prof. Wolfgang J. Paul
Computer Science Department, University of the Saarland

Friday, November 12, 2004, 3:30-4:30 p.m.

Forum, Hughes-Trigg Student Center, SMU

Refreshments will be served in front of the Forum from 3:00 to 3:30 pm.

Abstract: The development of computer systems is becoming increasingly prone to faults. This is mostly due to growing complexities combined with shorter development cycles and the use of testing methodologies that are insufficient to show correct operation. For current operating systems this problem can be frequently experienced by the occurrences of system crashes, hang-ups and the vulnerability by viruses.

It is the goal of our current efforts to enable computer systems that are free of design errors. This is done by showing their correctness using formal methods. Our ultimate goal is the formal verification of entire computer systems consisting of hardware, system software, communication system and applications. The focus of this talk is the correctness of an operating system which is a difficult problem in itself. We explain our approach to make operating systems fault free. We outline the paper and pencil correctness proof for an operating system microkernel written in C. The key ingredients of the proof are:

 1) a simulation of virtual machines by physical processors with swap memory. Here physical memory serves as a cache for virtual memory. In the correctness proof one argues simultaneously about hardware (memory management units) and low level software (page fault handlers).

2) semantics and provably correct compiler for an appropriate subset of C. One needs small steps semantics resp. structured operational semantics, because the computations of the kernel needs to be interleaved with computations of the users. One needs also to consider in line assembler code, because the variables of an abstract C machine do not show the user processes. The correctness proof for the compiler is nontrivial, because the recursion of small steps semantics does not match the recursion for the code generation very well.

3) the definition of an abstract machine model for an operating system kernel providing multiprocessing and virtual memory. In this model interrupt handling and function calls can be treated in a very uniform way. The simulation of this model by a physical machine combines the techniques from the first two parts.

This is joint work with M. Gargano, M. Hillebrand and D. Leinenbach. It is part of a large project funded by the German national government, which aims at the formal verification of entire computer systems consisting of hardware, system software, communication system and applications.

Biography: Prof. Paul has received his PhD in Computer Science from the University of the Saarland, Germany in 1973. He has been a PostDoc at Cornell University 1974-1976 and became an Associate Professor for Mathematics in Bielefeld, Germany in 1976. In 1982 he joined the IBM-Research LAB in San Jose, CA as a Research Staff Member and received the IBM Invention Achievement Award in 1986. In 1986, Wolfgang Paul joined the faculty of Computer Science at the University of the Saarland, Germany as a Full Professor. In 1987, Prof. Paul received the prestigious Leibnitz Award. At the University of the Saarland, he was head of the University Computing Center 1987-1991, the Chair of the Computer Science Department 1990-1992 and the Dean of the Technical School from 1998-2000. Prof. Paul has been awarded an honorary Doctoral Degree from Khabarovsk State University of Technology, Russia in 2004. He has graduated 37 PhD students and more than 100 Master’s students. He was a co-founder of the consulting company "Think&Solve" in 1999. His major research projects include the implementation of the SB-PRAM, a MIMD shared main memory CRCW-PRAM with 64 physical processors (1992-2002) and the lead in the VERISOFT System Verification Project (2003-) which is currently funded with more than $5M/year. He has published numerous conference and journal articles and co-authored three books on computer architecture and hardware design and one book on complexity theory. His current research interests have a focus in: hardware design, systems software and formal verification.

Hosted by CSE Dept. Everyone invited!