Abstract
We present a weakest preconditions calculus à la Dijkstra for a small common kernel of existing data-parallel languages. We use two-part assertions, where the current extent of parallelism is specified by a separate boolean vector expression. Our main contribution is concerned with the conditioning construct where which modifies the current extent of parallelism. We prove that the weakest (strict) preconditions of a where block is definable by an assertion as soon as its body is. This is not the case with its weakest liberal preconditions. This sheds a new light on the deep semantic nature of the data-parallel conditioning construct.
This work has been partly supported by the French CNRS Coordinated Research Program on Concurrency, Communication and Cooperation C 3, and Department of Defense DRET contract 91/1180.
This is a preview of subscription content, log in via an institution to check access.
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. On the expressivity of a weakest precondition calculus for a simple data-parallel programming language (extended version). Technical report, LIFO: RR94-07, Université d'Orléans, and LIP: RR94-12, ENS Lyon, April 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 the IFIP WG10.3 Int. Conf. on Application in Parallel and Distributed Computing, Caracas, Vénézuela, April 1994. Elsevier.
L. Bougé and J.-L. Levaire. Control structures for data-parallel SIMD languages: semantics and implementation. FGCS, 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.
High Performance Fortran Forum. High Performance Fortran language specification (draft version). CITI/CRPC, Rice Univ., Houston, January 1993. Version 1.0 Draft.
J. Gabarró and R. Gavaldà. An approach to correctness of data parallel algorithms. Technical Report LSI-91-19, Univ. Politécnica de Catalunya, October 1991. To appear in Journ. of Parallel and Distr. Computing, 1994.
M.J.C. Gordon. Programming Language Theory and its Implementation. Int. Series in Comp. Sciences. Prentice Hall, 1988.
MasPar Computer Corporation, Sunnyvale CA. Maspar Parallel Application Language Reference Manual, 1990.
N. Paris. HyperC specification document. Technical Report 93-1, HyperParallel Technologie, 1993.
A. Stewart. An axiomatic treatment of SIMD assignment. Bit, 30:70–82, 1990.
Thinking Machine Corporation, Cambridge MA. C * programming guide, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bougé, L., Le Guyadec, Y., Utard, G., Virot, B. (1994). On the expressivity of a weakest precondition calculus for a simple data-parallel programming language (short version). In: Buchberger, B., Volkert, J. (eds) Parallel Processing: CONPAR 94 — VAPP VI. VAPP CONPAR 1994 1994. Lecture Notes in Computer Science, vol 854. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58430-7_10
Download citation
DOI: https://doi.org/10.1007/3-540-58430-7_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58430-8
Online ISBN: 978-3-540-48789-0
eBook Packages: Springer Book Archive