Related Work

This section compares my work with related research.

Legend:

• yes

◦ some no

Boundscheckelimination Control-flowsensitive Generalpointerarithmetic Reliesongarbagecollector Pseudo-instructions Build-indatatyperepr. Explicitmemoryreuse RealMachine Machinecheckedproofs

TAL ◦ • ◦ ◦ •

DTAL • • • ◦ •

LinTAL ◦ • •

LowTAL ◦ • ◦ • ◦ • •

TALT ◦ • ◦ • ◦ ◦ • •

Featherweight DSP • • ◦ • ◦

Figure 6.3: Comparison of different type system for low-level languages.

6.2.1 Typed Assembler Languages

Since the influential work of Morrisett et al. [33] there has been a lot of re-search of type systems for low-level languages. Figure 6.3 shows a schematic comparison of Featherweight DSP and five other typed assembly languages.

The other languages in Figure 6.3 are:

• TAL. Based on the papers [34, 36, 33, 50, 52, 21] which describe differ-ent subset of the implemdiffer-entation TALx86 for the IA32 instruction set architecture.

• DTAL. Based on [55, 56].

• LowTAL. Low-level Typed Assembly Language, based on [8]. The au-thors use the name LTAL but this creates a name conflict in this com-parison. LowTAL is based on Typed Machine Language [51]. It can be translated to real Sparc code.

• LinTAL. Based on [9]. Again, the original name used by the authors is LTAL. LinTAL also allow direct manual reuse of memory, in some sense theircelltype corresponds to myjunktype: one word of memory. But they do not have indexed types.

• TALT. TAL Two, based on [12]. Like LowTAL TALT is intended to be a fully formalised and have machine-checkable safety proof.

The categories measured in Figure 6.3 are:

Bounds check elimination. Does the type system track the value of inte-ger exressions so that bounds check for array indexing can be moved

around freely and potentially be completely eliminated. Only DTAL and Featherweight DSP offer full support. LowTAL and TALT track some limited form of information about integer expressions, which po-tentially could be used for eliminating bound check.

Control-flow sensitive. All the type systems support either alias types or sigleton types of some sort, which enables the type system to be control-flow sensitive.

General pointer arithmetic. Only LowTAL, TALT, and Featherweight DSP support pointer arithmetic. None support arbitrary arithmetric opera-tions on pointers. The focus for pointer arithmetic is different, Feather-weight DSP concentrates on supporting pointer arithmetic to enable ex-plicit and flexible data manipulation and reuse, whereas LowTAL and TALT concentrates on pointer arithmetic for code addresses. LowTAL supports just enough pointer arithmetic to enable position-independent code. TALT support enough pointer arithmetic to enable relative ad-dressing.

Relies on garbage collector. Only LinTAL and Featherweight DSP have the explicit goal of not relying on a garbage collector. But LinTAL have support for co-existing with a garbage collector. Featherweight DSP does not even support dynamic allocation of memory.

Pseudo-instructions. Some TALs have pseudo-instructions for compare-and-branch, datatype tag-checking, or memory allocation which is trans-lated to a sequence of real machine instructions or a call to a runtime system (this is called atomicity in [8]). For DTAL and LinTAL this is hard to determine because they do not compile to real machine code, the basis for the markings in this coloumn is that DTAL has analloc which cannot be implemented with a single instruction on conventional hardware. LinTAL on the other hand does not have analloc instruc-tion. The other markings in this coloumn is based on the table in [8].

Build-in data type repr. Does the system comes with predefined datatypes such as arrays and tuples, or can the user (human or compiler) of the system freely chose data type representation. DTAL comes with prede-fined arrays, and the only datatype in LinTAL is pairs.

Explicit memory reuse. Can memory be explicitly managed and reused or does the system enforce the type invariance principle. The only two system that have explicit memory management clearly stated as a goal is LinTAL and Featherweight DSP. TAL, LowTAL, and TALT seems to be using alias types, but only for seperating allocation and seperation initialisation.

Real Machine. Does the system support tranlation to a real machine lan-guage. TAL and TALT is based Pentium code and each LowTAL in-struction corresponds to at most one Sparc inin-struction. DTAL and Lin-TAL only have interpreters for their instruction sets. Featherweight DSP

can mostly be translated straightforwardly to real custom DSP assem-bler, the only exception is the branching instructions.

Machine checked proofs. TAL, DTAL, and LinTAL only have hand-checked proof. LowTAL and TALT have machine checked proofs (which are mostly done). Featherweight DSP has no formal proof at all.

The languages compared in Figure 6.3 are, by far, not the only related re-search on type system for low-level languages, others include Heap Bounded Assembly Language [3] and Crary and Weirich [13]. Both of these use type systems to give upper limit guarantees on resource bounds.

Ahmed and Walker [1] presents a logical framework for reasoning about adjacency, separation of memory blocks, and aliasing. The logic is deployed as a type system for a formal model stack-based assembly language. Their modality for adjancency is similar to my append operator @ for aggregate types. But their modalities are not combined with index types.

6.2.2 Sized Types

The work on Sized Types by Pareto [41] and Chin et al. [10] is similar to my work. We both employ type systems based on Presburger arithmetic to track the size of arrays and to find certain classes of errors in software for embedded systems. While Pareto devised type systems that can catch an impressive array of classes of program errors:

• non-exhaustive patterns,

• partial numerical operators,

• partial library functions,

• explicit failures,

• call chains too large for the stack,

• data-structures too large for the heap,

• space leaks,

• rate conflicts,

• busy loops,

• deadlocks.

Pareto does so by introducing two new programming languages (neither can handle the full list of classes of errors) with associated programming styles.

I, in contrast, concentrate on a much smaller list of classes of errors, and try to follow the guidelines from Section 1.1.4. That is, I work with the existing coding style and an existing assembler language used in embedded systems today.

6.2.3 Cyclone

As described in Section 1.4.4, Cyclone [28, 22] shares many goals with the work presented in this dissertation. Cyclone is a low-level language with a high-level type system, and Cyclone targets handwritten code. But Cy-clone concentrates on security and not resource contrained embedded soft-ware, thus some trade-offs have been made which are not appropriate for

embedded DSP code. Cyclone has for example support for several flavours of dynamic memory allocation: allocation in a global heap which is garbage collected, stack allocation corresponding to local-declaration blocks in C, and dynamically growable regions. But Cyclone does not support manual man-agement of static memory where a static location in memory can contain objects of different types at different points in time during execution.

I think that my work and Cyclone could be interesting to combine. This combination could be taken in two directions:

• To use Cyclone to widen the scope of my work. While I have concen-trated on code for embedded DSP programs, I believe that my combi-nation of alias types and indexed types, and aggregate types are useful outside the scope of embedded DSP code. An interesting project would be to extend Cyclone with these constructs.

Jim et al. [28], for example, reports that the biggest performance prob-lem of Cyclone stems from the use offat pointers.

My combination of alias types and indexed types can be seen as fat pointers checked at compile time rather than at runtime, and thus bringing no runtime overhead, neither in execution time nor memory for storing bounds.

• To extend Cyclone with features useful for embedded DSP code. Sim-ilar to how DSP-C [15] extends C. That is, Cyclone could be extended with language support for fixed-point number and circular arrays and pointers so that signal processing algorithms can be efficiently compiled to DSPs.

6.2.4 AnnoDomini

Eidorff et al. [16] and Ramalingam et al. [46] use a type system and type inference to detect and repair Year 2000 problems in COBOL programs. Their type construct for COBOL records are similar to my aggregate types. Like my aggregate types their record types allow different views. But their record type have statically known sizes whereas my aggregate types can have a symbolic size which might be unknown.