The mechanically certified derivation of concurrency and its application to systolic design
Chua-Huang Huang · 1987
We divide the development of programming solutions into two parts: the software development and the hardware development. The main issue of the software development is to produce program executions that satisfy a given problem specification; the main issue of the hardware development is to produce architectures that are suitable for the program executions. Program executions, also called traces, may contain parallelism. We are interested in systolic architectures. Our approach to develop parallel traces is by trace transformation. A transformation takes a sequential trace and transforms it into a parallel trace. Trace transformations must preserve the semantics of executions but may alter their execution time. In order to reason about the properties of a programming language precisely, we need a formal semantics. A semantic theory composed of trace semantics and trace transformation rules has been implemented in the Boyer-Moore mechanical logic. Given a program, we can easily derive a sequential trace. The derivation of parallel traces may proceed manually or by a mechanical transformation strategy. With the semantic theory, we can prove that the derived parallel trace is semantically equivalent to the sequential trace and the transformation strategy is semantics-preserving. In this thesis, we study the semantic theory on a particular programming language, sorting networks. We define sequential and parallel traces for several sorting networks, and prove that they are semantically equivalent. We also present a transformation strategy, and prove that it preserves semantics. Furthermore, we prove that the transformation strategy is optimal for sorting networks, i.e., it always returns a shortest trace. We employ the transformation strategy in a design method of systolic architectures. A systolic architecture is a network of processors that are connected in simple patterns and perform simple operations under global synchronization. The development of a systolic architecture requires the input of a processor layout and produces processor connections and data layout. We have implemented the design method on the Symbolics 3600. Our system displays stylized systolic arrays and simulates systolic executions graphically. The graphics system is specially helpful in an extensive search and comparison of alternative systolic designs for a given problem.