CADP, une boîte à outils diffusée dans le monde entier
Le bâtiment-paquebot du centre Inria Grenoble – Rhône-Alpes à Montbonnot Saint-Martin, en périphérie de Grenoble, accueille la quinzaine de membres de Convecs, équipe-projet commune entre Inria Grenoble – Rhône-Alpes et le laboratoire d’informatique de Grenoble. Quatre chercheurs Inria, un professeur de l’université Grenoble Alpes, des doctorants, postdoctorants, ingénieurs experts et stagiaires, mènent ici des recherches sur la modélisation et la vérification des systèmes parallèles et interconnectés.
La boîte à outils CADP (pour "Construction and Analysis of Distributed Processes" en anglais) est issue de leurs travaux. Il s'agit d'une plate-forme modulaire, mise en route en 1986, qui comporte une cinquantaine d'outils dont l'impact est notable dans la recherche et l’enseignement : ils ont déjà donné lieu à plus de 200 publications et à plus de 100 prototypes de recherche. Plusieurs entreprises comme Airbus, Google, Bull, STMicroelectronics, Tiempo Secure, et des centres de recherche industrielle comme le CEA-Leti et l’IRT Saint-Exupéry, ont acquis des licences. « Nous travaillons aussi, par exemple, avec des industriels de l'automobile, des spécialistes des composants mécatroniques (comme Crouzet) et de grands acteurs des télécoms ou du Cloud (comme Orange et Nokia Bell Labs) », indique Wendelin Serwe, chercheur de l’équipe Convecs.
Des systèmes informatiques de plus en plus complexes
« Les recherches de Convecs portent sur la modélisation et la vérification des systèmes parallèles asynchrones », précise Radu Mateescu, en charge de cette équipe-projet lancée en 2012 dans le sillage d'une équipe-projet antérieure appelée Vasy. « Un système parallèle asynchrone repose sur plusieurs agents (ou processus) qui travaillent de façon largement indépendante, sauf quand ils doivent se synchroniser ou communiquer par le biais de messages. »
La complexité de ces systèmes provient du fait que ces interactions sont difficiles à prévoir (on parle de "non-déterminisme"). Elle s'accroît à mesure que les progrès techniques les font évoluer. « Les premiers ordinateurs fonctionnaient avec un seul processeur, qui exécutait ligne à ligne ce qui lui était imposé par le programme, rappelle le chercheur Hubert Garavel. Mais l’augmentation de performance conduit à avoir plusieurs processeurs et des programmes capables de s'exécuter en même temps, ce qui fait naître d’épineux problèmes de synchronisation et de communication. » Il faut organiser correctement les différentes tâches pour éviter des blocages ou des corruptions de données.
Sémantique du parallélisme : une théorie riche mais peu comprise
« Le parallélisme est un concept universel, souligne Hubert Garavel. Vous en trouvez dans beaucoup d’activités humaines, notamment la gestion des organisations et des groupes de travail, pour laquelle on doit mettre en place des mécanismes de concertation et de planification pour coordonner au mieux les tâches de chacun et éviter les situations bloquées ou incohérentes. Il y en a aussi dans les téléphones et les ordinateurs portables, qui comportent désormais plusieurs cœurs et des coprocesseurs afin d’exécuter simultanément des actions très diverses : tâches de l’utilisateur, opérations du système d’exploitation, affichage, communications réseau... Il est aussi présent dans les objets connectés et les bâtiments intelligents. » Pour les supercalculateurs, on parle de "parallélisme massif" : ils s'appuient sur des dizaines ou des centaines de milliers de processeurs différents.
Des méthodes à la portée des acteurs de l'industrie
La théorie du parallélisme ("concurrency theory" en anglais) propose des modèles généraux pour décrire les interactions, prédire leur comportement et vérifier leur correction. Elle rassemble les résultats des recherches menées par de grands pionniers de l’informatique, dont plusieurs ont été distingués par le prix Turing. C’est sur ce riche, mais ardu, corpus théorique que se fondent les travaux de l’équipe-projet Convecs. « On s'efforce de mettre ces méthodes à la portée des acteurs de l'industrie, en leur fournissant des langages et des outils qui peuvent être appris et maîtrisés sans avoir de connaissances pointues dans les équations mathématiques », indique Radu Mateescu. « Il s’agit de décrire le fonctionnement des systèmes parallèles asynchrones sous une forme intelligible par des humains, tout en étant suffisamment rigoureuse pour être comprise sans ambiguïté par des machines. »
La vérification peut ensuite débuter, avec l'aide d'outils de vérification compositionnelle, qui permettent de décomposer les processus les plus complexes en fragments plus simples à analyser. Un objectif majeur de Convecs est en effet « de tester et de valider la plupart des scénarios de comportement en amont, avant que les systèmes soient déployés sur le terrain », conclut Frédéric Lang, chercheur de l’équipe Convecs.