Abstract
We present a proof system for a simple data parallel kernel language. This proof system is based on two-component assertions, where the current extent of parallelism is explicitly described. We define a weakest preconditions (WP) calculus and discuss the associated definability property. Thanks to this weakest preconditions calculus, we establish the completeness of the proof system. We finally discuss other approaches.
This work has been partly supported by the French CNRS Coordinated Research Program on Parallelism C 3/PRS, the French PRC/MRE Research Contract ParaDigme, Department of Defense DRET Contract 91/1180, and INRIA Project ReMaP.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
K.R. Apt and E.-R. Olderog. Verification of Sequential and Concurrent Programs. Text and Monographs in Computer Science. Springer Verlag, 1990.
L. Bougé, Y. Le Guyadec, G. Utard, and B. Virot. A proof system for a simple data-parallel programming language. In C. Girault, editor, Proc. of IFIP WG 10.3, Applications in Parallel and Distributed Computing, Caracas, Venezuela, April 1994. North-Holland.
L. Bougé and J.-L. Levaire. Control structures for data-parallel SIMD languages: semantics and implementation. Future Generation Computer Systems, 8:363–378, 1992.
L. Bougé. The Data Parallel Programming Model: A Semantic Perspective. In A. Darte and G.-R. Perrin, editors, Infra, Lecture Notes in Computer Science, chapter 1. Springer Verlag, 1996.
Luc Bougé and Gil Utard. Escape constructs in data-parallel languages: semantics and proof system. Technical Report 94–18, LIP, ENS Lyon, 1994.
D. Cachera. Two completeness results about a proof system for simple data-parallel language. Technical Report 95–29, LIP, ENS Lyon, 1995.
M. Clint and K.T. Narayana. On the completeness of a proof system for a synchronous parallel programming language. In Third Conf. Found. Softw. Techn. and Theor. Comp. Science, Bangalore, India, December 1983.
D. Cachera and G. Utard. Proving data-parallel programs: a unifying approach. Parallel Processing Letters, 1996. To appear.
J. Gabarró and R. Gavaldà. An approach to correctness of data-parallel algorithms. Journal of Parallel and Distributed Computing, 22(2):185–201, August 1994.
M.J.C. Gordon. Programming Language Theory and its Implementation. Prentice-Hall International, 1988.
Yann Le Guyadec and Bernard Virot. Sequential-like proofs of dataparallel programs. Parallel Processing Letters, 1996. To appear.
C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–583, October 1969.
W.D. Hillis and G.L. Steele Jr. Data-parallel algorithms. Communications of the ACM, 29(12):1170–1183, 1986.
Bjørn Lisper. Data Parallelism and Functional Programming. In A. Darte and G.-R. Perrin, editors, Infra, Lecture Notes in Computer Science, chapter 11. Springer Verlag, 1996.
MasPar Computer Corporation, Sunnyvale CA. MasPar Parallel Application Language Reference Manual, 1990.
S. Owicki and D. Gries. Verifying properties of parallel programs: an axiomatic approach. Communication of the ACM, 19(5):279–285, 1976.
N. Paris. HyperC specification document. Technical Report 93-1, HyperParallel Technologies, 1993.
R. H. Perrot. A language for array and vector processors. ACM Transactions on Programming Languages, 1(2):177–195, 1979.
A. Stewart. An axiomatic treatment of SIMD assignment. BIT, 30:70–82, 1990.
Thinking Machine Corporation, Cambridge MA. C * programming guide, 1990.
G. Utard. Semantics of data-parallel languages. Applications to validation and compilation. PhD thesis, cole Normale Supérieure de Lyon, 1995. In french.
Author information
Authors and Affiliations
Corresponding author
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Bougé, L., Cachera, D., Le Guyadec, Y., Utard, G., Virot, B. (1996). Formal validation of data parallel programs: Introducing the assertional approach. In: Perrin, GR., Darte, A. (eds) The Data Parallel Programming Model. Lecture Notes in Computer Science, vol 1132. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61736-1_51
Download citation
DOI: https://doi.org/10.1007/3-540-61736-1_51
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61736-5
Online ISBN: 978-3-540-70646-5
eBook Packages: Springer Book Archive