Journée LaMHA + LTP
Vendredi 18 octobre 2019

Université Paris-Est Créteil - LACL

Inscription avant le 2 octobre 2019



Nous avons le plaisir de vous inviter à la journée annuelle conjointe des groupes de travail LaMHA et LTP du GDR GPL du CNRS, qui aura lieu au LACL à Créteil le vendredi 18 octobre 2019.

La salle réservée pour cette journée est la salle TD5 de l'ESIPE du centre Saint-Simon (salle à droite au fond au rez-de-chaussée quand on rentre). Voici quelques photos pour vous aider à trouver votre chemin.



Les inscriptions sont closes.


Afin de faciliter l’organisation de la rencontre, nous vous invitons à ne pas attendre la date limite et à vous inscrire même si vous ne proposez pas d’exposé.

Vous pouvez proposer des présentations de vos travaux sous la forme d'un exposé oral, d'un tutoriel, d'une démonstration d'outil, etc.

Le GT LaMHA du GDR GPL du CNRS

Les principaux thèmes abordés dans le groupe de travail LaMHA (Langages et Modèles de Haut niveau pour la programmation parallèle, distribuée, de grilles de calcul et Applications) du GDR GPL du CNRS sont :

Le GT LTP du GDR GPL du CNRS

Les thèmes du groupe de travail LTP (Langages, Types et Preuves) du GDR GPL du CNRS sont :

Programme de la journée

09h00 Accueil
09h30 Jean-Jacques Lévy (INRIA / IRIF), conférencier invité Trois preuves formelles de l’algorithme de Tarjan pour calculer les composantes fortement connexes dans un graphe.

Nous présentons une preuve formelle d’un algorithme sur les graphes dans trois assistants de preuves. C’est l’occasion de comparer la formalisation d’un problème non trivial en Why3, Coq et Isabelle. Travail présenté à ITP 2019 avec Ranh Chen, Cyril Cohen, Stephan Merz et Laurent Théry.

10h30 Pause café
11h00 Wijnand Suijlen (Huawei Technologies France) A parallel collectives library using delayed one-sided communications

In a parallel environment with only global barriers as synchronisation mechanism it is not obvious how to implement collective operations on data-dependent process subsets, especially if subsets can overlap. We demonstrate how delayed one-sided communications can do this elegantly, and within the limits of C89 and BSPlib. Delayed communications also allow independent collective operations to automatically coalesce at runtime so that the optimal parallel algorithm can be applied to the combined total volume. These conveniences bring parallel programming on distributed memory systems in plain C to a higher level.


11h30 Maxime Jacquemin (CEA) A Dividing Method Minimizing the Linearization Term in Affine Arithmetic

Affine arithmetic is a well known tool to derive first order guaranteed approximations of general formulas over real numbers. It is also a useful tool in static analysis to keep track of linear correlations between program variables. However non-linear operations, like multiplications or divisions, introduce compensation terms to over-approximate the residue of the linearization Process. Tight estimations of those terms are of utmost importance to obtain precise abstractions and thus a useful analysis. In this paper, we propose a new and simple technique to compute precise compensation terms for divisions.


12h00 Ludovic Henrio (CR CNRS, équipe Cash --- Univ Lyon, EnsL, UCBL, CNRS, Inria, LIP) Dataflow explicit futures: Principles and implementation (présentation jointe avec Amaury Maillé)

A future is a place-holder for a value being computed, and we generally say that a future is resolved when the associated value is computed. In existing languages futuresare either implicit, if there is no syntactic or typing distinction between futures and non-futurevalues, or explicit when futures are typed by a parametric type and dedicated functions existfor manipulating futures. One contribution of this article is to advocate a new form of future, named data-flow explicit futures, with specific typing rules that do not use classical parametrictypes. The new futures allow at the same time code reuse and the possibility for recursive functions to return futures like with implicit futures, and let the programmer declare whichvalues are futures and where synchronisation occurs, like with explicit futures. We prove thatthe obtained programming model is as expressive as implicit futures but exhibits a different behaviour compared to explicit futures. The second and main contribution of this article is anexhaustive overview and precise comparison of the semantics of futures in existing program-ming languages. We show that, when classifying future implementations, the most distinctive aspect is the nature of the synchronisation not the explicitness of the future declaration.


12h30 Déjeuner
14h00 Jocelyn Sérot (Institut Pascal), conférencier invité De CAPH à HoCL. A propos de l’utilisation des langages fonctionnels dans le domaine de l’embarqué

L’exposé comprendra deux parties. Dans une première, on fera un bilan des travaux menés par l’auteur autour depuis une décennie autour du langage CAPH, un langage fonctionnel dédié à l’implémentation d’applications flot de données sur circuits FPGA . On essaiera d’identifier, en particulier, pourquoi, en dépit de caractéristiques originales, directement inspirées des langages de programmation fonctionnels et absentes des outils de synthèse matérielle plus classiques, le langage n’a pas connu une diffusion importante. Dans une seconde partie, on présentera le langage HoCL (Higher Order Coordination Language), qui peut être vu comme une tentative de recycler certaines idées de CAPH dans le contexte plus général de la programmation de systèmes multi-processeurs ou multi-cœurs.
URLs: http://dream.ispr-ip.fr/CAPH/CAPH/CAPH.html et https://github.com/jserot/HoCL

15h00 Pause café
15h30 Hélène Coullon (IMT Atlantique, Inria) Efficient and Safe Distributed Software Commissioning

With the emergence of large-scale virtualized distributed infrastructures, such as Cloud, Fog and Edge computing, for instance, and the increasing complexity and dynamicity of distributed software systems, the automation of distributed software commissioning and their dynamic reconfiguration is of great importance for IT administrators and developers. Nowadays many production tools already help developers automate their deployment tasks. Though, scientific challenges have to be solved in this area to improve at least three aspects of distributed software management: efficiency, software-engineering properties and verification. In this talk I will first present Madeus, a formal component-based model for distributed software commissioning that enhances the efficiency of deployments. Second, I will present the use of model-checking techniques to help in the design of safe and efficient software commissioning procedures written with Madeus.


16h00 Jolan Philippe (IMT Atlantique) PySke: Algorithmic Skeletons for Python

Algorithmic skeletons are patterns of parallel computations. Skeletal parallel programming eases parallel programming: a program is merely a composition of such patterns. Data-parallel skeletons operate on parallel data-structures that have often sequential counterparts. In algorithmic skeleton approaches that offer a global view of programs, a parallel program has therefore a structure similar to a sequential program but operates on parallel data-structures. PySke is such an algorithmic skeleton library for Python to program shared or distributed memory parallel architectures in a simple way.


16h30 Thibaut Tachon (Huawei PRC) HTL: High-level Tensor Language with Automatic Parallelization

Nous présentons HTL, un langage spécifique pour la programmation d'opération sur des tenseurs en parallèle. Son petit ensemble de primitive et son analyse de forme statique facilite les optimisations, la différenciation et la parallélisation. La parallélisation en particulier sera développée en détaillant nos stratégies de partitionnement de tenseur en fonction de l'expression des opérateurs.


17h00 Réunion d'information et d'échanges
17h30 Fin de la journée

Particpants à cette journée

Alain Giorgetti

À bientôt,

Frédéric Gava (organisateur local),
Emmanuel Chailloux et Sylvain Jubertie (responsables du GT LaMHA)
Sylvain Conchon et Alain Giorgetti(responsables du GT LTP)