Certified run-time code generation

Run-time code generation (RTCG) has been shown to be an effective optimization. Systems such as DyC, 'C, Tempo, and Fabius have demonstrated order of magnitude improvements on benchmark programs. In addition, by using binding time analyses, the benefits of RTCG can be obtained with minimal programmer effort. Languages like MetaML and PML have explored type systems for RTCG that can ensure programs using RTCG do not crash. In earlier work we presented Cyclone—a type-safe language based on C with support for RTCG.; The safety guarantee provided by a type-safe source language may fail to hold of the compiler's output. Rather than trusting that the compiler is correctly implemented, we can use a certifying compiler to check that the output is type safe. A certifying compiler produces a certificate, along with the object code, which together can be used to verify that the object code is safe.; Here we develop a certifying and optimizing compiler for Cyclone supporting run-time code generation. The output of our compiler is TAL/T—x86 object code augmented with typing annotations. Part of our system is a verifier for TAL/T capable of mechanically checking that TAL/T programs are type safe—they cannot crash. This guarantee provides increased confidence in the compiler-generated code.; The contributions of this thesis include: (1) a framework for compiling and optimizing programs supporting RTCG, (2) a formal proof that well-typed TAL/T programs cannot crash, and (3) an evaluation of our compiler using micro-benchmarks, a raytracer, and an instruction set simulator.