[Prev][Next][Index][Thread]

Papers on Typed Assembly Language

I would like to announce that revised and extended versions of two papers on
typed assembly language, "From System F to Typed Assembly Language" and
"Stack-Based Typed Assembly Language," are now available at the URL
http://www.cs.cmu.edu/~crary/papers/.

As always, comments and suggestions are most welcome.

Karl Crary

-----

>From System F to Typed Assembly Language
Greg Morrisett    David Walker    Karl Crary    Neal Glew

We motivate the design of a statically typed assembly language (TAL)
and present a type-preserving translation from System F to TAL.  The
TAL we present is based on a conventional RISC assembly language, but
its static type system provides support for enforcing high-level
language abstractions, such as closures, tuples, and user-defined
abstract data types.  The type system ensures that well-typed programs
cannot violate these abstractions.  In addition, the typing constructs
admit most low-level compiler optimizations.

Our translation to TAL is specified as a sequence of type-preserving
transformations, including CPS and closure conversion phases;
type-correct source programs are mapped to type-correct assembly
language.  A key contribution is an approach to polymorphic closure
conversion that is considerably simpler than previous work.  The
compiler and typed assembly language provide a fully automatic way to
produce proof carrying code, suitable for use in systems where
untrusted and potentially malicious code must be checked for safety
before execution

-----

Stack-Based Typed Assembly Language
Greg Morrisett    Karl Crary    Neal Glew    David Walker

In previous work, we presented Typed Assembly Language (TAL).  TAL is
sufficiently expressive to serve as a target language for compilers of
high-level languages such as ML.  That work assumed such a compiler would
perform a continuation-passing style transform and eliminate the control
stack by heap-allocating activation records.  However, most compilers are
based on stack allocation.  This paper presents STAL, an extension of TAL
with stack constructs and stack types to support the stack allocation
style.  We show that STAL is sufficiently expressive to support languages
such as Java, Pascal, and ML; constructs such as exceptions and displays;
and optimizations such as tail call elimination and callee-saves registers.
This paper also formalizes the typing connection between CPS-based
compilation and stack-based compilation and illustrates how STAL can
formally model calling conventions by specifying them as formal
translations of source function types to STAL types.