Development and Usage of a Simulation Environment for Testing and Verifying the L4 Microkernel Mapping Database

摘要

Nowadays, the increasing elaboration and performance of computing platforms have led to an augment of the complexity of operating systems. This augment inevitably causes an increment of the programming and design errors. New techniques to test and verify these systems, with more emphasis on those that are regarded as more critical, have been proven necessary. In this paper, we present a new methodology that can be used in testing the validity of the different components of a computer program. It is based on the implementation of a simulation environment that extracts a component from the rest of the system and runs on it several automated tests and verification processes. This methodology has already been used in the late stages of the L4 development. L4 is a small microkernel that serves as base for numerous research and development projects. One of its design paradigms is the externalization from the kernel of the user level memory allocation policies. This externalization forces the microkernel to maintain a precise and complete mapping database of the status of the different address spaces. To manage this database, it uses complex structures and convoluted algorithms. With the simulation environment, several errors were discovered in early development stages of a new mapping database. A fast feedback loop of coding and testing soon led to a final version even more stable than the old, simpler, mapping database.