Abstract
We prove the completeness of an assertional proof system for a simple loop-free data-parallel language. This proof system is based on two-part assertions, where the predicate on the current value of variables is separated from the specification of the current extent of parallelism. The proof is based on a Weakest Precondition (WP) calculus. In contrast with the case of usual scalar languages, not all WP can be defined by an assertion. Yet, partial definability suffices to prove the completeness thanks to the introduction of hidden variables in assertions. The case of data-parallel programs with loops is briefly discussed in the conclusion.
The full version of this paper can be found in [2].
This work has been partly supported by the French CNRS Research Program on Parallelism, Networks and Systems(PRS).
Chapter PDF
Keywords
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é and D. Cachera. On the completeness of a proof system for a simple dataparallel programming language. Research Report 94-42, LIP ENS Lyon, France, December 1994. Available at URL ftp://ftp.lip.ens-lyon.fr/pub/Rapports/ RR/RR94/RR94-42.ps.Z.
L. Bougé, Y. Le Guyadec, G. Utard, and B. Virot. On the expressivity of a weakest preconditions calculus for a simple data-parallel programming language. In ConPar'94-VAPP VI, Linz, Austria, September 1994.
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 Applications in Parallel and Distributed Computing, Caracas, Venezuela, April 1994. IFIP WG 10.3, 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.
M. Clint and K.T. Narayana. On the completeness of a proof system for a synchronous parallel programming langage. In Third Conf. Found. Softw. Techn. and Theor. Comp. Science, Bangalore, India, December 1983.
E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.
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.
C.A.R. Hoare. An axiomatic basis for computer programming. Comm of the ACM, 12:576–580, 1969.
A. Stewart. An axiomatic treatment of SIMD assignment. BIT, 30:70–82, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bougé, L., Cachera, D. (1995). On the completeness of a proof system for a simple data-parallel programming language (extended abstract). In: Haridi, S., Ali, K., Magnusson, P. (eds) EURO-PAR '95 Parallel Processing. Euro-Par 1995. Lecture Notes in Computer Science, vol 966. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0020461
Download citation
DOI: https://doi.org/10.1007/BFb0020461
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60247-7
Online ISBN: 978-3-540-44769-6
eBook Packages: Springer Book Archive