Howdy, I thought this paper was interesting:
Abstract: This paper presents a method for creating formally correct just-in- time (JIT) compilers. The tractability of our approach is demon- strated through, what we believe is the first, verification of a JIT compiler with respect to a realistic semantics of self-modifying x86 machine code. Our semantics includes a model of the instruction cache. Two versions of the verified JIT compiler are presented: one generates all of the machine code at once, the other one is incre- mental i.e. produces code on-demand. All proofs have been per- formed inside the HOL4 theorem prover. http://www.cl.cam.ac.uk/~mom22/jit/jit.pdf Duke -- Jonathan "Duke" Leto [email protected] http://leto.net _______________________________________________ http://lists.parrot.org/mailman/listinfo/parrot-dev
