Application d’une méthode pour montrer qu’une parallélisation est correcte
Pendant un cours de processus concurrents et parallélisme, je me suis questionné sur la difficulté de démontrer qu’un programme séquentiel est pareil à sa version parallèle. J’ai découvert qu’il est possible de prouver avec exactitude cette équivalence de manière non exhaustive. C’est ainsi qu’en tant que néophyte en matière de système de preuve appliqué à l’informatique, j’ai exploré une méthode qui me semblait applicable dans un laps de temps raisonnable.
Cet ouvrage s’attarde principalement à une méthode qui a été développée dans la thèse de Raphaël Couturier, à l’époque étudiant au doctorat en informatique. Dans un premier temps, je ferai une description de cette méthode. Ensuite, je décrirai un programme séquentiel, servant à faire une sommation, que j’ai écrite dans le but de servir d’exemple d’application. Je décrirai aussi comment je me suis pris pour faire sa parallélisation. Un second programme pour briser des mots de passe sera aussi décrit de la même façon, mais je n’ai pas écrit le code étant donné sa trivialité. Après, je commencerai les exemples d’applications en élaborant les post-conditions nécessaires. Pour terminer, j’appliquerai la preuve au programme servant à briser les mots de passe.