A BRICS Mini-Course
August 7-10, 1995
Lectures by
Yuri Gurevich
University of Michigan
Egon Börger
University of Pisa
Computation models and commercial specification methods seem to be worlds apart. The evolving algebra project started as an attempt to bridge the gap by improving on Turing's thesis. We sought more versatile machines able to simulate arbitrary algorithms in a direct and coding-free way on their natural abstraction level (rather than implementing algorithms on lower abstraction levels).
The EA thesis asserts that evolving algebras are such versatile machines and suggests an approach to the correctness problem in mathematical modeling of discrete dynamic systems: Construct an evolving algebra that reflects the given system so closely that the correctness can be established by observation and experimentation. (There are tools for running evolving algebras.) The use of the successive refinement method is facilitated by the ability of evolving algebras to reflect arbitrary abstraction levels.
There is an active and growing evolving algebra community. Evolving algebras have been used to specify languages (e.g. C++, Prolog and VHDL), to specify real and virtual architectures (e.g. APE, PVM and Transputer), to validate standard language implementations (e.g. of Prolog, Occam), to verify numerous distributed and/or real-time protocols, to prove complexity results, etc.. Some examples may be found in the proceedings of IFIP 1994 World Computer Congress.
In the lecture series, we define evolving algebras from scratch, argue for the EA thesis and survey EA applications, but most time will be devoted to case studies of distributed algorithms.
Literature (roughly in the order to be used during the course, except the guide [4] will be used in all four lectures): [1,2,3,4,5,6,7,8].
We provide a logical specification of Hennessy's and Patterson's RISC processor DLX and prove the correctness of its pipelined model with respect to the sequential ground model. In the first part we concentrate our attention to the provably correct refinement of the sequential ground model DLX on the pipelined parallel version DLXp in which structural hazards are eliminated. Then we extend the result to the full pipelined model DLXpipe in which also data and control hazards are treated.
Our specification proceeds by stepwise refinement, the proof method is modular. The specification and verification method is general and can be applied to other microprocessors and pipelining techniques as well.
(Joint work with S. Mazzanti)
We present a mathematical analysis of the Transputer Instruction Set architecture for executing Occam together with a correctness proof for a general compilation scheme of Occam programs into Transputer code. We start from a formal Occam model for an abstract processor, running a high and a low priority queue of Occam processes which formalizes the semantics of Occam at the abstraction level of atomic Occam instructions. We present increasingly more refined levels of Transputer semantics, proving correctness (and where possible also the completeness) for each refinement step. The proof assumptions collected along the way turn out to be natural conditions for a compiler to be correct.
The case of Occam and the Transputer is paradigmatic; the proposed mathematical framework for the study of compilation techniques can be used also for other programming languages with nondeterminism and concurrency and provides a rigorous technique for design and analysis of instruction set architectures.
(Joint work with I. Durdanovic, University of Paderborn)
The APE100 parallel processor has been developed by a group of physicists in Pisa and Rome as a dedicated machine for floating point intensive scientific applications, in particular numerical simulation in Lattice Gauge Theory. It constitutes an interesting example of a lock-step parallel architecture, providing - assisted by an appropriate high level language - a very smooth transition from sequential to parallel programming and computing.
We give a full mathematical description of the APE100 architecture. The description consists of several models, at different levels of abstraction, corresponding to views of the architecture provided by different languages used within the APE compilation chain (a crucial part of the software environment of APE).
The primary model is based on the relevant subset of APESE, a high level language specially designed for APE and constituting the source language in the compilation chain: APESE reflects closely the APE model of parallel execution and is therefore adequate for an abstract description of the main features of the latter. By stepwise refinement we lead from this APESE model to the hardware level of APE, going through macro assembler and micro code level down to optimized loadable executable code.
Use of evolving algebras as specification method allows to make these mathematical models of the APE100 architecture understandable to the user of the machine; there is no combinatorial explosion and only basic facts from programming and machine architecture are presupposed.
(Joint work with G. Del Castillo)