Skip to main content
main-content

Über dieses Buch

In a time of multiprocessor machines, message switching networks and process control programming tasks, the foundations of programming distributed systems are among the central challenges for computing sci enti sts. The foundati ons of di stributed programming compri se all the fasci nating questions of computing science: the development of adequate com putational , conceptual and semantic model s for distributed systems, specification methods, verification techniques, transformation rules, the development of suitable representations by programming languages, evaluation and execution of programs describing distributed systems. Being the 7th in a series of ASI Summer Schools at Marktoberdorf, these lectures concentrated on distributed systems. Already during the previous Summer School s at Marktoberdorf aspects of di stributed systems were important periodical topics. The rising interest in distributed systems, their design and implementation led to a considerable amount of research in this area. This is impressively demonstrated by the broad spectrum of the topics of the papers in this vol ume, although they are far from being comprehensive for the work done in the area of distributed systems. Distributed systems are extraordinarily complex and allow many distinct viewpoints. Therefore the literature on distributed systems sometimes may look rather confusing to people not working in the field. Nevertheless there is no reason for resignation: the Summer School was able to show considerable convergence in ideas, approaches and concepts for distributed systems.

Inhaltsverzeichnis

Frontmatter

On the nature of computing science

On the nature of computing science

Abstract
Now this Summer School draws to a close, it seems appropriate to try to put its topic into some perspective.
Edsger W. Dijkstra

Operational Models of Distributed Systems

Frontmatter

Distributed Systems, Partial Orderings of Events, and Event Structures

Abstract
These lecture notes are divided in two parts, dedicated to two models, concurrent histories and Graphs for Distributed Systems (GDS), both based on partial orderings. The models are largely consistent, the latter being a richer version of the former, conceived as a specification formalism for distributed systems. The semantic aspects of the first model are studied in finer detail, including properties of non terminating computations and the definition of an observational equivalence.
Pierpaolo Degano, Ugo Montanari

On Mixed Computation: Informal Account of the Strict and Polyvariant Computational Schemes

Abstract
Mixed computation [2,4] is a rather general concept embracing quite many notions and techniques in programming that appeared and applied independently in various times and under various circumstances. We shall list some of them: incremental computation, incomplete information processing, partial evaluation (computation, execution), lazy evaluation, program projection, constant propagation, binding, data driven processing, symbolic computation, compile-time facilities, etc.
Andrei P. Ershov

Abstract Modelling of Distributed Systems

Frontmatter

Notes on Communicating Sequential Systems

Abstract
These notes present a coherent and comprehensive introduction to the theory and applications of Communicating Sequential Processes. Most of the illustrative examples have appeared earlier in PRG-22. The theory described in PRG-16 has been taken as the basis of a number of algebraic laws, which can be used for proofs of equivalence and can justify correctness-preserving transformations. A complete method for specifying processes and proving their correctness has been taken over from PRG-20 and PRG-23. Many of the concepts have been implemented in LISPKIT, as described in PRG-32.
C. A. R. Hoare

Lectures on a Calculus for Communicating Systems

Abstract
Sequential computation, which until quite recently was the only mode of computation available in well-known programming languages, has a well-established model theory. This fact owes much to the lambda-calculus, which existed long before any notion of implementing a programming language. Yet the primary purpose of the lambda calculus was to study evaluation or execution; it was (and is) a paradigm for evaluation, in the same way that the predicate calculus is a paradigm for deduction. More recently, and largely due to Dana Scott, the model theory of the lambda calculus has grown and has been harmonised with its evaluation theory.
Robin Milner

Extensional Behaviour of Concurrent, Nondeterministic, Communicating Systems

Abstract
A simple denotational model for nondeterministic communicating, concurrent agents is introduced that allows to represent the extensional behaviour of communicating agents. Based on this model several concepts of program correctness are introduced analysed and related to classical concepts. Observability concepts are discussed for an operational semantics given in the form of labelled rewriting systems. In particular the close connections between domain theory and fixed point theory for concurrent programs and concepts of correctness are investigated and outlined, and generalizations of the notions of partial and total correctness are given.
Manfred Broy

Hardware as Distributed Systems

Frontmatter

The Architecture of Parallel Computers

Abstract
Throughout this paper, we write lg x for log2 x, ln x for the natural logarithm log e x, and log x when the base is immaterial; we use log k x for (logx) k .
Clyde P. Kruskal, Larry Rudolph, Ron Cytron

Data Flow Computation

Abstract
All data flow models describe computation in terms of locally controlled events; each event is the “firing” of an “actor”. There is no notion of a single point or locus of control—nothing corresponding to the program location counter of a conventional sequential computer. Since many actors may be ready to fire, these models can represent many asynchronous concurrent computational events. Nevertheless, they can guarantee an input/output behavior that is unaffected by the order in which the firing of actors is carried out. This property of data flow models—determinacy—ensures that their input/output behavior is functional. Thus the semantics of data flow graphs are closely related to the semantics of applicative programming languages, and we will illustrate the correspondence of data flow graphs to textual programs by means of program fragments written in Val, an applicative programming language developed at MIT for scientific applications.
Jack B. Dennis

Concurrent Computations and VLSI Circuits

Abstract
VLSI is a medium in which computations can be realized that exhibit a high degree of concurrency. Concurrent computations require a very careful design technique, for, as we know, uncontrolled concurrency results in uncontrollable complexity. This observation makes complexity control a conditio sine qua non for VLSI design. We know of only one effective technique of complexity control: modular design. Using this technique, the design of a component amounts to the choice of subcomponents and relations. The relations express how the parts (the subcomponents) constitute the whole. Designing the subcomponents in a similar fashion, we obtain hierarchical components. Given the specifications of the subcomponents and the way in which the subcomponents constitute the component, we must be able to show that the whole component meets its specification. The specifications should not reflect the internal structures of the components: they must specify their net effects only.
Martin Rem

Design and Verification of Distributed Systems

Frontmatter

Proving Correctness of CSP Programs — A Tutorial

Abstract
A structured presentation of a proof system for CSP programs is given. The presentation is based on the approach of Apt, Francez and de Roever [AFR]. Its new aspects are the use of static analysis and of proofs from assumptions instead of proof outlines. Also, in contrast to [AFR] total correctness is studied.
Krzysztof R. Apt

Real Time Clocks Versus Virtual Clocks

Abstract
Symmetric distributed termination algorithms are systematically developed. Solution are first presented in an abstract setting of Dijkstra, Feijen and Van Gasteren [DFG] and then gradually transformed into solutions to the distributed termination problem of Francez [F]. The initially used global real time clock is eventually replaced by local virtual clocks. A dependence between the degree of clock synchronization and the efficiency of the solutions is indicated.
Krzysztof R. Apt, Jean-Luc Richier

The Image Construction in Computerized Axial Tomography (CAT)

Abstract
The purpose of computerized axial tomography is to approximate the distribution of the absorption density in a cross-section of a specimen probed by many X-rays in the plane of the cross-section. This approximation, which is a non-negative function on a circular domain, is called the “image” because it is usually displayed on a screen, brightness representing the function value.
Edsger W. Dijkstra

Derivation of a termination detection algorithm for distributed computations

Abstract
The purpose of this paper is twofold, viz. to present a new [0] algorithm for the detection of the termination of a distributed computation and to demonstrate how the algorithm can be derived in a number of steps.
Edsger W. Dijkstra, W. H. J. Feijen, A. J. M. van Gasteren

The Distributed Snapshot of K.M. Chandy and L. Lamport

Abstract
We consider a distributed system of the form of a strongly connected, finite, directed graph, of which each vertex is a machine and each edge a uni-directional first-in-first-out buffer of sufficient capacity. (Strongly connected means that there is a directed path from any vertex to any vertex.)
Edsger W. Dijkstra

A simple fix-point argument without the restriction to continuity

Abstract
In this text, the letters B, P, R, X, and Y stand for predicates on the state space of a program and square brackets are used as notation for universal quantification of the enclosed over the program variables. The letter S stands for a statement and DO for the repetitive construct do B → S od (see [3]). (End of Notation.)
Edsger W. Dijkstra, A. J. M. van Gasteren
Weitere Informationen