Cette thèse se propose d'étudier des problèmes de factorisations des régions cubiques. Dans le cadre de l'analyse de programme concurrent via des méthodes issues de la topologie algébrique, les régions cubiques sont un modèle géométrique simple mais expressif de la concurrence. Tout programme concurrent (sans boucle ni branchement) est ainsi représenté comme sous partie de R^n auquel on enlève des cubes interdits représentant les états du programme interdit par les contraintes de la concurrence (mutex par exemple) où n est le nombre de processus. La première partie de cette thèse s’intéresse à la question d'indépendance des processus. Cette question est cruciale dans l'analyse de programme non concurrent car elle permet de simplifier l'analyse en séparant le programme en groupe de processus indépendants. Dans le modèle géométrique d'un programme, l'indépendance se traduit comme une factorisation modulo permutation des processus. Ainsi le but de cette section est de donner un algorithme effectif de factorisation des régions cubiques et de le démontrer. L'algorithme donné est relativement simple et généralise l'algorithme très intuitif suivant (dit algorithme syntaxique). A partir du programme, on met dans un même groupe les processus qui partagent une ressource, puis l’on prend la clôture transitive de cette relation. Le nouvel algorithme s'effectue de la même manière, cependant il supprime certaines de ces relations. En effet par des jeux d'inclusion entre cubes interdits, il est possible d'avoir deux processus qui partagent une ressource mais qui sont toutefois indépendant. Ainsi la nouvelle relation est obtenue en regardant l'ensemble des cubes maximaux de la région interdite. Lorsque deux coordonnées sont différentes de R dans un cube maximal on dira qu’elles sont reliées. Il suffit alors de faire la clôture transitive de cette relation pour obtenir la factorisation optimale. La seconde partie de ce manuscrit s'intéresse à un invariant catégorique que l'on peut définir sur une région cubique. Celui-ci découpe la région cubique en cubes appelés "dés" auxquels on associe une catégorie appelée catégorie émincée de la région cubique. On peut voir cette catégorie comme un intermédiaire fini entre la catégorie des composantes et la catégorie fondamentale. On peut ainsi montrer que lorsque la région cubique factorise alors la catégorie émincée associée va elle-même se factoriser. Cependant la réciproque est plus compliquée et de nombreux contre exemples empêchent une réciproque totale. La troisième et dernière partie de cette thèse s'intéresse à la structure de produit tensoriel que l'on peut mettre sur les régions cubiques. En remarquant comment les opérations booléennes sur une région cubique peuvent être obtenues à partir des opérations sur les régions cubiques de dimension inférieure, on tente de voir ces régions cubiques comme un produit tensoriel des régions de dimension inférieure. La structure de produit tensoriel est hautement dépendante de la catégorie dans laquelle on la considère. Dans ce cas, si l'on considère le produit dans les algèbres de Boole, le résultat n'est pas celui souhaité. Au final il se trouve que le produit tensoriel dans la catégorie des demi-treillis avec zéro donne le résultat voulu. / This thesis studies some problems of the factorization of cubical areas. In the setting of analysis of programs through methods coming from algebraic topology, cubical areas are geometric models used to understand concurrency. Any concurrent programs (without loops nor branchings) can be seen as a subset of R^n where we remove some cubes which contains the states forbidden by the concurrency (think of a mutex) and where n is the number of process in the program. The first part of this thesis is interested in the question the independence of process. This question is particularly important to analyse a program, indeed being able to separate groups of process into independent part will greatly reduce the complexity of the analysis. In the geometric model, the independency is seen as a factorization up to permutation of processes. Hence the goal is to give a new effective algorithm which factorizes cubical areas, and proves that it does. The given algorithm is quite straightforward and is a generalization of the following algorithm (that we called syntactic algorithm). From the written program, groups together process that shares a resource, then take the transitive closure of this relation. This algorithm is not always optimal in that it can groups together process that actually could be separated. Thus we create a new (more relax) relationship between process. From the maximal cubes of the forbidden area of the program, if two coordinate are not equal to R, then groups them together. We can then take the transitive closure of this and get the optimal factorization. Each cube is an object of the category and between two adjacent cubes is an arrow. We can see that this category is in between the fundamental category and the components category of the cubical area. We can then show that if the cubical area factorize then so does the minced category. The reciprocal is harder to get. Indeed there's a few counter example on which we cant go back. The third and last part of this thesis is interested in seeing cubical areas as some kind of product over lower dimension cubical areas. By looking at how the booleans operations of a cubical area arise from the same operation on lower dimensional cubical areas we understand that it can be expressed as a tensor product. A tensor product is highly dependent on the category on which it is built upon. We show that to take the category of Boolean algebra is too restrictive and gives trivial result, while the category of semi-lattice with zeros works well. are not equal to R, then groups them together. We can then take the transitive closure of this and get the optimal factorization. The second part of this thesis looks at some categorical invariant that we define over cubical areas. These categories (called the minced category) slice the space into cubes.
| Identifer | oai:union.ndltd.org:theses.fr/2017SACLS542 |
| Date | 11 December 2017 |
| Creators | Ninin, Nicolas |
| Contributors | Université Paris-Saclay (ComUE), Curien, Pierre-Louis |
| Source Sets | Dépôt national des thèses électroniques françaises |
| Language | French |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation, Text |
Page generated in 0.0023 seconds