Formal Refinement for Operating System Kernels

<P>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 Kernel’s 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.-</P>