%A J.R. Gurd %A I. Watson %A J.R.W. Glauert %T A Multilayered Dataflow Computer Architecture %R Data Flow Group - Internal Report %I Department of Computer Science, University of Manchester %D March 1980 %P 90 %O (3rd issue) %X Introduces the multilayered dataflow computer architecture which is based upon a high level language and an underlying graphical notation for representing computations. The language, Lapse, employs a single-assignment rule together with some more familiar parallel programming constructs. It permits both iteration and recursion. The graphical notation utilises the concept of labels for those tokens which use computational subgraphs reentrantly. The operation of labels in implementing iteration, recursion and simple data structures is illustrated. The architecture is based on a ring structure in which binary representations of tokens, known as results, circulate. A processing unit computes results as required by a stored program representing the computational graph. Each result carries a name derived from the notational label. Names perform two functions: firstly they separate distinct instances of reentered code; secondly they are associatively matched with other inputs to their destination node to allow the node to be executed. The ring structure may be pipelined to achieve a rate of node execution limited by the amount of parallel activity permitted in the program and by the technology used. An extensible version of the architecture contains many rings in a multilayered, parallel structure whose execution rate is bound solely by the parallelism of the programs running on it. %A Ann Welsh %T The Specification, Design and Implementation of NDB %R Technical Report UMCS-82-10-1 %I Department of Computer Science, University of Manchester %D 1982 %P 126 %O M.Sc. Thesis %X An attempt is made to become familiar with the "rigorous" method of software development and to identify some associated problems, using the binary-relational non-programmer database system, NDB, as a vehicle for this research. A complete specification and development of NDB, and an implementation in Pascal, are produced. The decomposition of specifications and designs into manageable and reusable untis is seen to be desirable, especially when concerned with a large and reusable system. %A Ian Mearns %T A Denotational Semantics for Concurrent Ada Programs %R Technical Report UMCS-83-10-1 %I Department of Computer Science, University of Manchester %D 1983 %P 330 %O PhD Thesis %X The dynamic semantics for a subset of the Ada tasking constructs is presented. The constructs denote processes, following the general theory developed by de Bakker and Zucker, and do not require translation into an intermediate lamguage. All operations on processes are defined and theoretically justified. An existing proof system for Ada tasks is revised, and proved sound and relatively complete with respect to the semantics. %A Ann Welsh %T A Database Programming Language: Definition, Implementation and Correctness Proofs %R Technical Report UMCS-84-10-1 %I Department of Computer Science, University of Manchester %D 1984 %P 239 %O PhD Thesis %X A high level binary relational database programming language is designed using formal specification. The restrictions imposed by the underlying model are minimised, thus removing the distinction between implicit and explicit database constraints and increasing the freedom of the user. A new method is devised for handling semantic integrity by means of program correctness proofs, rather than the conventional approach of dynamic checking. For this purpose, a set of database-oriented Hoare-style axioms and proof rules are dsigned for a subset of the language. This method avoids many associated constraint handling problems such as efficiency of implementation and action on constraint variation. The implementation of the language on MDB, a formally specified database system, is described. %A P.M.C.C. Barahona %T Performance Evaluation of a Multi-ring Dataflow Machine %R Technical Report UMCS-84-10-2 %I Department of Computer Science, University of Manchester %D 1984 %P 137 %O M.Sc. Thesis %X The prototype Manchester dataflow computer is a uniprocessor composed of several units pipelined together in a ring. This thesis is a preliminary attempt to assess the performance of a multi-ring dataflow machine built with several such processing elements. The switch unit required to interconnect the rings, and the allocation of the dataflow instructions to the processing elements are topics which are discussed in detail. Simulation has been used to predict performance. Minor changes are proposed in the ring architecture to avoid certain inefficiencies that have been found. %A J.N.F. Oliveira %T The Formal Semantics of Deterministic Dataflow Programs %R Technical Report UMCS-84-2-1 %I Department of Computer Science, University of Manchester %D 1984 %P 349 %O PhD Thesis %X Addresses the impact of dataflow computing on software technology and, in particular, studies the semantics of dataflow programs. The Manchester dataflow system design is used as an example for the study. Semantics for the Manchester machine are described at the usual graphical level using notation characteristic of dataflow programming. Properties of the Manchester system are studied from both theoretical and practical points of view. Based on this semantics, methods for constructive design and proof of programs written for the Manchester machine are proposed. A transformational approach to dataflow program development based on functional programming is presented as the basis for a more ambitious reasoning methodology. %A David E. Rydeheard %A Rod M. Burstall %T The Unfication of Terms: A Category-theoretic Algorithm %R Technical Report UMCS-85-8-1 %I Department of Computer Science, University of Manchester %D 1985 %P 33 %X As an illustration of the role of abstract mathematics in program design, an algorithm for the unification of terms is derived from constructions of colimits in category theory. %A John Sargeant %T Efficient Stored Data Structures for Dataflow Computing %R Technical Report UMCS-85-8-2 %I Department of Computer Science, University of Manchester %P 220 %O PhD Thesis %X One of the major problems in dataflow computing has been the handling of data structures. The concept of stored data structures must be integrated at reasonable cost into the dataflow model of computation. The thesis describes how this can be achieved, particularly in the context of the Manchester prototype dataflow machine. Problems are tackled at several levels, including that of the underlying hardware. An extension to the prototype architecture, the Structure Store, is described. The code generated for the dataflow language SISAL is discussed in detail. Particular attention is paid to the issue of garbage collection. Optimisations which improve the quality of dataflow code are described. As a result of this work, it is now possible to generate from SISAL dataflow code which is efficient in terms of the total number of instructions executed, while retaining the ability to exploit large amounts of parallelism. Simulation results are presented to demonstrate this achievement. %A Ian D. Cottam %T Extending Pascal with One-entry/Multi-exit Procedures %R Technical Report UMCS-85-9-1 %I Department of Computer Science, University of Manchester %D 1985 %P 24 %X To make the verification of Pascal programs more manageable their so-called standard and exceptional behaviour is separated syntactically with a simple exception handling mechanism (due to Flaviu Cristian). The programming language Pascal (BS 6192 / ISO 7185 level 1) is augmented with the following constructs: one-entry/multi-exit procedures, a guarded statement sequence that may signal a (parameterised) exception, and exception handlers. Two different implementations have been undertaken; a Pascal compiler has been modified to accept and compile the extensions, and a stand-alone preprocessor from the extended language to standard Pascal has been developed. The merits, and otherwise, of both strategies are reported. The constructs are presented informally; a companion paper will give the formal semantics. %A Trevor P. Hopkins %T Image Transfer by Packet-switched Network %R Technical Report UMCS-85-9-2 %I Department of Computer Science, University of Manchester %D 1985 %P 35 %X The advantages and disadvantages of using packet-switching technology for the transfer of image information in real time are considered. An experimental implementation of parts of a system based on a high-speed Local Area Network is described; these include a simple screen output device and a real-time camera input device. The generation of images using a number of microprocessors is also described. A number of applications for such a system are investigated and the extension of this approach to implement an Integrated Information Presentation system is considered. %A Howard Barringer %T Up and Down the Temporal Way %R Technical Report UMCS-85-9-3 %I Department of Computer Science, University of Manchester %D 1985 %P 40 %X A formal specification of a multiple lift system is constructed. The example illustrates and justifies one of many possible system specification styles based on temporal techniques. %A Tobias Nipkow %T Non-deterministic Data Types: Models and Implementations %R Technical Report UMCS-85-10-1 %I Department of Computer Science, University of Manchester %D 1985 %P 32 %X The model theoretic basis for (abstract) data types is generalized from algebras to multi-algebras in order to cope with non-deterministic operations. A programming oriented definition of implementations of data types is given and applied to the new framework. This results in a generalization of the commonly used homomorphism criterion for implementations. A set of constraints on a programming language are derived which guarantee that this criterion is sound w.r.t. the above definition of implememtations. It is argued that any language supporting data abstraction does fulfill these constraints. As an example a simple but expressive language L is defined and it is proved that L does conform to these restrictions. %A Anton P. W. Bohm %A John Sargeant %T Efficient Dataflow Code Generation for SISAL %R Technical Report UMCS-85-10-3 %I Department of Computer Science, University of Manchester %D 1985 %P 27 %X The efficiency of dataflow code generated from a high level language can be improved drastically by both conventional and dataflow-specific optimisations. Such techniques are used in implementing the functional language SISAL on the Manchester Dataflow Machine. %A Pedro Barahona %A John R. Gurd %T Processor Allocation in a Multi-ring Dataflow Machine %R Technical Report UMCS-85-10-4 %I Department of Computer Science, University of Manchester %D 1985 %P 32 %X Partitioning a program into processes and allocating these processes to different processors determines the efficiency of a multiprocessor architecture. In the dataflow model, where each process consists of a single instruction (e.g. an arithmetic or logic operation), an automatic decomposition of a program into fine-grain processes can be achieved. A prototype dataflow machine is in operation at the University of Manchester. The machine comprises a single processing element ( PE ), which contains several units connected together in a pipelined ring. A Multi-ring Dataflow Machine ( MDM ), containing several such processing elements connected together via a switching network, is currently under investigation. This paper describes a method of allocating the dataflow instructions to the processing elements of the Multi-ring Dataflow Machine and examines the influence of the method on the selection of a switching network. Results obtained from simulation of the machine are presented, and it is shown that programs are executed efficiently when their parallelism matches the parallelism of the machine hardware.