[TYPES] Paper: Foundational Typed Assembly Language for Grid Computing

[Joe Vanderwaart]

Types readers,

We are pleased to announce the availability of our paper, "Foundational 
Typed Assembly Language for Grid Computing".  The paper focuses on our type 
theory for bounding the CPU usage of mobile code; an abstract is below.

The paper is available for download from
	http://www.cs.cmu.edu/~joev/work.html
(currently the first item in the list of papers there).  As always, 
comments are welcome.

-- Joseph C. Vanderwaart and Karl Crary


--------------------------------------------------------
Foundational Typed Assembly Language for Grid Computing
Joseph C. Vanderwaart and Karl Crary

Abstract:

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.