CS 260r 2017 L3: Formal Verification of a Realistic Compiler (1/30)
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.
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?
Never submit passwords through Google Forms.
This form was created inside of Google Apps for Harvard.
Terms of Service