Abstract
The framework of this paper is the formal specification and proof of applications distributed on symmetric interconnection networks, e.g. the torus or the hypercube. The algorithms are distributed over the nodes of the networks and use well-identified communication primitives. Using the notion of Cayley graph, we model the networks and their communications in the inductive theorem prover Nqthm. Within this environment, we mechanically perform correctness verifications with a specific invariant oriented method. We illustrate our approach with the verification of two distributed algorithms implemented on the hypercube.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
S. B. Akers and B. Krishnamurthy. A Group Theoretic Model for Symmetric Interconnection Networks. IEEE Transactions on Computers, 38(4), 1989.
B.W. Arden and K.W. Tang. Representations and Routing of Cayley Graphs. IEEE Transactions on Communications, 39(11), November 1991.
J-C. Bermond, T. Kodate, and S. Perennes. Gossiping in Cayley Graphs by Packets. In Proceedings of Franco-Japanese conference Brest July 95, volume 1120 of Lectures Notes in Computer Science. Springer Verlag, 1996.
R. Boyer and J Moore. A Computational Logic Hand-book. Perspectives in Computing, Vol. 23. Academic Press, Inc., 1988.
R. Couturier and D. Méry. An experiment in parallelizing an application using formal methods. In CAV’98. LNCS 1427, Springer Verlag, 1998.
R. A. Gamboa. Mechanically Verifying the Correctness of the Fast Fourier Transform in ACL2. In Third International Workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA), 1998.
E. Gascard and L. Pierre. Two Approaches to the Formal Proof of Replicated Hardware Systems using the Boyer-Moore Theorem Prover. In Proc. International Workshop on First Order Theorem Provers (FTP’97), October 1997.
C. GowriSankaran. Broadcasting on Recursively Decomposable Cayley Graphs. Discrete Applied Mathematics, 53:171–182, 1994.
B. Hendrickson, R. Leland, and S. Plimpton. An Efficient Parallel Algorithm for Matrix-Vector Multiplication. Int. J. High Speed Computing, 7(1):73–88, 1995.
W. H. Hesselink. A mechanical proof of Segall’s PIF algorithm. Formal Aspects of Computing, 9:208–226, 1997.
D. Kapur and M. Subramaniam. Automated Reasoning about Parallel Algorithms using Powerlists. In Proc. Algebraic Methodology and Software Technology, AMAST’95, volume 936 of LNCS, pages 416–430. Springer-Verlag, 1995.
M. Kaufmann and J S. Moore. An Industrial Strength Theorem prover for a Logic Based on Common Lisp. IEEE Trans. on Software Engineering, 23(4), April 1997.
J. Kornerup. Mapping Powerlists onto Hypercubes. Technical Report TR-94-04, Department of Computer Sciences, University of Texas at Austin, 1994.
V. Kumar, A. Grama, A. Gupta, and G. Karypis. Intoduction to Parallel Computing: Design and Analysis of Algorithms. Benjamin Cummings Pub., 1994.
T.M. Kurç, C. Aykanet, and B. Özguç. A parallel scaled conjugate-gradient algorithm for the solution phase of gathering radiosity on hypercubes. The Visual Computer, 13(1):1–19, 1997.
Y. Lee, S. Horng, T. Kao, and Y. Chen. Parallel computation of the Euclidean distance transform on the mesh of trees and the hypercube computer. Computer Vision and Image Understanding, 68(1):109–119, October 1997.
J. Misra. Powerlist: A structure for parallel recursion. ACM Transactions on Programming Languages and Systems, 16(6):1737–1767, November 1994.
J S. Moore. A mechanically checked proof of a multiprocessor result via a uniprocessor view. Formal Methods in System Design, 14(2):213–228, 1999.
K. Qiu and S.G. Akl. Novel Data Communication Algorithms on Hypercubes and Related Interconnection Networks and Their Applications in Computational Geometry. Technical Report 97-415, Department of Computing and Information Science, Queen’s University, Kingston, Ontario, December 1997.
M. Snir, S. Otto, S. Huss-Lederman, D. Walker, and J. Dongarra. MPI: The Complete Reference. The MIT Press, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gascard, E., Pierre, L. (2001). Induction-Oriented Formal Verification in Symmetric Interconnection Networks. In: Margaria, T., Melham, T. (eds) Correct Hardware Design and Verification Methods. CHARME 2001. Lecture Notes in Computer Science, vol 2144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44798-9_32
Download citation
DOI: https://doi.org/10.1007/3-540-44798-9_32
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42541-0
Online ISBN: 978-3-540-44798-6
eBook Packages: Springer Book Archive