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 archi- tecture. Proc. AFIPS 1972 SJCC, Vol. 40, AFIPS Press, Montvale, N.J. pp. 369-377. 23. Feustal, E.A. On time advantages 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., Carnegie- Mellon 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 imple- mentations. 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. 579- 586. 46. Wulf, W.A., et al. HYDRA: The kernel ofa 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. 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 third- generation-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, Oc- tober 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 De- partment, University of California, Los Angeles CA 90024; Robert P. Goldberg, Honeywell Information Systems,Waltham, MA 02154. 412 Communications July 1974 of Volume 17 the ACM Number 71. Virtual Machine Concepts There are currently a number of viewpoints suggest- ing what a virtual machine is, how it ought to be con- structed, 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 in- tuitively