nach oben

International Journal of Parallel Programming

Erschienen in:

07.04.2016

Calculating Parallel Programs in Coq Using List Homomorphisms

verfasst von: Frédéric Loulergue, Wadoud Bousdira, Julien Tesson

Erschienen in: International Journal of Parallel Programming | Ausgabe 2/2017

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

SyDPaCC is a set of libraries for the Coq proof assistant. It allows to write naive functional programs (i.e. with high complexity) that are considered as specifications, and to transform them into more efficient versions. These more efficient versions can then be automatically parallelised before being extracted from Coq into source code for the functional language OCaml together with calls to the Bulk Synchronous Parallel ML library. In this paper we present a new core version of SyDPaCC for the development of parallel programs correct-by-construction using the theory of list homomorphisms and algorithmic skeletons implemented and verified in Coq. The framework is illustrated on the maximum prefix sum problem.

Vorheriger Artikel Data Parallel Algorithmic Skeletons with Accelerator Support

Nächster Artikel Towards Systematic Parallelization of Graph Transformations Over Pregel

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

In Coq all the following commands are synonym: Fact, Lemma, Proposition, Theorem.

Actually A is implicit but making it explicit makes the explanation clearer.

http://traclifo.univ-orleans.fr/SyDPaCC, version core-0.2.

Aldinucci, M., Danelutto, M.: Skeleton-based parallel programming: functional and parallel semantics in a single shot. Comput. Lang. Syst. Str. 33(3–4), 179–192 (2007)MATH

Bird, R., de Moor, O.: Algebra of Programming. Prentice Hall, New Jersey (1996)CrossRefMATH

Bousdira, W., Loulergue, F., Tesson, J.: A verified library of algorithmic skeletons on evenly distributed arrays. In: Algorithms and Architectures for Parallel Processing (ICA3PP). pp. 218–232. No. 7439 in LNCS, Springer, Fukuoka, Japan (2012)

Cavarra, A., Riccobene, E., Zavanella, A.: A formal model for the parallel semantics of P3L. In: ACM Symposium on Applied Computing (SAC). pp. 804–812. ACM (2000)

Cole, M.: Parallel programming with list homomorphisms. Parallel Process. Lett. 5(2), 191–203 (1995)CrossRef

Daum, M.: Reasoning on data-parallel programs in Isabelle/Hol. In: C/C++ Verification Workshop (2007)

Emoto, K., Loulergue, F., Tesson, J.: A verified generate-test-aggregate Coq library for parallel programs extraction. In: Interactive Theorem Proving (ITP). pp. 258–274. No. 8558 in LNCS, Springer, Wien (2014)

Fortin, J., Gava, F.: BSP-Why: a tool for deductive verification of BSP algorithms with subgroup synchronisation. Int. J. Parallel Prog. (2015). doi:10.1007/s10766-015-0360-y

Gava, F.: Formal proofs of functional BSP programs. Parallel Process. Lett. 13(3), 365–376 (2003)MathSciNetCrossRef

10.

Gava, F., Gesbert, L., Loulergue, F.: Type system for a safe execution of parallel programs in BSML. In: 5th ACM SIGPLAN Workshop on High-Level Parallel Programming and Applications, pp. 27–34. ACM (2011)

11.

Gibbons, J.: The third homomorphism theorem. J. Funct. Program. 6(4), 657–665 (1996)MathSciNetCrossRefMATH

12.

Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRef

13.

Loulergue, F., Gava, F., Billiet, D.: Bulk synchronous parallel ML: modular implementation and performance prediction. In: International Conference on Computational Science (ICCS). LNCS, vol. 3515, pp. 1046–1054. Springer, Berlin (2005)

14.

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 (2014)

15.

Lupinski, N., Falcou, J., Paulin-Mohring, C.: Sémantique d’une langage de squelettes. http://www.lri.fr/~paulin/Skel/article (2012)

16.

Malecha, G., Morrisett, G., Wisnesky, R.: Trace-based verification of imperative programs with I/O. J. Symb. Comput. 46(2), 95–118 (2011)MathSciNetCrossRefMATH

17.

Mu, S.C., Ko, H.S., Jansson, P.: Algebra of programming using dependent types. In: Audebaud, P., Paulin-Mohring, C. (eds.) Mathematics of Program Construction, LNCS, vol. 5133, pp. 268–283. Springer, Berlin (2008)CrossRef

18.

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)MathSciNetCrossRefMATH

19.

Stewart, A., Clint, M., Gabarró, J.: Barrier synchronisation: axiomatisation and relaxation. Form. Asp. Comput. 16(1), 36–50 (2004)CrossRefMATH

20.

Swierstra, W.: More dependent types for distributed arrays. High. Order Symb. Comput. 23(4), 489–506 (2010)MathSciNetCrossRefMATH

21.

Tesson, J., Loulergue, F.: A verified bulk synchronous parallel ML heat diffusion simulation. In: International Conference on Computational Science (ICCS). pp. 36–45. Elsevier, Singapore (2011)

22.

The Coq Development Team: The Coq Proof Assistant. http://coq.inria.fr

23.

Valiant, L.G.: A bridging model for parallel computation. Commun. ACM 33(8), 103 (1990)CrossRef

24.

Wildmoser, M., Nipkow, T.: Certifying machine code safety: shallow versus deep embedding. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) Theorem Proving in Higher Order Logics, LNCS, vol. 3223, pp. 133–142. Springer, Berlin (2004)

25.

Yokoyama, T., Hu, Z., Takeichi, M.: Yicho: a system for programming program calculations. Technical Report METR 2002–07, Department of Mathematical Engineering, University of Tokyo (Jun 2002)

26.

Zhou, J., Chen, Y.: Generating C code from LOGS specifications. In: 2nd International Colloquium on Theoretical Aspects of Computing (ICTAC’05). pp. 195–210. No. 3407 in LNCS, Springer, Berlin (2005)

Titel: Calculating Parallel Programs in Coq Using List Homomorphisms
verfasst von: Frédéric Loulergue
Wadoud Bousdira
Julien Tesson
Publikationsdatum: 07.04.2016
Verlag: Springer US
Erschienen in: International Journal of Parallel Programming / Ausgabe 2/2017
Print ISSN: 0885-7458
Elektronische ISSN: 1573-7640
DOI: https://doi.org/10.1007/s10766-016-0415-8

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 2/2017

Multi-ML: Programming Multi-BSP Algorithms in ML

Tackling Complexity in High Performance Computing Applications

Parallel Patterns for Window-Based Stateful Operators on Data Streams: An Algorithmic Skeleton Approach

Towards Systematic Parallelization of Graph Transformations Over Pregel

Data Parallel Algorithmic Skeletons with Accelerator Support

Autonomic Coordination of Skeleton-Based Applications Over CPU/GPU Multi-Core Architectures