1992 - Technical Reports
J.V. Pitt, K.G. Van den Bergh, J. Cunningham, 16ppReport: 1992/1
This paper discusses a practical representation of 'meaning' relative to a 'context', and the use of 'reasoning' to control the interaction between meaning and context which produces 'understanding'. A discourse processing system is implemented, in which (a) techniques from Montague Grammar and Discourse Representation Theory are used to determine the meaning of a sentence; and (b) reasoning methods developed for maintaining integrity in databases are used to validate this meaning and to evaluate the change it induces in the context (ie understanding). Although still some way, perhaps, from either our long-term goal (using natural language specifications for requirements validation), or an exact model of human cognition, the experiment reinforces the intuition that inference mechanisms developed in logic, databases and Artificial Intelligence can have practical applications in natural language understanding.
FOREST Research Report. VSCS: AN OBJECT ORIENTED METHOD FOR REQUIREMENTS ELICITATION AND FORMALISATIONJ. Castro, A. Finkelstein, 107ppReport: 1992/2
In this report we present a prescriptive method called Very Structured Common Sense (VSCS). It has the objective of guiding and organizing the activity by which a formal requirement specification is obtained from an informal application concept. VSCS is a method for eliciting requirements and formalizing then in structured modal action logic (M[A]L II), which supports concepts of the object-oriented paradigm.
We shall make use of the ViewPoint Framework, which explicitly avoids the use of a single representation scheme or common schema for elicitation. Instead, multiple ViewPoints are used to partition the domain of information, the development method and the representations used to express software specifications. Several ViewPoints are deployed, including Object, Text, Event life-cycle, Statechart, Causal and Structured M[A]L. The method can then be viewed as configurations of these related ViewPoints.
F. Simplicio-Filho, 33ppReport: 1992/3
Opportunistic behaviour, which is characterized by shifts between partial solutions and deviations from planned actions, has been identified as legitimate and expected behaviour during software specification understanding. In contrast to goal-oriented behaviour, opportunistic behaviour proceeds without support of a method or general problem solving plan. Nevertheless, about half of the understanding behaviour has been characterized as opportunistic. So, it cannot be ignored in designing methods and tools for supporting specification building and understanding. This paper presents an engineering model of cognitive behaviour in specification understanding. It focuses on the control mechanisms that drive opportunistic and goal-oriented behaviours. The proposed model is based on an interpretation of an established psychological model and described in terms of a set theoretical visual formalism, the state-graph, able to represent concurrent and distributed components.
It suggests that, in general, opportunistic behaviour constitutes the most promising way of succeeding in dealing with unpredictable events, typical of human interaction with the world. As a conclusion, in contrast to the view in which opportunistic behaviour is described as plan violation, the model suggests that opportunistic behaviour does not totally rule out goal-oriented behaviour. A number of understanding activities can operate in parallel and to some extent, this enables the cognitive system to keep the course of actions according to plan while undertaking other cognitive activities. The model specifies the mechanisms that underlie this.
J. Magee, N. Dulay, J. Kramer, 19ppReport: 1992/4
MP is a programming environment for message passing parallel computers. The paper describes the basic set of communication primitives provided by MP and demonstrates how higher level communication operations such as symmetric exchange and remote rendezvous can be directly constructed from the basic set. The paper further shows how global parallel operations such as parallel sum, barrier synchronisation and parallel prefix can be elegantly constructed by combining the basic set of primitives with generic process structures described in the configuration language Darwin which forms part ofthe MP programming environment. Implementation and performance aspects of the primitives and constructed operations are discussed in relation to a transputer based multicomputer.
D.C. Dracopoulos, 34ppReport: 1992/5
In this report an introduction to the Connection Machine model-2 implementation and programming is given. The Connection Machine system is an integrated combination of hardware and software designed for high- speed data parallel computing. The hardware elements of the CM-2 system include front-end computers that provide the development and execution environments for the system software, a parallel processing unit of 64K (65536) processors that execute the data parallel operations, and a high- performance data parallel I/O system. Operations can take place in parallel on data in all the processors. The system software is based upon the operating system or environment of the front-end (host) computer. Users can program using familiar languages and programming constructs, with all the development tools provided by the front end.
A. Saulsbury, T. Stiemerling, 31ppReport: 1992/6
This report describes the implementation of distributed virtual shared memory (DVSM) on the TOPSY multicomputer. The TOPSY machine is a distributed memory multiprocessor based on MC68030 nodes connected by a custom circuit-switched mesh interconnection network (MESHNET), and runs the MESHIX operating system which is Unix System V compatible. The DVSM allows distributed processes to share a paged virtual memory region, whose coherence is maintained by user-level servers using the dynamic distributed manager algorithm. The DVSM implementation is described at the user, server and kernel level, and an overview of the relevant parts of the MESHIX operating systems is also given. A subsequent document will describe performance testing of the system.
B.T. Ng, K. Broda, 21ppReport: 1992/7
This paper brings together partial evaluation and negation in logic programming and proposes a new partial evaluation technique based on a modified Clark's completed database. The technique partially evaluates normal programs and queries and is simple and easily mechanizable. Moreover, it ensures that the partial evaluation will always terminate.
T. Wilkinson, T. Stiemerling, P. Osmon, A. Saulsbury, P. Kelly, 15ppReport: 1992/8
We describe an operating system design for multiprocessor systems called ANGEL, based on a single, coherent, uniform virtual address space. This unifies naming and interprocess communication in both shared and distributed memory multiprocessors by using distributed shared memory techniques when shared memory is not already provided by the hardware.
The design is motivated by analysis of our earlier operating system implementation, based on message passing, and we show how the uniform address space attempts to solve problems with that approach. In particular, we consider the use of client-server cross-mapping to optimise interprocess communications, as used in Bershad et al.'s lightweight RPC. We investigate the use of capabilities to manage protection, and conclude by detailing our implementation plans.
This document describes initial motivations for ANGEL and subsequent detailed design - we will review and may modify many of the details described as the design progresses.
Z. Schreiber, 67ppReport: 1992/9
We investigate what value-passing CCS agents can be automatically verified and present some algorithms. Since algorithms should not have to deal with syntactic interpretation, we start by showing how to represent a value-passing agent by a finite graph with parameters, analogous to a flow-chart. This also makes our work independent of the underlying process algebra. Throughout, agents may have infinite sorts but not unbounded parallelism.
If we allow arbitrary functions and tests, bisimulation is undecidable. But we show that we can find a first-order predicate (involving the functions used in the agent) which is true iff ~n holds between given agents, for given n. Here ~0, ~1, ... are the standard approximations to bisimulation equivalence. These predicates are left as a proof obligation. In special cases such as data- independent agents (where all functions are the identity or constant), we can also automatically find a finite predicate equivalent to ~=
This approach of treating value-passing as fundamental can be combined with Milner's presentation of value-passing as a shorthand for basic CCS. Suppose an agent has some control parameters of finite-sort, but involving tests and functions which are too general for the approach above. We show how to treat these parameters as a shorthand for basic CCS (and expand them) while treating the remaining parameters (which typically represent data and have large sorts) as fundamentally value-passing. We show how this combined view leads to an automatic verification of the alternating bit protocol, without having to "leave out" the data parameters.
P.G. Harrison, E. Pitel, 18ppReport: 1992/10
We derive expressions for the Laplace transform of the sojourn time density in a single server queue with exponential service times and independent Poisson arrival streams of both ordinary, positive customers and negative customers which eliminate a positive customer if present. We compare first come first served and last come first served queueing disciplines for the positive customers, combined with elimination of the last customer in service by a negative customer. We also derive the corresponding result for processor sharing discipline with random elimination. The results show not only differences in the Laplace transforms but also in the means of the distributions which is in contrast to the case where there are no negative customers. The various combinations of queueing discipline and elimination strategy are ranked with respect to these mean values.
P.G. Harrison, 28pp , 0ppReport: 1992/11
A unified approach to the development of algorithms tailored to various classes of parallel computer architecture is presented. The central theme is to identify a small set of higher-order functions that can be implemented efficiently on the target architecture and which can be used to express parallel algorithms - in general via mechanised program transformation from some higher-level specification. Such higher-order functions enable generic programs to be written in which much parallelism may be explicit. Although the analysis uses purely functional languages, it is the functional paradigm that is important and not the particular syntax. The proposed methodology is illustrated with a numerical problem which is solved directly by a non- recursive program. We also describe schemes that map programs onto both static and dynamic MIMD architectures which have communication links which are fixed and changeable at run-time respectively.
R.L. While, 10ppReport: 1992/12
This paper describes a software implementation of the read-barrier for incremental copying garbage collection which adds less than 10% to the execution time of a program using conventional copying garbage collection. This is comparable with published figures for the overhead of a hardware implementation.
The reader is assumed to be familiar with copying garbage collection and Baker-style incremental garbage collection.
THE SEMANTICS AND IMPLEMENTATION OF VARIOUS "BEST- FIT" PATTERN MATCHING SCHEMES FOR FUNCTIONAL LANGUAGESA.J. Field, S. Hunt, R.L. While, 24ppReport: 1992/13
We give a formal definition of a best-fit strategy for handling overlapping patterns in declarative languages based upon the specificity of patterns. Our approach to best-fit renders the order of the equations of a function unimportant and provides a general method for handling "otherwise" clauses in function definitions. We explore several variations of the scheme by examining the various ways in which the components of individual patterns can be tested; the ramifications of using left-strict, bi-strict and parallel matching schemes within individual equations are investigated. We establish a generalised framework for describing the semantics of pattern matching and show how this can be used to give a formal semantics for each of the best-fit strategies. The semantics is given in terms of a specificity ordering functions >>, derived from the standard domain ordering, and a semantic Î - a parameter of the semantic equations for best-fit. We describe a general algorithm for translating a set of best-fit patterns into a sequential intermediate code based upon the use of matching trees and prove the correctness of the translation by establishing a correspondence between the semantics of the matching trees and denotational semantics of the matching scheme being compiled. Issues of both strong and maximal sequentially are raised in the context of parallel pattern matching.
S. Coury, P.G. Harrison, 13ppReport: 1992/14
This paper derives the waiting time distribution for a class of multi-queue systems served in cyclic order at discrete intervals. An immediate application for such a model is in communication networks where a number of different traffic sources compete to access a group of transmission channels operating under a time-slotted sharing policy. This system maps naturally onto a model in which the service time distribution has discrete phase-type. This leads to a set of matrix equations, easily tractable iterative procedures for their solution and controllable accuracy in their numerical evaluation. Furthermore, the methodology is extendable to several other polling strategies, particularly those in which the service time distribution is continuous phase-type, where analytical solutions can be derived using existing methods.
P.G. Harrison, H. Khoshnevisan, 10ppReport: 1992/15
The efficient implementation of abstract data types and all functions that manipulate them would permit application-oriented solutions to be developed without having to take undue account of executional properties. The synthesis of efficient concrete types and functions forms the basis of the present paper, which appeals to a theory of inverse functions for additional axioms to augment those of a first-order functional algebra. These axioms are then applied in the simplification of the combinator-expressions arising in the synthesis of the functions between the concrete types. We also show how the abstraction function itself may be deduced in certain situations where it is required to optimise particular operations on an abstract type. In addition to possessing rigorous mathematical foundations, the function-level axioms are more generally applicable than previous approaches to this problem, and induce a more mechanisable rewrite-based transformation system.
P.G. Harrison, H. Khoshnevisan, 23ppReport: 1992/16
Iterative forms are derived for a class of recursive functions, i.e. the recursion is "removed". The transformation comprises first analysis of the defining equation of a recursive function and then synthesis of an imperative language loop from the primitive subexpressions so obtained. This initially leads to a two-loop program but further transformation provides a single loop version under appropriate conditions. The analysis-synthesis approach contrasts with previous methods using template matching and induces a constructive method which is better suited to mechanisation, although its implementation is not considered here.
B. Strulo, D. Gabbay, P.G. Harrison, 24ppReport: 1992/17
Temporal logic has proved to be a useful tool for the specification of computer systems interacting with their environment. Meanwhile a common approach to the analysis of the performance of such systems has been based on stochastic process theory and in particular Markov chains. The central result of this paper is to show that a natural model of a temporal logic system in a random environment is equivalent to a finite-state Markov chain with a particular structure of state space. This requires a proof that temporal logic specifications may have their past dependence transformed away.
C. Hankin, S. Hunt, 26ppReport: 1992/18
Much of the earlier development of abstract interpretation, and its application to imperative programming languages, has concerned techniques for finding fixed points in large (often infinite) lattices. The standard approach in the abstract interpretation of functional languages has been to work with small, finite lattices and this supposedly circumvents the need for such techniques. However, practical experience has shown that, in the presence of higher order functions, the lattices soon become too large (although still finite) for the fixed-point finding problem to be tractable. This paper develops some approximation techniques which were first proposed by Hunt and shows how these techniques relate to the earlier use of widening and narrowing operations by the Cousots.
G.L. Burn, 19ppReport: 1992/19
A number of different semantics-based program analysis techniques, such as abstract interpretation, projection-based analyses and type inference, have been developed by various people. How can they be compared?
In answering this question, we have found it particularly fruitful to focus on the properties that an analysis can manipulate, and how these properties can be combined.
We demonstrate the value of this methodology by clarifying the relationship between abstract interpretation and projection-based analyses; giving an explanation of why the tensor product arises in abstract interpretation; and gaining some insight into the problems caused by higher-order functions.
Furthermore, our investigations suggest finer classifications of particular abstract interpretations than those given by the terms independent attribute method and relational method.
G.L. Burn, D. Le Metayer, 16ppReport: 1992/20
We show that compiler optimisations based on strictness analysis can be expressed formally in the functional framework using continuations. This formal presentation has two benefits: it allows us to give a rigorous correctness proof of the optimised compiler; and it exposes the various optimisations made possible by a strictness analysis. These benefits are especially significant in the presence of partially evaluated data structures.
J.A. Muylaert-Filho, G.L. Burn, 13ppReport: 1992/21
We prove that performing a continuation passing style (CPS) transformation on a higher-order program and then doing a program analysis gives more information than analysing the original program. Doing this in a typed setting has given some surprising difficulties.
C. Hankin, D.L. Le Metayer, D. Sands, 28ppReport: 1992/22
Gamma is a minimal language based on conditional multiset rewriting. The virtues of this paradigm in terms of systematic program construction and design of programs for highly parallel machines have been demonstrated in previous papers. We introduce here sequential and parallel operators for combining Gamma programs and we study their properties. The main focus of the paper is to give conditions under which sequential composition can be transformed into parallel composition and vice versa. Such transformations are especially valuable for adapting Gamma programs for execution on a particular target architecture.
M. Mansouri-Samani, M. Sloman, 46ppReport: 1992/23
Monitoring is an essential means for obtaining the information required about the components of a distributed system in order to make management decisions and subsequently control their behaviour. Monitoring is also used to obtain information about component execution and interaction when debugging distributed or parallel systems. This report presents a general functional model of monitoring in terms of generation, processing, distribution and presentation of information. This model can provide a framework for deriving the facilities required for the design and construction of a generalised monitoring service for distributed systems. A number of approaches to monitoring of distributed systems are compared in the report.
S. Abramsky, R. Jagadeesan, 40ppReport: 1992/24
We present a game semantics for Linear Logic, in which formulas denote games and proofs denote winning strategies. We show that our semantics yields a categorical model of Linear Logic and prove full completeness for Multiplicative Linear Logic with the MIX rule: every winning strategy is the denotation of a unique cut-free proof net. A key role is played by the notion of history-free strategy; strong connections are made between history-free strategies and the Geometry of Interaction. Our semantics incorporates a natural notion of polarity, leading to a refined treatment of the additives. We make comparisons with related work by Joyal, Blass et al.
I. Mackie, 34ppReport: 1992/25
We take Abramsky's term assignment for Intuitionistic Linear Logic (the Linear Term Calculus) as the basis of a functional programming language. This is a language where the programmer must embed explicitly the resource and control information of an algorithm. We give a type reconstruction algorithm for our language in the style of Milner's W algorithm, together with a description of the implementation, and examples of use.
D. Sharp, M. Cripps, 9ppReport: 1992/26
We present a technique for systematically synthesizing parallel algorithms starting from a high-level specification of the problem to be solved and a functional abstraction of the target architecture. We show how functional language program transformation can be used to generate various algorithms that match the characteristics of the target architecture and demonstrate the technique by synthesizing various Fast Fourier Transforms for various parallel architectures from a specification of the Discrete Fourier Transform.
D. Sharp, A.J. Field, H. Khoshnevisan, 13ppReport: 1992/27
We explore the use of functional languages and program transformation in the specification and derivation of algorithms for parallel architectures based upon message-passing. Using the unbounded knapsack problem as an example, we show how an abstract specification of the problem can be transformed into an efficient sequential algorithm, and then by further transformation into a form suitable for dynamic message passing architectures with static scheduling. To obtain the sequential algorithm, we first transform the specification into a recursive function, and then memoise the function to avoid repeated calculation of the same expression. In parallelising the resulting function for a distributed-memory machine, the function requires further transformation to expose explicitly the communication structure required. This is achieved by specifying the abstract target architecture as a program skeleton (a higher-order function), and then using transformation to marry the algorithm specification to that of the skeleton.
D. Sharp, M. Cripps, 10ppReport: 1992/28
Most current parallel computers are made from tens of processors that may communicate with each other (fairly slowly) by means of static intercommunication paths. However, in the future the use of optical communication media & wafer scale integration will facilitate construction of computers with thousands of simple processors each of which may communicate simultaneously with any other.
What will these computers run? We present three novel algorithms that solve problems by communication. One, fractal image generation, works purely by iterative communication which is interesting because studies of the human brain indicate that the connections between neurons are mainly responsible for our powers of thought.
These algorithms combine features of both imperative and connectionist programming styles and arose from a systematic study of goal-directed program transformation, including the target architecture with the program specification. They are examples of a whole class of such algorithms which we expect will be developed similarly.
D. Sharp, R.L. While, 4ppReport: 1992/29
We present a novel algorithm for the detection of the pitch period in short- term quasi-stationary periodic data. The algorithm uses no multiplications - it involves only integer addition and indirect addressing. It executes in real time on a 16-bit microprocessor and is thus suitable for real-time pitch period extraction in speech, as well as for pitch extraction in other applications where low cost is required, e.g. pitch-to-MIDI (musical instrument digital interface) conversion. The algorithm uses the 16-bit microprocessor to simulate the operation of a massively-parallel machine running a communication- intensive, massively-parallel algorithm. Communications are modelled as variable assignments and array-indexing operations. This style of algorithm has also been used in other application areas such as pattern recognition, with considerable success.
D. Sharp, R.L. While, 16ppReport: 1992/30
We present a novel algorithm for the automatic recognition and classification of fractally-encoded images. The algorithm can recognise images from a fractal transformation library in the presence of scaling, displacement and rotation and is robust in the presence of noise. The algorithm forms the basis for a more general recognition mechanism if non-fractal images are encoded as fractal pictures using Barnsley's Collage Theorem.
The algorithm is a member of a recently-discovered novel class of "Communication-Intensive Massively-Parallel" (CIMP) algorithms that have already been used for sorting and tessellation of the plane and which show great promise for use in other application areas.
D. Sharp, P.G. Harrison, J. Darlington, 21ppReport: 1992/31
We present a technique for systematically synthesising algorithms for message passing parallel machines and illustrate it by the derivation of a message passing sorting algorithm, based on Quicksort, that is, we claim, the fastest parallel quick sort algorithm having a complexity of 0( log n * log n ) for a machine with n physical processors sorting an element list. The algorithm is thus highly suitable for massively parallel machines such as the Thinking Machines Connection Machine and execution times on an 8192 processor Connection Machine are presented to confirm this. The basis of the method is to formally represent the message passing architecture of the machine, specify the problem as an initial, highly inefficient but obviously correct message passing algorithm and then refine the specification so that more and more of the computation is accomplished via message-passing. We use a functional programming language to model these activities and use sets to model the inherently non-deterministic aspects of message passing architectures while ensuring that the final algorithm is deterministic.
F. Simplicio-Filho , 23ppReport: 1992/32
This paper describes a prototype of software tool, the Narrator. The major design goal of the Narrator is to demonstrate the feasibility of a "relax and watch" approach to facilitate comprehension of software specifications. The Narrator presents specifications represented in statecharts by way of a narrative. The presentation consists of an ordered highlighting of graphic components of the diagram. The order in which the components are highlighted constitutes the narrative. The narrator software environment combines a number of interaction artifacts such as: a graphic editor for statechart diagrams; the compilation of diagram and the formulaton of an execution producing a script for the narrative's introduction; the facility for exploring system configurations and, an animator which co-ordinates the highlighting of components of the diagram according to the script. The implementation of these features are discussed.
M. Geerling, 34ppReport: 1992/33
Several parallel-program derivations for two problems are given. The derivations are in a transformational-style and aim at a program in skeleton- form. The parallel programs are intended for SIMD (Single Instruction Multiple Data) architectures.
For the prefix computation there are derivations for processor arrays and hypercubes, both leading to an optimal algorithm for these architectures, i.e., O(n) and O(log n), respectively.
The algorithm derived for matrix multiplication on MESHs with wraparound connections is transformed to MESH architectures without these connections, by the use of data type transformations.
G.L. Burn, 13ppReport: 1992/34
Using logics to express program properties, and deduction systems for proving properties of programs, gives a very elegant way of defining program analysis techniques. This paper addresses a shortcoming of previous work in the area by establishing a more general framework for such logics, as is commonly done for program analysis using abstract interpretation. Moreover, there are natural extensions of this work which deal with polymorphic languages.
P.A.S. Veloso, T.S.E. Maibaum, 12ppReport: 1992/35
The Modularization Property is a basic tool for guaranteeing the preservation of modular structure under refinements and its importance has been noted by several researchers. In the context of logical specifications, i.e. those presented by sets of first-order sentences of a (possibly many-sorted) language, the role played by the Modularization Property is examined and a proof of the Modularization Theorem is presented.
G.L. Burn, 10ppReport: 1992/36
This paper reports on our initial work on assessing how using the evaluation transformer model of reduction affects the performance of lazy functional programs. The model uses information about how much evaluation of an expression is required, in order to evaluate an expression as much as possible, as early as possible. Our results show that there is a definite gain over just using strictness information, but that it is difficult to characterise exactly how much gain there will be, and in what programs it will occur.