Groupe de Travail Compsys |
salle B2
Titre: Résolution d’équations de programmes
Christophe Alias, Compsys
Résumé:
Dans le monde physique, beaucoup de problèmes s’expriment par des contraintes équationnelles. Nous pensons qu’il en va de même en informatique, et nous proposons dans cet exposé d’étudier la notion d’"équations de programmes". Une équation de programme est la mise en équivalence d’un programme et d’un schéma de programme, c’est à dire un programme avec des variables libres d’ordre 1 (scalaire) ou 2 (fonction). Une solution est une valeur des variables libres qui rendent le schéma et le programme équivalents. La première étape est de définir proprement cette équivalence, et de proposer une heuristique pour la décider. Dans cet exposé, je présenterais quelques idées pour résoudre ce problème.
Attention, ce n’est pas le jour habituel
14h, salle du Conseil du Lip
Titre : Programming critical real-time systems with PRELUDE
Julien Forget, LIFL, équipe DaRt/émeraude, Université de Lille
Abstract :
(exposé grand public)
An Embedded Control System consists of a multi-rate control loop, which indefinitely acquires the current state of the system through sensors and, based on these inputs, produces commands to apply to the actuators of the system. We are interested in critical embedded control systems, such as the flight control system of an airplane for instance. The implementation of such a system must be deterministic both functionally (always produce the same output values) and temporally (always produce outputs at the same time).
PRELUDE is a formal language designed for the specification of the software architecture of such systems. It belongs to the synchronous data-flow languages family and its main specificity is that it focuses on dealing with the functional and real-time aspects of multi-periodic systems conjointly. From a Prelude program the compiler generates a semantically equivalent C program consisting of a set of periodic communicating tasks (threads) executed concurrently.
This presentation will give an overview of the language, its formal semantics and its compilation.
Attention, changement de salle et d’heure
14h, salle B1
Alexandre Isoard: Allocation mémoire et ordonnancement partiel
Le retour récent vers le parallélisme pour la programmation des accélérateurs matériels fait resurgir de vieux problèmes sous de nouvelles formes. L’allocation mémoire sur des programmes comportant une part de sémantique parallèle en est un exemple, la dépendance vis à vis de l’ordonnancement étant différente de celle d’un programme séquentiel ou à parallélisme synchrone. En effet, un ordonnancement non déterministe (c’est-à-dire qui n’induit pas un ordre total sur les opérations), que ce soit pour des raisons matérielles (parallélisme à l’exécution), des raisons sémantiques (ordonnancement non totalement déterminé), ou des raisons d’optimisation (permettre un réordonnancement a posteriori), pose le problème d’optimisation de l’allocation mémoire dans un cadre plus général.
On se propose d’étudier le problème de l’allocation mémoire de taille minimale pour un ordonnancement partiel. Ce problème peut aussi bien s’appliquer à l’allocation de registres dans des blocs de base concurrents, au double buffering de tableaux avec communications asynchrones sur un code tuilé (logiciel Chuba), ou à l’allocation mémoire dans un code parallèle (un programme X10 par exemple). L’ordonnancement sera représenté par un ordre partiel de type "happens before" sur les instructions, dont on extraira une relation de conflits mémoire qui permettra d’effectuer l’allocation mémoire de taille minimale (autant que faire se peut) et ne présentant aucun conflit sous toutes les traces d’exécution possibles.
Si le temps le permet, nous montrerons également comment les principes mis en évidence s’applique au cas de Chuba (pipeline logiciel de tuiles) et ce, même dans le cas de tuiles dont la taille est paramétrée.
11h30, salle de réunion Lug II.
Guillaume Ioos: Tuilage Sémantique
Certains programmes d’algèbre linéaire (ou de théorie des graphes) manipulant des scalaires possèdent une version alternative manipulant des matrices, et utilisant des opérations matricielles à la place des opérations scalaires. Cette version (blockée) possède une structure identique à la version scalaire, tout en ayant une granularité plus important que la version initiale (scalaire) du programme.
On cherche donc à formaliser la transformation sémantique qui passe d’un programme scalaire à un programme blocké, nommée "tuilage sémantique". Cette transformation peut être vu comme un blockage des données en matrices, puis un découpage sémantique des instructions d’un programme, afin de gagner en localité. Ses conditions d’applicabilités différent d’un tuilage conventionnel: quelques (rares) applications peuvent donc être tuilable sémantiquement, tout en admettant des dépendances ne permettant pas un tuilage conventionnel.
Plusieurs formalisations possibles de cette transformation sont en cours d’exploration: * Une première possibilité consiste à distinguer les opérations selon les blocs de données utilisés, afin de les isoler pour former des opérations matricielles.On essaye donc d’arriver sur un programme bloqué par transformations sémantiques successives du programme scalaire initial. * La seconde possibilité (plus brutale) consiste à substituer les données et opérations scalaires du programme initial par des données et des opérations matricielles "correspondantes" pour obtenir un programme bloqué candidat. Puis, il nous reste plus qu’à essayer de prouver l’équivalence entre le programme bloqué obtenu et la version scalaire initiale.
Dans les deux approches, un algorithme d’équivalence de programme est utilisé (dans le premier cas, pour reconnaître les opérations matricielles des blocks d’opérations que l’on forme / dans le second cas, pour prouver l’équivalence du programme scalaire avec le programme blocké). En particulier, un tel algorithme doit être capable de gérer les propriétés d’associativité et de commutativité d’un opérateur sur un nombre paramétrique de terme. Nous présenterons donc une extension de l’algorithme de Barthou-Feautrier-Redon afin de gérer (partiellement) de tels cas.
13h30, salle TBA.
Addressing the Challenge of Exaflopic Computation
Exaflopic systems, composed of millions of heterogeneous cores will appear at the end of this decade. This technological breakthrough will engage the HPC community in defining new generations of applications and simulation platforms. The challenge is particularly severe for multi-physics, multi-scale simulation platforms that will have to combine massively parallel software components developed independently from each others. Another difficult issue is to deal with legacy codes, which are constantly evolving and have to stay in the forefront of their disciplines. This will also require new compilers, libraries, middleware, programming environments (including debuggers and performance optimizers), languages, as well as numerical methods, code architectures, and pre- and post-processing tools (e.g., for mesh generation or visualization).
The goal of the European Exascale Software Initiative project (EESI) is to build a European roadmap along with a set of recommendations to address the challenge of performing scientific computing on this new generation of computers. The talk will present the objective, motivations and results of EESI.
High-performance sparse direct solvers
Direct methods for the solution of sparse systems of linear equations are extensively used in a wide range of numerical simulation applications. Such methods are based on a matrix decomposition of the form A = LU, LLt, LDLt or QR, followed by triangular solves. In comparison to iterative methods, they are known for their numerical robustness. However, they are also characterized by a high memory consumption (especially for 3D problems) and a large amount of computations. In this talk, we present some of the challenges that need to be tackled to solve huge problems with direct methods on the emerging computing platforms: (i) exploiting more parallelism, (ii) optimizing memory usage, (iii) maintaining numerical stability without significant sacrifice on performance. We present this in the context of the MUMPS solver (see http://graal.ens-lyon.fr/MUMPS or http://mumps.enseeiht.fr), a parallel sparse direct solver developed in Toulouse, Lyon-Grenoble, and Bordeaux.
10h30, Salle Lug 2
Préparation du séminaire d’évaluation de Compsys (réunion privée)
14h Salle Lug-1
Tanguy Risset et. al. : Radio Logicielle.
10h, salle de réunion du LUG II.
Benoît de Dinechin (Kalray): le projet Manycore Lab.
Ce document a été traduit de LATEX par HEVEA