Utilisation du Paralléliseur : comparatif

Introduction

L’intérêt du Paralléliseur est de lancer simultanément plusieurs instances de l’Atelier B afin d’accélérer les traitements de preuves, qui peuvent très rapidement nécessiter des temps de calculs importants, au fur et à mesure que le projet gagne en complexité. On présente ici l’analyse du temps nécessaire à la preuve de force « rejeu » (-2) d’un projet de taille industrielle.

Projet utilisé

Le projet utilisé pour réaliser ce comparatif est de taille relativement importante ; il comporte en effet 285 composants. Le temps de traitement d’un tel rejeu s’exprime en minutes, même avec des moyens informatiques modernes et performants.

Résultats obtenus

Le premier essai se base sur l’utilisation du Paralléliseur sur une seule et unique machine, en permettant le lancement d’une unique instance de l’Atelier B. Cela revient donc à une « utilisation classique » du logiciel, et sera en quelque sorte notre témoin au cours de cette étude.

Le deuxième test est une reprise du précédent, en autorisant toutefois une deuxième instance sur la même machine que précédemment. Il a pour but de tester l’intérêt des machines multi-processeurs.

Le troisième test correspond au lancement simultané de 3 instances de l’Atelier B sur 3 machines différentes. Ce troisième test s’intéresse donc aux gains de la distribution des tâches sur le réseau.

Enfin, le dernier test s’intéresse au lancement de 2 instances simultanées sur 2 machines différentes, ce qui fait un total de 4 Ateliers B simultanés.

Ces choix dans l’utilisation du matériel de test sont motivés par le besoin de comparer d’une part l’intéret qu’apporte la parallélisation de l’exécution des tâches, et d’autre part l’efficacité des machines disposant de plusieurs processeurs / coeurs par rapport à une utilisation simultanée de plusieurs machines.

Les résultats du rejeu (preuve force -2) suite à un oubli complet de la preuve (après avoir remit le projet dans un état non prouvé), selon les différents cas exposés ci-dessus, sont les suivants :

Nous pouvons synthétiser ces résultats dans le diagramme ci-dessous :

Interprétation des résultats

On remarque que plus le nombre d’instances simultanées est important, et plus le test s’exécute rapidement, ce qui est logique.

Toutefois, on se rend compte par ailleurs que le gain de l’éxecution sur des machines multi-coeurs est à privilégier, plutôt que la dispersion sur plusieurs machines mono-processeurs, comme le montre la différence de résultat entre le test n°3 et le test n°4.

Dans tous les cas, l’utilisation du Paralléliseur semble tout à fait intéressante dans le cadre de développements sur des projets industriels relativement importants.