Le Paralléliseur – Documentation utilisateur

Contexte d’utilisation

Parallèliseur est une application visant a optimiser les temps de traitement des projets B par une utilisation transparente, distante et parallèle de l’Atelier B.

Lorsqu’il s’agit de prouver des projets relativement simples, comme des calculs de PGCD ou de détermination de minimum, le temps de calcul est négligeable, mais dès lors que les projets gagnent en complexité, le processus de preuve d’un projet B devient très couteux en temps.

Or il existe des possibilités de parallélisation des tâches entre plusieurs machines ; toutefois, il n’existait pas de solution autre que manuelle pour assurer cette optimisation.

Ainsi, l’objectif de Paralléliseur est d’assurer cette automatisation, en gérant les ressources serveur disponibles et en étant capable d’ordonnancer intelligemment les tâches.

Configuration

Dans tous les cas, avant de pouvoir utiliser le Paralléliseur, il est nécessaire d’avoir un client SSH disponible sur la machine client.

Windows

Sous la version Windows, il faut utiliser un agent SSH ; pageant, par exemple, livré en standard avec l’installeur de putty. Il est par ailleurs aisé de vérifier que ce dernier est en cours d’éxecution, par la présence d’une icône dans la barre des tâches.

La génération d’une clé est réalisée via l’utilisation du binaire puttygen, livré en standard dans l’installation de Putty.

Cliquez sur le bouton Generate. Sauvegardez la clé privée générée en local, et gardez-la en lieu sûr. Cette clé privée s à destination de Pageant.

Sauvegardez la clé publique ; cette dernière est à destination des machines sur lesquelles vous souhaitez vous connecter automatiquement. Ouvrez les connexions aux serveurs SSH, éditez le fichier distant :

% ~/.ssh/authorized-keys

Copiez/ collez-y la clé publique précédemment générée.

Configurez dorénavantpageant afin qu’il ait connaissance de votre clé privée.

Vérifiez a l’aide de putty par exemple, que l’utilisation d’un mot de passe pour se connecter aux différents serveurs n’est plus nécessaire.

GNU/Linux et MacOS

Bien que le principe soit le même que celui exposé dans la partie précédente, la démarche est quelque peu différente sous GNU/Linux. Lancez la commande suivante, afin de générer une paire de clé publique / clé privée :

% ssh-keygen -t rsa

Ne protégez pas votre clé à l’aide d’une passphrase. Assurez-vous que votre Agent SSH est bien lancé (le processus ssh-agent) ; copiez ensuite votre clé publique sur les serveurs sur lesquels vous chercherez à vous connecter par la suite :

% ssh-copy-id user@host

La connexion sans demande de mot de passe devrait maintenant être possible.

Configuration de l’application

Si cela n’a pas été fait via l’assistant de configuration, affiché lors de la première utilisation, il est nécessaire d’ajouter au moins un serveur Atelier B, avant de pouvoir se servir du Paralléliseur. Dans tous les cas, la configuration peut se faire en selectionnant dans le menu « Edition / Préférence ». Une nouvelle fenêtre s’ouvre alors. Il convient d’y renseigner correctement son nom d’utilisateur – nom de login SSH, configuré de telle sorte que la connexion aux serveurs soit automatique et ne nécessite pas de mot de passe -, et d’indiquer les noms des serveurs un à un (ou leur addresse IP), ainsi que l’information sur le nombre de coeurs (ou processeurs) disponibles sur le serveur considéré.

Utilisation

Après configuration et ajout d’au moins un serveur AtelierB, la liste des projets B disponibles sur ce serveur doit avoir été mise à jour. Il devient alors possible d’en sélectionner.

Un simple click gauche dans la liste des projets sur la fenêtre principale permet alors d’ouvrir et de récupérer l’état global courant du projet.

Il devient ensuite intuitif de sélectionner des machines du projet sur l’interface, et de leur appliquer des tâches à effectuer dessus. Ces tâches seront exécutées dès que possible en fonction des ressources disponibles.

Les opérations disponibles implémentées dans le paralléliseur effectuables sur les composants sont les suivantes :

• Vérification des types.
• Génération des obligations de preuve.
• Preuves.

Ces options sont disponibles via sélection des composants sur lesquels travailler, puis en effectuant un click droit sur la sélection, ou via le menu général « Action », une fois les composants sélectionnés.

La sortie BBatch pour une tâche spécifique peut etre demandée en cliquant sur la tâche considérée et en sélectionnant « Afficher la sortie BBatch » dans le menu déroulant.