Skip to main content
SpringerLink
Log in

Verification of a Heat Diffusion Simulation Written with Orléans Skeleton Library

  • Conference paper
Parallel Processing and Applied Mathematics (PPAM 2011)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7204))

  • 1701 Accesses

Abstract

Orléans Skeleton Library (OSL) provides a set of algorithmic skeletons as a C++ library on top of MPI. The parallel programming approach of OSL is a structured one, which eases the reasoning about the performance and correctness of the programs. In this paper we present the verification of a heat diffusion simulation program, written in OSL, using the Coq proof assistant. The specification used in proving the correctness is a discretisation of the heat equation.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aldinucci, M., Danelutto, M.: Skeleton-based parallel programming: Functional and parallel semantics in a single shot. Computer Languages, Systems and Structures 33(3-4), 179–192 (2007)

    Article  MATH  Google Scholar 

  2. Berthold, J., Dieterle, M., Lobachev, O., Loogen, R.: Parallel FFT with Eden Skeletons. In: Malyshkin, V. (ed.) PaCT 2009. LNCS, vol. 5698, pp. 73–83. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  3. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004)

    MATH  Google Scholar 

  4. Bird, R.S.: Lectures on constructive functional programming. In: Broy, M. (ed.) Constructive Methods in Computing Science. NATO ASI, vol. 55. Springer, Marktoberdorf (1989)

    Google Scholar 

  5. Bird, R., de Moor, O.: Algebras of Programming. Prentice Hall (1996)

    Google Scholar 

  6. Boldo, S.: Floats and Ropes: A Case Study for Formal Numerical Program Verification. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S.E., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 91–102. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  7. Boldo, S., Clément, F., Filliâtre, J.C., Mayero, M., Melquiond, G., Weis, P.: Formal Proof of a Wave Equation Resolution Scheme: The Method Error. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 147–162. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  8. Caromel, D., Henrio, L., Leyton, M.: Type safe algorithmic skeletons. In: 16th Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP 2008), pp. 45–53. IEEE Computer Society (2008)

    Google Scholar 

  9. Ciechanowicz, P., Poldner, M., Kuchen, H.: The Münster Skeleton Library Muesli – A Comprenhensive Overview. Tech. Rep. Working Paper No. 7, European Research Center for Information Systems, University of Münster, Germany (2009)

    Google Scholar 

  10. Cole, M.: Algorithmic Skeletons: Structured Management of Parallel Computation. MIT Press (1989)

    Google Scholar 

  11. Di Cosmo, R., Pelagatti, S., Li, Z.: A calculus for parallel computations over multidimensional dense arrays. Computer Language Structures and Systems 33(3-4), 82–110 (2007)

    Article  MATH  Google Scholar 

  12. Dijkstra, E.W.: Letters to the editor: goto statement considered harmful. Comm. of the ACM 11(3), 147–148 (1968)

    Article  MathSciNet  Google Scholar 

  13. Falcou, J., Sérot, J.: Formal Semantics Applied to the Implementation of a Skeleton-Based Parallel Programming Library. In: Bischof, C.H., Bücker, H.M., Gibbon, P., Joubert, G.R., Lippert, T., Mohr, B., Peters, F.J. (eds.) Parallel Computing: Architectures, Algorithms and Applications, ParCo 2007. Advances in Parallel Computing, vol. 15, pp. 243–252. IOS Press (2007)

    Google Scholar 

  14. Falcou, J., Sérot, J., Chateau, T., Lapresté, J.T.: Quaff: Efficient C++ Design for Parallel Skeletons. Parallel Computing 32, 604–615 (2006)

    Article  Google Scholar 

  15. Gesbert, L., Hu, Z., Loulergue, F., Matsuzaki, K., Tesson, J.: Systematic Development of Correct Bulk Synchronous Parallel Programs. In: The 11th International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT), pp. 334–340. IEEE Computer Society (2010)

    Google Scholar 

  16. González-Vélez, H., Leyton, M.: A survey of algorithmic skeleton frameworks: high-level structured parallel programming enablers. Software, Practrice & Experience 40(12), 1135–1160 (2010)

    Article  Google Scholar 

  17. Gorlatch, S.: Send-receive considered harmful: Myths and realities of message passing. ACM TOPLAS 26(1), 47–56 (2004)

    Article  Google Scholar 

  18. Hidalgo-Herrero, M., Ortega-Mallén, Y.: An Operational Semantics for the Parallel Language Eden. Parallel Processing Letters 12(2), 211–228 (2002)

    Article  Google Scholar 

  19. Hu, Z., Takeichi, M., Chin, W.N.: Parallelization in calculational forms. In: POPL 1998: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 316–328. ACM Press (1998)

    Google Scholar 

  20. Javed, N., Loulergue, F.: OSL: Optimized Bulk Synchronous Parallel Skeletons on Distributed Arrays. In: Dou, Y., Gruber, R., Joller, J.M. (eds.) APPT 2009. LNCS, vol. 5737, pp. 436–451. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  21. Javed, N., Loulergue, F.: A Formal Programming Model of Orléans Skeleton Library. In: Malyshkin, V. (ed.) PaCT 2011. LNCS, vol. 6873, pp. 40–52. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  22. Leroy, X.: A formally verified compiler back-end. Journal of Automated Reasoning 43(4), 363–446 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  23. Leyton, M., Henrio, L., Piquer, J.M.: Exceptions for Algorithmic Skeletons. In: D’Ambra, P., Guarracino, M., Talia, D. (eds.) Euro-Par 2010. LNCS, vol. 6272, pp. 14–25. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  24. Loulergue, F., Gava, F., Billiet, D.: Bulk Synchronous Parallel ML: Modular Implementation and Performance Prediction. In: Sunderam, V.S., van Albada, G.D., Sloot, P.M.A., Dongarra, J. (eds.) ICCS 2005, Part II. LNCS, vol. 3515, pp. 1046–1054. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  25. Matsuzaki, K., Iwasaki, H., Emoto, K., Hu, Z.: A Library of Constructive Skeletons for Sequential Style of Parallel Programming. In: InfoScale 2006: Proceedings of the 1st International Conference on Scalable Information Systems. ACM Press (2006)

    Google Scholar 

  26. Tesson, J., Loulergue, F.: A Verified Bulk Synchronous Parallel ML Heat Diffusion Simulation. In: 11th International Conference on Computational Science (ICCS 2011), pp. 36–45. Procedia Computer Science, Elsevier (2011)

    Google Scholar 

  27. Valiant, L.G.: A bridging model for parallel computation. Comm. of the ACM 33(8), 103 (1990)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LIFO, University of Orléans, France

    Noman Javed & Frédéric Loulergue

Authors
  1. Noman Javed
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Frédéric Loulergue
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Computer and Information Science, Czestochowa University of Technology, Dabrowskiego 69, 42-201, Czestochowa, Poland

    Roman Wyrzykowski  & Konrad Karczewski  & 

  2. Electrical Engineering and Computer Science Department, University of Tennessee, 1122 Volunteer Blvd, 37996-3450, Knoxville, TN, USA

    Jack Dongarra

  3. Department of Informatics and Mathematical Modeling, Technical University of Denmark, Richard Petersens Plads, Building 321, 2800, Kongens Lyngby, Denmark

    Jerzy Waśniewski

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Javed, N., Loulergue, F. (2012). Verification of a Heat Diffusion Simulation Written with Orléans Skeleton Library. In: Wyrzykowski, R., Dongarra, J., Karczewski, K., Waśniewski, J. (eds) Parallel Processing and Applied Mathematics. PPAM 2011. Lecture Notes in Computer Science, vol 7204. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31500-8_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-31500-8_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-31499-5

  • Online ISBN: 978-3-642-31500-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation