Certifying Run-time Code Generation

Run-time code generation (RTCG) improves performance by letting programmers dynamically generate special-purpose code to exploit run-time invariants. A certifying compiler is one that produces ourput that can be mechanically checked to have certain properties (in our case type safety). We have developed an infrastructure for certifying compilation supporting RTCG. Our system includes:

Cyclone: a safe C-like language with explicit support for RTCG. Cyclone adds four simple RTCG constructs (codegen, cut, splice, and fill) and no new types to a standard core language.
TAL/T: an extension to Typed Assembly Language (TAL) that supports RTCG. It is possible to check statically that all code that might be generated at run time will be type safe. Stated otherwise, no type-checking is performed at run time.
A certifying compiler: The Cyclone certifying compiler translates Cyclone into TAL/T while performing standard optimizations such as register allocation, dead code elimination, function inlining, and null-check elimination.
Example applications: We have developed a number of example applications that are (or will be soon) included in the distribution:
- A port of a processor simulator from the SimpleScalar Toolset.
- A port of the winning raytracer from the ICFP 2000 programming contest.
- Various micro-benchmarks like dot product, fft, ....

All these tools are included in the TAL distribution, and have been used both under Linux and Windows.