@PHDTHESIS\{IMM2006-04216,
    author       = "K. F. Larsen",
    title        = "Types for {DSP} Assembler Programs",
    year         = "2006",
    school       = "Informatics and Mathematical Modelling, Technical University of Denmark, {DTU}",
    address      = "Richard Petersens Plads, Building 321, {DK-}2800 Kgs. Lyngby",
    type         = "",
    note         = "Supervised by Jens Spars{\o}, {IMM,} and Peter Sestoft, {ITU}/KVL",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/4216-full.html",
    abstract     = "In this dissertation I present my thesis:

A high-level type system is a good aid for developing signal processing programs in handwritten Digital Signal Processor (DSP) assembler code.

The problem behind the thesis is that it if often necessary to programing software for embedded systems in assembler language. However, programming in assembler causes numerous problems, such as memory corruption, for instance.

To test the thesis I define a model assembler language called Featherweight {DSP} which captures some of the essential features of a real custom {DSP} used in the industrial partner’s digital hearing aids. I present a baseline type system which is the type system of {DTAL} adapted to Featherweight {DSP}. I then explain two classes of programs that uncovers some shortcomings of the baseline type systesm. The classes of problematic programs are exemplified by a procedure that initialises an array for reuse, and a procedure that computes point-wise vector multiplication. The latter uses a common idiom of prefetching memory resulting in out-of-bounds reading from memory. I present two extensions to the baseline type system: The first extension is a simple modification of some type rules to allow out-ofbounds reading from memory. The second extension is based on two major modifications of the baseline type system:

• Abandoning the type-invariance principle of memory locations and using a variation of alias types instead.
• Introducing aggregate types, making it possible to have different views of a block of memory, thus enabling type checking of programs that directly manage and reuse memory.

I show that both the baseline type system and the extended type system can be used to give type annotations to handwritten {DSP} assembler code, and that these annotations precisely and succinctly describe the requirements of a procedure. I implement a proof-of-concept type checker for both the baseline type system and the extensions. I get good performance results on a small benchmark suite of programs representative of handwritten {DSP} assembler code. These empirical results are encouraging and strongly suggest that it is possible to build a robust implementation of the type checker which is fast enough to be called every time the compiler is called, and thus can be an integrated part of the development process."
}