CS 260r 2017 L3: Formal Verification of a Realistic Compiler (1/30)
Email address
Question 1
The seL4 paper, and our class discussion on 1/25, discussed the forward simulation that shows the functional correctness of seL4’s implementation relative to its spec. The CompCert paper also discusses functional correctness, in Section 2, but it does not use simulation. Describe at least two ways that Equation (1) differs from a forward simulation.
Your answer
Question 2
Section 4.3 gives the following relation between original registers and allocated registers: “R(r) = R'(φ(r)) for all pseudo-registers r live at point 𝓁.” Say that CompCert’s designer made a mistake in the definition of “live pseudo-registers,” so that in some cases, a pseudo-register was incorrectly considered dead at point 𝓁 (even though its value was used at some later point). What would be a consequence of this mistake?
Your answer
Submit
Never submit passwords through Google Forms.
This form was created inside of Google Apps for Harvard. Report Abuse - Terms of Service - Additional Terms