E1AR0002@SMUVM1.BITNET (02/14/86)
The Department of Computer Science, University of Manchester, is pleased to announce the availability of the technical reports listed below. Enquiries by electronic mail should be addressed to :- [JANET] techreports@uk.ac.man.cs.ux [UUCP] ...!mcvax!ukc!man.cs.ux!techreports [ARPA] techreports%uk.ac.man.cs.ux@ucl.cs.arpa U.S. sites should use the ARPA rather than UUCP when possible. For copies, please write, enclosing the necessary payment, to Mrs. A. McCauley Department of Computer Science University of Manchester Oxford Road Manchester, M13 9PL England. Payment should be made by sterling cheque made payable to `The University of Manchester'. UMCS-85-8-1 The Unification of Terms: A Category-theoretic Algorithm No charge UMCS-85-9-1 Extending Pascal with One-entry/Multi-exit Procedures No charge UMCS-85-9-2 Image Transfer by Packet-switched Network No charge UMCS-85-9-3 Up and Down the Temporal Way No charge UMCS-85-10-1 Non-deterministic Data Types: Models and Implementations No charge UMCS-85-10-2 Efficient Dataflow Code Generation for SISAL No charge UMCS-85-10-3 Processor Allocation in a Multi-ring Dataflow Machine No charge UMCS-82-10-1 The Specification, Design and Implementation of NDB (pounds) 3.50 UMCS-83-10-1 A Denotational Semantics for Concurrent Ada Programs (pounds) 6.50 UMCS-84-2-1 The Formal Semantics of Deterministic Dataflow Programs (pounds) 7.00 UMCS-84-10-1 A Database Programming Language: Definition ... (pounds) 5.50 UMCS-84-10-2 Performance Evaluation of a Multi-ring Dataflow Machine (pounds) 3.00 UMCS-85-8-2 Efficient Stored Structures for Dataflow Computing (pounds) 4.50 A Multilayered Dataflow Machine Architecture No charge A B S T R A C T S ================= [UMCS-85-8-1] The Unfication of Terms: A Category-theoretic Algorithm David E. Rydeheard and Rod M. Burstall 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. Technical Report, 33pages. [UMCS-85-9-1] Extending Pascal with One-entry/Multi-exit Procedures Ian D. Cottam 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. Technical Report, 24pages [UMCS-85-9-2] Image Transfer by Packet-switched Network Trevor P. Hopkins 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. Technical Report, 35pages. [UMCS-85-9-3] Up and Down the Temporal Way Howard Barringer 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. Technical Report, 40pages. [UMCS-85-10-1] Non-deterministic Data Types: Models and Implementations Tobias Nipkow 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. Technical Report, 32pages. [UMCS-85-10-3] Efficient Dataflow Code Generation for SISAL Anton P. W. Bohm and John Sargeant 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. Technical Report, 27pages. [UMCS-85-10-4] Processor Allocation in a Multi-ring Dataflow Machine Pedro Barahona and John R. Gurd 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. Technical Report, 32pages. The following theses are also available as technical reports. [UMCS-82-10-1] The Specification, Design and Implementation of NDB Ann Welsh 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. M.Sc. Thesis, 126pages. [UMCS-83-10-1] A Denotational Semantics for Concurrent Ada Programs Ian Mearns 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. PhD Thesis, 330pages. [UMCS-84-2-1] The Formal Semantics of Deterministic Dataflow Programs J.N.F. Oliveira 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. PhD Thesis, 349pages. [UMCS-84-10-1] A Database Programming Language: Definition, Implementation and Correctness Proofs Ann Welsh 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. PhD Thesis, 239pages. [UMCS-84-10-2] Performance Evaluation of a Multi-ring Dataflow Machine P.M.C.C. Barahona 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. M.Sc. Thesis, 137pages. [UMCS-85-8-2] Efficient Stored Data Structures for Dataflow Computing John Sargeant 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. PhD Thesis, 220pages. The following internal report of the DataFlow Group is also available. A Multilayered Dataflow Computer Architecture J.R. Gurd and I. Watson, J.R.W. Glauert 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. Internal Report, March 1980, 90pages (3rd issue)