OFFRE DE STAGE : VALIDATION FORMELLE D’UN CACHE À COHÉRENCE GLOBALE - S12
S-12-CTO
Montbonnot / Alternances et stages
Offre de stage : Validation formelle d’un cache à cohérence globale
S-12-CTO
L’entreprise :
Kalray est une des plus innovantes sociétés de la « DeepTech » françaises. Kalray est une société de semi-conducteurs « fabless », pionnière dans une nouvelle génération de processeurs, spécialisés dans le traitement intelligent des données. Kalray vise les marchés en pleine expansion du Cloud, du « Edge Computing » et de l’IA, tels que les data centers modernes, les réseaux 5G, les véhicules autonomes, les équipements de santé, l’industrie 4.0, les drones et les robots…
En forte croissance, Kalray compte une centaine de collaborateurs à Grenoble et Sophia-Antipolis, un bureau en Californie, ainsi qu’au Japon et accueille à son capital des investisseurs de premier plan comme l’Alliance Venture (Renault-Nissan-Mitsubishi), Safran, NXP Semiconductors, le CEA et Bpifrance. Kalray est également cotée en bourse sur Euronext Growth (FR0010722819 – ALKAL). Kalray, c’est avant tout une équipe de femmes et d’hommes passionnés, enthousiastes et solidaires, qui mettent l’excellence et la collaboration au cœur de leur quotidien. Que vous soyez expert de votre domaine ou jeune diplômé, vous saurez trouver votre place et vous épanouir dans un environnement agile et dynamique, où vous pourrez pleinement exprimer votre talent et contribuer très concrètement au succès de l’entreprise.
Au programme : des challenges passionnants, mais aussi de la bonne humeur, de l’entraide, la montagne, la mer… et bien plus encore !
Vous souhaitez en savoir plus, découvrez l’histoire de Kalray en vidéo.
MISSIONS ET OBJECTIF DU STAGE
Kalray produit le processeur MPPA, qui comporte 80 cœurs applicatifs d’architecture 64-bit VLIW appelée KVX répartis en cinq ‘clusters’ de 16 cœurs. Au niveau de chaque cluster, les cœurs ont des caches L1D cohérents et se partagent un cache L2. Par défaut, les caches L2 ne sont pas cohérents entre eux. Cependant, un développement avancé en cours permet d’assurer la cohérence de ces caches L2 en utilisant la TLB des cœurs comme cache L3 avec des blocs de 4KO au niveau desquels un protocole MESI est appliqué, tandis que les transferts de données restent à granularité de ligne L2.
La mission consiste à modéliser et analyser formellement ce mécanisme de cohérence globale des caches L2 en utilisant la boîte à outils CADP (http://cadp.inria.fr) développée par l’équipe Inria CONVECS (http://convecs.inria.fr). CADP fournit des langages formels de nouvelle génération pour décrire le comportement (LNT) et les propriétés (MCL) des systèmes parallèles asynchrones, ainsi que des outils de vérification et de génération de tests. Les chercheurs de CONVECS ont été récompensés en 2021 par le Prix de l’innovation Inria – Académie des sciences – Dassault Systèmes.
L’objectif est de développer un modèle du système de cache L2 dans le langage LNT afin d’abstraire les interactions des composants maître/esclave. Ce modèle permettra de proposer des scénarios de test qui seront repris par l’équipe vérification pour les déployer au moyen de l’outil trekapp de Breker Systems (https://brekersystems.com/products/cache-coherency/) utilisé à Kalray.
CANDIDAT
Profil :
- Étudiant en dernière année d’école d’ingénieur ou en M2
Compétences requises :
- Intérêt ou connaissance des sujets de « Computer Architecture » relatifs à la hiérarchie mémoire.
- Intérêt pour les méthodes formelles appliquées à l’inginiérie.
MODALITÉS DU STAGE
Date de démarrage : 1er trimestre 2022
Durée : 6 mois, stage de fin d’études
Localisation : Kalray, 180 avenue de l’Europe, 38330 Montbonnot-Saint-Martin (ligne bus C1 – Arrêt Baudonnière)
Stage rémunéré : 1100 € Brut / mois + tickets restaurant
