Foundational Typed Assembly Language for Grid Computing

This report describes a type theory for certified code, called TALT-R, in which type safety guarantees cooperation with a mechanism to limit the CPU usage of untrusted code. At its core is the foundational typed assembly language TALT, extended with an instruction-counting mechanism, or “virtual clock”, intended to bound the number of non-yielding instructions a program may execute in a row. The type theory also contains a form of dependent refinement that allows reasoning about integer values to be reflected in the typing of a program; in particular, the refinement system enables a simple but effective dynamic checking scheme for the clock, which we predict will greatly improve the performance of TALT-R programs. We exhibit a translation from a clock-ignorant source language into a form of TALT-R, demonstrating that the type system is expressive enough to write general programs in. This material is based on work supported in part by NSF grants CCR-9984812 and CCR-0121633. Any opinions, findings, and conclusions or recommendations in this publication are those of the authors and do not reflect the views of this agency