With two examples we show the suitability of the bulk-synchronous parallel (BSP) model for discrete-event simulation of homogeneous large-scale systems. This model provides a unifying approach for general purpose para...
详细信息
ISBN:
(纸本)0818679654
With two examples we show the suitability of the bulk-synchronous parallel (BSP) model for discrete-event simulation of homogeneous large-scale systems. This model provides a unifying approach for general purpose parallel computing which in addition to efficient and scalable computation, ensures portability across different parallel architectures. A valuable feature of this approach is a simple cost model that enables precise performance prediction of BSP algorithms. We show both theoretically and empirically that systems with uniform event occurrence among their components, such as colliding hard-spheres and ising-spin models, can be efficiently simulated in practice on current parallel computers supporting the BSP model.
This paper is a description of a simple operating system, which runs in a virtual machine (implemented on a real machine by an interpreter). OS6 copes with only one user at a time, and is not a multi-programming syste...
A framework for model-checking timed CSP processes within a new model of standard CSP was discussed. The timing of events was provided by the consistent and regular communication of a special tock event, analogous to ...
详细信息
A framework for model-checking timed CSP processes within a new model of standard CSP was discussed. The timing of events was provided by the consistent and regular communication of a special tock event, analogous to the tick of a clock. A translation function TCSP&rarrCSP was done inductively over syntax of TCSP processes to equate every elapsed time unit with the communication of k tocks. It was observed that event occurance and timeout did not lead to an accumulation of timing errors.
We present a basis for the formal specification and stepwise development of distributed systems, i.e. programs which are intended (at least conceptually) to run on distributed-memory parallel machines which communicat...
详细信息
This paper argues that our recent progress in the development of a sound programming methodology should not lead us to ignore the more difficult aspects of engineering;and that in future we should pay more attention t...
详细信息
The two models presented in this paper provide two different semantics for an extension of Dijkstra's language of guarded commands. The extended language has an additional operator, namely probabilistic choice, wh...
详细信息
The two models presented in this paper provide two different semantics for an extension of Dijkstra's language of guarded commands. The extended language has an additional operator, namely probabilistic choice, which makes it possible to express randomized algorithms. An earlier model by Claire Jones included probabilistic choice but not non-determinism, which meant that it could not be used for the development of algorithms from specifications. Our second model is built on top of Claire Jones' model, using a general method of extending a probabilistic cpo to one which also contains non-determinism. The first model was constructed from scratch, as it were, guided only by the desire for certain algebraic properties of the language constructs, which we found lacking in the second model. We compare and contrast the properties of the two models both by giving examples and by constructing mappings between them and the non-probabilistic model. On the basis of this comparison we argue that, in general, the first model is preferable to the second. (C) 1997 Elsevier Science B.V.
A process communicates with its environment and with other processes by syncronized output and input on named channels. The current state of a process is defined by the sequences of messages which have passed along ea...
A process communicates with its environment and with other processes by syncronized output and input on named channels. The current state of a process is defined by the sequences of messages which have passed along each of the channels, and by the sets of messages that may next be passed on each channel. A process satisfies an assertion if the assertion is at all times true of all possible states of the process. We present a calculus for proving that a process satisfies the assertion describing its intended behaviour. The following constructs are axiomatised: output; input; simple recursion; disjoint parallelism; channel renaming, connection and hiding; process chaining; nondeterminism; conditional; alternation; and mutual recursion. The calculus is illustrated by proof of a number of simple buffering protocols.
In this paper we present two languages that are refinements of timed CSP (Davies and Schneider, this volume): a probabilistic language, and a fully deterministic language with a notion of priority. In the first part o...
详细信息
In this paper we present two languages that are refinements of timed CSP (Davies and Schneider, this volume): a probabilistic language, and a fully deterministic language with a notion of priority. In the first part of the paper we describe the deterministic language and its semantic model. The syntax is based upon that of timed CSP except some of the operators are refined so as to remove all nondeterminism;this produces prioritized operators. The semantics for our language represents a process as the set of possible behaviours for the process, where a behaviour models the priorities for different actions. A number of algebraic laws for our language are given and the model is illustrated with two examples. In the second part of the paper, we extend the language by adding a probabilistic choice operator. We produce a semantic model for our language which gives the probabilities of different behaviours occurring, as well as modelling the relative priorities for events within a behaviour. The model is illustrated with an example of a communications protocol transmitting messages over an unreliable medium.
作者：
HOARE, CAROxford University
Computing Laboratory Programming Research Group 8-11 Keble Road Oxford OX1 3QD UK
This paper shows how propositional logic may be used to reason about synchronous combinational switching circuits implemented in C-mos. It develops a simple formalism and theory for describing and predicting their beh...
详细信息
This paper shows how propositional logic may be used to reason about synchronous combinational switching circuits implemented in C-mos. It develops a simple formalism and theory for describing and predicting their behaviour. On this it builds a calculus of design which is driven by proof obligations. The design philosophy for software introduced in [1] is thereby extended to a certain kind of hardware design. No prior knowledge of hardware is assumed of the reader;but useful background, motivation, examples and pictures may be found in [2]. Many of the problems described in that paper have been solved in this one.
General purpose parallel computing systems come in a variety of forms. We have various kinds of distributed memory architectures, shared memory multiprocessors, and clusters of workstations. New technologies may incre...
详细信息
General purpose parallel computing systems come in a variety of forms. We have various kinds of distributed memory architectures, shared memory multiprocessors, and clusters of workstations. New technologies may increase this range still further. Can one hope to design portable and scalable parallel software in the face of such architectural diversity? In this paper we show that it is indeed possible to produce fully portable parallel software which will run with highly efficient, scalable and predictable performance on any general purpose parallel architecture. The approach we describe is based on the bulk synchronous parallel (BSP) model of computation. The BSP model provides a simple, unified framework for the design and programming of all kinds of general purpose parallel systems. Over the last few years, a number of important research activities in algorithms and architectures have been pursued as part of this new approach to scalable parallel computing. In this paper we give some simple BSP algorithms and show how they can be expressed as programs. We also briefly describe some of the BSP programming language developments which are now being pursued.
暂无评论