Thu Apr 13, 2006, 1-2pm, 4549 Boelter Hall

Typed STIR: Formalising Type Systems for SSA and Fact Checking

Neal Glew
Intel

Typed intermediate languages have proven useful for debugging
compilers, driving optimisations, and providing a foundation for
language-based security.  Much previous work has been done on the
theoretical foundations of typed-intermediate and typed-target
languages, and on how to compile functional languages using them.
While some work has been done on object-oriented languages,
particularly Java, little previous work has addressed optimising
just-in-time compilers (JITs) for Java or C#.  My group at Intel has
been working on such JITs for several years, and our main JIT,
StarJIT, is a product-quality Java to IPF-native-code JIT that can
also JIT C# and target IA-32 native code.  Over the last two years, we
have designed, implemented, and redesigned a type system for the main
intermediate language of StarJIT, called STIR.  This intermediate
language is lower-level than Java or Java bytecodes (or the CLI
equivalents), and so the type system needs to track dependencies
between values and facts about values such as some integer being
within the bounds of some array.  In this talk I will describe the
current design of the type system and some of the interesting aspects
of a formalisation we did for a core version of STIR.  In particular I
will describe how we track fact information through explicit proof
variables, and how we formalised a type system for SSA.  SSA, and more
generally control-flow graphs, as a program representation is
different from the typical lambda calculus based representations used
studied in formal language theory.  Thus, formulating a type system
for SSA turned out to be quite subtle and I had to explore a number of
different formulations before finding one that worked.

Host: Jens Palsberg