Formal Models of Operating System Kernels (eBook)
XIII, 333 Seiten
Springer London (Verlag)
978-1-84628-718-3 (ISBN)
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.
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.
Preface 7
Acknowledgements 8
Contents 9
List of Figures 12
1 Introduction 13
1.1 Introduction 13
1.2 Feasibility 14
1.3 Why Build Models? 16
1.4 Classical Kernels and Refinement 17
1.5 Hardware and Its Role in Models 23
1.6 Organisation of this Book 25
1.7 Choices and Their Justifications 26
2 Standard and Generic Components 29
2.1 Introduction 29
2.2 Generic Tables 29
2.3 Queues and Their Properties 33
2.4 Hardware Model 39
2.4.1 CCS Model 39
2.4.2 Registers 41
2.4.3 Interrupt Flag 43
2.4.4 Timer Interrupts 44
2.4.5 Process Time Quanta 48
2.5 Processes and the Process Table 51
2.6 Context Switch 63
2.7 Current Process and Ready Queue 64
3 A Simple Kernel 67
3.1 Introduction 67
3.2 Requirements 67
3.3 Primary Types 68
3.4 Basic Abstractions 70
3.5 Priority Queue 83
3.6 Current Process and Prioritised Ready Queue 89
3.7 Messages and Semaphore Tables 93
3.8 Process Creation and Destruction 96
3.9 Concluding Remarks 97
4 A Swapping Kernel 99
4.1 Introduction 99
4.2 Requirements 99
4.3 Common Structures 100
4.3.1 Hardware 100
4.3.2 Queues 105
4.3.3 Process Queue 106
4.3.4 Synchronisation and IPC 109
4.4 Process Management 115
4.5 The Scheduler 138
4.6 Storage Management 156
4.6.1 Swap Disk 170
4.6.2 Swapper 175
4.6.3 Clock Process 185
4.6.4 Process Swapping 198
4.7 Process Creation and Termination 203
4.8 General Results 210
5 Using Messages in the Swapping Kernel 215
5.1 Introduction 215
5.2 Requirements 216
5.3 Message-Passing Primitives 217
5.4 Drivers Using Messages 236
5.4.1 The Clock 237
5.5 Swapping Using Messages 240
5.6 Kernel Interface 243
6 Virtual Storage 251
6.1 Introduction 251
6.2 Outline 251
6.3 Virtual Storage 252
6.3.1 The Paging Disk Process 275
6.3.2 Placement: Demand Paging and LRU 279
6.3.3 On Page Fault 280
6.3.4 Extending Process Storage 300
6.4 Using Virtual Storage 311
6.4.1 Introduction 311
6.4.2 Virtual Addresses 312
6.4.3 Mapping Pages to Disk (and Vice Versa) 317
6.4.4 New (User) Process Allocation and Deallocation 318
6.5 Real and Virtual Devices 321
6.6 Message Passing in Virtual Store 322
6.7 Process Creation and Termination Swapping
7 Final Remarks 325
7.1 Introduction 325
7.2 Review 325
7.3 Future Prospects 328
References 331
List of Definitions 333
Index 343
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.
Erscheint lt. Verlag | 6.3.2007 |
---|---|
Zusatzinfo | XIII, 333 p. |
Verlagsort | London |
Sprache | englisch |
Themenwelt | Mathematik / Informatik ► Informatik ► Betriebssysteme / Server |
Mathematik / Informatik ► Informatik ► Software Entwicklung | |
Mathematik / Informatik ► Informatik ► Theorie / Studium | |
Schlagworte | Complexity • Computer • data structures • formal specification • Hardware • Kernel • operating system • Operating Systems (Kernels) • Performance • Process Algebra • security • Text |
ISBN-10 | 1-84628-718-9 / 1846287189 |
ISBN-13 | 978-1-84628-718-3 / 9781846287183 |
Haben Sie eine Frage zum Produkt? |
![PDF](/img/icon_pdf_big.jpg)
Größe: 2,1 MB
DRM: Digitales Wasserzeichen
Dieses eBook enthält ein digitales Wasserzeichen und ist damit für Sie personalisiert. Bei einer missbräuchlichen Weitergabe des eBooks an Dritte ist eine Rückverfolgung an die Quelle möglich.
Dateiformat: PDF (Portable Document Format)
Mit einem festen Seitenlayout eignet sich die PDF besonders für Fachbücher mit Spalten, Tabellen und Abbildungen. Eine PDF kann auf fast allen Geräten angezeigt werden, ist aber für kleine Displays (Smartphone, eReader) nur eingeschränkt geeignet.
Systemvoraussetzungen:
PC/Mac: Mit einem PC oder Mac können Sie dieses eBook lesen. Sie benötigen dafür einen PDF-Viewer - z.B. den Adobe Reader oder Adobe Digital Editions.
eReader: Dieses eBook kann mit (fast) allen eBook-Readern gelesen werden. Mit dem amazon-Kindle ist es aber nicht kompatibel.
Smartphone/Tablet: Egal ob Apple oder Android, dieses eBook können Sie lesen. Sie benötigen dafür einen PDF-Viewer - z.B. die kostenlose Adobe Digital Editions-App.
Zusätzliches Feature: Online Lesen
Dieses eBook können Sie zusätzlich zum Download auch online im Webbrowser lesen.
Buying eBooks from abroad
For tax law reasons we can sell eBooks just within Germany and Switzerland. Regrettably we cannot fulfill eBook-orders from other countries.
aus dem Bereich