Journée du GDR GPL 2017 - Montpellier - Session LaMHA/Compil

Nous tenterons de répondre formellement à la question : qu'est-ce qu'un algorithme BSP ? Pour ce faire, nous étendrons à BSP la définition axiomatique des algorithme séquentiels de Gurevich et ses "abstract state machines" (ASM). Puis nous donnerons une équivalence algorithmique entre ces ASM -BSP et un mini langage impératif via une simulation pas-à-pas.

Les systèmes hétérogènes (combinant plusieurs types d'unités de calcul) sont maintenant très répandus. Soigneusement utilisés, ils permettent une augmentation de performances impressionnante. Cependant, ils exigent généralement que les développeurs combinent plusieurs modèles de programmation, à travers des langages et des outils très complexes. Les programmes hétérogènes sont ainsi difficiles à concevoir et à déboguer. L'écriture de programmes hétérogènes corrects est difficile. Obtenir de bonnes performances l'est encore plus.

Pour aider les développeurs, de nombreuses solutions de haut niveau ont été développées. La plupart d'entre elles génèrent une partie du code qui sera effectivement exécuté et isolent le programmeur des détails de bas niveau. Elles aident à créer des programmes efficaces et plus sûrs, mais laissent les programmeurs confus face à des bogues complexes ou lorsqu'ils tentent d'optimiser leur application.

Dans cette présentation, je décrirai notre solution pour le profilage d'applications hétérogènes portables décrites avec SPOC (Stream Processing with OCaml). Pour cela, je présenterai d'abord rapidement SPOC : une bibliothèque portable pour le langage OCaml associée à un DSL permettant de générer du code GPGPU à l'exécution. Je détaillerai ensuite notre solution de profilage qui se concentre sur deux points principaux :

• rester portable et offrir des informations pertinentes, quelle que soit la combinaison d'architectures présentes dans le système hétérogène
• offrir au programmeur des informations utiles facilement repliables au code écrit à l'origine et non au code généré par SPOC.

We propose a novel approach to model architectures featuring relaxed memory behaviours. The approach used here takes inspiration from standard denotational tools for semantics of concurrency and game semantics to give a denotational model based on event structures of an idealized assembly language. The approach is neatly decomposed into a thread semantics and a storage semantics: the first one dealing with intra-thread causality (program order) and the second one dealing with inter-thread causalities (memory order). The two are then combined by taking the synchronized product. In this talk, we demonstrate this technology on the architecture TSO, and build a model for a simple assembly language.

Dans le but d'analyser statiquement des systèmes distribués, nous présentons un modèle de concurrence dont les états de programmes sont représentés par des langages reconnus par des automates symboliques. Nous utilisons ces automates (lattice automata) en tant que domaine abstrait pour notre analyse. La fonction de transition de notre système raisonne sur ces automates en réécrivant le langage reconnu à l'aide d'un ensemble de règles de réécritures encodant la sémantique des instructions de notre programme.

Grâce à la méthodologie de l'interprétation abstraite, nous sommes capables d'établir une sur-approximation de l'espace d'atteignabilité d'états de programmes concurrents. L'utilisation modulaire de domaines abstraits numériques sous-jacents permet d'inférer des invariants entre les processus et donc de prouver, entre autre, des propriétés numériques séquentielles ou globales.

Nous conclurons par la présentation de notre prototype permettant une analyse de valeur d'un sous-ensemble de la bibliothèque de calcul parallèle MPI/C. Cet outil s'intégre en tant que plugin à la plateforme Frama-C dédiée à l'analyse de programmes C.

Simple, single-core processors have been the main execution platform for critical real-time software for years. Such software can be handwritten in imperative languages, but code generation from higher-level languages such as the synchronous data-flow SCADE (industrial version of the Lustre language) are also used in production today. Single-core processors are reaching their limits. Performance, or energy efficiency constraints are leading the industry towards multi-core or many-core including for critical systems. These architectures raise new major challenges for timing analysis. In this talk, we present a code generation flow from SCADE that produces parallel and yet predictable code for Kalray MPPA architecture. The code generation scheme is designed together with a timing analysis that take into account interference between cores when they access the local memory. This work is performed as part of the CAPACITES project: http://capacites.minalogic.net/