From: REID WILKES (reidwilkes_at_verizon.net)
Date: Tue Jan 06 2004 - 11:54:07 PST
This paper discusses the high level design of the 'THE' operating system (a somewhat clumsy name to use). This operating system was designed and implemented by a group at Technological University in The Netherlands in the late 1960's led by Edsger Dijkstra, who is the author of the paper. The paper emphasises three major issues: the hierarchical, layed structure of the OS itself; the design and development processes employed; and the formal correctness claims made of the system by the author. The discussion of the OS structure mainly focuses on a linear hierarchy of processes where each process level performs some system service and builds that service on top of services provided (and abstracted) by the processes lower in the hierarchy. Therefore, for instance, at level 1 memory management is provided, and processes above level 1 need not be concerned with the specifics of what we would today call 'virtual memory management'. As a related note, the paper interestingly describes something that is a precursor to or an early incarnation of a true virtual memory system - without ever using the term 'virtual memory'. Presumably the term was coined sometime after the basic ideas had been employed. The discussion of the development process is also quite interesting to read. Of particular interest to me were Dijkstra's comments about the necessity of having well trained, talented people on the team to be successful, and also his comments concerning the difficulty of properly testing systems. Dijkstra states that the proper testing of the system was extremely hard, but makes a point of saying that it is possible to generate all possible relevant states. (something which I might be tempted to take issue with). There is certainly an emphasis made that the design of the system should both facilitate testing, and at the same time be sufficiently well conceived as to render extensive testing unnecessary. Along this line, Dijkstra makes a number of claims throughout the paper that his system can be formally proved to be correct. Although only a very general, high level glimpse of the correctness proofs is given, I would say it is quite likely that such formal verification methods would be much harder to extend to the significantly more complicated systems common today.
This archive was generated by hypermail 2.1.6 : Tue Jan 06 2004 - 11:54:30 PST