The Design and Verification of an Operating System Kernel.

摘要

Practical aspects of the design, implementation, and verification of operating systems are explored in this thesis. Axiomatic techniques for proving parallel programs (developed by Hoare, Owicki, and Gries) are extended and applied in the proof of an operating system kernel. The techniques developed apply directly only to environments with a single physical processor. A technique for mutual exclusion that is simple to implement and has properties that contribute to verification is presented. It is based on the disabling of context switching to allow a single process to execute without pre-emption. In such an excluded region, sequential verification techniques can be applied.