Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Verified High Performance Computing: The SyDPaCC Approach

  • Conference paper
  • First Online:
Verification and Evaluation of Computer and Communication Systems (VECoS 2023)

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

  • 134 Accesses

Abstract

The SyDPaCC framework for the Coq proof assistant is based on a transformational approach to develop verified efficient scalable parallel functional programs from specifications. These specifications are written as inefficient (potentially with a high computational complexity) sequential programs. We obtain efficient parallel programs implemented using algorithmic skeletons that are higher-order functions implemented in parallel on distributed data structures. The output programs are constructed step-by-step by applying transformation theorems. Leveraging Coq type classes, the application of transformation theorems is partly automated. The current version of the framework is presented and exemplified on the development of a parallel program for the maximum segment sum problem. This program is experimented on a parallel machine.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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 EPUB and 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

Similar content being viewed by others

Notes

  1. 1.

    The type annotations have been added manually and the argument renamed to increase readability.

References

  1. Armbrust, M., et al.: Scaling spark in the real world: performance and usability. PVLDB 8(12), 1840–1851 (2015). http://www.vldb.org/pvldb/vol8/p1840-armbrust.pdf

  2. Bertot, Y.: Coq in a hurry (2006). http://hal.inria.fr/inria-00001173

  3. Bird, R.: An introduction to the theory of lists. In: Broy, M. (ed.) Logic of Programming and Calculi of Discrete Design. NATO ASI Series, vol. 36, pp. 5–42. Springer, Heidelberg (1987). https://doi.org/10.1007/978-3-642-87374-4_1

    Chapter  Google Scholar 

  4. Cao, L.: Data science: a comprehensive overview. ACM Comput. Surv. 50(3), 1–42 (2017). https://doi.org/10.1145/3076253

    Article  Google Scholar 

  5. Chen, Y.-F., Hong, C.-D., Lengál, O., Mu, S.-C., Sinha, N., Wang, B.-Y.: An executable sequential specification for spark aggregation. In: El Abbadi, A., Garbinato, B. (eds.) NETYS 2017. LNCS, vol. 10299, pp. 421–438. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-59647-1_31

    Chapter  Google Scholar 

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

    Google Scholar 

  7. Cole, M.: Parallel programming, list homomorphisms and the maximum segment sum problem. In: Joubert, G.R., Trystram, D., Peters, F.J., Evans, D.J. (eds.) Parallel Computing: Trends and Applications, PARCO 1993, pp. 489–492. Elsevier (1994)

    Google Scholar 

  8. Daum, M.: Reasoning on Data-Parallel Programs in Isabelle/Hol. In: C/C++ Verification Workshop (2007). http://www.cse.unsw.edu.au/rhuuck/CV07/program.html

  9. Dean, J., Ghemawat, S.: MapReduce: simplified data processing on large clusters. In: OSDI, pp. 137–150. USENIX Association (2004)

    Google Scholar 

  10. Dosch, W., Wiedemann, B.: List homomorphisms with accumulation and indexing. In: Michaelson, G., Trinder, P., Loidl, H.W. (eds.) Trends in Functional Programming, pp. 134–142. Intellect (2000)

    Google Scholar 

  11. Emoto, K., Fischer, S., Hu, Z.: Filter-embedding semiring fusion for programming with MapReduce. Formal Aspects Comput. 24(4–6), 623–645 (2012). https://doi.org/10.1007/s00165-012-0241-8

    Article  MathSciNet  Google Scholar 

  12. Emoto, K., Loulergue, F., Tesson, J.: A verified generate-test-aggregate Coq library for parallel programs extraction. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 258–274. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08970-6_17

    Chapter  Google Scholar 

  13. Fang, R., Pouyanfar, S., Yang, Y., Chen, S.C., Iyengar, S.S.: Computational health informatics in the big data age: a survey. ACM Comput. Surv. 49(1), 1–36 (2016). https://doi.org/10.1145/2932707

    Article  Google Scholar 

  14. Filliâtre, J.-C., Marché, C.: The why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73368-3_21

    Chapter  Google Scholar 

  15. Gava, F., Fortin, J., Guedj, M.: Deductive verification of state-space algorithms. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 124–138. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38613-8_9

    Chapter  Google Scholar 

  16. Gesbert, L., Hu, Z., Loulergue, F., Matsuzaki, K., Tesson, J.: Systematic development of correct bulk synchronous parallel programs. In: Parallel and Distributed Computing, Applications and Technologies (PDCAT), pp. 334–340. IEEE (2010). https://doi.org/10.1109/PDCAT.2010.86

  17. Gibbons, J.: The third homomorphism theorem. J. Funct. Program. 6(4), 657–665 (1996). https://doi.org/10.1017/S0956796800001908

    Article  MathSciNet  Google Scholar 

  18. Gorlatch, S., Bischof, H.: Formal derivation of divide-and-conquer programs: a case study in the multidimensional FFT’s. In: Mery, D. (ed.) Formal Methods for Parallel Programming: Theory and Applications, pp. 80–94 (1997)

    Google Scholar 

  19. Hill, J.M.D., et al.: BSPlib: the BSP programming library. Parallel Comput. 24, 1947–1980 (1998)

    Article  Google Scholar 

  20. Hu, Z., Iwasaki, H., Takeichi, M.: Construction of list homomorphisms by tupling and fusion. In: Penczek, W., Szałas, A. (eds.) MFCS 1996. LNCS, vol. 1113, pp. 407–418. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61550-4_166

    Chapter  Google Scholar 

  21. Hu, Z., Takeichi, M., Iwasaki, H.: Diffusion: calculating efficient parallel programs. In: ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM 1999), pp. 85–94. ACM (1999)

    Google Scholar 

  22. Hu, Z., Iwasaki, H., Takeichi, M.: Formal derivation of efficient parallel programs by construction of list homomorphisms. ACM Trans. Program. Lang. Syst. 19(3), 444–461 (1997). https://doi.org/10.1145/256167.256201

    Article  Google Scholar 

  23. Lämmel, R.: Google’s MapReduce programming model - revisited. Sci. Comput. Program. 70(1), 1–30 (2008). https://doi.org/10.1016/j.scico.2007.07.001

    Article  MathSciNet  Google Scholar 

  24. Leroy, X., Doligez, D., Frisch, A., Garrigue, J., Rémy, D., Vouillon, J.: The OCaml system release 5.00 (2022). https://v2.ocaml.org/manual/

  25. Letouzey, P.: Extraction in Coq: an overview. In: Beckmann, A., Dimitracopoulos, C., Löwe, B. (eds.) CiE 2008. LNCS, vol. 5028, pp. 359–369. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-69407-6_39

    Chapter  Google Scholar 

  26. Loulergue, F.: A BSPlib-style API for bulk synchronous parallel ML. Scalable Comput. Pract. Experience 18, 261–274 (2017). https://doi.org/10.12694/scpe.v18i3.1306

    Article  Google Scholar 

  27. Loulergue, F.: A verified accumulate algorithmic skeleton. In: Fifth International Symposium on Computing and Networking (CANDAR), pp. 420–426. IEEE, Aomori, Japan (2017). https://doi.org/10.1109/CANDAR.2017.108

  28. Loulergue, F., Bousdira, W., Tesson, J.: Calculating parallel programs in Coq using list homomorphisms. Int. J. Parallel Prog. 45(2), 300–319 (2016). https://doi.org/10.1007/s10766-016-0415-8

    Article  Google Scholar 

  29. 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.J. (eds.) ICCS 2005. LNCS, vol. 3515, pp. 1046–1054. Springer, Heidelberg (2005). https://doi.org/10.1007/11428848_132

    Chapter  Google Scholar 

  30. Loulergue, F., Philippe, J.: Towards verified scalable parallel computing with Coq and Spark. In: Proceedings of the 25th ACM International Workshop on Formal Techniques for Java-like Programs (FTfJP), pp. 11–17. ACM, New York, NY, USA (2023). https://doi.org/10.1145/3605156.3606450

  31. Loulergue, F., Robillard, S., Tesson, J., Légaux, J., Hu, Z.: Formal derivation and extraction of a parallel program for the all nearest smaller values problem. In: ACM Symposium on Applied Computing (SAC), pp. 1577–1584. ACM, Gyeongju, Korea (2014). https://doi.org/10.1145/2554850.2554912

  32. Malewicz, G., et al.: Pregel: a system for large-scale graph processing. In: SIGMOD, pp. 135–146. ACM (2010). https://doi.org/10.1145/1807167.1807184

  33. Matsuzaki, K.: Functional models of hadoop mapreduce with application to scan. Int. J. Parallel Prog. 45(2), 362–381 (2016). https://doi.org/10.1007/s10766-016-0414-9

    Article  Google Scholar 

  34. Minsky, Y.: OCaml for the masses. Commun. ACM 54(11), 53–58 (2011). https://doi.org/10.1145/2018396.2018413

    Article  Google Scholar 

  35. Morihata, A., Matsuzaki, K., Hu, Z., Takeichi, M.: The third homomorphism theorem on trees: downward & upward lead to divide-and-conquer. In: Shao, Z., Pierce, B.C. (eds.) POPL 2009, pp. 177–185. ACM (2009). https://doi.org/10.1145/1480881.1480905

  36. Morihata, A.: Calculational developments of new parallel algorithms for size-constrained maximum-sum segment problems. In: Schrijvers, T., Thiemann, P. (eds.) FLOPS 2012. LNCS, vol. 7294, pp. 213–227. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29822-6_18

    Chapter  Google Scholar 

  37. Mu, S., Ko, H., Jansson, P.: Algebra of programming in Agda: dependent types for relational program derivation. J. Funct. Program. 19(5), 545–579 (2009). https://doi.org/10.1017/S0956796809007345

    Article  MathSciNet  Google Scholar 

  38. Odersky, M., Spoon, L., Venners, B.: Programming in Scala, 2nd edn. Artima, Walnut Creek (2010)

    Google Scholar 

  39. Ono, K., Hirai, Y., Tanabe, Y., Noda, N., Hagiya, M.: Using Coq in specification and program extraction of hadoop mapreduce applications. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 350–365. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24690-6_24

    Chapter  Google Scholar 

  40. Skillicorn, D.B., Hill, J.M.D., McColl, W.F.: Questions and answers about BSP. Sci. Program. 6(3), 249–274 (1997)

    Google Scholar 

  41. Smith, D.R.: Applications of a strategy for designing divide-and-conquer algorithms. Sci. Comput. Program. 8(3), 213–229 (1987). https://doi.org/10.1016/0167-6423(87)90034-7

    Article  MathSciNet  Google Scholar 

  42. Snir, M., Gropp, W.: MPI the Complete Reference. MIT Press, Cambridge (1998)

    Google Scholar 

  43. Swierstra, W.: More dependent types for distributed arrays. Higher-Order Symbolic Comput. 23(4), 489–506 (2010). https://doi.org/10.1007/s10990-011-9075-y

    Article  MathSciNet  Google Scholar 

  44. Valiant, L.G.: A bridging model for parallel computation. Commun. ACM 33(8), 103 (1990). https://doi.org/10.1145/79173.79181

    Article  Google Scholar 

Download references

Acknowledgments

We wish to thank the reviewers for their suggestions and highlighting some typos.

Author information

Authors and Affiliations

  1. Univ. Orléans, INSA CVL, LIFO EA 4022, Orléans, France

    Frédéric Loulergue & Ali Ed-Dbali

Authors
  1. Frédéric Loulergue
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ali Ed-Dbali
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Frédéric Loulergue .

Editor information

Editors and Affiliations

  1. CEA LIST, Gif-sur-Yvette, France

    Belgacem Ben Hedia

  2. Université Sultan Moulay Slimane, Beni Mellal, Morocco

    Yassine Maleh

  3. Al-Baha University, Al Baha, Saudi Arabia

    Moez Krichen

Rights and permissions

Reprints and permissions

Copyright information

© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Loulergue, F., Ed-Dbali, A. (2024). Verified High Performance Computing: The SyDPaCC Approach. In: Ben Hedia, B., Maleh, Y., Krichen, M. (eds) Verification and Evaluation of Computer and Communication Systems. VECoS 2023. Lecture Notes in Computer Science, vol 14368. Springer, Cham. https://doi.org/10.1007/978-3-031-49737-7_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-49737-7_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-49736-0

  • Online ISBN: 978-3-031-49737-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation