Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
The Multics kernel design project

Michael D. Schroeder, David D. Clark, and Jerome H. Saltzer


We describe a plan to create an auditable version of Multics. The engineering experiments of that plan are now complete. Type extension as a design discipline has been demonstrated feasible, even for the internal workings of an operating system, where many subtle intermodule dependencies were discovered and controlled. Insight was gained into several tradeoffs between kernel complexity and user semantics. The performance and size effects of this work are encouraging. We conclude that verifiable operating system kernels may someday be feasible.


Publication typeInproceedings
Published inProcedings of the 6th ACM Symposium on Operating Systems Principles
PublisherAssociation for Computing Machinery, Inc.
> Publications > The Multics kernel design project