Month: June 2019

[Jun. 2019] Phd Defense : Thibaut Tachon, June 28th 2019

La soutenance aura lieu le Vendredi 28 juin 2019 à 14h30 en salle Soutenance de Thèse (Salle 101), 1er Étage au Bâtiment S (Faculté Des Sciences), Orléans.

Résumé : 

Depuis la stagnation de la fréquence d’horloge des processeurs, l’accroissement de la puissance de calcul a dépendu entièrement de l’accroissement du nombre d’unités de calcul.

Plus que la difficulté algorithmique impliquée par l’écriture de tout programme séquentiel, la programmation parallèle demande au programmeur de gérer de nombreuses unités de calcul, incluant leurs tâches et leurs interactions.

Pour alléger le fardeau du programmeur, cette thèse propose deux approches différentes de génération automatique de code parallèle.

Le modèle parallèle isochrone BSP possède des propriétés intéressantes telles que son modèle de coût qui en font la cible de notre génération de code parallèle.

Les automates et expressions régulières sont souvent choisis pour modéliser les calculs séquentiels et leurs parallélisation devrait, à long terme, aboutir à de solide fondations pour la génération de code parallèle.

Pour notre approche principale, nous développons la théorie des automates BSP avec leur génération et déterminisation.

Cette théorie est utilisé dans une nouvelle méthode pour la recherche de motif à l’aide d’expressions régulières.

Notre autre approche propose un langage spécifique au domaine des réseaux de neurones où la composition fonctionnelle d’un petit nombre de primitives facilite le développement, la maintenance et la définition formelle du langage par rapport aux approches existantes.

Mots-clés :       Programmation parallèle, BSP, Génération de code, Automate, Expression régulière, Réseaux de neurones.

[Jun. 2019] Phd Defense: Arvid Jakobsson, June 28th 2019

 La soutenance aura lieu le Vendredi
28 juin 2019 à 10h en salle Soutenance de Thèse (Salle 101), 1er Etage
au Bâtiment S (Faculté Des Sciences), Orléans.
Résumé de la thèse :

La programmation parallèle consiste à utiliser des architectures à
multiples unités de traitement, de manière à ce que le temps de calcul
soit inversement proportionnel au nombre d'unités matérielles.  Le
modèle de BSP (Bulk Synchronous Parallel) permet de rendre le temps de
calcul prévisible.  BSPlib est une bibliothèque pour la programmation
BSP en langage C.  En BSPlib on entrelace des instructions de contrôle
de la structure parallèle globale, et des instructions locales pour
chaque unité de traitement.  Cela permet des optimisations fines de la
synchronisation, mais permet aussi l'écriture de programmes dont les
calculs locaux divergent et masquent ainsi l'évolution globale du
calcul BSP.

Toutefois, les programmes BSPlib réalistes sont syntaxiquement
alignés, une propriété qui garantit la convergence du flot de contrôle
parallèle.  Dans ce mémoire nous étudions les trois dimensions
principales des programmes BSPlib du point de vue de l'alignement
syntaxique: la synchronisation, le temps de calcul et la
communication.  D'abord nous présentons une analyse statique qui
identifie les instructions syntaxiquement alignées et les utilise pour
vérifier la sûreté de la synchronisation globale.  Cette analyse a été
implémentée en Frama-C et certifiée en Coq.  Ensuite nous utilisons
l'alignement syntaxique comme base d'une analyse statique du temps de
calcul.  Elle est fondée sur une analyse classique du coût pour les
programmes séquentiels.  Enfin nous définissons une condition
suffisante pour la sûreté de l'enregistrement des variables.
L'enregistrement en BSPlib permet la communication par accès aléatoire
à la mémoire distante (DRMA) mais est sujet à des erreurs de
programmation.  Notre développement technique est la base d'une future
analyse statique de ce mécanisme.

Mots clés : Programmation parallèle, Bulk Synchronous Parallelism,
SPMD, Analyse statique, Synchronisation, Analyse de coût,
Communication

===== English version =====

Dear all,

It is my pleasure to invite you to my Ph.D. defense titled
"Static Analysis for BSPlib Programs"
 
The defense will take place on Friday, June 28th 2019 at 10:00 AM (UTC+02:00) at

     Université d’Orléans, Salle Soutenance de Thèse (Salle 101), 1er
     Etage au Bâtiment S (Faculté Des Sciences), Rue de Chartres,
     45100 Orléans

You are also welcome to join us to a small cocktail in the afternoon
around 16:00-16:30, which will take place in 'Salle de réunion 3',
first floor of LIFO, Bâtiment IIIA Rue Léonard de Vinci B.P. 6759
F-45067 ORLEANS Cedex 2.


The committee will be composed of:
 KUCHEN, Herbert – Professor, WWU Münster
 BARTHOU, Denis – Professor, Université de Bordeaux
 BOUSDIRA-SEMMAR, Wadoud – Associate Professor, Université d’Orléans
 DABROWSKI, Frédéric – Associate Professor, Université d’Orléans
 HAINS, Gaétan  – Research-Engineer, Huawei Technologies
 SUIJLEN, Wijnand – Research-Engineer, Huawei Technologies
 LOULERGUE, Frédéric – Professor, Northern Arizona University et Université d’Orléans
 CHAILLOUX, Emmanuel – Professor, Sorbonne Université


Abstract: The goal of scalable parallel programming is to program
computer architectures composed of multiple processing units so that
increasing the number of processing units leads to an increase in
performance.  Bulk Synchronous Parallel (BSP) is a widely used model
for scalable parallel programming with predictable performance. BSPlib
is a library for BSP programming in C.  In BSPlib, parallel algorithms
are expressed by intermingling instructions that control the global
parallel structure, and instructions that express the local
computation of each processing unit. This lets the programmer
fine-tune synchronization, but also implement programs whose diverging
parallel control flow obscures the underlying BSP structure.  In
practice however, the majority of BSPlib program are textually
aligned, a property that ensures parallel control flow convergence.

We examine three core aspects of BSPlib programs through the lens of
textual alignment: synchronization, performance and communication.
First, we present a static analysis that identifies textually aligned
statements and use it to verify safe synchronization. This analysis
has been implemented in Frama-C and certified in Coq.  Second, we
exploit textual alignment to develop a static performance analysis for
BSPlib programs, based on classic cost analysis for sequential
programs.  Third, we develop a textual alignment-based sufficient
condition for safe registration.  Registration in BSPlib enables
communication by Direct Remote Memory Access but is error prone.  This
development forms the basis for a future static analysis of
registration.