Skip to main content
SpringerLink
Log in

Formal validation of data parallel programs: Introducing the assertional approach

  • Chapter
  • First Online:
Book cover The Data Parallel Programming Model

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1132))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. K.R. Apt and E.-R. Olderog. Verification of Sequential and Concurrent Programs. Text and Monographs in Computer Science. Springer Verlag, 1990.

    Google Scholar 

  2. 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.

    Google Scholar 

  3. L. Bougé and J.-L. Levaire. Control structures for data-parallel SIMD languages: semantics and implementation. Future Generation Computer Systems, 8:363–378, 1992.

    Google Scholar 

  4. 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.

    Google Scholar 

  5. Luc Bougé and Gil Utard. Escape constructs in data-parallel languages: semantics and proof system. Technical Report 94–18, LIP, ENS Lyon, 1994.

    Google Scholar 

  6. D. Cachera. Two completeness results about a proof system for simple data-parallel language. Technical Report 95–29, LIP, ENS Lyon, 1995.

    Google Scholar 

  7. 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.

    Google Scholar 

  8. D. Cachera and G. Utard. Proving data-parallel programs: a unifying approach. Parallel Processing Letters, 1996. To appear.

    Google Scholar 

  9. 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.

    Google Scholar 

  10. M.J.C. Gordon. Programming Language Theory and its Implementation. Prentice-Hall International, 1988.

    Google Scholar 

  11. Yann Le Guyadec and Bernard Virot. Sequential-like proofs of dataparallel programs. Parallel Processing Letters, 1996. To appear.

    Google Scholar 

  12. C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–583, October 1969.

    Google Scholar 

  13. W.D. Hillis and G.L. Steele Jr. Data-parallel algorithms. Communications of the ACM, 29(12):1170–1183, 1986.

    Google Scholar 

  14. 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.

    Google Scholar 

  15. MasPar Computer Corporation, Sunnyvale CA. MasPar Parallel Application Language Reference Manual, 1990.

    Google Scholar 

  16. S. Owicki and D. Gries. Verifying properties of parallel programs: an axiomatic approach. Communication of the ACM, 19(5):279–285, 1976.

    Google Scholar 

  17. N. Paris. HyperC specification document. Technical Report 93-1, HyperParallel Technologies, 1993.

    Google Scholar 

  18. R. H. Perrot. A language for array and vector processors. ACM Transactions on Programming Languages, 1(2):177–195, 1979.

    Google Scholar 

  19. A. Stewart. An axiomatic treatment of SIMD assignment. BIT, 30:70–82, 1990.

    Google Scholar 

  20. Thinking Machine Corporation, Cambridge MA. C * programming guide, 1990.

    Google Scholar 

  21. G. Utard. Semantics of data-parallel languages. Applications to validation and compilation. PhD thesis, cole Normale Supérieure de Lyon, 1995. In french.

    Google Scholar 

Download references

Author information

Author notes

  1. Y. Le Guyadec

    Present address: VALORIA, 8 rue Montaigne, BP 1104, F-56014, Vannes, France

Authors and Affiliations

  1. LIP, ENS Lyon, 46 allée d'Italie, F-69364, Lyon cedex 07, France

    L. Bougé, D. Cachera & G. Utard

  2. LIFO, Université d'Orléans, 4 rue Léonard de Vinci, BP 6759, F-45067, Orléans cedex 2, France

    Y. Le Guyadec & B. Virot

Authors
  1. L. Bougé
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. D. Cachera
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Y. Le Guyadec
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. G. Utard
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. B. Virot
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Y. Le Guyadec .

Editor information

Guy-René Perrin Alain Darte

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation