Register Transfer Lists

• Form of RTLs
• Types in RTLs
• RTL languages and translation
• Interpretations of RTLs

Computer scientists have used register transfers in many different forms. For lambda-RTL, we have chosen a form designed for use by tools, not by people. We have therefore insisted that as much information as possible be explicit in the RTL itself. Under our current plan,

• RTLs are represented as trees.
• All operators are fully disambiguated, e.g., as to type and size.
• There is no aliasing of locations.
• Fetches are explicit, as are changes in the size or type of data.
• Stores are annotated with the size of the data stored.
• Explicit tree nodes specify byte order. More generally, they specify how to transfer data between storage spaces of different granularity.
• RTL is a typed representation. We plan to generate RTL type checkers from CSDL specifications. Optimizations and other transformations that are intended to preserve semantics should also preserve the property of being well typed. Typing is a good way to catch bugs in optimizers [cite morrisett:compiling].

<ASDL specification of the form of RTLs>=
ty = (int) -- size of a value, in bits
exp = CONST (const)
    | FETCH (location, ty)
    | APP (operator, exp*)
location = AGG(aggregation, cell)
cell = CELL(space, exp)
effect = STORE(location dst, exp src, ty)
       | KILL(location)
       | KILLALL(space)
guarded = GUARD(exp, effect)
rtl = RTL (guarded*)

ASDL specification of the form of RTLs [*]

Form of RTLs

Figure [<-] uses the Zephyr Abstract Syntax Description Language [cite wang:asdl] to show the form of RTLs. A register transfer list is a list of guarded effects. Each effect represents the transfer of a value into a storage location, i.e., a store operation. The transfer takes place only if the guard (an expression) evaluates to true. Locations may be single cells or aggregates of consecutive cells within a storage space. Values are computed by expressions without side effects, which simplifies analysis and transformation. These expressions include integer constants, fetches from locations, and applications of RTL operators to lists of expressions. Effects in a list take place simultaneously, as in Dijkstra's multiple-assignment statement, so one RTL represents one change of state. This decision makes it possible to specify swap instructions without having to introduce temporary locations.

Not every effect is a true assignment. A kill effect changes the value in a storage location in an undefined way. Kill effects are needed to model such architectural specifications as ``the effect of a logical instruction on the AF flag is undefined.''

The ``kill all'' effect in Figure [<-] kills all of the cells in the given storage space. It is needed to give a semantics to certain phrases of lambda-RTL. We haven't demonstrated a need for it yet, but it may be useful to model stores into arbitrary memory locations.

As an example of a typical RTL, consider a SPARC load instruction using the displacement addressing mode, written in the SPARC assembly language as

<sample SPARC instruction>=
ld [%sp-12], %i0

Although we would not want to specify just a single instance of a single instruction, the effect of this load instruction might be notated in lambda-RTL as follows: [The ~ in ~12 is a unary minus.]

<lambda-RTL for sample instruction>=
$r[24] <-- $m[$r[14]+sx(~12)]

because the stack pointer is register 14 and register i0 is register 24. The corresponding RTL is much more verbose, with the sizes of all quantities identified explicitly, as a fully disambiguated tree:

\pstree[nodesep=2pt,levelsep=15pt] \TRSTORE #32 \pstree\TRAGG B #32 #32 \pstree\TRCELL 'r'\pstree\TRCONST #5\TR24 \pstree\TRFETCH #32 \pstree\TRAGG B #8 #32 \pstree\TRCELL 'm' \pstree\TRADD #32 \pstree\TRFETCH #32 \pstree\TRAGG B #32 #32\pstree\TRCELL 'r' \pstree\TRCONST #5\TR14 \pstree\TRSX #13 #32 \pstree\TRCONST #13\TR-12

Figure [->] shows the operators used in this tree. The left child of the STORE is a subtree representing the location consisting of the single register i0, which is register 24. The right-hand child represents a 32-bit word (a big-endian aggregration of four bytes) fetched from memory at the address given by the subtree rooted at ADD. This node adds the contents of the stack pointer (register 14) to the constant -12. The constant is a 13-bit constant, and the SX operator sign-extends it to 32 bits, so it can be added to the stack pointer.

STORE : all n. n loc * n bits ->effect	Store an n-bit value in a given location. The type indicates that for any n, STORE  n takes an n-bit location and an n-bit value and produces an effect.
FETCH : all n. n loc -> n bits	For any n, FETCH  n takes an n-bit location and returns the n-bit value stored in that location.
AGG B : all n.all w. n cell -> w loc	For any n and w, AGG B  n  w aggregates an integral number of n-bit cells into a w-bit location, making the first cell the most significant part of the new location, i.e., using big-endian byte order. w must be a multiple of n. (w and n are mnemonic for wide and narrow.)
CELL 'm' : 32 bits -> 8 cell	Given a 32-bit address, CELL 'm' returns the 8-bit cell in memory referred to by that address.
CELL 'r' : 5 bits -> 32 cell	Given a 5-bit register number, CELL 'r' returns the corresponding 32-bit register (a mutable cell).
ADD : all n. n bits * n bits -> n bits	For any n, ADD  n takes two n-bit values and returns their n-bit sum. Carry and overflow are ignored.
SX : all n.all w. n bits -> w bits	For any n and w, SX  n  w takes an n-bit value, interprets it as a two's-complement signed integer, and sign-extends it to produce a w-bit representation of the same value. w must be greater than n.
CONST : all n . <constant> -> n bits	For any n, CONST  n k represents the n-bit constant k. k must be representable in n bits. The same k could be used with different ns.

Some RTL operators and their types [*]

Types in RTLs

RTL is a typed format. The type system includes the following types:

n bits	A value that is n bits wide.
n loc	A location containing an n-bit value.
n cell	One of a sequence of n-bit storage cells, which can be aggregated together to make a larger location, as by the AGG B nodes in the example tree.
bool	A Boolean condition.
effect	A side effect on storage.

Figure [<-] uses these types to show the types of the operators used above. We have extended Milner's type inference to this system, so that those writing specifications in lambda-RTL can omit types and widths.[*] Unlike in ML, type inference alone does not guarantee that terms make sense; in general, it will be necessary to check additional constraints. For example, in the RTL shown above, it would be necessary to check that the signed integer -12 can be represented using 13 bits, and that 32 is a multiple of both 8 and 32. We are currently investigating ways of formalizing and checking such constraints.

RTL languages and translation

Although we have prescribed the form of RTLs, we can't write any RTLs until we choose a set of locations and a set of RTL operators. These choices define an RTL language. Any specification written in lambda-RTL can introduce new storage spaces (and therefore new locations) and new RTL operators, determining an RTL language for use in that specification.

For use during compilation, we restrict RTLs to a subset of a full RTL language. Each RTL used in a back end based on the vpo optimizer [cite benitez:portable] must satisfy the vpo invariant for the target machine. An RTL satisfies that invariant if and only if it can be represented in a single instruction on the target machine. All RTLs manipulated by vpo satisfy this invariant, so vpo can stop and emit machine code at any time. We use the name X-RTLs refer to the set of RTLs satisfying the vpo invariant for machine X.

Interpretations of RTLs

One reason we restrict the form of RTLs is to limit their possible meanings or interpretations. For example, access to the mutable state of a machine is available only through the fetch and store operations built into the RTL form, so we can easily tell what state is changed by an RTL and how that change depends on the previous state. Researchers and tools working with our form of RTLs have freedom to define interpretations of only two parts of the RTL form: aggregations and operators.

RTL aggregations specify byte order. More generally, aggregations make it possible to write an RTL that stores a w-bit value in (or fetches a w-bit value from) k consecutive n-bit locations, provided that w=kn. Such an aggregation has type n cell -> w loc, and its interpretation must be a bijection between a single w-bit value and k n-bit values. Moreover, when w=n, the bijection must be the identity function. Storing uses the bijection, and fetching uses its inverse, making it possible to combine RTLs using forward substitution. Little-endian and big-endian aggregations will be built into lambda-RTL, as will an ``identity aggregation'' that is defined only when w=n. We imagine that users could define other aggregations by giving systems of equations, as in [cite ramsey:solver].

RTL operators must be interpreted as pure functions on bit vectors. Consequently, the result of applying an RTL operator must not depend on processor state; the operator must give the same answer every time. Chapter [->] presents a collection of RTL operators that we expect can be used to describe many different machines. We don't expect this set to be complete; on the contrary, we expect that any machine description written in lambda-RTL will introduce a handful of new RTL operators which will be unique to that machine.

CSDL Overview

RTLs

Lambda-RTL

Basic RTL Operator Library

SPARC Description

Pentium excerpts

Back to Lambda-RTL home page