Final Test CS378 A Formal Model of the JVM Spring, 2012 There are 5 questions, each worth 20 points. Partial credit will be given. All 5 questions are on this page. Everything else is for reference: a sample state and the definition of M5. Answer the 5 questions on your own paper. Be sure to write your name on each page of your answers. You have 90 minutes. (1) M5 differs from the JVM in many ways. One way is that M5 does not support arrays but the JVM does. List, in English, two other features of the JVM not in M5. (2) Answer the following questions about the sample state on the next page. Correct answers are numbers, strings, or lists (e.g., 7 or "move" or (LOAD 3)), not expressions like (len (cs (top-frame id s))). (a) How many threads are there? (b) How many threads have been started? (c) How many Objects have been created? (d) How many Objects are locked? (e) What is the most specific class to which the Object at (REF 4) belongs? (f) Suppose p is the Point at (REF 0). What is (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 table? (h) What instruction will be executed when thread 0 is stepped? (i) Thread 2 is about to execute an INVOKEVIRTUAL instruction. Stepping thread 2 will thus create a new frame. What will the :MLOC of that frame be? (It is sufficient to give the class name and method name in the :MLOC; I don't care about the index in the MLOC.) (j) How many methods in the class table catch 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: well-formed M5 state S, thread id ID, field name FD, class name CL, heap reference REF, and data item V. (a) the number of threads in state S (b) the depth of the call stack of thread ID in state S (c) the superclass chain of the Object reference on top of the stack of thread ID in 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.) (e) the heap obtained from the heap of S by setting field FD of class CL in the Object at REF to V (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? (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. (There is no such instruction on the JVM!) Form: (PEEK) Stk: ..., ref ==> ..., x Description: 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 i, where i is the thread id of the thread created when ref was created. (You may assume that the top-most frame of thread i has a non-empty stack.) Your answer should be of the form (defsem (PEEK) _____) but it will require several lines. [Correction: During the test I announced that ``x is found on the top of the stack in the top-most frame of thread i'' though I gave full credit for pushing the entire top-frame of thread i, since that is how the question read.] [The End]