Article

Free access

From sequential layers to distributed processes: deriving a distributed minimum weight spanning tree algorithm

Authors:

Job ZwiersAuthors Info & Claims

PODC '92: Proceedings of the eleventh annual ACM symposium on Principles of distributed computing

Pages 215 - 227

https://doi.org/10.1145/135419.135461

Published: 01 October 1992 Publication History

Abstract

Analysis and design of distributed algorithms and protocols are difficult issues. An important cause for those difficulties is the fact that the logical structure of the solution is often invisible in the actual implementation. We introduce a framework that allows for a formal treatment of the design process, from an abstract initial design to an implementation tailored to specific architectures. A combination of algebraic and axiomatic techniques is used to verify correctness of the derivation steps. This is shown by deriving an implementation of a distributed minimum weight spanning tree algorithm in the style of [GHS].

References

[1]

K.R. Apt, E.-R. Olderog, Verification of sequential and concurrent programs, Springer, 1991.

Digital Library

[2]

P.A. Bernstein, V. Hadzilacos and N. Goodman, Concurrency Control and Recovery in Database Systems, Addison-Wesley, 1987.

Digital Library

[3]

O. Boruvka, O jist~m probl~mu minimgfinfm, Prdca Moravsk~ P~rodovgdeck~ Spole~nosti, 3, 1926. (In Czech.)

[4]

C. Chou and E. Ga~ni, Understanding and Verifying Distributed Algorithms Using Stratified Decomposition, Proc. of the 7th Annual Syrup. on Principles of Distributed Computing, 1988.

Digital Library

[5]

K.M. Chandy and J. Misra, Parallel Program Design: A Foundation, Addison-Wesley, 1988.

Digital Library

[6]

F. Critian, H. Aghili, R. Strong, D. Dolev, Atomic Broadcast: From Simple Message Diffusion to Byzantine Agreement, Proceedings 15th International Symposium on Fault- Tolerant Computing, 1985.

[7]

E. Dijkstra, Two Problems in Connection with Graphs, Numer. Math., Vol. 1, pp. 269-271, 1959.

Digital Library

[8]

T. Elrad and N. Francez, Decomposition of distributed programs into communication closed layers, Science of Computer Programming 2, 1982.

[9]

R.T. Gallager, P.A. Humblet and P.M. Spira, A distributed algorithm for minimum-weight spanning trees, A CM TOPLA$ 5-1, 1983.

Digital Library

[10]

W. Janssen, M. Poel and J. Zwiers, Action Systems and Action Refinement in the Development of Parallel Systems, an Algebraic Approach, proceedings CONCUR '91, Springer LNCS 527, 1991.

Digital Library

[11]

W. Janssen and J. Zwiers, Protocol Design by Layered Decomposition, A compositional approach, Pvoc. Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 571, 1992.

Digital Library

[12]

W. Janssen and J. Zwiers, From Sequential Layers to Distributed Processes: Deriving a Distributed Minimum Weight Spanning Tree Algorithm, Memoranda Informatica, University of Twente, 1992.

Digital Library

[13]

S. Katz and D. Peled, Verification of Distributed Programs using Representative Interleaving Sequences, to appear in: Distributed Computing.

Digital Library

[14]

J. Kruskal, On the shortest spanning subtree of a graph and the traveling salesman problem, in: Proc. of the American Mathematical Society, VoI. 7, pp. 48-50, 1956.

[15]

L. Lamport, The Hoare Logic of concurrent programs, Acta Informatica 1J, 1980.

[16]

Z. Manna, A. Pnueli, Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs, Science of Computer Programming j, 1984.

Digital Library

[17]

S. Owicki and D. Cries, An axiomatic proof technique for parallel programs, Acta Informatica 6, 1976.

[18]

V. Pratt, Modelling Concurrency with Partial orders, International Journal of Parallel Programming 15, 1986, pp. 33-71.

Digital Library

[19]

R. Prim, Shortest connection networks and some generalizations, Bell $yst. Tech. Journal, Vol. 36, pp. 1389-1401, 1957.

[20]

M. Poel and J. Zwiers, Layering Techniques for the Development of Parallel Systems, An Algebraic Approach, to appear in: Proc. Computer Aided Verification, 1992.

Digital Library

[21]

J.C. Reynolds, The Craft of Programming, Prentice Hall, 1981.

Digital Library

[22]

F.A. Stomp and W.P. de Roever, Designing distributed algorithms by means of formal sequentially phased reasoning, Proc. of the 3rd International Workshop on Distributed Algorithms, Nice, LNCS 392, Eds. J.-C. Bermond and M. Raynal, 1989, pp. 242-253.

Digital Library

[23]

F.A. Stomp, A derivation of a broadcasting protocol using sequentially phased reasoning, in: Stepwize Refinement of Distributed Systems, J.W. de Bakker et al. (Eds), Springer LNCS 430, 1989.

Digital Library

[24]

R.E. Tarjan, Data Structures and Network Algorithms, Society for Industrial and Apllied Mathematics, 1983.

Digital Library

[25]

J.L. Welch, L. Lamport, N. Lynch, A Lattice- Structured Proof Technique Applied to a Minimum Weight Spanning Tree Algorithm, Proc. of the 7th Annual Syrup. on Principle8 of Distributed Computing, 1988.

Digital Library

[26]

J. Zwiers, Layering and Action Refinement for Timed Systems, in: Proc. REX Workshop on Real Time: Theory in Practice, Springer Lecture Notes in Computer Science, 1992.

Digital Library

Cited By

Sharma AKatoen J(2014)Layered Reduction for Abstract Probabilistic AutomataProceedings of the 2014 14th International Conference on Application of Concurrency to System Design10.1109/ACSD.2014.10(21-31)Online publication date: 23-Jun-2014
https://dl.acm.org/doi/10.1109/ACSD.2014.10
Swaminathan MKatoen JOlderog E(2012)Layered reasoning for randomized distributed algorithmsFormal Aspects of Computing10.1007/s00165-012-0231-x24:4-6(477-496)Online publication date: 29-Jun-2012
https://doi.org/10.1007/s00165-012-0231-x
Engelhardt KMoses Y(2009)Causing communication closureDistributed Computing10.1007/s00446-009-0081-922:2(73-91)Online publication date: 1-Oct-2009
https://dl.acm.org/doi/10.1007/s00446-009-0081-9
Show More Cited By

Index Terms

From sequential layers to distributed processes: deriving a distributed minimum weight spanning tree algorithm
1. Mathematics of computing
  1. Discrete mathematics
    1. Graph theory
      1. Trees
2. Theory of computation
  1. Models of computation
    1. Concurrency
      1. Parallel computing models
  2. Randomness, geometry and discrete structures

Recommendations

Upward drawings of trees on the minimum number of layers
WALCOM'08: Proceedings of the 2nd international conference on Algorithms and computation

In a planar straight-line drawing of a tree T on k layers, each vertex is placed on one of k horizontal lines called layers and each edge is drawn as a straight-line segment. A planar straight-line drawing of a rooted tree T on k layers is called an ...
Distributed Decision Trees
Structural, Syntactic, and Statistical Pattern Recognition
Abstract
In a budding tree, every node is part internal node and part leaf. This allows representing the tree in a continuous parameter space and training it with backpropagation, like a neural network. Unlike a traditional tree whose construction is ...
Distributed verification of minimum spanning trees

The problem of verifying a Minimum Spanning Tree (MST) was introduced by Tarjan in a sequential setting. Given a graph and a tree that spans it, the algorithm is required to check whether this tree is an MST. This paper investigates the problem in the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PODC '92: Proceedings of the eleventh annual ACM symposium on Principles of distributed computing

October 1992

304 pages

ISBN:0897914953

DOI:10.1145/135419

Chairman:
Norman C. Hutchinson
Univ. of British Columbia, Vancouver, B. C., Canada

Copyright © 1992 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 October 1992

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

PODC92

Sponsor:

PODC92: 11th Annual ACM Symposium in Principles of Distributed Computing

August 10 - 12, 1992

British Columbia, Vancouver, Canada

Acceptance Rates

Overall Acceptance Rate 740 of 2,477 submissions, 30%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
329
Total Downloads

Downloads (Last 12 months)51
Downloads (Last 6 weeks)9

Reflects downloads up to 14 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Sharma AKatoen J(2014)Layered Reduction for Abstract Probabilistic AutomataProceedings of the 2014 14th International Conference on Application of Concurrency to System Design10.1109/ACSD.2014.10(21-31)Online publication date: 23-Jun-2014
https://dl.acm.org/doi/10.1109/ACSD.2014.10
Swaminathan MKatoen JOlderog E(2012)Layered reasoning for randomized distributed algorithmsFormal Aspects of Computing10.1007/s00165-012-0231-x24:4-6(477-496)Online publication date: 29-Jun-2012
https://doi.org/10.1007/s00165-012-0231-x
Engelhardt KMoses Y(2009)Causing communication closureDistributed Computing10.1007/s00446-009-0081-922:2(73-91)Online publication date: 1-Oct-2009
https://dl.acm.org/doi/10.1007/s00446-009-0081-9
Elrad T(2009)Aspect Oriented Approach for Capturing and Verifying Distributed PropertiesLanguages: From Formal to Natural10.1007/978-3-642-01748-3_6(83-96)Online publication date: 22-May-2009
https://dl.acm.org/doi/10.1007/978-3-642-01748-3_6
Aaltonen TKatara MKurki-Suonio RMikkonen T(2006)On horizontal specification architectures and their aspect-oriented implementationsTransactions on Aspect-Oriented Software Development II10.5555/2172290.2172292(1-29)Online publication date: 1-Jan-2006
https://dl.acm.org/doi/10.5555/2172290.2172292
Aaltonen TKatara MKurki-Suonio RMikkonen T(2006)On Horizontal Specification Architectures and Their Aspect-Oriented ImplementationsTransactions on Aspect-Oriented Software Development II10.1007/11922827_1(1-29)Online publication date: 2006
https://doi.org/10.1007/11922827_1
Moses YShimony B(2006)A new proof of the GHS minimum spanning tree algorithmProceedings of the 20th international conference on Distributed Computing10.1007/11864219_9(120-135)Online publication date: 18-Sep-2006
https://dl.acm.org/doi/10.1007/11864219_9
Abdulla PJonsson BKindahl MPeled D(2005)A general approach to partial order reductions in symbolic verificationComputer Aided Verification10.1007/BFb0028760(379-390)Online publication date: 18-Jun-2005
https://doi.org/10.1007/BFb0028760
Siegel MStomp F(2005)Extending the limits of sequentially phased reasoningFoundation of Software Technology and Theoretical Computer Science10.1007/3-540-58715-2_141(402-413)Online publication date: 1-Jun-2005
https://doi.org/10.1007/3-540-58715-2_141
Janssen WPoel MZwiers JXu Q(2005)Layering of real-time distributed processesFormal Techniques in Real-Time and Fault-Tolerant Systems10.1007/3-540-58468-4_175(393-417)Online publication date: 8-Jun-2005
https://doi.org/10.1007/3-540-58468-4_175
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Figures

Tables

Media

View Table of Conten