The study of computing is split at an early stage between the separate branches that deal with hardware and software;there is also a corresponding split in later professional specialisation. This paper explores the es...
详细信息
The study of computing is split at an early stage between the separate branches that deal with hardware and software;there is also a corresponding split in later professional specialisation. This paper explores the essential unity of the two branches and attempts to point to a common framework within which hardware-software codesigns can be expressed as a single executable specification, reasoned about, and transformed into implementations. We also describe a hardware/software co-design environment which has been built, and we show how designs can be realised within this environment. A rapid development cycle is achieved by using FPGAs to host the hardware components of the system. The architecture of a hardware platform for supporting experimental hardware/software co-designs is presented. A. particular example of a real-time video processing application built using this design environment is also described.
作者：
MORGAN, CComputing Laboratory
Programming Research Group Oxford University 8-11 Keble Road Oxford United Kingdom OXI 3QD
A set of local variables in a program is considered auxiliary if its members occur only in assignments to members of the same set. Data refinement changes a program, replacing one set of local variables by another se...
详细信息
A set of local variables in a program is considered auxiliary if its members occur only in assignments to members of the same set. Data refinement changes a program, replacing one set of local variables by another set, in order to move toward a more efficient representation of data. Most techniques of data refinement give a direct transformation, but there exists an indirect technique, using auxiliary variables, that proceeds in several stages. Generally, the 2 techniques are considered separately. It is demonstrated that the several stages of the indirect technique are themselves special cases of the direct one, thus unifying the separate approaches. Removal of auxiliary variables is formalized incidentally.
This paper describes the use of Ruby, a language of functions and relations, to develop serialised implementations of array-based architectures. Our Ruby expressions contain parameters which can be varied to produce a...
详细信息
This paper describes the use of Ruby, a language of functions and relations, to develop serialised implementations of array-based architectures. Our Ruby expressions contain parameters which can be varied to produce a wide range of designs with different space-time trade-offs. Such expressions can be obtained by applying correctness-preserving transformations to an initial simple description. This approach provides a unified treatment of serialisation schemes similar to LPGS (Locally Parallel Globally Sequential) and LSGP (Locally Sequential Globally Parallel) partitioning methods, and will be illustrated by the development of a variety of circuits for convolution.
We give a model-theoretic semantics for the logic of higher-order Horn clauses, the basis of a form of the lambdaProlog higher-order logic programming language. We define certain intensional general models and show th...
详细信息
We give a model-theoretic semantics for the logic of higher-order Horn clauses, the basis of a form of the lambdaProlog higher-order logic programming language. We define certain intensional general models and show that higher-order Horn clause logic is sound and complete with respect to them.
We explore the suitability of two semantic spaces as a basis for a probabilistic variant of the language of Communicating Sequential Processes (CSP), so as to provide a formalism for the specification and proof of cor...
详细信息
We explore the suitability of two semantic spaces as a basis for a probabilistic variant of the language of Communicating Sequential Processes (CSP), so as to provide a formalism for the specification and proof of correctness of probabilistic algorithms. The two spaces give rise to two sublanguages, each of which is characterised by an algebraic axiomatisation which is shown to be sound and complete for finite processes. In the first semantics, processes are defined as probability measures on the space of infinite traces and operators are defined as functions (mostly transformations) of probability measures, The advantage of this semantics is that it is simple and good for reasoning about probabilistic properties such as self-stabilisation or fairness of random algorithms. The disadvantage is that neither external choice nor parallel composition other than fully synchronised parallel composition can be defined in this semantics. This problem is solved in the second model which is based on the space of conditional probability measures of infinite traces. This model leads to a set of proof rules for the deterministic properties of probabilistic algorithms, but it is more difficult to use in the analysis of probabilistic properties. The last part of the paper shows how the two models are related and how this can be exploited to combine their advantages and get around their disadvantages, This is illustrated by the example of a self-stabilising tokenring.
We describe and analyse a new parallel algorithm for event-driven simulation of hard-particle systems that is based on the ideas of the bulk-synchronous parallel (BSP) model. This model provides a unifying approach fo...
详细信息
We describe and analyse a new parallel algorithm for event-driven simulation of hard-particle systems that is based on the ideas of the bulk-synchronous parallel (BSP) model. This model provides a unifying approach for general purpose parallel computing which in addition to efficient computation ensures portability across different parallel architectures. The hard-particle system is divided into regions that are owned by a unique processor. Events involving particles located in the region boundaries are called border zone events and are used to synchronize the parallel operation of the processors. On a P-processor BSP computer the algorithm works doing iterations composed of two phases: the parallel phase where each processor is simultaneously allowed to simulate serially and asynchronously its own region, and the synchronization phase where the occurrence of at most P border zone events is scheduled for the next iteration considering the state of neighboring regions. We show that this algorithm is efficient in practice provided that a sufficiently large hard-particle system is to be simulated.
In data refinement, a concrete data type replaces an abstract data type used in the design of an algorithm or system (Gries and Prins, 1985; Hoare, 1972; Jones, 1980). We present two methods for calculating the weakes...
详细信息
In data refinement, a concrete data type replaces an abstract data type used in the design of an algorithm or system (Gries and Prins, 1985; Hoare, 1972; Jones, 1980). We present two methods for calculating the weakest specification of each operation on a concrete data type from the specification of the corresponding abstract operation, together with a single simulation relation (Milner, 1980; Park, 1981), which specifies the correspondence between the two types. The methods are proved sound and (jointly) complete for a nondeterministic procedural programming language slightly more powerful than Dijkstra's (1976). Operations (in general, nondeterministic) are represented by relations, and significant use is made of prespecification and postspecification (Hoare and He, Jifeng, 1987).
Dijkstra's (1975) weakest precondition is generalized in 4 ways, including: 1. The parameter Q may be a program, or it may be just the specification of a program that is not yet written. 2. The programming lang...
详细信息
Dijkstra's (1975) weakest precondition is generalized in 4 ways, including: 1. The parameter Q may be a program, or it may be just the specification of a program that is not yet written. 2. The programming language is extended to include general recursion. The increase in generality is obtained at the expense of some increase in complexity, and it can be justified only when it is needed. It is suggested that, in the design and development of correct programs, a calculus should be adopted in which: 1. programs and specifications are freely mixed, and 2. P is a program or design that correctly implements a design or specification Q, represented by the relational inclusion of P as a subset of Q. These suggestions generate some paradoxes, but they can be solved by recognizing that the set of programs is a proper subset of the set of specifications. Specifically, they are confined to relations that can be described using the primitives and operators of some programming language only.
A mathematical model of reconfigurability. We restrict is presented. The study is restricted to reconfigurations that can be implemented by connecting and disconnecting the wires that link nodes;these wires could be p...
详细信息
A mathematical model of reconfigurability. We restrict is presented. The study is restricted to reconfigurations that can be implemented by connecting and disconnecting the wires that link nodes;these wires could be physical or logical.
Two collaborative projects, the European ESPRIT BRA ProCoS project and the UK IED safemos project, are currently investigating methods to prove software and hardware systems correct at a number of different levels of ...
详细信息
Two collaborative projects, the European ESPRIT BRA ProCoS project and the UK IED safemos project, are currently investigating methods to prove software and hardware systems correct at a number of different levels of abstraction. Both projects intend to concentrate on subsets of Occam, and the transputer instruction set. The projects will aim to use the same machine language so that results obtained on both projects will be compatible. The initial selection of the projects (a simple subset of the transputer) is presented using the specification language Z. The role of the specification in the two projects is explained and the benefits and drawbacks of such a specification are discussed.
暂无评论