Craig Formal Models of Operating System Kernels

2007
ISBN: 978-1-84628-718-3
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 341 Seiten, eBook

Operating systems kernels are central to the functioning of computers. Security of the overall system, as well as its reliability and responsiveness, depend upon the correct functioning of the kernel. This unique approach – presenting a formal specification of a kernel – starts with basic constructs and develops a set of kernels; proofs are included as part of the text.

Zielgruppe

Professional/practitioner

Autoren/Hrsg.

Craig, Iain D.

Inhaltsverzeichnis

Standard and Generic Components.- A Simple Kernel.- A Swapping Kernel.- Using Messages in the Swapping Kernel.- Virtual Storage.- Final Remarks.

Leseproben

1.4 Classical Kernels and Refinement (p. 5)

The focus in this book is on what might be called the "classical" operating system kernel. This is the kind of kernel that is amply documented in the literature (the books and papers cited in this paragraph are all good examples).

It is the approach to kernel design that has evolved since the early days of computers through such systems as the TITAN Supervisor [34], the the operating system [19] and Brinch Hansen’s RC4000 supervisor [5], it is the approach to kernels described in standard texts on operating systems (for example, [29, 11, 26] to cite but three from the past twenty years).

The classical operating system kernel is to be found in most of the systems today:

Unix, POSIX and Linux, Microsoft’s NT, IBM’s mainframe operating systems and many real-time kernels. In days of greater diversity, it was the approach adopted in the design of Digital Equipment’s operating systems: RSTS, RSX11/M, TOPS10, TOPS20, VMS and others. Other, now defunct manufacturers also employed it for their product ranges, each with a different choice of primitives and interfaces depending upon system purpose, scope and hardware characteristics.

Such richness was then perceived as a nuisance, not a reservoir of ideas. The classical approach regards operating system kernels as layered entities: a layer of primitives must be defined to execute above the hardware, providing a collection of abstractions to be employed by the remainder of the system.

Above this layer are arranged layers of increasing abstraction, including storage management, various clocks and alarms. Finally, there comes the layer in which .le management, database interfaces and interfaces to network services appear. At the very top of the hierarchy, there is usually a mechanism that permits user code to invoke system services, this mechanism has been variously called SVCs, Supervisor Calls, System Calls, or, sometimes, Extracodes.

This approach to the design of operating systems can be traced back at least to the the operating system of Dijkstra et al. [19]. (It could be argued that the the system took many current ideas and welded them into a coherent and elegant whole.) The layered approach makes for easier analysis and design, as well as for a more orderly construction process. (It also assists in the organisation of the work of teams constructing such software, once interfaces have been defined.)

It is sometimes claimed that layered designs are inherently slower than other approaches, but with the kernel some amount of layering is required, raw hardware provides only electrical, not software, interfaces. The classical approach has been well-explored as a space within which to design operating system kernels, as the list of examples above indicates.

This implies that the approach is relatively stable and comparatively wellunderstood, this does not mean, of course, that every design is identical or that all properties are completely determined by the approach. The classical model assumes that interacting processes, each with their own store, are executed.