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:
All these tools are included in the TAL
distribution, and have been used both under Linux and Windows.
- 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
- Example applications: We have developed a number of example
applications that are (or will be soon) included in the
- A port of a processor simulator from the SimpleScalar Toolset.
- A port of the winning raytracer from the ICFP 2000 programming
- Various micro-benchmarks like dot product, fft, ....