Craig Formal Models of Operating System Kernels

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

E-Book, Englisch, 341 Seiten, eBook

The work that this book represents is something I have wanted to do since 1979. While in Ireland, probably in 2001, I sketched some parts of a small operating system speci?cation in Z but left it because of other duties. In 2002, I worked on the sketches again but was interrupted. Finally, in April, 2005, I decided to devote some time to it and produced what amounted to a ?rst version of the kernel to be found in Chapter 3 of this book. I even produced a few proofs, just to show that I was not on a completely insane tack. I decided to suggest the material as the subject of a book to Beverley Ford. The material was sent on a Thursday (I think). The following Monday, I received an email from her saying that it had gone out for review. The review process took less than 2 weeks; the response was as surprising as it was encouraging: a de?nite acceptance. So I got on with it. This book is intended as a new way to approach operating systems - sign in general, and kernel design in particular. It was partly driven by the old ambition mentioned above, by the need for greater clarity where it comes to kernels and by the need, as I see it, for a better foundation for operating systemsdesign.Securityaspects,too,playedapart—asnotedintheintrod- tory chapter, if a system’s kernel is insecure or unreliable, it will undermine attemptstoconstructsecuresoftwareontopofit.Securitydoesnototherwise play a part in this book.

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.