Formally Correct JIT Paper

[Jonathan Leto]

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
jonathan at leto.net
http://leto.net