No Access

FORMAL PROOF OF APPLICATIONS DISTRIBUTED IN SYMMETRIC INTERCONNECTION NETWORKS

ERIC GASCARD

LIFO - Université d'Orléans, BP 6759, 45067 Orléans Cedex 2, France

Search for more papers by this author

and

LAURENCE PIERRE

I3S - Université de Nice, BP 121, 06903 Sophia Antipolis Cedex, France

Search for more papers by this author

https://doi.org/10.1142/S0129626403001094Cited by:1 (Source: Crossref)

Abstract

This paper focuses on the formal proof of parallel programs dedicated to distributed memory symmetric interconnection networks; communications are realized by message passing. We have developed a method to formally verify the computational correctness of this kind of application. Using the notion of Cayley graphs to model the networks in the Nqthm theorem prover, we have formally specified and mechanically proven correct a large set of collective communication primitives. Our compositional approach allows us to reuse these libraries of pre-proven procedures to validate complex application programs within Nqthm. This is illustrated by three examples.

Keywords:

References

S. B. Akers and B. Krishnamurthy, IEEE Transactions on Computers 38(4), (1989), DOI: 10.1109/12.21148. Google Scholar
B. W. Arden and K. W. Tang, IEEE Transactions on Communications 39(11), (1991), DOI: 10.1109/26.111428. Google Scholar
J.-C. Bermond , T. Kodate and S. Perennes , Gossiping in Cayley Graphs by Packets , Proceedings of Franco-Japanese conference Combinatorics and Computer Science , LNCS 1120 ( Springer-Verlag , 1996 ) . Google Scholar
R. Boyer and J. Moore , A Computational Logic Hand-book , Perspectives in Computing 23 ( Academic Press, Inc. , 1988 ) . Google Scholar
Kuo-Liang Chung, Pattern Recognition Letters 16, (1995). Google Scholar
R. Couturier , Formal Engineering of the Bitonic Sort using PVS , Proceedings 2nd. Irish Workshop on Formal Methods, IWFM'98 . Google Scholar
R. Couturier and D. Méry , An experiment in parallelizing an application using formal methods , CAV'98 , LNCS 1427 ( Springer Verlag , 1998 ) . Google Scholar
R. A. Gamboa , Mechanically Verifying the Correctness of the Fast Fourier Transform in ACL2 , Proc. FMPPTA'98 . Google Scholar
E. Gascard and L. Pierre , Induction-Oriented Formal Verification in Symmetric Interconnection Networks , Proc. CHARME'01 , LNCS 2144 ( Springer-Verlag , 2001 ) . Google Scholar
E. Gascard and L. Pierre , Mechanical Verification of Hypercube Algorithms , Proc. FMPPTA'02 ( IEEE Computer Society Press , 2002 ) . Google Scholar
C. GowriSankaran, Discrete Applied Mathematics 53, 171 (1994), DOI: 10.1016/0166-218X(94)90183-X. Crossref, Web of Science, Google Scholar
B. Hendrickson, R. Leland and S. Plimpton, Int. J. High Speed Computing 7(1), 73 (1995), DOI: 10.1142/S0129053395000051. Link, Web of Science, Google Scholar
W. H. Hesselink, Formal Aspects of Computing 9, 208 (1997), DOI: 10.1007/BF01211619. Crossref, Google Scholar
W. H. Hesselink, Formal Aspects of Computing 11, 44 (1999). Google Scholar
D. Kapur and M. Subramaniam, Automated Reasoning about Parallel Algorithms using Powerlists, Proc. Algebraic Methodology and Software Technology, AMAST'95, LNCS 936 (Springer-Verlag, 1995) pp. 416–430. Google Scholar
M. Kaufmann and J. S. Moore, IEEE Trans. on Software Engineering 23(4), (1997), DOI: 10.1109/32.588534. Google Scholar
J. Kornerup. On "An O(log N) algorithm to solve linear recurrences on hypercubes". Technical report, Univ. of Texas at Austin, Dept. of Computer Science, August 1994 . Google Scholar
V. Kumar et al. , Intoduction to Parallel Computing: Design and Analysis of Algorithms ( Benjamin Cummings Pub. , 1994 ) . Google Scholar
T. M. Kurç, C. Aykanet and B. Özguç, The Visual Computer 13(1), 1 (1997). Crossref, Web of Science, Google Scholar
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, Queen's University, Kingston, December 1997 . Google Scholar
S. Ranka and S. Sahni , Hypercube Algorithms for Image Processing and Pattern Recognition ( Springer , 1989 ) . Google Scholar
M. Snir et al. , MPI: The Complete Reference ( The MIT Press , 1996 ) . Google Scholar