Seconde journée du groupe de travail LaMHA

In this talk we presents a Bulk-Synchronous Parallel (BSP) algorithm to compute the discrete state space of structured models of security protocols.

The BSP model of parallelism allows us to design an efficient algorithm that is at the same time simple to express. A prototype implementation has been developed, allowing to run benchmarks showing the benefits of our algorithm.

We also present our first works of how formally proving (machine-checked) the correctness of the algorithms using the well-structured nature of the BSP model of computation.

La composition d'applications scientifiques consiste à mettre en commun des codes et applications produits par différents chercheurs afin de former des applications plus complètes pour la compréhension des phénomènes étudiés (géo-sciences, biologie moléculaire, ...).

Dans ce contexte, les composants logiciels à assembler existent donc bien au départ mais sont largement hétérogènes du point de vue de leurs fonctions et/ou des langages de programmation. Il existe une grande variété d'outils (frameworks) pour construire ce genre d'applications. Certains sont même optimisés pour le calcul haute-performance. Mais, à notre connaissance, aucun ne supporte encore correctement les applications de visualisation scientifique interactives où toutes les actions de l'utilisateur doivent être répercutées en temps réel sur l'ensemble des composants de calcul, d'interaction et de visualisation. En particulier, un framework dédié à de telles applications doit permettre de construire les bonnes politiques de synchronisation à placer entre les composants pour exprimer leur manière de collaborer et doit permettre d'assurer la cohérence temporelle des données.

Nous présenterons dans cet exposé nos travaux pour définir un tel framework qui réponde à ces contraintes tout en étant utilisable par de non-informaticiens.

Parallelism is already mainstream technology at the architectural level and will soon be so at the application programming level.

Skeletons research claims to have answers to some of the questions this will pose.

This is our moment - are we ready?

I will examine some of the evidence. I will also present the ideas behind ongoing work at Edinburgh in skeletal programming and machine-learning led optimization.

Algorithmic Skeletons offer high-level abstractions for parallel programming based on recurrent parallelism patterns. Patterns can be combined and nested into more complex parallelism behaviors.

Programmers fill the skeleton patterns with the functional (business) code, which transforms the generic skeleton into a specific application.

In this talk we will speak about support for the programmer of algorithmic skeletons by mentioning two contributions we made in the recent years: the typing of algorithmic skeletons to ensure type safety of skeletons, and the handling of exceptions in programs made of algorithmic skeletons. In both cases the objective is to provide more safety in the execution of skeleton programs, without t breaking the high-level abstractions of the programming model.

For both of these features, our approach was both theoretical, eith a formal specification of the langiuage, and practical, implementing those features in a Java skeleton library.

In this talk we will present the design and implementation of BSP++, a C++ parallel programming library based on the Bulk Synchronous Parallelism model to perform high performance computing on both SMP and SPMD architectures using OpenMPI and MPI.

We show how C++ support for genericity provides a functional and intuitive user interface which still delivers a large fraction of performance compared to hand written code.

We show how the library structure and programming models allow simple hybrid programming by composing BSP super-steps and letting BSP++ handling the middleware interface.

The performance and scalability of this approach are then assessed by various benchmarks of classic HPC application kernels and distributed algorithms on various hybrid machines including a subset of the GRID5000 grid.

Distributing applications over PC clusters to speed-up or size-up is now commonplace. Yet effectively tolerating faults of these systems is a major issue.

To ease the addition of checkpoint-based fault tolerance at the application level, we introduce a Model for Low-Overhead Tolerance of Faults (MoLOToF) which is based on structuring applications using fault-tolerant algorithmic skeletons. The application of MoLOToF to some family of SPMD parallel algorithms termed GReLoSSS (i.e.: Globally Relaxed Locally Strict Synchronization SPMD is a relaxed variation of BSP) resulted in the FT-GReLoSSS framework.

In this talk I will present both MoLOToF and FT-GReLoSSS as well as some experimental evaluation results.