Compilation and Synthesis for Real-Time Embedded Controllers - Correct System Design: Recent Insights and Advances - page 248

illustrated by toy source and target languages [33,43,24,38]. Target code for
commercially available processors is only seldomly formally investigated. The
work at CLI (Computational Logic Inc.) on the `small stack' [7], a hierarchy
of languages with mechanically proved translations between them, particularly
Moore's work on the veried translation of the PITON assembly language to
the binary machine code of the FM 9001 chip [31], is one of the rare exceptions.
Even the impressive work on VLisp, a veried translator for Scheme, [17] ends
at the level of an abstract machine that, given the abstractness of the source
language Scheme, is rather close to actual hardware but is still more abstract
than commercially available processors.
Apart from mathematical insight there is, however, a more practical motiva-
tion for an interest in compiler verication that certainly calls for an investigation
of actual machine code: the justication of compiler-generated code from the cor-
rectness of the source code. In particular in the area of safety-critical systems,
trusted verifed compilers would allow to certify control software on the source
code level which would be less time-consuming and thus less costly than the
current practice of inspecting machine code [39]. Moreover it would encourage a
good documentation or even formal verication of the source code.
In this section we highlight an approach to verifying translations to machine
code of actual processors. As a major case study we investigated the Transputer
manufactured by the British company INMOS (now part of SGS-THOMSON
Microelectronics Ltd) as target architecture. The source language is a prototyp-
ical hard real-time language, which allows the programmer to explicitly state
upper bound requirements for the execution time of basic blocks. Such a code
generator correctness proof may easily become monolithic, aimed at a narrow
source language with a specic code generator for the given target processor.
A proof of this kind would have little interest beyond the particular applica-
tion, and might still require a large eort. We have pursued a more modular
approach that should adapt to both extensions of the source and modications
to the target which justies the eort. Like most literature on compiler veri-
cation we concentrate on the correctness proof for code generators here because
construction of scanners and parsers is well-understood.

2.1 Prologue

It is natural to think of instructions of von Neumann machines as denoting as-
signments to machine components like accumulators and store. Hence, the eect
of machine instructions can conveniently be described by imperative programs.
The Transputer instruction ldc (1), for instance, which loads the constant value
1 to the accumulator called A ,andmoves A 's contents to accumulator B ,aswell
as B 's contents to accumulator C (in the Transputer the registers A , B and C are
used in a stack-like manner), can be represented by the multiple assignment

de = A ; B ; C := 1

E ( ldc (1)) ; A ; B :