Formal Models of Operating System Kernels phần 1

Tài liệu cung cấp kiến thức về thiết kế hệ điều hành nói chung và thiết kế hạt nhận hệ điều hành nói riêng.1. Introduction2. Standard and Generic Components3. A Simple Kernel4. A Swapping Kernel5. Using Messages in the Swapping Kernel6. Virtual Storage7. Final Remarks
Nội dung trích xuất từ tài liệu:
Formal Models of Operating System Kernels phần 1Formal Models of Operating System KernelsIain D. CraigFormal Models ofOperating SystemKernelsIain D. Craig, MA, PhD, FBCF, CITPBritish Library Cataloguing in Publication DataA catalogue record for this book is available from the British LibraryLibrary of Congress Control Number: 2006928728ISBN-10: 1-84628-375-2 Printed on acid-free paperISBN-13: 978-1-84628-375-8© Springer-Verlag London Limited 2007Apart from any fair dealing for the purposes of research or private study, or criticism or review, aspermitted under the Copyright, Designs and Patents Act 1988, this publication may only bereproduced, stored or transmitted, in any form or by any means, with the prior permission in writingof the publishers, or in the case of reprographic reproduction in accordance with the terms oflicences issued by the Copyright Licensing Agency. Enquiries concerning reproduction outside thoseterms should be sent to the publishers.The use of registered names, trademarks, etc. in this publication does not imply, even in the absenceof a specific statement, that such names are exempt from the relevant laws and regulations andtherefore free for general use.The publisher makes no representation, express or implied, with regard to the accuracy of theinformation contained in this book and cannot accept any legal responsibility or liability for anyerrors or omissions that may be made.987654321Springer Science+Business Mediaspringer.comTo a very special friend—Eheu fugaces labuntur anniPrefaceThe work that this book represents is something I have wanted to do since1979. While in Ireland, probably in 2001, I sketched some parts of a smalloperating system specification in Z but left it because of other duties. In2002, 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 toa first version of the kernel to be found in Chapter 3 of this book. I evenproduced a few proofs, just to show that I was not on a completely insanetack. I decided to suggest the material as the subject of a book to BeverleyFord. 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. Thereview process took less than 2 weeks; the response was as surprising as itwas encouraging: a definite acceptance. So I got on with it. This book is intended as a new way to approach operating systems de-sign in general, and kernel design in particular. It was partly driven by theold ambition mentioned above, by the need for greater clarity where it comesto kernels and by the need, as I see it, for a better foundation for operatingsystems design. Security aspects, too, played a part—as noted in the introduc-tory chapter, if a system’s kernel is insecure or unreliable, it will undermineattempts to construct secure software on top of it. Security does not otherwiseplay a part in this book. As Pike notes in [24], operating systems has become a rather boring area.The fact that two systems dominate the world is a stultifying problem. Thereare good ideas around and there is always new hardware that needs control-ling. The advent of ubiquitous computing is also a challenge. I would be verypleased if formal models helped people define new models for operating sys-tems (the lack of implementation problems is a real help—I have used formalmodels as a way of trying out new software ideas since the late 1980s). Of course, I hope that people from formal methods and operating systems,as well as computer science more generally, will read this book. I would likeviii Prefaceto think that it is a demonstration that system software can be modelled andspecified formally, endowing it with all the benefits of formal methods. What makes this book different are the facts that it contains proofs ofproperties and that it is broader in scope. The majority of the studies in theliterature omit proofs ([14] discusses proof but includes none). It seems to methat proof is necessary for, otherwise, one is just describing systems in justanother fancy notation. This book was written in a relatively short period of time (May–December,2005). Every effort has been made to ensure that it is error-free. The way Iapproached the process of writing it was intended to reduce errors. SteveSchuman has also read the entire text and the proofs. However, I cannotsay that the text does not contain any errors. For the mistakes that occur, Iapologise in advance.AcknowledgementsFirst of all, I would like to thank Beverley Ford. Next, I would like to thankHelen Desmond for running the project so smoothly. Steve Schuman promotedthe project, gave extremely useful advice on how to pitch it and read thevarious intermediate versions of the manuscript (some a little chaotic) ...