Abstract FR:

Cette thèse concerne la formalisation des problèmes de concurrence dans les systèmes parallèles. Un comportement parallèle de plusieurs processus étant représenté par un mot obtenu par mélange des actions de ces processus, sont considérés comme corrects les comportements sérialisables, i. E. Pour lesquels l'ordre des actions dites conflictuelles est le même que pour un comportement résultant d'une exécution séquentielle de ces processus. Des exemples d'application montrent que l'on peut ainsi aborder des problèmes de synchronisation de nature aussi différente que les accès concurrents à une Base de données, le partage de ressources ou encore certains problèmes de robotique. Dans un premier temps les processus sont des suites d'actions autorisées à se répéter un nombre arbitrairement grand de fois et l'on montre que l'ensemble des calculs sérialisables est reconnaissable par un automate fini. Ce modèle est ensuite généralisé dans deux directions: -on affine le critère de sérialisabilité en le définissant à partir d'un ensemble de relations de conflit différentes. Cette nouvelle notion permet de caractériser le problème de l'exclusion mutuelle. - on aborde le problème de la synchronisation de programmes concurrents en considérant les processus comme des ensembles (finis ou infinis) de mots. Après avoir étendu la notion de sérialisabilité à ce nouveau modèle, on montre que le contrôle optimal de tels processus peut également être obtenu à partir d'un automate fini. D'autres algorithmes de synchronisation sont étudiés et l'on montre en particulier l'existence d'un algorithme de sérialisation équitable au sens où les processus du système considéré sont exécutés au terme d'un délai fini