Context of Use
The Parallelizer is an application that seeks to optimize the processing time for B projects thanks to a transparent, remote and parallel use of Atelier B.
When proving projects that are relatively simple, such as GCD calculations or the determination of minimums, the calculation time is negligible, but when projects are more complex, the proof process for a B project becomes very time-consuming.
However, there are now parallelization possibilities for tasks between a number of machines, whereas only a manual solution existed for this form of optimization in the past.
Therefore, the Parallelizer’s objective is to ensure this automatization by managing the server resources that are available and being able to intelligently schedule tasks.
Configuration
In all cases, before being able to use the Parallelizer, you must have a SSH client available on the client machine.
Windows
With the Windows version, you must use an SSH agent, pageant, for example, delivered in standard versions with the putty installer. It is also easy to make sure that it is being executed as the taskbar displays an icon.
A key is generated by using the puttygen binary in the Putty installation delivered in standard versions.
Click on the Generate button. Save the private key generated locally and keep it in a safe place. This private key is intended for Pageant.
Save the public key. It is intended for the machines on which you want to connect automatically. Open the connections to the SSH servers and edit the remote file:
% ~/.ssh/authorized-keys
Cut and paste the public key you generated.
Now configure pageant so that it recognizes your private key.
With putty, for example, ensure that the use of a password to connect to the various servers is no longer necessary.
GNU/Linux and MacOS
Although the principle is the same as the one set out above, the approach is somewhat different with GNU/Linux. Launch the following command in order to generate a public key/private key pair:
% ssh-keygen -t rsa
Do not protect your key with a passphrase. Make sure your SSH Agent has been launched (the ssh-agent process). Then copy your public key onto the servers with which you will want to connect later:
% ssh-copy-id user@host
The connection should now be possible without a password request.
Configuration of the Application
If you have not done so via the configuration assistant displayed when used for the first time, you must add at least one Atelier B server before being able to use the Parallelizer. In all cases, the configuration may be completed by selecting “Edition/Preference” in the menu. A new window will open. Fill in the correct user name – SSH login name that was configured so that the connection with the servers is automatic and does not require a password, and indicate the names of the servers one by one (or their IP addresses), as well as the information on the number of cores (or processors) available on the relevant server.
Use
After the configuration and inclusion of at least one Atelier B server, the list of B projects available on this server must have been updated. You can then select one.
A simple left-click in the project list on the main window then allows for the opening and retrieval of the global current status of the project.
The selection of the project machines on the interface is then intuitive, as is the assignment of the tasks to be performed. These tasks will be executed as soon as possible in accordance with the availability of resources.
The operations available and implemented in the parallelizer that can be effected on the components are as follows:
- Verification of types
- Generation of proof obligations
- Proof.
These options are available by selecting the components on which you want to work, then right-clicking on the selection, or via the general “Action” menu once the components have been selected.
The BBatch output for a specific task may be requested by clicking on the relevant task and selecting “Display the BBatch output” in the pull-down menu.
English
French 
