Formal Models of Operating System Kernels (eBook)

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.