Report

Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Popek & Goldberg’s notation Haipeng Cai and Siyuan Jiang 1 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg • • Conventional third generation computer Virtual machine monitor(VMM) Haipeng Cai and Siyuan Jiang 2 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Conventional Third Generation Computer Haipeng Cai and Siyuan Jiang 3 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Processor Mode M • s: supervisor mode • u: user mode Conventional Third Generation Computer 4 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg No I/O instructions Conventional Third Generation Computer 5 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Memory as Executable storage E • • E Linear Uniformly addressable … E[i] 0 … i Conventional Third Generation Computer q-1 6 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Relocation-bounds Register R • • R=(l, b) An index to E l E … 0 l+b … q-1 Conventional Third Generation Computer 7 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg R=(l, b), address a is reached like: l E l+a … 0 a<b l+b … q-1 a>b-1 a+l>q-1 Memorytrap Memorytrap (Discuss (Discusslater) later) Conventional Third Generation Computer 8 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Relocation-bounds Register R works in both processor modes • supervisor mode • user mode Conventional Third Generation Computer 9 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Program Counter P Address of next instruction • Relative to R l E … l+p 0 l+b … q-1 P=p Conventional Third Generation Computer 10 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg State S=<E, M, P, R> The current state of the real computer system • • • • E: executable storage M: processor mode P: program counter R: relocation-register Conventional Third Generation Computer PSW: Program status word 11 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg PSW=<M, P, R> Old-PSW l E … 0 1 l+b … q-1 Next-PSW Conventional Third Generation Computer 12 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg State S=<E, M, P, R> Notation C • is the finite set of states Conventional Third Generation Computer 13 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Instruction i • is a function f: C C C i C Conventional Third Generation Computer 14 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Trap (an action of instruction) S1=<E1, M1, P1, R1> trap S2,=<E2, M’, P’, R’> l1l' l1+b1 l'+b' E1 E2 … … <M1, P1, R1> <M’,P’,R’> 0 1 Conventional Third Generation Computer q-1 15 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg MemoryTrap • A trap that caused by an attempt to access an address which is beyond the bounds l E l+b … 0 … q-1 address a>b-1 a>q-1 (memorytrap) (memorytrap) Conventional Third Generation Computer 16 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Privileged instruction i • For any PSW=<e, p, r> that i does not memorytrap, • if M=u, i traps • else if M=s, i does not trap Conventional Third Generation Computer 17 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Sensitive instruction i • Control sensitive • Behavior sensitive Conventional Third Generation Computer 18 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Control sensitive instruction i There exists a state S1=<e1, m1, p1, r1> , note i(S1)=<e2,m2,p2,r2> such that i(S1) does not memorytrap AND (r1≠r2 OR m1≠m2) is true In other words, i is control sensitive if i intends to change one or both of • R: the available memory resources • M: the processor mode Conventional Third Generation Computer 19 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Operator (for Behavior sensitive instruction) l E l+b … … 0 E … 0 r q-1 l+x l+x+b … rx q-1 Conventional Third Generation Computer 20 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Behavior sensitive instruction i i is behavior sensitive if there exists integer x and S1, S2 where S1 has m1, r1, p1 and S2 has m2(≠m1), r2=r1x, p2=p1 such that i(S1) and i(S2) differ in one or both of • the values of available memory • the program counter Conventional Third Generation Computer 21 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Behavior sensitive instruction i • is location sensitive, if the difference is caused by R • is mode sensitive , if the difference is caused by M Behavior Sensitive Relocation-bounds Register Location Sensitive Processor Mode Conventional Third Generation Computer Mode Sensitive 22 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Conventional third generation computer Wrap Up • S=<E,M,P,R> • Executable storage • PSW • • • • Instruction • Trap Processor Mode Program counter Relocation-bounds Register • Memorytrap • Privileged instruction • Sensitive instruction • Control Sensitive • Behavior Sensitive Conventional Third Generation Computer 23 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Virtual Machine Monitor (VMM) Virtual Machine Monitor 24 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Control Program (CP) VMM is a kind of CP Virtual Machine Monitor 25 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Control Program Assume • Control Program runs in s mode • Other programs run in u mode (In later discussion, ”program” represents the other programs) Virtual Machine Monitor 26 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Control Program CP=<D, A, {vi}> • Dispatcher D • Allocator A • Interpreters {vi} Virtual Machine Monitor 27 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Dispatcher D D decides which module to call. E[1] has P set to D l E … l+b … q-1 0 1 PSWnext=<M, P->D, R> Virtual Machine Monitor 28 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Allocator A A decides what resource(s) are to be provided. Virtual Machine Monitor 29 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Interpreters {vi} One interpreter routine vi for one privileged instruction i Virtual Machine Monitor 30 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Virtual Machine Monitor A CP with three properties: • • • Efficiency property Resource control property Equivalence property Virtual Machine Monitor 32 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Efficiency property: All innocuous instructions are executed by hardware directly (with no intervention on the part of the control program) Virtual Machine Monitor 33 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Resource control property: Programs cannot affect the system resources. (Whenever an attempt to affect system resources, A is to be invoked Virtual Machine Monitor 34 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Equivalence property: With two exceptions(listed in the next slide), any program k performs in a manner indistinguishable from: (1) CP does not exist (2) k has freedom of access to privileged instructions Virtual Machine Monitor 35 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Exceptions for equivalence property: (1) The length of time required for execution changes when program runs with a CP present (2) A may not satisfy a particular request for space, then k will not execute in a same manner Virtual Machine Monitor 36 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Virtual Machine The environment which any program sees when running with a VMM present Virtual Machine Monitor 37 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Virtual machine monitor Wrap up • Control Program (CP) • Dispatcher • Allocator • Interpreters{vi} • Virtual machine monitor properties • Efficiency • Resource control • Equivalence Virtual Machine Monitor 38 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Formal Requirements for Conventional Third Generation Computer to be Virtualizable Formal requirements for virtualizable third generation computer 39 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Theorem 1 For any conventional third generation computer, a VMM can be constructed, if the set of sensitive instructions (for that computer) is a subset of the set of privileged instructions Formal requirements for virtualizable third generation computer 40 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Construct a VMM (in conventional 3rd generation computer) • VM Map • Define “Equivalence property” • VM Map that satisfies three VMM properties Formal requirements for virtualizable third generation computer 41 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg VM Map • is a function f: Cr->Cv which is a one-one homomorphism that is for any Si, ei, there exists a e’i, such that f(ei(Si))=e’i(f(Si)) Cr(states without VMM) Si f ei Cv(states with VMM) S’i e'i Sj f Formal requirements for virtualizable third generation computer S’j 42 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg VM Map VM Map only maps states: • • after the completion of one instruction in the real machine before the beginning of the next instruction Formal requirements for virtualizable third generation computer 43 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Equivalence (Formal) Assume a real machine runs from S1, VM runs from f(S1). The VM is equivalent to the real machine, if and only if, for any S1, if the real machine halts in S2, then the VM halts in f(S2). Formal requirements for virtualizable third generation computer 44 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Standard VM Map(detail in next slide) Sr Standard VM Map Sv l E … 0 same <m’=s, p’=CP, r’=(0,q-1)> E’ 2 0 … CP <m, p, r> <m’, p’, r’> l+k … k l+b … w-1 l+k+b … w+k-1 set by trap handler Formal requirements for virtualizable third generation computer 45 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Standard VM Map Sr<E,M,P,R>Sv<E’, M’, P’, R’> where R=(l, b), |E|=w, |CP|=k-2 • E’[i+k] E[i], for i=0, w-1 • E’[i] CP, for i=2 to k-1 • E’[1] <m’, p’, r’> where m’=s, p’=1st location of CP, r’=(0, q-1) • E’[0] <m, p, r> as last set by trap handler • M’ u, P’P, R’(l+k, b) Formal requirements for virtualizable third generation computer 46 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Standard VM Map It can satisfies three properties if the sensitive instructions are all privileged instructions in third generation computer Formal requirements for virtualizable third generation computer 47 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Overall Wrap up • Conventional third generation computer • Virtual machine monitor (control program) • The condition under which VMM can be built in the conventional third generation computer Formal requirements for virtualizable third generation computer 48 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Related results: Recursive virtualization • Can a VM run a copy of the VMM? • Theorem 2: A conventional third generation computer is recursively virtualizable if it is: (a) virtualizable, and (b) a VMM without any timing dependencies can be constructed for it Formal requirements for virtualizable third generation computer 49 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Relax VMM definition: Hybrid VMM • Relax VMM definition so that more third generation computers can be virtualizable • Theorem 3: A hybrid VMM may be constructed for any conventional third generation computer where user sensitive instructions are privileged. Note1: in Theorem 1, it is all ”sensitive instructions” Note2: user sensitive instructions are defined in next slide Formal requirements for virtualizable third generation computer 50 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg User Sensitive Instructions • Def. i is said to be user sensitive, if there exists a state S=<E, u, P, R>, for which i is sensitive • In other words, i is user sensitive if i is sensitive under user mode Formal requirements for virtualizable third generation computer 51 Formal Requirements for Virtualizable Third Generation Architecture Gerald J. Popek and Robert P. Goldberg Reference [1] G. Popek, R. Goldberg, “Formal requirements for virtualizable third generation architectures”, Commun. ACM, vol. 17, pp. 412-421, 1974. Haipeng Cai and Siyuan Jiang 52