The Design and Verification of an Operating System Kernel.
Abstract
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 19, 1979
- Accession Number
- ADA072552
Entities
People
- Philip Gary Levy
Organizations
- University of California, Santa Cruz