Final Test CS378 A Formal Model of the JVM Spring, 2012 (1) M5 differs from the JVM in many ways. M5 does not support * types * private v public * bytecode verification * class loading * floating point * longs * interfaces There are, of course, other differences. (2) Answer the following questions about the sample state on the next page: Answers (a) How many threads are there? 4 (b) How many threads have been started? 3 (c) How many Objects have been created? 7 (d) How many Objects are locked? 0 (e) What is the most specific class to which "Track" the Object at (REF 4) belongs? (f) Suppose p is the Point at (REF 0). What is 3 (p.track).x, i.e., the contents of the x field of the Object in the track field of p? (g) How many classes are declared in the class 6 table? (h) What instruction will be executed when thread (INVOKEVIRTUAL ("Thread" "start" 0)) 0 is stepped? (i) Thread 2 is about to execute an INVOKEVIRTUAL ("FastPoint" "move" 0) instruction. Stepping thread 2 will thus create a new frame. What is the :MLOC of that frame? (It is sufficient to give the class name and method name in the :MLOC and skip the ``index'' in the locator.) (j) What methods in the class table can catch none exceptions? (3) Formalize the following ideas by writing ACL2 terms that use functions in the M5 model. I have used uppercase to highlight the variable names that may appear in your terms. [My answers below are, of course, not the only correct ones. There are many equivalent ways to write these same ideas, including defining functions of your own.] (a) ``the number of threads in state S'' Answer: (len (tt S)) (b) ``the depth of the call stack of thread ID in state S'' Answer: (len (cs (find :id ID (tt S)))) (c) ``the superclass chain of the object on top of the stack of thread ID in S'' Answer: (super-classes (class-name-of-ref (top (stk (top-frame ID S))) (hp S)) (ct S)) (d) ``the reference to the Object whose creation created thread ID in S'' (For example, in the example state shown, thread 1 was created when the Object at (REF 0) was created.) Answer: (ref (find :ID ID (tt s))) (e) ``the heap obtained from the heap of S by setting field FD of class CL in the Object at REF to V'' Answer: (bind REF (putf CL FD V (deref REF (hp s))) (hp s)) (4) When M5 creates new Objects it initializes every field to 0. What function in the model would you have to modify to instead initialize every field to -1? Answer: NEW-OBJECT-IMMEDIATE (5) Add the PEEK instruction, which peeks into a computation running in another thread and brings the value on top of that thread's stack back to the current thread's stack: Form: (PEEK) Stk: ..., ref ==> ..., x Description: ref is a reference to some Object. You may assume ref points to an Object of class Thread. Pop ref from the stack and push the value, x, found on the top-most frame of thread k, where k is the thread id of the thread created when ref was created. (You may assume that the top-most frame of thread k has a non-empty stack.) Answer: (defsem (PEEK) (let* ((ref (top -stk-)) (other-id (id (find :ref ref (tt s)))) (x (top (stk (top-frame other-id s))))) (modify id s :stk (push x (pop -stk-)))))