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	323
	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