Specifying Instructions' Semantics Using CSDL (Preliminary Report)

Authors:Ramsey, Norman, Department of Computer ScienceUniversity of Virginia Davidson, Jack, Department of Computer ScienceUniversity of Virginia

The Zephyr project is part of an effort to build a National Compiler Infrastructure, which will support research in compiling techniques and high-performance computing. Compilers work with source code, abstract syntax, intermediate forms, and machine instructions. By using high-level descriptions of the representations and semantics of these forms, we expect to be able to create compiler components that will be usable with different source languages, front ends, and target machines. To help deal with multiple machines, we are developing a family of Computer Systems Description Languages (CSDL) to describe properties that are relevant to the construction of compilers and other systems software. The languages describe properties of a machine's instructions or its mutable state, or both. Of particular interest is the description of the semantics of instructions, i.e., their effects on the state of the machine. This report describes our preliminary design of Lambda-RTL, a CSDL language for specifying instructions' semantics. We describe the effects of instructions using register transfer lists (RTLs). A register transfer list is a collection of assignments to locations, which represent registers, memory, and all other mutable state. We prescribe a form of RTLs that makes it explicit how to compute the values assigned and on what state the computation depends. The form also makes byte order explicit and provides for instructions whose effects may be undefined. Because our form of RTLs contains so much information, it is convenient for use by tools, but it would be tedious to write RTLs by hand. Lambda-RTL, which is based on the lambda-calculus and on register transfer lists, is a metalanguage designed to make it easier for people to write RTLs and to associate them with machine instructions. It enables us to omit substantial information from hand-written specifications; the Lambda-RTL translator infers the missing information and puts the resulting RTLs into canonical form. Lambda-RTL also provides a ``grouping'' construct designed to help specify large groups of similar instructions. We are still designing Lambda-RTL. This report presents a short overview of Lambda-RTL, followed by examples. The examples include definitions of basic operators, which we believe will be useful for describing a wide variety of machines, as well as excerpts from descriptions of the SPARC and Pentium. We have chosen excerpts that illustrate features which are characteristic of these particular machines; for example, we show a model of SPARC register windows, and we show how Lambda-RTL can help manage the complexity of the Pentium instruction set. Both the machine descriptions and Lambda-RTL itself are under development, so this report is a snapshot of a work in progress. We issue it now to solicit feedback both on our overall approach and on the details of Lambda-RTL. Please send feedback by electronic mail to zephyr-investigators@virginia.edu.

All rights reserved (no additional license for public reuse)
Source Citation:

Ramsey, Norman, and Jack Davidson. "Specifying Instructions' Semantics Using CSDL (Preliminary Report)." University of Virginia Dept. of Computer Science Tech Report (1997).

University of Virginia, Department of Computer Science
Published Date: