A verified operating system kernel

Abstract

Kernel Layer The task layer defines the communication transitions in which a task may engage, but says nothing of how tasks are activated. The abstract kernel layer defines a scheme for activating a finite set of tasks. The distinction between a task and an I/O device is made more concrete. Each task has a state known completely to the abstract kernel, while the state of an I/O device is unspecified. Devices communicate with the kernel only through shared ports. A number of task management operations are specified, including time slicing, scheduling and error handling. The state space of the abstract kernel is described by the shell AK which defines a 10-tuple. The AK-PSTATES field is a fixed-size array of the private states of tasks. The private state of a task is easily proved to be isolated from the others by virtue of the properties of array access. The fields AK-IBUFFERS, AK-OBUFFERS and AK-MBUFFERS contain the shared state and, when grouped into a list, are identical to the chann...