L'Université d'Orléans

Contenu de la page principale

Offre de formation

Travailler à l'Université d'Orléans

Agenda

20
ENE.
Zoom sur
Ecole d'hiver à l'UO pour 30 étudiants chinois de BIT
L’Université d’Orléans a accueilli 30 étudiants ainsi que 3 accompagnateurs chinois de Beijing Institute of Technology pour une Winter School qui s’est déroulée du 20 janvier au 2 février 2019.
29
ABR.
Etudiants
Césure : candidature 2019-2020
Organisateurs: Direction de l'Orientation et de l'Insertion Professionnelle - DOIP Vous disposez jusqu'au 18 octobre prochain pour déposer votre dossier de candidature à un projet
28
MAYO.
Evénements
Coopération avec l'Université de Yangzhou, Chine
L'Université d'Orléans intensifie sa coopération avec l'Université de Yangzhou
18
JUN.
Evénements
Formation doctorale "Éthique et Intégrité scientifique"
Les écoles doctorales de l'Université d'Orléans organisent une formation intitulée "Éthique et Intégrité scientifique".
20
JUN.
Soutenances
Soutenance de l’Habilitation à Diriger des Recherches de Fateh BELAID
En dépit des efforts déployés par les économistes ces dernières décennies, les politiques publiques ont besoin d’éclairages complémentaires leur permettant d’implémenter les instruments les plus
28
JUN.
Soutenances
Soutenance de thèse de Filip Arvid JAKOBSSON
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.

View all news