Utilisation des méthodes formelles pour le développement de programmes parallèles - Université de Lorraine Access content directly
Theses Year : 2000

Utilisation des méthodes formelles pour le développement de programmes parallèles

Abstract

The goalofthework described in this thesis is to study how formaI methods can be applied to the parallelization of sequentialprograms. The use offormal methods helps to ensure that parallelization is correct. One of our objectives being towork on real applications,we havecollaborated with physicists and chemists of our University to parallelize three of their simulations. These applications have been parallelized on the Origin 2000at the Charles Hermite Centre, using either OpenMP, or MPI, or both.To prove that domain decompositiop based parallelization is correct, we have developed a method that requires the user ta make an abstraction of his/her sequentialcode in order to obtaLu a postcondition. We must then generalize. it for the parallel code. Consequently, we must prove that the postconditions of theparallelcode together with the postcondition of the code glueing
Le travail décrit dans cette thèse a pour but d'étudier comment on peut appliquer les méthodes formelles à la parallélisassions, pour développer des programmes parallèles corrects. Comme un de nos objectifs est de travailler sur des applications en grandeur nature, nous avons, durant ce travail, collaboré avec des physiciens et chimistes de notre université afin de paralléliser trois de leurs applications. Ces applications ont été parallélisées, sur l'origin 2000 du centre Charles Hermite, soit avec openmp, soit avec mpi, soit avec ces deux paradigmes à la fois. Afin de prouver qu'une parallèlisation basée sur une décomposition de domaines est correcte, nous avons développé une méthodologie adéquate qui demande à l'utilisateur d'abstraire son code séquentiel afin d'en obtenir une post-condition. Celle-ci nécessite d'être généralisée pour le code parallèle. Ensuite, on doit prouver que les post-conditions du code parallèle, plus la post-condition du code réalisant le collage des informations obtenues en parallèle, impliquent la post-condition du programme séquentiel. Si on ne spécifie pas la post-condition du code réalisant le collage, la preuve échoue, mais les obligations de preuves constituent la post-condition du code d'assemblage des calculs parallèles. Nous avons appliqué cette méthodologie à deux des parallelisations que nous avons effectuées. Pour montrer que l'on peut élaborer un programme à partir d'une spécification formelle et en faire la preuve, nous avons prouvé que le tri bitonique, facilement parallelisable, est correct en utilisant pvs. Nous avons également construit un compilateur qui permet de transformer une spécification unity d'un programme parallèle déterministe en un programme fortran que l'on peut exécuter sur une machine avec openmp.
Fichier principal
Vignette du fichier
SCD_T_2000_0001_COUTURIER.pdf (9.14 Mo) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

tel-01747537 , version 1 (29-03-2018)

Identifiers

  • HAL Id : tel-01747537 , version 1

Cite

Raphaël Couturier. Utilisation des méthodes formelles pour le développement de programmes parallèles. Informatique [cs]. Université Henri Poincaré - Nancy 1, 2000. Français. ⟨NNT : 2000NAN10001⟩. ⟨tel-01747537⟩
72 View
475 Download

Share

Gmail Facebook X LinkedIn More