19 Fabry R S A user s view of capabilities ICR Quart Rep 15 Nov 1967 ICR U of Chicago Sec IC 20 Fabry R S Preliminary description of a supervisor for a machine oriented around capabilities ICR Quart Rep 18 Aug 1968 ICR U of Chicago Sec lB 21 Fabry R S List structured addressing Ph D Th U of Chicago 1971 22 Feustal E A The Rice research computer a tagged architecture Proc AFIPS 1972 SJCC Vol 40 AFIPS Press Montvale N J pp 369 377 23 Feustal E A On timeadvantages of tagged architecture IEEE Trans on Computers C 22 7 July 1973 644 656 24 Graham G S and Denning P J Protection principles and practice Proc AFIPS 1972 SJCC Vol 40 AFIPS Press Montvale N J pp 417 429 25 Halton D Hardware of the System 250 for communication control Presented at the lnternat Switching Syrup Cambridge Mass June 6 9 1972 7 pp 26 Hamer Hodges K J Fault resistance and recovery within System 250 Presented at I C C Conf Washington D C Oct 1972 6 pp 27 Iliffe J K Basic maehhw principles American Elsevier New York 1968 28 Iliffe J K and Jodeit J G A dynamic storage allocation scheme Comput J 5 Oct 1962 200 209 29 Jones A K Protection structures Ph D Th CarnegieMellon U 1973 30 Lampson B W On reliable and extendable operating systems In Techniques in Software Engineering NATO Science Committee Workshop Material Vol 11 Sept 1969 31 Lampson B W Dynamic protection structures Proc AFIPS 1969 FJCC Vol 35 AFIPS Press Montvale N J pp 27 38 32 Lampson B W Protection Proc 5th Ann Princeton Conf Princeton U Mar 1971 pp 437 443 33 LeClerc J Y Memory structures for interactive computers Project GENIE document No 40 10 110 U of California Berkeley 1966 34 Needham R M Protection systems and protection implementations Proc AFIPS 1972 FJCC Vol 41 AFIPS Press Montvale N J pp 571 578 35 Organick E I Computer System Organization the B5700 B6700 Series Academic Press New York 1973 36 Organick E I Tile Multics System An Examination lts Structure MIT Press Cambridge Mass 1972 37 Saltzer J H Traffic control in a multiplexed computer system MAC TR 30 Proj MAC MIT Cambridge Mass 1966 38 Schroeder M D Performance of the GE 645 associative memory while Multics is in operation Proc Workshop on System Performance Evaluation Cambridge Mass 1971 pp 227 245 39 Schroeder M D Cooperation of mutually suspicious subsystems in a computer utility Ph D Th MIT 1972 40 Sevick K C et al Project SUE as a learning experience Proc AFIPS 1972 FJCC Vol 41 AFIPS Press Montvale N J pp 331 339 41 Shepherd J Principal design features of the multi computer The Chicago Magic Number Computer ICR Quart Rep 19 Nov 1968 1CR U of Chicago Sec 1 C 42 Sturgis H E A postmortem of a time sharing system Ph D Th U of California Berkeley 1973 43 Wilkes M V Time Sharing Computer Systems 2nd ed American Elsevier New York 1972 44 Wilner W T Design of the Burroughs BI700 Proc AFIPS 1972 FJCC Vol 41 AFIPS Press Montvale N J pp 489 497 45 Wilner W T Burroughs BI700 memory utilization Proc AFIPS 1972 FJCC Vol 41 AFIPS Press Montvale N J pp 579586 46 Wulf W A et al H Y D R A The kernel o f a multiprocessor operating system Carnegie Mellon U Comput Sci Dep rep June 1973 47 Yngve V H The Chicago Magic Number Computer ICR Quart Rep 18 Nov 1968 ICR U of Chicago Sec 1 B 412 Formal Requirements for Virtualizable Third Generation Architectures Gerald J Popek University of California Los Angeles and Robert P Goldberg Honeywell Information Systems and Harvard University Virtual machine systems have been implemented on a limited number of third generation computer systems e g CP 67 on the IBM 360 67 From previous empirical studies it is known that certain third generation computer systems e g the DEC PDP 10 cannot support a virtual machine system In this paper model of a thirdgeneration like computer system is developed Formal techniques are used to derive precise sufficient conditions to test whether such an architecture can support virtual machines Key Words and Phrases operating system third generation architecture sensitive instruction formal requirements abstract model proof virtual machine virtual memory hypervisor virtual machine monitor CR Categories 4 32 4 35 5 21 5 22 Copyright 1974 Association for Computing Machinery Inc General permission to republish but not for profit all or part of this material is granted provided that ACM s copyright notice is given and that reference is made to the publication to its date of issue and to the fact that reprinting privileges were granted by permission of the Association for Computing Machinery This is a revised version of a paper presented at the Fourth ACM Symposium on Operating Systems Principles IBM Thomas J Watson Research Center Yorktown Heights New York October 15 17 1973 This research was supported in part by the U S Atomic Energy Commission Contract No AT ll 1 Gen 10 Project 14 and in part by the Electronic Systems Division U S Air Force Hanscom Field Bedford Massachusetts under Contract Number F19628 70 0217 Authors addresses Gerald J Popek Computer Science Department University of California Los Angeles CA 90024 Robert P Goldberg Honeywell Information Systems Waltham MA 02154 Communications of the ACM July 1974 Volume 17 Number 7 1 Virtual Machine Concepts There are currently a number of viewpoints suggesting what a virtual machine is how it ought to be constructed and what hardware and operating system implications result 1 6 7 9 12 This pap r examines computer architectures of third generation like machines and demonstrates a simple condition which may be tested to determine whether an architecture can support a virtual machine This condition may also be employed in machine design In the following we specify intuitively what is meant by the above then develop a more exact model of third generation like machines and finally state and prove a sufficient condition for such a system to be virtualizable A virtual machine is taken to be an efficient isolated duplicate of the real machine We explain these notions through the idea of a virtual machine monitor V M See Figure 1 As a piece of software a VMM has three essential characteristics First the VMM provides an environment for programs which is essentially identical with the original machine second programs run in this environment show at worst only minor decreases in speed and last the VMM is in complete control of system resources By an essentially identical environment the first characteristic is meant the following Any program run under the VMM should exhibit an effect identical with