On the formal foundation of a verification approach for system-level concurrent programs
Matthhias Daum · Publications of the UdS (Saarland University) · 2010
Though program verification is known and used since decades, the verification of a complete computer system still remains a grand challenge. In essence, this challenge stems from the interaction of various programs. Different techniques have been proposed for the verification of communicating programs. Common to all, however, is that they rely on several (usually implicit) assumptions about the underlying system. Typically, such assumptions include compiler correctness, scheduler fairness, and a certain noninterference between the local program behavior and its environment. This thesis aims at discharging these assumptions for the processes of the microkernel Vamos. More specifically, this work formally justifies the abstraction from a kernel model with explicit, deterministic scheduling to a concurrent process system with non-deterministic but temporally fair scheduling. Our formal results form the foundation of a verification approach for system-level concurrent programs. We outline this approach on example properties of a user-mode operating system. Obwohl es schon jahrzehntelang Programmverifikation gibt, wird die Verifikation eines kompletten Computersystems auch heute noch als eine grose Herausforderung angesehen. Im Wesentlichen ergibt sich diese Herausforderung aus der vielfaltigen Interaktion von Programmen. Verschiedene Techniken wurden fur die Verifikation kommunizierender Programme vorgeschlagen. Alle haben jedoch gemein, dass sie sich auf mehrere (meist implizite) Annahmen uber das zugrunde liegende System stutzen. In der Regel sind solche Annahmen Compiler-Korrektheit, Scheduler-Fairness und eine gewisse Storfreiheit des lokalen Programmverhaltens vom Verhalten seiner Umgebung. Die vorliegende Dissertation beschaftigt sich mit der Entlastung dieser Annahmen fur die Prozesse des Mikrokerns Vamos. Genauer gesagt, rechtfertigt diese Arbeit formal die Abstraktion von einem Kernmodell mit explizitem, deterministischem Scheduling zu einem nebenlaufigen Prozesssystem mit nicht-deterministischem, aber temporal fairem Scheduling. Die formalen Ergebnisse bilden die Grundlage eines Verifikationsansatzes fur nebenlaufige, systemnahe Programme. Dieser Ansatz wird am Beispiel von Eigenschaften eines User-Mode-Betriebssystems erlautert.