Doctorant F/H Conception rigoureuse de circuits basée sur les méthodes formelles
Contract type : Fixed-term contract
Level of qualifications required : Graduate degree or equivalent
Other valued qualifications : master en informatique
Fonction : PhD Position
Level of experience : Recently graduated
About the research centre or Inria department
Le Centre Inria de l’Université Grenoble Alpes, regroupe un peu moins de 600 personnes réparties au sein de 22 équipes de recherche et 8 services support à la recherche.
Son effectif est distribué sur 3 campus à Grenoble, en lien étroit avec les laboratoires et les établissements de recherche et d'enseignement supérieur (Université Grenoble Alpes, CNRS, CEA, INRAE, …), mais aussi avec les acteurs économiques du territoire.
Présent dans les domaines du calcul et grands systèmes distribués, logiciels sûrs et systèmes embarqués, la modélisation de l’environnement à différentes échelles et la science des données et intelligence artificielle, le Centre Inria de l’Université Grenoble Alpes participe au meilleur niveau à la vie scientifique internationale par les résultats obtenus et les collaborations tant en Europe que dans le reste du monde.
Context
Les projets du PEPR Cloud soutiennent la souveraineté européenne dans ce domaine, qui comprend également le matériel, notamment les processeurs et les accélérateurs de calcul. Dans un contexte technologique de ralentissement de la loi de Moore, l’amélioration des performances des processeurs nécessite des architectures matérielles avec plus de parallélisme (multi-cœurs), plus de spécialisation (accélérateurs), un rapprochement du calcul et de la mémoire, ainsi que de nouveaux types d’interconnexions entre les composants. En dissociant les ressources matérielles (calcul, mémoire, interconnexion) des ressources logiques, la virtualisation facilite le déploiement des architectures convergées qui regroupent l'infrastructure de calcul, de stockage et de réseau. Le cloud gagne ainsi en modularité, en vitesse et en agilité pour le déploiement de nouveaux services avec une utilisation optimale des ressources.
La désagrégation matérielle et la virtualisation des ressources rendent la couche d’adaptation intermédiaire de plus en plus complexe, difficile à valider et sujette aux pannes. Le projet Archi-CESAM du PEPR Cloud propose de repenser le matériel (calcul, mémoire et interconnexion) afin qu’il soit co-conçu avec l’applicatif dans une perspective d’architecture convergée et de confiance, en présence de données massives à traiter.
Les travaux de recherche de l'équipe CONVECS du centre Inria de l'UGA portent sur la modélisation et la vérification formelle de systèmes concurrents asynchrones, qui s'instancient dans de nombreux domaines (protocoles de communication, algorithmes distribués, systèmes embarqués, réseaux sur puce, etc.). A cette fin, CONVECS propose des langages formels de nouvelle génération pour spécifier le comportement et les propriétés des systèmes concurrents, ainsi que des algorithmes de vérification efficaces. Ces travaux sont instanciés dans des outils de l'environnement CADP [GLMS13], qui assiste les différentes phases du processus de conception (compilation et prototypage rapide, simulation interactive et guidée, vérification par logiques temporelles et par équivalences, génération de tests de conformité, co-simulation et évaluation de performances) et est largement utilisé en milieu académique et indutriel.
Assignment
Dans un premier temps, le travail consistera à étudier HPDcache [Fug23], un cache de données L1 hautes performances compatible avec les processeurs RISC-V. HPDcache est utilisé dans l'implémentation CVA6 [ZB19] du RISC-V utilisé par plusieurs industriels (Bosch, Thales, ...). Il s'agit d'un cache hautement configurable, avec exécution dans le désordre (out-of-order) et reexécution (replay), muni d'interfaces compatibles avec AMBA AXI5 et RISC-V.
L'étude du HPDcache sera faite en construisant un modèle formel de son architecture, qui comporte un pipeline à trois étages, permettant de traiter environ 10 transactions simultanées. Plusieurs configurations seront considérées, en fonction des différentes fonctionnalités activées du HPDcache. Ce modèle formel servira de base pour vérifier des propriétés de correction (absence de livelocks et de deadlocks, respect du modèle de cohérence du processeur, etc.), pour générer des tests de conformité et pour estimer les performances du cache.
Dans un deuxième temps, le travail consistera à proposer des extensions de la méthodologie de conception des circuits avec des méthodes formelles (modélisation, vérification, test de conformité), notamment en considérant les architectures à composants communicants (chiplets). Une partie intéressante de cette méthodologie pourrait être des passerelles entre les langages de description de ces circuits et de leurs protocoles de communication sous-jacents et les langages formels utilisés pour la vérification.
Références
[Fug23] César Fuguet Tortolero. HPDcache: Open-Source High-Performance L1 Data Cache for RISC-V Cores. Proc. of the 20th ACM International Conference on Computing Frontiers (CF'2023), Bologna, Italy, pp. 377-378, ACM Press, 2023. https://cea.hal.science/cea-04110679/en
[ZB19] Florian Zaruba and Luca Benini. The Cost of Application-Class Processing: Energy and Performance Analysis of a Linux-Ready 1.7-GHz 64-Bit RISC-V Core in 22-nm FDSOI Technology. IEEE Transactions on Very Large Scale Integration (VLSI) Systems 27(11):2629-2640, 2019. https://doi.org/10.1109/TVLSI.2019.2926114
[GLMS13] Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe. CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes. Springer International Journal on Software Tools for Technology Transfer (STTT) 15(2):89-107, 2013. http://hal.inria.fr/hal-00715056/en
Main activities
- Modéliser les systèmes à étudier en utilisant les langages formels développés par CONVECS
- Etudier différentes configurations et les analyser formellement (vérification, génération de tests, évaluation de performances)
- Participer aux réunions de projet et à la rédaction des livrables
Skills
Compétences techniques : connaissance des langages de spécification pour systèmes concurrents asynchrones
Langues : français requis ; bon niveau d'anglais
Relationnel : travail en équipe
Benefits package
- Restauration subventionnée
- Transports publics remboursés partiellement
- Congés: 7 semaines de congés annuels + 10 jours de RTT (base temps plein) + possibilité d'autorisations d'absence exceptionnelle (ex : enfants malades, déménagement)
- Possibilité de télétravail et aménagement du temps de travail
- Équipements professionnels à disposition (visioconférence, prêts de matériels informatiques, etc.)
- Prestations sociales, culturelles et sportives (Association de gestion des œuvres sociales d'Inria)
- Accès à la formation professionnelle
- Sécurité sociale
Remuneration
- Salaire brut :
- 1ère année : 2082 euros mensuel
- 2e et 3e année : 2190 euros mensuel
General Information
- Theme/Domain :
Proofs and Verification
Software engineering (BAP E) - Town/city : Montbonnot
- Inria Center : Centre Inria de l'Université Grenoble Alpes
- Starting date : 2024-09-01
- Duration of contract : 3 years
- Deadline to apply : 2024-08-15
Warning : you must enter your e-mail address in order to save your application to Inria. Applications must be submitted online on the Inria website. Processing of applications sent from other channels is not guaranteed.
Instruction to apply
Defence Security :
This position is likely to be situated in a restricted area (ZRR), as defined in Decree No. 2011-1425 relating to the protection of national scientific and technical potential (PPST).Authorisation to enter an area is granted by the director of the unit, following a favourable Ministerial decision, as defined in the decree of 3 July 2012 relating to the PPST. An unfavourable Ministerial decision in respect of a position situated in a ZRR would result in the cancellation of the appointment.
Recruitment Policy :
As part of its diversity policy, all Inria positions are accessible to people with disabilities.
Contacts
- Inria Team : CONVECS
-
PhD Supervisor :
Mateescu Radu / radu.mateescu@inria.fr
The keys to success
Motivation, sérieux et discipline. Goût pour le développement logiciel.
About Inria
Inria is the French national research institute dedicated to digital science and technology. It employs 2,600 people. Its 200 agile project teams, generally run jointly with academic partners, include more than 3,500 scientists and engineers working to meet the challenges of digital technology, often at the interface with other disciplines. The Institute also employs numerous talents in over forty different professions. 900 research support staff contribute to the preparation and development of scientific and entrepreneurial projects that have a worldwide impact.