Semantics of machine instructions: Lambda-RTL
Lambda-RTL is a
CSDL language for specifying instructions' semantics.
Lambda-RTL uses register transfer lists
(RTLs) to describe the effects of each instruction on the state of the machine.
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, makes 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.
The lambda-RTL translator is immature, but it is possible
to download it
to do experiments.
We have written a report describing CSDL and
lambda-RTL.
The report includes example descriptions of
SPARC and Pentium instructions, and they are presented as
literate programs.
The report is available in
Automatically converted from the LaTeX source, we have HTML
versions of chapters of the report:
In these versions, some of the figures and syntax examples may look odd, and there
are other formatting errors, but
they may be useful for browsing.
To get the full story, you're better off with one of the postscript versions.
Please write!
We're providing this report to make it easier for
potential users and other interested parties to comment on our work.
Please send comments to zephyr-discussion@virginia.edu
(for public discussion) or to zephyr-investigators@virginia.edu
(private mail to the investigators).
(You can also subscribe to one or more Zephyr
mailing lists.)
This document is designed to be viewed using Cascading Style Sheets. If you
can see this text, your browser does not support them.
Please consider upgrading to Netscape 4, to Internet Explorer
3 or 4, or one of the other browsers recommended by the
W3 Consortium.
Zephyr