The kernel of any operating system is its most critical component, as the rest of the system depends on it. This book shows how the formal specification of kernels can be followed by a completely formal refinement process that leads to the extraction of executable code. This formal refinement process ensures that the code precisely meets the specification. The author documents the complete process, including proofs.
1 Introduction.- 1.1. Reasons for Selecting the Examples.- 1.2. Refinement Method.- 1.3 Code Production.- 1.4 Organisation of this Book.- 1.5 Relationship to Other Work.- 2 The Simple Kernels Organisation.- 3 A Simple Kernel.- 3.1 Types.- 3.2 Hardware.- 3.3 The Process Table.- 3.3.1 Top Level.- 3.3.2 Refinement One.- 3.3.3 Refinement Two.- 3.4 Process Queue.- 3.4.1 Top Level.- 3.4.2 Refinement One.- 3.4.3 Refinement Two.- 3.5 Priority Queue.- 3.5.1 Top Level.- 3.5.2 Refinement One.- 3.5.3 Refinement Two.- 3.6 The Scheduler.- 3.6.1 Top Level.- 3.6.2 Refinement One.- 3.6.3 Refinement Two.- 3.7 Semaphores.- 3.7.1 Top Level.- 3.7.2 Refinement.- 3.8 Semaphore Table.- 3.8.1 Top Level.- 3.8.2 Refinement One.- 3.8.3 Refinement One-Again.- 3.9 Synchronous Messages.- 3.9.1 Preliminaries.- 3.9.2 Top Level.- 3.9.3 Refinement One.- 3.9.4 Refinement Two.- 3.10 The Clock.- 3.11 Sleepers.- 3.11.1 Top Level.- 3.11.2 Refinement One.- 3.11.3 Refinement Two.- 3.12 User Interface.- 3.12.1 System Initialisation.- 3.12.2 Process Creation.- 3.12.3 Process Management.- 3.12. 4 Inter-process Communication and Synchronisation.- 3.12. 5 Clock Operations and the Clock ISR.- 4 The Separation Kernel.- 4.1 Basic Architecture.- 4.2 Extending the Architecture.- 4.3 Summary.- 4.4 An Overview of the Formal Specification.- 5 A Separation Kernel.- 5.1 Basic Types.- 5.2 Hardware Issues.- 5.3 Security Exits and Return Values.- 5.4 The Process Table.- 5.4.1 Top Level.- 5.4.2 Refinement One.- 5.4.3 Refinement Two.- 5.5 Process Queues.- 5.5.1 Top Level.- 5.5.2 Refinement.- 5.6. The Scheduler.- 5.7 Storage Pools.- 5.7.1 Top Level.- 5.7.2 Refinement One.- 5.8 Raw Storage.- 5.8.1 Top Level.- 5.8.2 Message Buffering.- 5.9 Message Queues.- 5.9.1 Top Level.- 5.9.2 Refinement One.- 5.10 Kernel Interface-User Processes.- 5.10.1 Auxiliary Operations.- 5.10.2 Initialisation.- 5.10.3 Process Management.- 5.10.4 Message Passing.- 5.11 Devices-Trusted Code.- 5.11.1 Device Replies.- 5.11.2 Device Numbers.- 5.11.3 Device Process Creation.- 5.12 Process Interface to the Kernel.- 5.13 Final Thoughts.- 5.14 Closing Thoughts.- References.- List of Definitions.-