# A syntactic approach to the directed semantics of programs

Aly-Bora Ulusoy

<figure><img src="image_1.png" /></figure>

## To cite this version:

Aly-Bora Ulusoy. A syntactic approach to the directed semantics of programs. Computer Science [cs]. Ecole Polytechnique (Palaiseau, France), 2023. English. NNT: 2023IPPAX139. tel-04610758

HAL Id: tel-04610758

https://hal.science/tel-04610758

Submitted on 13 Jun 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>
# Une approche syntactique à la sémantique dirigée des programmes

Thèse de doctorat de l'Institut Polytechnique de Paris préparée à École Polytechnique

École doctorale n°626 École doctorale de l'Institut Polytechnique de Paris (EDIPP)
Spécialité de doctorat : Mathématiques et Informatique

Thèse présentée et soutenue à Palaiseau, le 8 Décembre 2023, par

Aly-Bora Ulusoy

## Composition du Jury :

<table><tr><td>Jean-Cristophe Filliâtre<br/>Directeur de recherche, ENS Paris-Saclay (LMF)</td><td>Président</td></tr><tr><td>Georg Struth<br/>Professeur, University of Sheffield</td><td>Rapporteur</td></tr><tr><td>Jean Goubault-Larrecq<br/>Professeur, ENS Paris-Saclay (LSV)</td><td>Rapporteur</td></tr><tr><td>Lisbeth Fajstrup<br/>Associate Professor, Aalborg University</td><td>Examineur</td></tr><tr><td>Claudia Faggian<br/>Chargée de recherche, IRIF</td><td>Examineur</td></tr><tr><td>Samuel Mimram<br/>Professeur, École Polytechnique (LIX)</td><td>Directeur de thèse</td></tr><tr><td>Emmanuel Haucourt<br/>Professeur, École Polytechnique (LIX)</td><td>Co-directeur de thèse</td></tr><tr><td>Paul-André Melliès<br/>Directeur de recherche, IRIF</td><td>Invité</td></tr></table>
Not startled, like a lion at sounds

Not snared, like the wind in a net

Not soiled, like a lotus by water

Like the horn of the rhinoceros

Wander alone

Without resistance in all directions

Content with whatever you get

Enduring troubles undismayed

Like the horn of the rhinoceros

Wander alone

However, should you find a companion

Upon whose soul you can rest yours

Across all manner of adversity

Brimming with joy

Wander with him

– Extracts from the *Rhinoceros Sutra*
Acknowledgments

"If something seems impossible, you probably haven't tried asking for help."

– Meeting of Minds

This thesis is not the product of a lone existence, existing in a perfect frictionless void. This work is the accumulation of a thousand insignificant everyday events that piled up to become science. So without further ado, and in no particular order, I would like to express my thanks to all those who have accompanied me during these three and a half years, through the good times and the not so good times.

Although I just announced that I would not play favourites, it doesn't feel quite right not starting by thanking my family. For the twenty-seven years of love and support, for always believing in me, for giving me everything that I could ever want or need, I don't think there are enough words to thank you, Mom. And Joy, my dear sister, although we bicker and fight all the time, you should know that you have always inspired me, and without you paving the way, I probably wouldn't be here today, so take my thanks, and please don't be too smug about it.

Now, although some might jest that I wasn't seem much, I want to thank all my fellow doctoral students from the lab. First to Roman and Mehdi, with whom I shared office and tips on surviving the thesis and its administrative maze. To Nan, who never failed to show up during the rough covid times so that people wouldn't be alone in the lab. To Bernardo and Nathan, who listened to me ramble on about my life while stealing some snacks. To Martin and Ricardo, and all the others who brought board games to the office. To Maria for all the times when you reminded me of some important administrative task I had forgotten. And to all others for making the lab an amazing place. Thank you.

Unto those, which fate has brought close and far, I have the privilege to call friends. First to my oldest friend, Makarije, a hundred thanks for staying all these years. I hope this friendship can last for the next fifteen years. Then the same for Nathan and Etienne, for being the amazing people and flatmates that they are. Pierre, Martin, Andrey and Raphaël for being equally awesome and sharing our daily lives. Valentin and Eve, for lending their ears to my problems. Yann and Thibault for all the game sessions that may or may not have been during my working hours. Athénaïs, for the pickles. Mateï, for following me in my dumbest ideas and never failing to out dumb me. And the many others, for being who they are, for being my friends.

As we arrive towards the end, I want to thank all the members of my jury. Jean-Cristophe, Paul-André, Claudia and Lisbeth, great researchers whose name I am very proud to have figure in this thesis. I would also like to particularly thank both my
reviewers, Jean and Georg, who generously accepted to make some room in their packed
scheduled, with little time to spare, to review my thesis. Their advice helped achieve
the manuscript you read today. A thesis, that, thanks to their guidance, I am proud to
present today.

Finally, the last but not least, a great thanks to the best supervisors, Sam and Manu,
who helped me reach the end of this three year odyssey.
# Contents

<table><tr><td>Introduction (Français)</td><td>1</td></tr><tr><td>Introduction</td><td>9</td></tr><tr><td>1 Directed topological models of concurrency</td><td>19</td></tr><tr><td>1.1 Concurrent programming languages</td><td>19</td></tr><tr><td>1.1.1 A toy language for concurrent programs</td><td>19</td></tr><tr><td>1.1.2 Operational semantics</td><td>21</td></tr><tr><td>1.1.3 Toward verification of programs</td><td>25</td></tr><tr><td>1.2 Control flow graphs</td><td>28</td></tr><tr><td>1.2.1 Transition graphs</td><td>28</td></tr><tr><td>1.2.2 Introducing resources</td><td>31</td></tr><tr><td>1.2.3 Conservative programs</td><td>33</td></tr><tr><td>1.2.4 Pruned transition graph</td><td>35</td></tr><tr><td>1.3 Directed geometric semantics</td><td>37</td></tr><tr><td>1.3.1 Asynchronous semantics</td><td>37</td></tr><tr><td>1.3.2 Geometric semantics</td><td>45</td></tr><tr><td>1.3.3 Homotopy in directed algebraic topology</td><td>50</td></tr><tr><td>1.4 The boolean algebra of cubical regions</td><td>56</td></tr><tr><td>1.4.1 Cubical cover of simple programs</td><td>57</td></tr><tr><td>1.4.2 Maximal cubical covers</td><td>58</td></tr><tr><td>1.4.3 Computing deadlocks</td><td>60</td></tr><tr><td>2 Factoring models of programs</td><td>67</td></tr><tr><td>2.1 Factorisation à la Ninin</td><td>68</td></tr><tr><td>2.1.1 Independent processes</td><td>68</td></tr><tr><td>2.1.2 The free commutative monoid of cubical covers</td><td>69</td></tr><tr><td>2.1.3 Factorization and partition</td><td>71</td></tr><tr><td>2.2 The category of components</td><td>73</td></tr><tr><td>2.2.1 Category of components of loop-free programs</td><td>73</td></tr><tr><td>2.2.2 Computing the category of components of loop-free programs</td><td>77</td></tr><tr><td>2.3 Factoring loop-free categories</td><td>78</td></tr><tr><td>2.3.1 Properties of loop-free categories</td><td>79</td></tr><tr><td>2.3.2 Hashimoto's theorem for loop-free categories</td><td>81</td></tr><tr><td>3 A syntactic model of programs</td><td>99</td></tr><tr><td>3.1 Syntactic semantics of concurrent programs</td><td>100</td></tr></table>
<table><tbody><tr><td>3.1.1</td><td>Positions in programs</td><td>100</td></tr><tr><td>3.1.2</td><td>A partial order on positions</td><td>106</td></tr><tr><td>3.1.3</td><td>Syntactic semantics properties</td><td>109</td></tr><tr><td>3.2</td><td>The boolean algebra of syntactic regions</td><td>113</td></tr><tr><td>3.2.1</td><td>Cubes and regions of posets</td><td>113</td></tr><tr><td>3.2.2</td><td>Finitely complemented regions</td><td>118</td></tr><tr><td>3.2.3</td><td>Boolean algebra of finitely complemented regions</td><td>125</td></tr><tr><td>3.3</td><td>Syntactic covers of programs</td><td>129</td></tr><tr><td>3.3.1</td><td>Computing covers and complements</td><td>129</td></tr><tr><td>3.3.2</td><td>Implementation</td><td>133</td></tr><tr><td>4</td><td>Handling programs with loops</td><td>153</td></tr><tr><td>4.1</td><td>Finite unfolding of concurrent programs</td><td>154</td></tr><tr><td>4.1.1</td><td>Finite unfolding techniques in directed models</td><td>154</td></tr><tr><td>4.1.2</td><td>Slight adjustment to the syntactic model</td><td>160</td></tr><tr><td>4.1.3</td><td>2-unfolding of programs: syntactic version</td><td>166</td></tr><tr><td>4.2</td><td>Syntactic cubical covers for programs with loops</td><td>169</td></tr><tr><td>4.2.1</td><td>Generalizing syntactic cubes</td><td>171</td></tr><tr><td>4.2.2</td><td>Characterizing cubes of the unfolding</td><td>179</td></tr><tr><td>4.2.3</td><td>Covers and normal forms</td><td>189</td></tr><tr><td>4.3</td><td>Unfolding conservative covers of loops</td><td>190</td></tr><tr><td>4.3.1</td><td>Conservative regions and covers</td><td>191</td></tr><tr><td>4.3.2</td><td>Lifting covers of loops</td><td>197</td></tr><tr><td>4.3.3</td><td>Maximal cubical cover as a quotient of the 2-unfolding</td><td>201</td></tr><tr><td>4.4</td><td>Deadlock detection algorithm for looped programs</td><td>213</td></tr><tr><td>4.4.1</td><td>Cubical partition and loops</td><td>214</td></tr><tr><td>4.4.2</td><td>Cubical partition as a quotient of the 2-unfolding</td><td>219</td></tr><tr><td>4.4.3</td><td>Deadlock computation for programs with loops</td><td>244</td></tr><tr><td>5</td><td>Perspectives</td><td>253</td></tr><tr><td>A</td><td>Technical Background</td><td>257</td></tr><tr><td>A.1</td><td>Category theory</td><td>257</td></tr><tr><td>A.2</td><td>Order theory</td><td>261</td></tr><tr><td>A.3</td><td>Topology</td><td>263</td></tr></tbody></table>
# Introduction (Français)

## Vérification de programmes concurrents

### Le Dîner des Philosophes

Nous sommes en l'an 2000. Le monde est très différent depuis la révolte robotique de la fin des années 90. Trois philosophes, Hume, Wittgenstein et Russell, ramenés à la vie pour lutter contre la menace mécanique, sont en train de dîner. Cependant, l'humanité est en train de perdre la guerre et leurs vivres s'amenuisent.

À leur table, seules trois baguettes ont été placées. Une entre chacune de leurs places. Chacun des philosophes suit un ordre strict pour leur dîner qu'ils ne briseront pour rien au monde :

1. Prendre la baguette à leur droite.

2. Prendre la baguette à leur gauche.

3. Manger leur repas.

4. Reposer la baguette à leur droite.

5. Reposer la baguette à leur gauche.

Si l'un des philosophes arrive à saisir deux baguettes, alors tous les philosophes pourront manger leur dîner et reprendre leurs efforts pour sauver l'humanité. Cependant, si tous récupèrent la baguette à leur droite en même temps, ils seront piégés éternellement à attendre que leur voisin respectif libère sa baguette. Têtus comme ils sont, l'humanité finira par périr avant qu'un seul des philosophes ne commence son repas.

### Programmes concurrents

Dans le cas hautement probable qu'une telle situation se produise, nous nous devons d'étudier de tels problèmes. Heureusement, ceux-ci sont liés à au cas plus concret d'accès concurrent aux ressources en programmation parallèle. En effet, le dîner des philosophes est un problème qui fut présenté par Dijkstra dans [12]. Dans cet exemple, chaque philosophe représente un processus en parallèle et les baguettes, une ressource qu'ils peuvent protéger (verrouiller) avant d'effectuer leurs tâches pour s'assurer qu'aucun autre processus n'ait accès à la même ressource au même moment. Lorsque l'accès et l'écriture à la mémoire ne sont pas des opérations atomiques, la modification de la mémoire peut avoir des résultats incontrôlables. D'où l'importance d'utiliser de telles pratiques.

L'utilisation de programmes concurrents est de plus en plus répandue, mais ces programmes sont notoirement plus complexes à concevoir et à vérifier. Les propriétés du
programme (comme l'atteignabilité d'un état) doivent être vérifiées indépendamment de l'ordre relatif dans lequel chaque instruction des différents processus en parallèle est exécutée.

Historiquement, les premiers modèles de la concurrence furent les *modèles d'entrelace-ments*. Ces modèles sont construits à partir de toutes les différentes exécutions possibles d'un programme. Par exemple, en considérant le programme $x:=1||y:=2$, composé de deux instructions d'affectation exécutées en parallèle. Le modèle d'entrelacement associé serait le graphe suivant avec quatre sommets et quatre arêtes.

<figure><img src="image_3.png" /></figure>

Les deux ordonnancements potentiels des affectations $x:=1$ et $y:=2$ sont données par les chemins maximaux libellés par $x:=1 \cdot y:=2$ et $y:=2 \cdot x:=1$. En théorie, il serait possible d'appliquer des techniques de vérifications classiques de programmation séquentielle sur chacun des ordonnancements possibles. En pratique, ceci n'est pas faisable, car le nombre d'entrelacements grandit exponentiellement avec la taille du programme.

La sémantique ci-dessus ne distingue pas si deux actions sont indépendantes ou non. En effet, dans notre cas, les deux exécutions mènent au même état à la fin des instructions $x:=1$ et $y:=2$, que nous définissons comme étant indépendantes. Ce ne serait pas le cas si, par exemple, nous remplacions l'instruction $y:=2$ par l'instruction $x:=2$. En effet, dans ce cas, la dernière instruction exécutée détermine l'état final de la mémoire.

Lorsque deux ordonnancements sont identiques à permutation d'instructions indépendantes près, on dit qu'ils sont équivalents. Dans un tel cas, au lieu de vérifier chaque ordonnancement, il suffit d'en vérifier un seul par classe d'équivalence.

## True Concurrency

La remarque du dessus suggère qu'un modèle des programmes concurrent ne devrait pas seulement prendre en compte tous les ordonnancements possibles d'un programme, mais également la commutation d'instructions indépendantes, appelé *True Concurrency*. À fin de distinguer les chemins indépendants de ceux qui ne le sont pas, les graphes sont équipés d'une relation ~ sur les chemins, qui indique leur équivalence. Nous obtenons ainsi, ce qu'on appelle des *graphes asynchrones*. Celui associé à notre exemple précédent est fourni ci-dessous.

<figure><img src="image_4.png" /></figure>

<figure><img src="image_5.png" /></figure>
La plupart des systèmes d’exploitations, fournissent un cas particulier des ressources abordées précédemment, appelées des mutex, qui ne peuvent être verrouillées par au plus un seul processus à la fois. Étant donné un mutex *a*, un processus peut soit verrouiller le mutex avec l’instruction $P_a$, soit le libérer avec l’instruction $V_a$. À l’instar de nos philosophes attendant leur baguette, un processus essayant de verrouiller un mutex qui l’est déjà sera figé en l’attente de celui-ci. L’utilisation de ces instructions a deux effets sur la sémantique de nos programmes : elle interdit l’accès à certains états de la mémoire (ceux qui correspondent au verrouillage d’un mutex par deux processus distinct simultanément) et par cette action déclare certains chemins comme explicitement non-équivalents. La sémantique des programmes $(A; B) \parallel (A; B)$ et $(P_a; V_a) \parallel (P_a; V_a)$ est respectivement donnée ci-dessous.

<figure><img src="image_6.png" /></figure>

<figure><img src="image_7.png" /></figure>

Dans le graphe de gauche, toute paire de chemin du début à la fin du graphe est équivalente, alors que dans le graphe de droite (obtenu en retirant les positions “interdites”), il n’y a plus aucun chemin équivalent. La plupart des modèles de la concurrence que nous présentons dans cette thèse supposeront que la consommation (la différence entre le nombre de fois qu’une ressource donnée est verrouillée et libérée) ne dépend pas du chemin choisit, mais uniquement de ses extrémités. De tels programmes sont appelés *conservatifs*. Ceci peut paraître restrictif, mais en plus d’être théoriquement très utile, c’est aussi une pratique standard imposée par beaucoup de systèmes concurrents.

## Géométrie des programmes

Dans les graphes asynchrones présentés précédemment, l’exécution de programme correspond à des chemins sur les graphes. Les carrés commutatifs peuvent être vus comme des carrés “remplis”, qui intuitivement permettent d’effectuer des déformations continues entre les chemins sur les extrémités de ce carré. Ces modèles auraient donc une structure algébrique avec une interprétation géométrique agréable. Ils correspondent à des espaces topologiques dans lesquels l’exécution correspond à des chemins et les équivalences d’instructions correspond à l’homotopie de chemin, c’est-à-dire une équivalence à déformation continue près.

Par exemple, nous pouvons associer au programme $(P_a; P_b; V_b; V_a) \parallel (P_b; P_a; V_a; V_b)$, appelé la *Croix Suisse* l’espace topologique ci-dessous, qui correspond au complémentaire de la région grisée dans l’espace $[0, 1] \times [0, 1]$. Les points de la région grisée correspondent aux positions interdites précédemment mentionnées, qui sont obtenues par double verrouillage d’un mutex.
<figure><img src="image_8.png" /></figure>

Dans cet espace, les chemins qui commencent dans le coin en bas à gauche et qui sont "croissants", c'est-à-dire ceux qui vont vers le haut et la droite, correspondent aux exécutions. Par exemple, le chemin en pointillés correspond à l'ordonnancement où toutes les instructions du premier processus sont exécutées en premier, puis toutes celles du deuxième processus.

Les chemins qui ne sont pas croissants ne correspondent pas à l'exécution d'un programme, qui ne peut se faire que dans une direction, celle du temps. C'est pourquoi nous avons besoin de considérer une variante dirigée des espaces topologiques, équipés de structure supplémentaire qui spécifie la direction du temps et quels chemins sont croissants.

On peut donc étudier une notion d'homotopie dirigée, qui doit une fois de plus correspondre aux classes d'équivalence d'exécution. Le sémantique topologique dirigée peut être reliée à nos graphes asynchrones, en effet en comparant notre exemple précédent, il semble y avoir un lien fort entre les deux.

## Vérification de programmes

Cette connexion entre la topologie algébrique et la sémantique de programmes concurrents nous fournit un nouveau point de vue sur ces programmes et permet de formuler de nouveaux algorithmes pour leur vérification.

<figure><img src="image_9.png" /></figure>

Dans la sémantique ci-dessus, le point *d* est un deadlock. De ce point, il n'y a aucun chemin strictement croissant, c'est-à-dire qu'aucune instruction ne peut être exécutée. Ce problème est spécifique aux programmes concurrents et arrive lorsque des processus (ou des philosophes) attendent mutuellement que l'autre libère une ressource (ou une baguette) Tous les points qui peuvent atteindre un deadlock par un chemin "dirigé" sont appelés à risque. Ils sont représentés par le carré en bas à gauche. Des points qui ne
peuvent qu'atteindre un deadlock sont appelés *condamnés*. Les points du carré en haut à droite sont *inatteignables*. Ils ne peuvent pas être atteint depuis un chemin dirigé partant du début de notre exécution. Ces points ne sont pas aussi problématiques que les précédents, mais peuvent révéler des défauts de conception dans le code (dont toutes les instructions devraient avoir une utilité).

Une autre application des techniques géométriques est la réduction du nombre de chemins et d'états à explorer. Ces méthodes sont basées sur l'idée que des chemins équivalents correspondent à des chemins homotopes. De la sémantique topologique dirigée d'un programme, une description compacte peut être obtenue par la *catégorie de composantes* qui identifie les parties du programme où "rien ne se passe" du point de vue de la concurrence. Reprenons l'exemple de la Croix Suisse. Sa catégorie de composante est donnée plus bas, où la commutation des diagrammes est signalée par $\sim$.

<figure><img src="image_10.png" /></figure>

## Représentation efficace des programmes

Un des problèmes des modèles topologiques est que l'espace d'états est infini, et donc difficilement implémentable. Ceci a motivé la recherche d'une représentation efficace des espaces topologiques dirigés. Dans le cas de la composition parallèle de $n$ processus séquentiels (sans branchements, ni boucles), appelé un *programme simple*, la sémantique géométrique associée est une version dirigée du $n$-cube standard $[0, 1]^n$, duquel un nombre fini de cube de dimension $n$ ont été retirés. Dans cette situation, il est possible de recouvrir l'espace par un ensemble fini de $n$-cubes, que l'on appelle un recouvrement cubique. Un espace admettant un tel recouvrement est appelé une région cubique. Ces régions sont d'un intérêt particulier, car les régions interdites et leur complémentaire sont des régions cubiques.

<figure><img src="image_11.png" /></figure>

Nous remarquons facilement que toutes les représentations d'un même espace $X \subseteq [0, 1]^n$ par un recouvrement cubique ne sont pas d'une qualité égale. En effet, dans les recouvrements de l'exemple ci-dessus, le recouvrement de gauche, composé de 8 est moins efficace que celui de droite qui ne contient que 4 cubes. Nous verrons qu'il existe en effet une notion naturelle de "meilleure" représentation cubique pour un espace donné, qui corre-
spond à tous les n-cubes maximaux par la taille qu'il contient. Dans l'exemple ci-dessus, cela correspond au recouvrement sur la droite.

Cette représentation est le fondement des algorithmes de détection de deadlocks existant sur les modèles géométriques et contiennent une grande quantité d'information sur l'indépendance des instructions, qui permet de définir la catégorie de composante susmentionnée à partir de la donnée du recouvrement maximal.

## Factorisation des programmes concurrents

Une autre approche pour réduire l'espace d'états d'un programme simple est de le séparer en plusieurs groupes de processus indépendants. Des processus sont dit indépendants quand n'importe laquelle de leurs instructions peuvent être permutées dans un ordonnancement sans effet sur l'état du programme.

Ceci implique que pour deux processus $P_1$ et $P_2$, indépendants selon la définition ci-dessus, la sémantique géométrique de leur composition parallèle sera obtenue comme le produit de la sémantique de $P_1$ et de celle de $P_2$. Cette propriété s'étend également à la catégorie de composantes et d'autres invariants dirigés de nos programmes. En un sens, cette indépendance est une généralisation de la notion d'indépendance des instructions présentée précédemment. Nous pourrons remarquer que l'existence d'une telle factorisation permet de décrire l'espace d'états de façon beaucoup plus compacte.

## Contributions

### Programmes concurrents et le théorème d'Hashimoto

Dans son papier [26], Hashimoto prouve un puissant théorème sur les ordres partiels dont tous les éléments sont connectés par des zigzags de comparaison. En effet, pour de tels ordres partiels, toute paire isomorphe de décomposition sous forme de produit admet une décomposition “plus fine”.

Plus précisément, dans un ordre partiel connecté, pour toute paire $\prod_{\alpha \in A} X_\alpha$ et $\prod_{\beta \in B} Y_\beta$ de décomposition en produit, il existe une décomposition $\prod_{\alpha \in A} \prod_{\beta \in B} Z_{\alpha,\beta}$ telle que $X_\alpha \cong \prod_{b \in B} Z_{\alpha,b}$ et $Y_\beta \cong \prod_{a \in A} Z_{a,\beta}$ pour tout $\alpha, \beta$. Cette propriété est appelée propriété de raffinement forte et implique, entre autre que pour tout ordre partiel fini, il existe une unique décomposition, à isomorphisme près, sous forme de produit d'ordres partiels irréductibles. Ce résultat est cependant beaucoup plus fort car la propriété de raffinement existe également pour des produits infinis.

Considérons l'espace euclidien $\mathbb{R}^3$ se décomposant des deux façons suivantes $\mathbb{R}^2 \times \mathbb{R}$ et $\mathbb{R} \times \mathbb{R}^2$. Nous avons le raffinement suivant $\mathbb{R} \times \mathbb{R} \times \mathbb{R} = \mathbb{R} \times \mathbb{R} \times \{*\} \times \mathbb{R}$ avec les affectations suivantes:

$$ Z_{1,1} = \mathbb{R} \qquad Z_{1,2} = \mathbb{R} \qquad Z_{2,1} = \{*\} \qquad Z_{2,2} = \mathbb{R} $$

Dans le chapitre 2, nous élargissons ce résultat pour le cas des catégories connectées sans boucles, qui sont des catégories sans endomorphismes non triviaux. Les catégories sans-boucles sont des généralisations directes des ensembles partiellement ordonnés, qui vérifient la même propriété (une sorte d'anti-symétrie généralisée). Contrairement aux ordres partiels, les catégories sans boucles peuvent admettre plusieurs morphismes en parallèles, les rendant plus complexes à étudier. Beaucoup des invariants mentionnés
précédemment, comme la catégorie de composante, sont des catégories sans boucle lorsque
le programme est lui-même sans boucle, ce qui motive notre approche.

L'existence d'une décomposition sous forme de produit de cette catégorie non seule-
ment réduit la taille des catégories à étudier, et donc de notre représentation, mais donne
également une factorisation de notre programme comme parallélisation de processus in-
dépendants.

Approche syntactique des programmes

Les modèles topologiques permettent l'utilisation d'outils et de résultats théoriques très
puissants. Cependant, ceux-ci n'amènent pas toujours aux algorithmes les plus simples
à implémenter. Nos travaux commencent par l'observation que pour beaucoup des outils
utilisés dans les sémantiques topologiques, très peu découlent des propriétés topologiques
de nos espaces, mais de la syntaxe des programmes. Dans le chapitre 3, nous définis-
sons un nouveau modèle de programmes, représenté par un ordre partiel induit par des
graphes dirigés. Au lieu de construire l'espace des états de façon globale, nous fournissons
des constructions inductives pour les états du programme qui permettent de représenter
plus efficacement l'espace d'états. Cela nous donne une représentation très intuitive des
positions de nos ordres partiels comme des préfixes d'une exécution.

Pour une unique instruction, nous ne considérons que deux états : $\perp$ (l'instruction n'a pas été exécutée) et $\top$ (l'instruction a été exécutée). Pour des constructions plus complexes, par exemple la composition séquentielle $P;Q$, nous définissons inductivement deux ensembles d'états possibles : $p;\perp$, où $p$ est un état de $P$ et $\top;q$, où $q$ est un état de $Q$. Pour la parallélisation $P\parallel Q$, les états sont définis par des paires d'états $p\parallel q$.

Nous obtenons des modèles très proches des graphes asynchrones, à la différence que nous ne retirons pas les positions interdites, mais que nous vérifions si celles-ci font parties des cubes que nous considérons. Même si cela ne parait pas très efficace, c'est ce qui nous permet de retrouver les constructions des modèles géométriques avec une implémentation efficace.

<figure><img src="image_12.png" /></figure>

<figure><img src="image_13.png" /></figure>

<figure><img src="image_14.png" /></figure>

Ensuite nous réimplémenterons la représentation compacte des régions autorisées et in-
terdites des programmes par des ensembles de cubes. Dans notre modèle, ces cubes sont
naturellement définis par des paires de positions $(p, q)$ de nos programmes qui recouvrent
des régions, que l'on appelle leur support, qui contient toutes les positions $x$ telles que
$p \le x \le q$. Nous obtenons des résultats similaires quant à l'existence d'une "meilleure
représentation" des régions par une couverture maximale dans le cas des programmes
conservatifs. Nous obtenons également un algorithme de détection de deadlock utilisant
les positions et cubes syntaxiques, dont une implémentation est donnée sur notre site
internet<fnref n="1" />. Notre implémentation supporte un grand nombre de programme conservatifs,

<footnote n="1">¹https://smimram.github.io/sparkling/</footnote>
dont une petite librairie est donnée en exemple pour que le lecteur curieux puisse s'y
essayer. Notre implémentation, par la nature inductive de nos positions est très efficace
et plus intuitive que l'approche géométrique.

Vérification des programmes avec des boucles

La vérification des programmes avec des boucles est d'une complexité notoire et les pro-
grammes concurrents ne font pas exception à la règle.

Nombre des outils présentés dans le chapitre 1 échouent en présence de boucles. Dans
le chapitre 4, nous allons élargir notre modèle syntaxique afin de pouvoir appliquer les
algorithmes de détection de deadlock dans le cas de programmes avec des boucles. L'idée
derrière cette méthode est assez simple. Chaque boucle est remplacée par deux copies du
code qu'elle contient, composées de façon séquentielle.

<figure><img src="image_15.png" /></figure>

<figure><img src="image_16.png" /></figure>

Une piste similaire a déjà été explorée sur un algorithme de détection différent dans
le papier [17]. Cependant, la borne supérieure du nombre de dépliages nécessaire pour
obtenir la région à risque et condamnée est élevée.

Nous prouverons, qu'avec notre méthode, il suffit de déplier chaque boucle deux fois
afin d'obtenir les régions concernées. Nous obtenons ce résultat en élargissant la corre-
spondance entre les points du dépliage et du programme de base aux recouvrements cu-
biques de ceux-ci. Cette approche est bien plus compliquée, puisqu'elle implique d'élargir
la notion d'intervalle et de cube aux préordres.
# Introduction

## Verification of concurrent programs

### Dining Philosophers:

It is the distant future, the year 2000. The world is vastly different since the robotic up-rising of the mid-nineties. Three philosophers, Hume, Wittgenstein and Russell, brought back to life to fight against the machine threat, are having dinner. But the forces of humanity are losing the war and supplies are running low. At their table, only three chopsticks are set. One between each seat. The philosophers each follow a very strict order for their dinner, that they shall never break:

1. They take the chopstick to their right.

2. They take the chopstick to their left.

3. They eat their meal.

4. They put back the chopstick to their right

5. They put back the chopstick to their left.

Should one of the philosophers get access to both chopsticks, then all the philosophers can have their meal and resume their quest to free mankind. However, should they all get hold of the chopstick on their right at the same time, they will all be locked in a deadly contest, each waiting on each other to release the fateful cutlery on their left before doing anything else. Stubborn as they are, humanity shall perish at the hand of its unfeeling oppressor before a single philosopher has started its meal.

### Concurrent programs:

In case of such a highly probable situation ever occurring, we must study these problems, which are thankfully linked to the more concrete problem of concurrent access to resources in parallel programming. Indeed, the dining philosophers was an example introduced by Dijkstra in [12] to represent multiple processes running in parallel. In this example each of our philosopher represent a process and the chopsticks a resource, which they can protect (lock) before performing tasks to ensure that no other process accesses the same resource at the same time. This is important as in most models of memory, where access and writing to the memory is not an atomic operation, concurrent modification of the memory can have undefined results (two processes incrementing a variable by 1 at the same time might increase it by only 1 instead of 2).
The use of concurrent programs has become more and more widespread in order to exploit the features of more recent architectures (multicore processors, clouds, etc.), but they are notoriously complex to design and conceptualize. Properties of the program (such as not reaching a certain memory state) have to hold regardless of the relative order in which each instruction of the different processes constituting the program is executed.

Historically, the first models of concurrent programs were the *interleaving models*. These models essentially consist of all different possible executions of a program. For instance, considering the program $x:=1||y:=2$, consisting of two assignment instruction executed in parallel, the associated interleaving model would be the following graph with four vertices and four edges.

<figure><img src="image_17.png" /></figure>

The two possible interleaving of the assignments $x:=1$ and $y:=2$ are given by the maximal paths labelled by $x:=1 \cdot y:=2$ and $y:=2 \cdot x:=1$. In theory, we could apply traditional verification techniques for sequential program on each potential ordering. This is not feasible in practice because of the sheer number of these executions, which may grow exponentially with the size of the program.

One could remark that the semantics above does distinguish whether two actions are independent or not. Indeed, in our case both executions lead to the same state at the end of $x:=1$ and $y:=2$, which we define as being independent. This would not be the case if, for example we replace the instruction $y:=2$ with the instruction $x:=2$. Indeed, in that case, whichever instruction is executed last determines the final state of the memory.

When two schedulings are the same up to permutation of independent instructions, we say that they are *equivalent*. Then, instead of checking all the potential executions, one can simply check a single execution in each equivalence class to verify the properties of the program.

**True concurrency:**

This suggests that a model for concurrent programs should not only incorporate all possible schedulings of a program (as in traditional interleaving semantics), but also the commutation of independent instructions, following the principle of what is now called *true concurrency*. In order to distinguish between paths that are independent and those that are not the graphs are equipped with a relation $\sim$ on paths, indicating whether they are equivalent in the way explained above. We thus obtain what are called asynchronous graphs, given for our previous examples below:
<figure><img src="image_18.png" /></figure>

<figure><img src="image_19.png" /></figure>

Most operating systems offer a particular kind of resource, called a mutex, which can be held by at most one process at a time: given a mutex *a*, a process has either the option of locking or releasing the mutex by respectively performing the instructions $P_a$ or $V_a$. Like our philosophers waiting on their chopsticks, a process trying to lock a mutex held by another process will remain frozen until that resource is released. The usage of these instructions has two effects on the semantics: it forbids some states (any states that corresponds to two different process locking the same resource *a* with the instruction $P_a$ has to be removed) and through this process explicitly declares some paths as not equivalent. For instance, the semantics of $(A; B) \parallel (A; B)$ and $(P_a; V_a) \parallel (P_a; V_a)$ are respectively:

<figure><img src="image_20.png" /></figure>

<figure><img src="image_21.png" /></figure>

In the first graph, any two paths from start to finish are equivalent, while in the second graph, (which can be obtained by removing the “forbidden” central position and related vertices), there are no equivalent paths. Most of the models of concurrency we will present assume that two paths on our state space reaching the same point will have locked/released a given resource the same number of times. Meaning that the “consumption” of resources does not depend on the path but only the endpoints. We say that such programs are *conservative*. This is a very useful consideration in our study of concurrent programs which is also generally enforced in practice.

Geometry of programs:

In the asynchronous graph semantics presented above, the executions of the program correspond to paths in the graph. Moreover, squares equipped with $\sim$ can be seen as “filled squares” in which intuitively, there is room to allow for a deformation between the paths on the extremities of this square. This means that the resulting models bear algebraic structure with a nice geometric interpretation: roughly, they correspond to topological spaces, in which executions correspond to paths and the equivalence between two executions corresponds to a homotopy of paths, i.e. equivalence up to continuous deformation.

For instance, to the program $(P_a; P_b; V_b; V_a) \parallel (P_b; P_a; V_a; V_b)$, called the *Swiss Cross*, is associated the topological space on the right below, which correspond to the complement
of the darkened region in the space $[0, 1] \times [0, 1]$. Points in the darkened region correspond to the forbidden states mentioned above, which correspond to mutexes being locked twice.

<figure><img src="image_22.png" /></figure>

In this space, paths that start from the lower-left corner and which are “increasing”, i.e. they only go up and to the right, correspond to executions. As an example, the dotted path traced above, will correspond to the scheduling where all instructions of the first process are executed first followed by all instructions of the second process.

Paths which are not increasing do not make sense from a computational point of view, they cannot correspond to the execution of a program. Indeed, going in any other direction would be equivalent to “un-executing” an instruction. That is why, to study program one needs to consider a *directed* variant of topological spaces, which comes equipped with a notion of direction of time and extra structure that specifies which paths are directed.

One can then study the geometry of these spaces, and in particular the structure of these directed paths up to a suitable notion of homotopy, which should once again correspond to equivalence classes of executions, up to commutation of independent actions. The directed topological semantics can also be related to the asynchronous semantics. Indeed, if we compare our space to the asynchronous graph, there seems to be a strong link between the two.

## Verification of programs:

This connection between algebraic topology and the semantics of concurrent program provides us with a new point of view on those programs and allows for the formulation of new algorithms for their verification.

<figure><img src="image_23.png" /></figure>

In the semantics above, the point *d* is a *deadlock* point. Starting from this point, there is no strictly increasing path, i.e. no instructions can be executed. This kind of undesirable
behaviour is specific to concurrent programs, and occurs when processes (or philosophers) are waiting on each other to free up a resource (the chopsticks). All points that can reach a deadlock by a "directed" path, are called *unsafe*. They are represented in the lower left corner. They are states from which an execution might lead to a deadlock. If the only points that can be eventually reached are deadlocks, then the states are called *doomed*. Points, in the upper right corner, are called *unreachable*, they cannot be reached by a directed path from the initial state of the program, i.e. they are states that will never appear in an execution. While this is not a concern in itself, it reflects poor design in the programming (or worse). Based on the geometric characterization of these states, we can derive algorithms to compute them, providing guarantees about the programs' safety.

Another application of the geometric techniques is to reduce the number of paths and states to explore based on the idea that equivalent paths (in the sense of permutation of independent actions) correspond to homotopic paths. From the directed topological semantics of a program, a compact description can be obtained by the *category of components* which identifies portions of the program where “nothing happens” from the concurrent point of view. This is done by reducing these paths to identities. As an example, consider the Swiss Cross from above. We give below its category of components, where commutation of actions is expressed by $\sim$. In any of the regions delimited by dotted lines, any path we take does not change how we could have reached its endpoint state or the states we can reach later on.

<figure><img src="image_24.png" /></figure>

**Efficient representation of programs:**

One problem with our topological models is that the state space is infinite and thus difficult to implement. This, amongst other things, has motivated the quest for an efficient representation of the directed topological spaces we are dealing with. In the case of a parallel composition of *n* sequential processes, i.e. processes with no conditional branching or loops, called *simple programs*, the geometric semantics associated correspond to a directed version of the standard *n*-cube [0, 1]ⁿ, which consists of the product of *n* copies of the unit interval, with a finite number of cubes removed. In this situation we can cover the space with a finite set of *n*-cubes (product of *n* intervals), called a cubical cover, as shown in the example below. When a space admits a cubical cover, we say it is a cubical region, which will be of special interest as the set of forbidden positions and its complement do correspond to such regions.
<figure><img src="image_25.png" /></figure>

To represent a specific space $X \subseteq [0, 1]^n$ we can use a set of $n$-cubes, called a cover, which
cover the space. Indeed, in the example above, the cover on the left with 8 cubes is less
efficient, as it uses more intervals to talk about the same space as the cover on the right
(which only has 4). We will see that there is indeed a natural notion of maximal cover for
a given space, corresponding to all the maximal intervals that cover it. In the example
above, it does indeed correspond to the cover given on the right.

This representation is the basis of the existing deadlock detection algorithm imple-
mented on these geometric models, and also encodes much information about indepen-
dence of instructions, which allows one to define the category of components of the geo-
metric semantics of a simple program from the maximal cover.

**Factorization of concurrent programs:**

Another way of reducing the size of the state space of a simple program, is to split
it into several groups of processes running independently of each other. We say that
two processes are independent when any of their instructions can be permuted in any
scheduling without changing the outcome. What this implies is that for two processes
$P_1$ and $P_2$, independent in the sense above, the geometric semantics of their parallel
composition $P_1 \parallel P_2$ can be obtained as the product of the geometric semantics of $P_1$ and
the geometric semantics of $P_2$. This also extends to the category of components and
other invariants of our programs. In a sense, this is a generalization of the notion of
independence of instructions presented above. One should note that the existence of such
a factorization allows one to describe the state space in a much more compact way. This
process introduced in [31], is very similar to the factorization of integers as products of
prime factors or of polynomials as products of monomials, and it relies on the maximal
covers introduced above.

# Contributions

**Hashimoto's theorem and concurrent programs:**

In [26], Hashimoto has proved a powerful theorem, stating that, for partial orders where all elements are connected by a "zigzag" of comparisons, which we call connected posets, for any pair of isomorphic product decomposition, there exists a "finer" decomposition.

More precisely, in a connected poset, for any pair of product decompositions $\prod_{\alpha \in A} X_\alpha$
and $\prod_{\beta \in B} Y_\beta$ that are isomorphic, there exists a decomposition $\prod_{\alpha \in A} \prod_{\beta \in B} Z_{\alpha,\beta}$ such
that $X_\alpha \cong \prod_{b \in B} Z_{\alpha,b}$ and $Y_\beta \cong \prod_{a \in A} Z_{a,\beta}$ for any $\alpha, \beta$. This is called the *strict refinement property*, and it implies, among other things, that for any finite connected poset,
there exists a unique decomposition as a product of irreducible factors (up to isomorphism).
But this result is much more powerful than this, as it also gives a "better"
factorization for any pair of infinite products.
For example, if we look at the Euclidean space $\mathbb{R}^3$, for the decompositions $\mathbb{R}^2 \times \mathbb{R}$ and $\mathbb{R} \times \mathbb{R}^2$, we have a refinement $\mathbb{R} \times \mathbb{R} \times \mathbb{R} = \mathbb{R} \times \mathbb{R} \times \{\ast\} \times \mathbb{R}$ of these two decompositions by assigning:

$$Z_{1,1} = \mathbb{R}$$

$$Z_{1,2} = \mathbb{R}$$

$$Z_{2,1} = \{\ast\}$$

$$Z_{2,2} = \mathbb{R}$$

In Chapter 2, we extend this result to the case of connected loop-free categories, which are categories with no non-trivial endomorphisms. Loop-free categories are a natural generalization of posets, which when seen as categories verify the same condition (which can be seen as more general notion of antisymmetry). But contrary to posets, loop-free categories might admit multiple parallel morphisms. These categories are a natural setting in which most of the topological invariants used in practice naturally appear. One very important example is the category of components mentioned earlier, which gives a compact representation of our programs.

The existence of a product decomposition for this category not only naturally reduces the size of the categories to study, and thus of our representation of the state space, but will also give a factorization of our program as a composition of independent processes (whose actions can be freely permuted in the scheduling of an execution).

## A syntactic approach to programs:

Although topological models bring with them quite powerful tools and theoretical results, the resulting algorithms they lead to are notoriously hard to implement. Our work starts by observing that many of the tools that are actually used in the directed topological models (cubical covers, category of components...) can be directly defined from the discrete syntax of the program. Most constructions are consequences of the directed nature of this syntax, and the very restrictive structure of programs. In Chapter 3 we define a new model of programs, represented by partial orders induced by directed graphs, but instead of constructing the state space globally, we provide an inductive construction for the states themselves, which allows us to represent the state space more efficiently. This gives us a very natural interpretation of positions in our posets as prefixes of executions.

For a simple instruction, we consider only two positions $\perp$ (not executed) and $\top$ (already executed). For more complex constructions, for example sequential composition $P;Q$, we define inductively the possible positions: $p;\perp$, where $p$ is a position of $P$ and $\top;q$, with $q$ a state of $Q$. For parallel composition $P\parallel Q$, the positions are defined as pairs of positions $p\parallel q$.

We obtain models very close to asynchronous graphs, except that we do not remove the forbidden positions, but check if our cubes intersect with the set of forbidden cubes. This might appear less efficient, but not removing these positions is what allows us to get back the tools from directed topology efficiently, as the resulting sets of positions are extremely simple to define and intersection is not costly. Below, we can compare from left to right the asynchronous graph, directed geometric semantics and syntactic semantics of the program $P_a;V_a\parallel P_a;V_a$.
<figure><img src="image_26.png" /></figure>

<figure><img src="image_27.png" /></figure>

<figure><img src="image_28.png" /></figure>

Then, we re-implement the efficient representation of programs as sets of cubes, that are naturally defined by pairs of positions $(p, q)$ in our programs covering regions, that we call their supports comprising all points $x$ such that $p \le x \le q$. We obtain similar result for the existence of “best representation” of regions by a maximal cover in the case of conservative programs. We also obtain a similar deadlock detection algorithm using syntactic positions and cover, of which we give an implementation on our website<fnref n="2" /> which handles all conservative programs, with a small library of examples for the curious reader to try out. By the inductive nature of our syntactic states, we get a very efficient implementation of the verification algorithms of the geometric approach in the context of our syntactic model.

### Verification of program with loops:

The verification of concurrent programs with loops is notoriously more complicated, even in the topological setting which has inspired our work.

Many tools and algorithms that we will present in Chapter 1 fail in the presence of loops. In Chapter 4 we upgrade our new syntactic model to extend the deadlock detection algorithm that we adapted in Chapter 3. The idea behind the extension is quite simple. We replace each loop of our program by two copies of the code in the body of the loop, composed sequentially.

<figure><img src="image_29.png" /></figure>

<figure><img src="image_30.png" /></figure>

A similar idea has already been explored on a different algorithm in [17]. But the upper bound on the number of time a single loop must be unfolded in order to find the correct unsafe region is quite high.

We will prove that, with our method, all loops must be unfolded at most twice to recover the correct unsafe and doomed region of our program with loops. We obtain this by not only defining a correspondence between points of the state space of a program and its unfolding, but also proving that this correspondence extends to the cubical covers of these regions. This is much harder to do, as it requires extending the notion of cube/interval to states with loops.

<footnote n="2">²https://smimram.github.io/sparkling/</footnote>
Notations

We follow standard notation and write $\mathbb{N}$ for the set of positive integers, $\mathbb{Z}$ for the set of all integers and $\mathbb{R}$ for the set of real numbers. We write $\mathfrak{P}(X)$ for the powerset of a set $X$; $Y^c = X \setminus Y$ for the complement of any subset $Y$ of $X$. We write $[1:n]$ for the set $\{1, \dots, n\}$; and $]x,y[$ (resp. $[x,y]$) for open (resp. closed) intervals (Following French convention). All the classical concepts and definitions used throughout the thesis can be found in Appendix A
# Chapter 1

# Directed topological models of concurrency

> The story so far: In the beginning the Universe was created. This has made a lot of people very angry and been widely regarded as a bad move.

> - Douglas Adams, The Restaurant at the End of the Universe

In this chapter, we introduce models based on the trace space (the set of all possible executions and their effect on the memory) and verification techniques for concurrent programming languages. We introduce these models on the PIMP language, introduced in [18] which is a slightly modified a version of the IMP language [53], equipped to handle threads running in parallel. This language was chosen as a good compromise between more theoretical approaches (CCS, π-calculus [40]) and real world implementations (e.g. Java, POSIX) of parallel computing. After a brief introduction of the language and verification of programs (Section 1.1) we introduce a first simple model of programs (Section 1.2) and adapt it to deal with the specific problems of concurrent programming. Finally, we introduce a more complex model of programs from [18, Chapter 4] based on directed topology in Section 1.3 in order to introduce powerful algorithms based on topological tools to verify programs. In later chapters, we will present our new model of programs, aiming to conserve the powerful tools introduced in this last topological model. All the material of this chapter is heavily sourced and inspired from the presentation in [18].

## 1.1 Concurrent programming languages

### 1.1.1 A toy language for concurrent programs

**Definition 1.1.1.** Let Var be a fixed, countable set of variables. We define the language PIMP from four kinds of syntactic expressions, defined by their grammar:

* The set $\mathcal{A}$ of arithmetic expressions:

$$a ::= x \mid n \mid a + a \mid a * a$$

where $x$ is a variable in Var and $n \in \mathbb{N}$.
* The set $\mathcal{B}$ of boolean expressions, or conditions:

$$ b ::= \texttt{true} \mid \texttt{false} \mid a < a \mid b \text{ and } b \mid \neg b \mid \texttt{skip} $$

* The set $\mathcal{X}$ of actions:

$$ c_{act} ::= x := a \mid \texttt{skip} $$

* The set $\mathcal{C}$ of commands, or programs:

$$ c ::= c;c \mid \texttt{while } b \texttt{ do } c \mid \texttt{if } b \texttt{ then } c \texttt{ else } c \mid c \parallel c \mid c_{act} $$

A program is executed with regard to an environment (a certain state of the memory) consisting of the values of each variable, in other terms a function $\sigma: \texttt{Var} \to \mathbb{Z}$. In **PIMP**, variable values are restricted to integers for the sake of simplicity. Arithmetic (resp. boolean) expressions evaluate to integers (resp. boolean) in the usual way. Programs that do not contain the constructor $\parallel$ are called sequential program. We refer to standard textbooks [53] for details about these.

*Remark 1.1.2.* For any arithmetic (resp. boolean) function symbol $f: \mathcal{A}^k \to \mathcal{A}$ (respectively $g: \mathcal{B}^k \to \mathcal{B}$) of arity $k$, we could extend the grammar of $\mathcal{X}$ (resp. $\mathcal{B}$) with the constructors $f(a, \dots, a)$ (resp. $g(b, \dots, b)$). The rules we have given can also be seen as a special case of this definition.

The actions have an effect on the memory of the program and commands define the control flow (the structure) of the program. Their meaning is given in Section 1.1.1

<table><tr><td>x:=a</td><td>assign the evaluation of a to the variable x</td></tr><tr><td>skip</td><td>do nothing</td></tr><tr><td>c<sub>1</sub>;c<sub>2</sub></td><td>sequentially execute c<sub>1</sub> and then c<sub>2</sub></td></tr><tr><td>if b then c<sub>1</sub> else c<sub>2</sub></td><td>evaluate the boolean expression b and execute c<sub>1</sub> (resp. c<sub>2</sub>) if the result is true (resp. false)</td></tr><tr><td>while b do c</td><td>execute the command c as long as the boolean expression b evaluates to true</td></tr><tr><td>c<sub>1</sub> || c<sub>2</sub></td><td>execute the command c<sub>1</sub> in parallel with the command c<sub>2</sub></td></tr></table>

We will focus our study on concurrent programs, in which subprograms (also called threads or processes) run in parallel. These programs are used to exploit shared computing resources to their full potential, to take advantage of distributed architecture or to be more reactive to external events. This structure is the most prevalent in parallel computing and can be used to represent most parallel tasks.

*Example 1.1.3.* A simple instance of a parallel program would be distributed computing where a task (for example processing an image) is first separated by a sequence of instructions $p_i$ into multiple smaller tasks $p_1, \dots, p_k$ (processing a small part of the image) and then assembled back together by a sequence $p_f$. This program would look like

$$ p_i; (p_1 \parallel \dots \parallel p_k); p_f $$

*Remark 1.1.4.* In this thesis, we will suppose that the parallel execution of process is sequentially consistent. That is that “the result of any execution is the same as if the operations of all the processors were executed in some sequential order, and the operations
of each individual processor appear in this sequence in the order specified by its program”, as phrased in [34]. This is not the case for real multiprocessors with relaxed memory models [50]. We will nonetheless make this assumption for the sake of simplicity, but this approach could be refined to encompass semantics with relaxed memory models, even though most modern compilers help ensure sequentially consistent semantics at a higher level.

*Remark 1.1.5.* In the rest of this thesis, we only consider programs with finitely many threads. Although real programming languages allow for threads to be defined recursively, this would not cover much more practical cases and would introduce a lot more problems and technical details that we would have to work around. Indeed, the reachability of a state for finitely multithreaded programs is already PSPACE-complete [32], and becomes undecidable with recursive threads [47].

1.1.2 Operational semantics

Now that we have a language and programs, we need to describe in a formal way what it means to execute the program. We do this by describing a *semantics* for the language [53]. As described before, our programs consists mostly of actions, boolean expressions and arithmetic expression. These commands are executed w.r.t. to a state, which corresponds to the state of the memory (variables, etc.) and other resources available to the programs, and affect said state by their execution or return a value depending on it. For example, the execution of an action $x := 1$ would modify the memory cell corresponding to $x$ and replace its value by 1. Similarly, a boolean expression such as $x == 1$ would check the cell where $x$ is stored and return true or false depending on its value.

**Definition 1.1.6.** We write $\Sigma = \mathbb{Z}^{\text{Var}}$ for the set of states, consisting of functions assigning an integer to each variable. The initial state $\sigma_0 \in \Sigma$ is the constant function equal to 0. The *operational semantics* of our programming language consists of three functions:

• $\llbracket - \rrbracket_A : A \to (\Sigma \to \mathbb{Z})$ describing the evaluation of arithmetic expressions,

• $\llbracket - \rrbracket_B : B \to (\Sigma \to \mathbb{B})$ describing the evaluation of boolean expressions,

• $\llbracket - \rrbracket_X : \mathcal{X} \to (\Sigma \to \Sigma)$ describing the effect of actions on the state.

as well as a *reduction relation* $\to$ on pairs $(\sigma, c)$ consisting of a command $c \in C$ and a state $\sigma \in \Sigma$, which formally describes how a command evaluates in a given environment.

Thus, for instance, $\llbracket - \rrbracket_A$ sends each arithmetic expression to a function from the set of states $\Sigma$ to the set of integers (corresponding to the evaluation of the expression where the variables of the program have the values given in the state). Given $a \in A$, we thus write $\llbracket a \rrbracket_A : \Sigma \to \mathbb{Z}$ for its semantic interpretation and similarly for the other functions.

**Definition 1.1.7.** Let $x \in \text{Var}$, $n \in \mathbb{N}$, $f$ (resp. $g$) an arithmetic (resp. boolean) function of arity $k$. Given a state $\sigma \in \Sigma$. The *evaluation* of arithmetic expressions is defined as:

$$ \llbracket x \rrbracket_A(\sigma) = \sigma(x) \quad \llbracket n \rrbracket_A(\sigma) = n \quad \llbracket f(a_1, \dots, a_k) \rrbracket_A(\sigma) = f(\llbracket a_1 \rrbracket_A(\sigma), \dots, \llbracket a_k \rrbracket_A(\sigma)) $$

The *evaluation* of boolean expressions is defined as:

$$ \llbracket \text{true} \rrbracket_B(\sigma) = \top \quad \llbracket \text{false} \rrbracket_B(\sigma) = \bot \quad \llbracket g(b_1, \dots, b_k) \rrbracket_B(\sigma) = g(\llbracket b_1 \rrbracket_B(\sigma), \dots, \llbracket b_k \rrbracket_B(\sigma)) $$
And the evaluation of actions is defined as:

$$ \llbracket x := a \rrbracket_X(\sigma) = \sigma[x \mapsto \llbracket a \rrbracket_A(\sigma)] $$

where $\sigma[x \mapsto n]$ is the function which associates $n$ to $x$ and $\sigma(y)$ to each $y \neq x$.

In the following, when the context is clear we will drop the subscripts for $\llbracket - \rrbracket$. The skip actions plays a particular role in the reduction.

**Definition 1.1.8.** Let $x \in \text{Var}$, $b \in \mathcal{B}$, $a \in \mathcal{A}$. The reduction relation $\to$ is defined inductively by the following inference rules:

$$ \frac{\langle\sigma, c_1\rangle \to \langle\sigma', c'_1\rangle}{\langle\sigma, c_1; c_2\rangle \to \langle\sigma', c'_1; c_2\rangle} $$

$$ \overline{\langle\sigma, \text{skip}; c\rangle \to \langle\sigma, c\rangle} $$

$$ \frac{\langle\sigma, c_1\rangle \to \langle\sigma', c'_1\rangle}{\langle\sigma, c_1 \parallel c_2\rangle \to \langle\sigma', c'_1 \parallel c_2\rangle} $$

$$ \overline{\langle\sigma, c_2\rangle \to \langle\sigma', c'_2\rangle}{\langle\sigma, c_1 \parallel c_2\rangle \to \langle\sigma', c_1 \parallel c'_2\rangle} $$

$$ \overline{\langle\sigma, \text{skip} \parallel c\rangle \to \langle\sigma, c\rangle} $$

$$ \overline{\langle\sigma, c \parallel \text{skip}\rangle \to \langle\sigma, c\rangle} $$

$$ \frac{\llbracket b \rrbracket(\sigma) = \top}{\langle\sigma, \text{if } b \text{ then } c_1 \text{ else } c_2\rangle \to \langle\sigma, c_1\rangle} $$

$$ \frac{\llbracket b \rrbracket(\sigma) = \bot}{\langle\sigma, \text{if } b \text{ then } c_1 \text{ else } c_2\rangle \to \langle\sigma, c_2\rangle} $$

$$ \frac{\llbracket b \rrbracket(\sigma) = \top}{\langle\sigma, \text{while } b \text{ do } c\rangle \to \langle\sigma, c; \text{while } b \text{ do } c\rangle} $$

$$ \frac{\llbracket b \rrbracket(\sigma) = \bot}{\langle\sigma, \text{if } b \text{ then } c\rangle \to \langle\sigma, \text{skip}\rangle} $$

$$ \frac{c \in \mathcal{X} \setminus \{\text{skip}\}}{\langle\sigma, c\rangle \to \langle\llbracket c \rrbracket(\sigma), \text{skip}\rangle} $$

We write $\to^*$ for the reflexive, transitive closure of $\to$. Notice that for a given language, there can be many different semantics. Most of the constructions that follow depend on our choices and would be (slightly) different had we chosen a different semantics.

We will define the state space as the graph whose vertices are the states and the edges are the transitions, between states. Here we briefly recall, and fix some notations for directed graphs that will be used throughout the book.

**Definition 1.1.9.** A directed graph $G = (V, E, \partial^{-}, \partial^{+})$ consists of a set $V$ of vertices (or states), a set $E$ of edges and two functions $\partial^{-}, \partial^{+}: E \to V$ respectively sending each edge to its source and target in $V$.

**Definition 1.1.10.** A labelled graph is a graph together with a set $\mathcal{L}$ of labels and a function $l: E \to \mathcal{L}$ associating a label to each edge.

We sometimes write $x \xrightarrow{A} y$ for the edge $e_A$ such that $l(e_A) = A$, $\partial^{-}(e_A) = x$ and $\partial^{+}(e_A) = y$.

**Example 1.1.11.** We give a simple example of a graph $G$, where $V = \{w, x, y, z\}$ $E = \{e_A, e_B, e_C, e_D\}$ such that $l(e_\omega) = \omega$, and

$$ w = \partial^{-}(e_A) $$

$$ x = \partial^{+}(e_A) = \partial^{-}(e_B) = \partial^{-}(e_C) $$

$$ y = \partial^{+}(e_B) = \partial^{+}(e_D) $$

$$ z = \partial^{+}(e_C) = \partial^{-}(e_D) $$

We can represent such a graph in the classical way below, associating to each vertex a point and each edge an arrow from its source to its target
<figure><img src="image_31.png" /></figure>

**Definition 1.1.12.** Given a graph $G$, a *path* $\pi$ on $G$ is

• a finite non-empty sequence $e_1 \cdots e_n$ of edges $e_i$ of $G$ such that $\partial^+(e_i) = \partial^-(e_{i+1})$,

• or the empty path $\varepsilon_x$ on a vertex $x$.

The source (resp. target) of a non-empty path $\pi$ is the source of $e_1$ (resp. target of $e_n$).
The source and target of the empty path on a vertex $x$, $\varepsilon_x$ are defined to be $x$.

Given two paths $\pi, \tau$ such that $\partial^-(\tau) = \partial^+(\pi)$, we write $\pi \cdot \tau$ for their concatenation.

**Definition 1.1.13.** Given a graph $G$, given two vertices $x, y$ of $G$, we say that $x$ is *reachable* from $y$ when there exists a path with source $x$ and target $y$.

**Definition 1.1.14.** Given a program $P$, the *state space* $G_P$ of this program is the graph whose vertices are the states $\langle\sigma, c\rangle$ and edges are the reductions from Definition 1.1.8.

**Definition 1.1.15.** Given a program $P$, its *initial state* is the state $\langle\sigma_0, P\rangle$ with $\sigma_0$ defined in Definition 1.1.6. Its terminal states are any states of the form $\langle\sigma, \textbf{skip}\rangle$.

**Definition 1.1.16.** A *path* on $G_P$ is a morphism of the free category $G_P^*$ over the graph $G_P$.

It is equivalent to a sequence $\pi = (\langle\sigma_i, c_i\rangle \to \langle\sigma_{i+1}, c_{i+1}\rangle)_{1\le i<n}$ of reductions. We write $\pi: \langle\sigma_1, c_1\rangle \to^* \langle\sigma_n, c_n\rangle$ to say that $\pi$ is a path from $c_1$ to $c_n$.

**Definition 1.1.17.** We call an *execution* of a command $c$ a sequence of reductions $\langle\sigma_0, c\rangle \to^* \langle\sigma', c'\rangle$. We say that an execution is *maximal* for a command $c$ when it is a path of the form $\langle\sigma_0, c\rangle \to^* \langle\sigma', \textbf{skip}\rangle$.

**Definition 1.1.18.** Given a program $P$, a state $\langle\sigma, c\rangle$ of $G_P$ is said to be *reachable* when there exists an execution with $\langle\sigma, c\rangle$ as its target, i.e. there exists a path $\pi: \langle\sigma_0, P\rangle \to^* \langle\sigma, c\rangle$. Otherwise, it is said to be *unreachable*.

As each of the reductions in Definition 1.1.8, comes from the evaluation of at most
single action or boolean expression, we can label each reduction by this evaluation. In all
other cases (mostly when removing **skip** instructions), it is labelled by the empty word.
The executions can then be represented by the sequence of actions and boolean conditions
that are executed along the path. More precisely, they will be represented by words on
the alphabet consisting of actions and boolean expression of the program, called the trace
of an execution.

**Definition 1.1.19.** A *word* $w$ of length $n > 1$ over an alphabet $\mathcal{A}$ is a finite sequence $w_1 \dots w_n$ of elements of $\mathcal{A}$. The empty word $\varepsilon$ is the only word of length 0.

We write $\mathcal{A}^n$ for the set of words of length $n$ and $\mathcal{A}^* = \bigcup_{n \in \mathbb{N}} \mathcal{A}^n$ for the set of all words.
**Definition 1.1.20.** Given two words $w = w_1...w_p$ and $w' = w'_1...w'_q$ on an alphabet $A^*$, their concatenation is

$$w \cdot w' = w_1...w_p w'_1...w'_q$$

We extend this to sets of words by setting

$$R \cdot R' = \{w \cdot w' | w, \in R, w' \in R'\} \approx R \times R'$$

Where $R \times R'$ is the standard cartesian product of sets.

**Definition 1.1.21.** To each path $\pi$ we associate a word $\text{tr}(\pi)$ of $(X \sqcup B)^*$, called the trace of $\pi$, where $\varepsilon$ is the empty word

* When $\pi$ corresponds to the one-step reduction $\frac{c \in X \setminus \{\text{skip}\}}{\langle\sigma, c\rangle \to \langle\llbracket b\rrbracket(\sigma), \text{skip}\rangle}$, $\text{tr}(\pi) = c$.

* When $\pi$ corresponds to a one-step reduction with $\llbracket b\rrbracket(\sigma) = \top$ as premise, $\text{tr}(\pi) = b$. Such a reduction corresponds to choosing a branch in a conditional branching or entering a while loop.

* When $\pi$ corresponds to a one-step reduction with $\llbracket b\rrbracket(\sigma) = \bot$ as premise, $\text{tr}(\pi) = \neg b$. Such a reduction corresponds to exiting a while loop, or exploring the else branch of a conditional branching.

* For each reduction $\pi$, different from the ones above, deduced with a rule of Definition 1.1.8 with no premise we have $\text{tr}(\pi) = \varepsilon$.

* For each reduction $\pi$ deduced with a rule of Definition 1.1.8 with one reduction $\pi'$ as premise, we have $\text{tr}(\pi) = \text{tr}(\pi')$.

* The word associated to a concatenation of reductions is the concatenation of their associated labels $\text{tr}(\pi' \cdot \pi) = \text{tr}(\pi') \cdot \text{tr}(\pi)$.

* The empty word $\varepsilon$ is associated to the empty path, i.e. $\text{tr}(\varepsilon) = \varepsilon$.

When $\pi: \langle\sigma_0, c\rangle \to^* \langle\sigma, c'\rangle$ is an execution of $c$ (Definition 1.1.17), we call $\text{tr}(\pi)$ an execution trace of $c$. It is a maximal execution trace when $\pi$ is a maximal execution. We often do not distinguish $\pi$ and $\text{tr}(\pi)$ and refer to both as execution traces.

We write $T(c, \sigma)$ the set of all traces of paths $\pi$ starting from $\langle\sigma, c\rangle$, and simply $T(c)$ for the set of execution traces.

*Example 1.1.22.* Let us consider the program $(x:=0 || x:=1); \text{ if } x==0 \text{ then } c_0 \text{ else } c_1$, where the == operator compares two integer values for equality. Because of parallelism, there are two family of maximal executions traces

$$x:=1 \cdot x:=0 \cdot x==0 \cdot \text{tr}(c_0) \\ x:=1 \cdot x:=0 \cdot \neg x==0 \cdot \text{tr}(c_1)$$

where $\text{tr}(c_i)$ is a maximal execution trace of the command $c_i$.
**Definition 1.1.23.** Let $\pi: x \to y$ a path in $G_P$. Let $l_\pi = (l_1, \dots, l_k)$ the subword of tr($\pi$) obtained by removing all letters not included in $\mathcal{X}$. We define the evaluation of the path $\pi$ as

$$ \llbracket \pi \rrbracket = \llbracket l_k \rrbracket \circ \dots \circ \llbracket l_1 \rrbracket(\sigma) $$

**Definition 1.1.24.** Two commands $c_1, c_2$ are contextually equivalent, written $c_1 \approx c_2$, when for every state $\sigma \in \Sigma$, we have $T(c_1, \sigma) = T(c_2, \sigma)$

Two contextually equivalent commands will have the same effect on the state and memory of the program, and can thus be simplified.

**Proposition 1.1.25.** For all commands $c, c', c''$, the following commands are contextually equivalent:

$$ \begin{array}{l@{\qquad}l} \texttt{skip}; c \approx c & (c \| c') \| c'' \approx c \| (c' \| c'') \\ \texttt{skip} \| c \approx c \approx c \| \texttt{skip} & c \| c' \approx c' \| c \end{array} $$

*Proof.* For the case `skip||c` $\approx c$, it is proved by directly remarking that the reduction $\langle\sigma, \texttt{skip}||c\rangle \to \langle\sigma, c\rangle$ does not have a premise, so the set of all traces will be the same.

All other contextual equivalences with a `skip` are treated similarly.

The case $(c||c')||c'' \approx c||(c'||c'')$ can be proved by remarking that the execution traces of $a||b$ are the interweaving of the execution traces of $a$ and $b$. $\square$

*Remark 1.1.26.* In this language, the following classical equivalence holds:

$$ \texttt{while } b \texttt{ do } c \approx \texttt{ if } b \texttt{ then } (c;\texttt{while } b \texttt{ do } c) $$

Thus, when only considering verification up to a certain depth, loops can be unrolled into a finite number of conditional branching for the purposes of verification

### 1.1.3 Toward verification of programs

The most common properties we aim at verifying in programs can be regrouped in the two following categories:

1. **Functional properties** which describe compliance of the program with a mathematical specification. For instance, ensuring that an implementation of the factorial actually associates for each integer $n$ as input, the factorial $n!$ as a result. These usually describe invariants of the program, expressed in proof-theoretic form [35] and generally verified using proof assistants, model-checking [8] or abstract interpretation [44].

2. **Reachability properties**, which correspond to checking that a set of forbidden positions/states $X$ cannot be reached (Definition 1.1.18) from the initial state through a series of reductions (*execution of our program*). When there is no such execution trace from the initial state of our program to a state of $X$, we say that the program is *correct* w.r.t. the set $X$. The set of positions could be an error instruction in a program, and we want to guarantee that it will never be reached. Sometimes we will also be interested in knowing which states of a program can be reached.
In this thesis we will focus on reachability properties which are a particular case of a liveness property (properties that stipulate that “something happens infinitely often”, detailed in [2]). A naive solution to verifying the correctness of a program would be to explore all the reduction paths using our favourite tree exploration strategy (e.g. depth-first, breadth-first...). Then for every state reached during the exploration, we could check whether it does belong to the set of forbidden positions. This, of course, is terribly inefficient, as we are essentially exploring all the possible schedulings of the program, and it may not even terminate when considering programs with loops as shown in the Example 1.1.27.

*Example 1.1.27.* Let us consider the following program, computing the *Syracuse Sequence* starting from *x*, described by the command below.

```
x := n;
while x!=1 do
    if x mod 2 !=0 then
        x := 3*x + 1
    else
        x := x/2
```

We want to check that this program terminates, i.e. the state $\langle x \mapsto 1, \text{skip} \rangle$ is always reached. Then we will need to check the infinite number of traces of the language on the following regular expression which describes all possible maximal executions:

$$ (x:=n) \cdot \left( (x!=1) \cdot ((x//2!=0) \cdot (x:=3x+1)) + (\neg(x \mod 2!=0) \cdot (x:=x/2)) \right)^* \cdot \neg(x!=1) $$

These problems come from the loops and are not specific to concurrent programs. For traditional sequential programs there already exist quite a number of techniques to deal with these problems (either by considering correctness properties of execution traces of bounded length and unrolling loops, or use widening operators associated to abstract interpretation domains [10]).

#### 1.1.3.1 Verification of concurrent programs

In the rest of this thesis, we will focus on the verification of properties specific to concurrent programs, and more precisely, on reachability properties of such programs. In this context, one of the biggest problems we face is the state space explosion problem [7]: in order to prove that a program is correct, we have to check out all the possible execution traces coming from all the potential schedulings of the different threads. Even without loops, the number of traces generated by a parallel composition of threads is exponential in the size of the program as shown in the Example 1.1.28.

*Example 1.1.28.* Consider the following program $P = A \parallel \dots \parallel A$, composed of $n$ copies of threads that are a single action $A$. Finding a scheduling amounts to finding an order on these $n$ copies. Thus, there are $n!$ different schedulings, and as many execution traces.

**Definition 1.1.29.** A state $\langle \sigma, c \rangle$ of a program $P$ is called:

* unreachable, if there are no execution traces from the initial state to this state,
* *deadlocked* when the state $\langle\sigma, c\rangle$ does not correspond to a terminal state of the program (Definition 1.1.15) and there is an execution from the initial state to the state $\langle\sigma, c\rangle$ that is not a proper prefix of another execution trace,

* *unsafe* when there is an execution trace with $\langle\sigma, c\rangle$ as target which is the prefix of an execution trace with a deadlock as target,

* *doomed* when there is an execution trace with $\langle\sigma, c\rangle$ as target which is not a prefix of an execution trace reaching the terminal state of the program.

*Unreachable* positions are positions that may never be reached during the execution of a program. These don't seem to be problematic at first, if they are never reached, they should not pose any problem. But these positions are witnessing the presence of dead code, that will never be executed. In critical systems, every line of code is there for a reason, so there should be no such unreachable positions. Finding these positions can help detect a misconception from the part of the programmer.

*Deadlocks* pose a much bigger problem. They are positions of the program in which it is blocked, or “frozen”, and cannot progress at all. This situation generally arises when two or more threads are waiting on each other to free up a resource before they do anything else. They are locked in place and functionally dead, hence the term “deadlock” [13].

Finally, *unsafe* positions are the positions from which it is possible to eventually reach a deadlock and *doomed* positions, are the positions that can only reach deadlocks or loop on forever. This precision is important as we will eventually be considering programs with loops.

**Definition 1.1.30.** A program *P* is *safe* when its initial state is not unsafe.

In such a program *P*, there are no execution traces that reach a deadlock. There might be other problems as shown in the Example 1.1.31 below. The term *safe* here is specifically for concurrent related problems and might miss some problems that are specific to sequential programs. It is good to keep this in mind going forward.

*Example 1.1.31.* Let's look at the classical blunder of programming: non-terminating loops. The program $P = x:=2; \ while \ x>0 \ do \ x:=x$ is technically safe. Even though it will be stuck in the *while* loop. If we look at the set of states and transitions, writing $L = \ while \ x>0 \ do \ x:=x$ for the loop:

<figure><img src="image_32.png" /></figure>

We see that all executions traces are words of the language $x:=2 \cdot (x > 0 \cdot x:=2)^*$ and thus can always be extended. The program is thus safe in the sense of Definition 1.1.30 even though a program that loops indefinitely might not be the desired result.
*Remark 1.1.32.* Deadlocks, unsafe and doomed positions are specific to concurrent programs. Sequential programs can be shown to not have deadlock positions. An example of such positions is given later on in Example 1.2.37.

*Remark 1.1.33.* For deadlocks (and similarly for unsafe and doomed regions) we do not require all executions reaching our deadlock to not have an extension. A point where any execution cannot be extended is considered a deadlock. This choice of definition is because we will, in the following consider programs where the properties of a position does not depend on the execution trace leading to it (Definition 1.2.23).

*Remark 1.1.34.* In the rest of this section, we will consider only finite executions. There are a lot of subtle differences that can arise from the presence of infinite executions (such as executions that are stuck in a loop, which would not count as deadlocks). More generally loops bring a lot of problems to the table that we will try to deal with.

The search for deadlocks, unsafe and doomed positions will be the main goal of the following chapters, as well as dealing with the state explosion problem.

## 1.2 Control flow graphs

In this section, we present a first model of programs based on a graph representation of the structure of our program: the transition graph (or a control-flow graph) [1]. This classical construction allows us to abstract away from the syntax of the programming language, and present in a simple fashion the subtleties of concurrent languages.

### 1.2.1 Transition graphs

The first model we introduce is based on directed graphs. Their definition was previously introduced in Definition 1.1.9. In the following, we will need some additional operations for combining graphs, to represent more elaborate programs.

**Definition 1.2.1.** Given three graphs $G = (V, E, \partial^{-}, \partial^{+})$, $G_1 = (V_1, E_1, \partial_1^{-}, \partial_1^{+})$ and $G_2 = (V_2, E_2, \partial_2^{-}, \partial_2^{+})$. We define the following operations:

* The disjoint union $G = G_1 \cup G_2 = (V_1 \cup V_2, E_1 \cup E_2, \partial^{-}, \partial^{+})$ where

$$ \partial^{-}(e) = \begin{cases} \partial_{1}^{-}(e) & \text{if } e \in E_{1} \\ \partial_{2}^{-}(e) & \text{if } e \in E_{2} \end{cases} \qquad \partial^{+}(e) = \begin{cases} \partial_{1}^{+}(e) & \text{if } e \in E_{1} \\ \partial_{2}^{+}(e) & \text{if } e \in E_{2} \end{cases} $$

* The tensor product $G_1 \otimes G_2 = (V_1 \times V_2, (E_1 \times V_2) \cup (V_1 \times E_2), \partial^{-}, \partial^{+})$ where

$$ \begin{aligned} \partial^{-}|_{E_1 \times V_2} &= \partial_1^{-} \times \text{id} & \partial^{+}|_{E_1 \times V_2} &= \partial_1^{+} \times \text{id} \\ \partial^{-}|_{V_1 \times E_2} &= \text{id} \times \partial_2^{-} & \partial^{+}|_{V_1 \times E_2} &= \text{id} \times \partial_2^{+} \end{aligned} $$

* Given $x, y \in V$, the quotient graph $G[x = y]$ is the graph obtained by identifying the vertices $x$ and $y$ in $G$

* Given $V' \subseteq V$, the induced subgraph $G|_{V'}$ is the restriction of the graph $G$ to the vertices of $V'$ i.e.

$$ G|_{V'} = (V', E' = \{e \in E \mid \partial^{-}(e) \in V' \text{ and } \partial^{+}(e) \in V'\}, \partial^{-}|_{E'}, \partial^{+}|_{E'}) $$
As we previously stated, each of the commands in $\mathcal{C}$ give rise to a structure in the code and allows us to easily formalize the notion of a transition graph (or control-flow graph) associated to a program of our language.

**Definition 1.2.2.** The transition graph $G_c = (G_c, l_c, s_c, t_c)$ associated to a command $c$ is a graph $G_c$ with labels in the set $\mathcal{L} = \mathcal{X} \coprod \mathcal{B}$, equipped with two distinguished vertices $s_c, t_c \in E$ called the start and end. It is defined inductively as follows.

* $G_{\text{skip}}$ is the graph with a single vertex and no edge:

$$s_{\text{skip}} \bullet t_{\text{skip}}$$

* $G_A$ with $A \in \mathcal{X}$ is the graph with two vertices and a single edge from $s_A$ to $t_A$ labelled $A$.

$$s_A \bullet \xrightarrow{A} t_A$$

* $G_{c_1;c_2} = (G_{c_1} \sqcup G_{c_2})[t_{c_1} = s_{c_2}]$ is the graph obtained by identifying $t_{c_1}$ and $s_{c_2}$.

$$s_{c_1;c_2} = s_{c_1} \bullet \quad G_{c_1} \quad t_{c_1} \bullet s_{c_2} \quad G_{c_2} \quad \bullet t_{c_2} = t_{c_1;c_2}$$

* $G_c$, with $c = \text{if } b \text{ then } c_1 \text{ else } c_2$ is the following graph, obtained by disjoint union of $G_{c_1}$ and $G_{c_2}$ adding a new vertex $s_c$ and two labelled transitions $b$ (resp. $\neg b$) from $s_c$ to $s_{c_1}$ (resp. $s_{c_2}$). Finally we identify $t_{c_1}$ and $t_{c_2}$.

<figure><img src="image_33.png" /></figure>

* $G_c$, with $c = \text{while } b \text{ do } c'$ is obtained from $G_{c'}$ by adding a vertex $t_c$, adding an edge from $t_{c'}$ to $t_c$ labelled $\neg b$, and adding an edge $t_{c'}$ to $s_{c'}$ labelled $b$, and $s_c = t_{c'}$.

<figure><img src="image_34.png" /></figure>

* $G_{c_1 \parallel c_2} = G_{c_1} \otimes G_{c_2}$. where $s_{c_1 \parallel c_2} = (s_{c_1}, s_{c_2})$ and $t_{c_1 \parallel c_2} = (t_{c_1}, t_{c_2})$
We call a vertex of $G_P$ a position of the program $P$.

The edges labelled by conditions in transition graphs are drawn with dotted arrows to distinguish them from those labelled by actions. This is only a drawing convention; there is no difference between the two types of edges except the sets in which they are labelled.

*Example 1.2.3.* Let us revisit our program of Example 1.1.22:

$$ (x:=0 \mid x:=1); \text{ if } x==0 \text{ then } c_0 \text{ else } c_1 $$

For now let us suppose that $c_0$ and $c_1$ are actions in $\mathcal{X}$. It has the following transition graph:

<figure><img src="image_35.png" /></figure>

If we count the paths, there are four different paths from $s_c$ to $t_c$, whereas there are only two maximal execution traces.

*Remark 1.2.4.* For a program $P$, by construction, there is always a path from $s_P$ to any of its positions $p$ and from $p$ to $t_P$.

There are usually more paths than execution traces as defined in Definition 1.1.21, as shown in the Example 1.2.3 above. Nonetheless, there is a link between execution traces and paths on the graph starting at $s_P$, but some refinement must be made.

**Definition 1.2.5.** A potential execution of a program $P$ is a path in $G_P$ starting from $s_P$. It is maximal when its target is $t_P$.

**Definition 1.2.6.** Given a potential execution $\pi$ of a program $P$, the associated potential execution trace $\text{tr}(\pi)$ is defined as the concatenation of the labels of $\pi$.

Determining which traces are actual executions traces of our program and will occur during its execution depends on the semantics we chose for our programming language, as formalized in Definition 1.1.6. In our case, it comes down to verifying that all boolean conditions are verified.

**Definition 1.2.7.** Given a potential execution $\pi$ of a program $P$, we say that it is valid when its trace $\text{tr}(\pi)$ is of the following form:

* the empty word $\varepsilon$.

* Or $\text{tr}(\pi') \cdot A$, with $A \in \mathcal{X}$ and $\pi'$ a valid execution.

* Or $\text{tr}(\pi') \cdot b$, with $b \in \mathcal{B}$, $\pi'$ a valid execution and $[[b]] \circ [[\pi']](\sigma_0) = \top$.

**Definition 1.2.8.** Given a program $P$, we define the execution traces $T(P)$ of our program $P$ as the set of all valid potential traces.
*Example 1.2.9.* Consider the following program

```pascal
while b do A; if b then B else C
```

Its set of potential executions are the paths with labels in the language associated to the regular expression:

$$((b \cdot A)^* \cdot \neg b \cdot b \cdot B) + ((b \cdot A)^* \cdot \neg b \cdot \neg b \cdot C)$$

The boolean conditions appearing in those traces should be thought of assumptions on the state of the memory, under which the path is valid. This is why they are called potential. Here it is easy to determine which are the maximal executions traces. As $\neg b$ and $b$ cannot both hold without any effect on the memory in between, all traces in the sub-language $(b \cdot A)^* \cdot \neg b \cdot b \cdot B$ cannot be maximal.

### 1.2.2 Introducing resources

As we have seen in Example 1.1.22, the execution of a concurrent program can be non-deterministic, which is a problem unique to these types of programs. This problem is not only linked to the scheduling of the actions as previously seen. Let us consider the following program in which two threads try to access and increment the same shared resource:

$$x := 0; (x := x+1 \parallel x := x+1) \qquad (1.1)$$

In a weak memory model (when sequential consistency is not enforced), this is an unspecified outcome [51]. Indeed, one might first think that at the end of the execution $x$ will be equal to 2, but because of how memory access is implemented in practice, the variable could contain 1 or a completely unrelated value.

*Example 1.2.10.* If we suppose that $x:=x+1$ is not atomic, for example if fetching $x$ from memory and writing to $x$ can be interleaved with other actions we could have the following “trace” for the 1.1:

1. The first thread fetches the value of $x$ (= 0) and writes it to a new fresh temporary variable

2. The second thread fetches the value of $x$ (= 0) and writes it to a new fresh temporary variable

3. First and second thread increment there respective fresh variable (both equal to 1)

4. First thread writes 1 to $x$

5. Second thread writes 1 to $x$

Which would give $x = 1$ at the end of the execution.

In order to avoid such unpredictable behaviour when using shared memory, most systems come with constructions called *mutex* restricting access to portion of codes. Given a mutex $a$, a thread may perform the following operations [11], called synchronization primitives:

* lock the associated *resource*, modelled by the instruction $P_a$

* unlock the associated *resource*, modelled by the instruction $V_a$
The system then guarantees that the mutex may not be locked more than once. Threads attempting to lock an already locked thread will be “frozen” and will not progress further until the resource is unlocked, and they manage to lock it themselves. Thus, to guarantee the predictability of the behaviour of the program of 1.1, it should be re-written:

$$x := 0; ((P_a; x := x+1; V_a) \parallel (P_a; x := x+1; V_a))$$

Mutexes ensure that the sequence of instruction between $P_a$ and $V_a$, called a blocking section, is atomic, i.e. it will not be interleaved with instruction from another thread using the mutex $a$ in the same way. For other examples of programs with resources we refer to [15].

*Remark 1.2.11.* The uses of mutexes do not decrease the number of execution traces of the Example 1.1.22. This non-determinism is intrinsic to parallel programs.

We extend our language (Definition 1.1.1) with a set $\mathcal{R} = \{a, b, \dots\}$ of resources (or semaphores), together with a function $\kappa: \mathcal{R} \to \mathbb{N}$ associating with each resource $a$ its *capacity* (the number of times it can be locked) $\kappa_a \in \mathbb{N}$.

**Definition 1.2.12.** We extend the syntax of PIMP programs with two additional actions in $\mathcal{X}$ for each resource in $\mathcal{R}$:

$$c_{act} ::= \mathcal{X} \mid P_a \mid V_a$$

*Remark 1.2.13.* This also extends the sets of labels and constructions rules for the transition graph $G_P$ in accordance with the rules defined for actions:

$$s_{P_a} \bullet \xrightarrow{P_a} \bullet t_{P_a} \qquad s_{V_a} \bullet \xrightarrow{V_a} \bullet t_{V_a}$$

*Remark 1.2.14.* Mutexes are a particular case of semaphores where $\kappa_a = 1$.

We must also extend the operational semantics of our language introduced in Definition 1.1.6 to encompass this new notion.

**Definition 1.2.15.** A state $\sigma$ for the language PIMP is now the data of two functions $\sigma_v: \mathrm{Var} \to \mathbb{Z}$ and $\sigma_r: \mathcal{R} \to \mathbb{Z}$. Where $\sigma_v$ (resp. $\sigma_r$) associates to each variable (resp. resource) its content (resp. availability). The initial state $\sigma_0$ is the function associating to each variable and each resource 0. We write $\Sigma = \mathbb{Z}^{\mathrm{Var}} \times \mathbb{Z}^{\mathcal{R}}$ for the set of states.

*Remark 1.2.16.* The assumption that resources are at their maximum capacity in the initial state can be made without loss of generality. Indeed, if for $a \in \mathcal{R}$, $\sigma_0(a) > 0$, studying $P$ is the same as studying the program $P' = \underbrace{P_a; \dots; P_a}_{\sigma_0(a) \text{ times}}; P$ where the program $P'$ starts at maximum capacity for $a$.

Given $x \in \mathrm{Var}$ (resp. $a \in \mathcal{R}$), we will often write $\sigma(x)$ (resp. $\sigma(a)$) for $\sigma_v(x)$ (resp. $\sigma_r(a)$) when the context makes it clear.

**Definition 1.2.17.** Let $x \in \mathrm{Var}$, $e \in \mathcal{A}$, $a \in \mathcal{R}$. Given a state $\sigma \in \Sigma$. The previous Definition 1.1.7 of the evaluation for the following case is replaced by:

$$[x := e]_\mathcal{X}(\sigma) = (\sigma_v[x \mapsto [e]_\mathcal{A}(\sigma)], \sigma_r)$$
The evaluation of the actions $P_a$ and $V_a$ are defined as follows:

$$ \llbracket P_a \rrbracket_X(\sigma_v, \sigma_r) = (\sigma_v, \delta_a^+(\sigma_r)) $$

$$ \llbracket V_a \rrbracket_X(\sigma_v, \sigma_r) = (\sigma_v, \delta_a^-(\sigma_r)) $$

where $\delta_a^+(\sigma)(a) = \sigma(a)+1$, $\delta_a^-(\sigma)(a) = \sigma(a)-1$, and $\delta_a^+(\sigma)(b) = \delta_a^-(\sigma)(b) = \sigma(b)$ if $b \neq a$.

**Definition 1.2.18.** Let $a \in \mathcal{R}$. We extend the reduction relation with special rules for the actions $P_a$ and $V_a$ which overrides the previous rules in Definition 1.1.8

$$ \frac{\sigma_r(a) < \kappa_a}{\langle \sigma, P_a \rangle \to \langle \llbracket P_a \rrbracket(\sigma), \text{skip} \rangle} $$

$$ \frac{\sigma_r(a) > 0}{\langle \sigma, V_a \rangle \to \langle \llbracket V_a \rrbracket(\sigma), \text{skip} \rangle} $$

The notion of validity of Definition 1.2.7 is extended accordingly to express that in a valid execution trace, the locked resources have to be available and one cannot add more instances of a resource of a resource than its capacity.

**Definition 1.2.19.** Given a potential execution $\pi$ of a program $P$ with resources, we say that it is valid when its trace $\text{tr}(\pi)$ is of the following form:

* the empty word $\varepsilon$.

* Or $\text{tr}(\pi') \cdot P_a$, with $a \in \mathcal{R}$, $\pi'$ a valid execution and $\llbracket \pi' \rrbracket(\sigma_0)(a) < \kappa_a$.

* Or $\text{tr}(\pi') \cdot V_a$, with $a \in \mathcal{R}$, $\pi'$ a valid execution and $\llbracket \pi' \rrbracket(\sigma_0)(a) > 0$.

* Or $\text{tr}(\pi') \cdot A$, with $A \in \mathcal{X} \setminus \{P_a, V_a\}$ and $\pi'$ a valid execution.

* Or $\text{tr}(\pi') \cdot b$, with $b \in \mathcal{B}$, $\pi'$ a valid execution and $\llbracket b \rrbracket \circ \llbracket \pi' \rrbracket(\sigma_0) = \top$.

*Remark 1.2.20.* The primitives $P_a$ and $V_a$ could have been implemented as features of the language, but it is much more complicated [11]. Similarly, we could have restricted to mutex without loss of generality.

*Remark 1.2.21.* We have chosen semaphores as our synchronization primitives. There are many other such mechanisms used in practice (e.g. monitors, barriers,...) used to simplify implementation of some structures. As they can be modelled by semaphores, we do not lose any generality in our approach.

### 1.2.3 Conservative programs

Consider the program if $b$ then $P_a$ else skip. Depending on the maximal path we follow, the number of times the resource $a$ was locked/released depends on whether $b$ is true or not. As we do not want to have to consider the whole trace space when verifying the program we will restrict our study to programs where the consumption of resources does not depend on the path, but only on its endpoints.

**Definition 1.2.22.** The consumption of a path $\pi$ w.r.t. a resource $a \in \mathcal{R}$ and a state $\sigma$ is defined as $\llbracket \pi \rrbracket(\sigma)(a) \in \mathbb{Z}$.

**Definition 1.2.23.** A program $P$ is conservative when for any pair of paths $\pi, \tau: x \to y$ in $G_P$ with same source and target we have for any state $\sigma \in \Sigma$ and any resource $a \in \mathcal{R}$:

$$ \llbracket \pi \rrbracket(\sigma)(a) = \llbracket \tau \rrbracket(\sigma)(a) $$
**Definition 1.2.24.** Given a conservative program $P$, its initial state $\sigma_0$ and a vertex $x$ in $G_P$, we define the consumption of $x$, written $[[x]]: \mathcal{R} \to \mathbb{Z}$ as the restriction of $[[\cdot]]$ to the set of resources $\mathcal{R}$:

$$[[x]] = [[\pi]](\sigma_0)|_{\mathcal{R}}$$

for some path $\pi: s_P \to x$

The above definition is well-defined. Indeed, the chosen path $\pi$ does not matter as the program $P$ is explicitly chosen to be conservative and all vertexes of $G_P$ are reachable by Remark 1.2.4. Furthermore, for any resource $a$, $[[x]](a)$ corresponds to its consumption w.r.t. the resource $a$ from Definition 1.2.22.

**Definition 1.2.25.** Given a conservative program $P$, a vertex of its transition graph $G_P$ is valid (and otherwise forbidden) when for every $a \in \mathcal{R}$, we have $O \le [[x]](a) \le \kappa_a$.

**Proposition 1.2.26.** Given a conservative program $P$ and a path $\pi: x \to^* y$ in $G_P$, a state $\sigma \in \Sigma$ and a resource $a \in \mathcal{R}$, then $[[\pi]](\sigma)(a) = \sigma(a) + [[y]](a) - [[x]](a)$.

*Proof.* See [18, Proposition 3.12]. □

This shows that, in a conservative program, the number of times a resource has been locked during a potential execution path $\pi$ depends only on the target of $\pi$.

**Proposition 1.2.27.** Given a conservative program $P$ and an execution trace $\pi: s_P \to x$ on $G_P$. Then $x$ is a valid vertex, in the sense of Definition 1.2.25.

*Proof.* See [18, Proposition 3.15]. □

For conservative programs, we can define a notion of global consumption, directly on the syntax.

**Definition 1.2.28.** The consumption of a program $P$ is the partial function $\Delta(P) : \mathcal{R} \to \mathbb{Z}$ defined by induction on $P$ by

$$\Delta(P_a) = \delta_a \qquad \Delta(V_a) = -\delta_a \qquad \Delta(A) = \underline{0}$$

$$\Delta(P;Q) = \Delta(P \| Q) = \Delta(P) + \Delta(Q)$$

$$\Delta(\text{if } b \text{ then } P \text{ else } Q) = \Delta(P) \quad \text{if } \Delta(P) = \Delta(Q)$$

$$\Delta(\text{while } b \text{ do } P) = \underline{0} \quad \text{if } \Delta(P) = \underline{0}$$

where $\underline{0}$ is the constant function equal to 0 and $\delta_a$ the indicator function of $a$.

**Proposition 1.2.29.** The function $\Delta$ is only partially defined on programs. A program $P$ is conservative if and only if $\Delta(P)$ is well-defined.

*Proof.* See [18, Proposition 3.8]. □

The resource consumption $\Delta(P)$ gives the amount of times each resource has been locked or released, i.e. the difference between the global number of instructions $P_a$ and $V_a$ encountered in an execution of $P$.
*Example 1.2.30.* Given a single mutex *a*, the program if *b* then *P*<sub>*a*</sub> else skip is not conservative. The two paths *b*·*P*<sub>*a*</sub> and ¬*b*·skip from *s*<sub>*P*</sub> to *t*<sub>*P*</sub> have a different consumption. Indeed,

$$ \llbracket b \cdot P_a \rrbracket (a) = 1 $$

$$ \llbracket \neg b \cdot \mathit{skip} \rrbracket (a) = 0 $$

*Remark 1.2.31.* Checking that a program is conservative is thus linear in the size of the program as it suffices to check $\Delta(P)$.

### 1.2.4 Pruned transition graph

In the rest of the thesis, we will always suppose that the program we are considering are conservative. By Proposition 1.2.27, no valid execution trace visits an invalid state. Thus, we can remove all invalid states from the transition graph, and any associated vertices without removing any valid paths. This gives us the *pruned transition graph* defined below.

**Definition 1.2.32.** The *pruned transition graph* $\overline{\mathcal{G}}_P$ is obtained from the transition graph $G_P$ by removing all invalid vertices (in the sense of Definition 1.2.25), keeping the terminal position $t_P$. Formally, with $V'_P$ the set of valid vertices,

$$ \overline{\mathcal{G}}_P = \begin{cases} G_P|_{V'_P} & \text{if } t_P \in V'_P \\ G_P|_{V'_P} \cup t_P & \text{if } t_P \notin V'_P \end{cases} $$

With $t_P$ the graph with a single vertex and no edge.

*Remark 1.2.33.* For future definitions, a program needs an initial and terminal position. That is why we ensure that $t_P$ is not removed in Definition 1.2.32. As the starting position is always valid, such concerns are unnecessary for $s_P$.

**Lemma 1.2.34.** The inclusion $\overline{\mathcal{G}}_P \hookrightarrow G_P$ induces a bijection between valid paths from the initial vertex (i.e. execution traces) in both graphs.

*Proof.* See [18, Lemma 3.18]. □

<figure><img src="image_36.png" /></figure>

The Remark 1.2.4 about reachability of all vertices no longer holds in the pruned transition graph. This allows us to discover the troublesome positions described in Definition 1.1.29.

**Proposition 1.2.35.** *Given a conservative program P:*

* Let $x \in \overline{\mathcal{G}}_P$ such that there is no path $s_P \to^* x$. Then $x$ is unreachable.

* Let $x \in \overline{\mathcal{G}}_P \setminus \{t_P\}$. If $x$ is reachable and there is no edge in $\overline{\mathcal{G}}_P$ with $x$ as its source, then $x$ is a deadlock

* Let $x \in \overline{\mathcal{G}}_P$, such that there is a path $s_P \to^* x \to^* y$ where $y$ is a deadlock, then $x$ is unsafe.

* Let $x \in \overline{\mathcal{G}}_P$, such that there is a path $s_P \to^* x$ and no path $x \to^* t_P$. Then $x$ is doomed.
Proof. See [18, Proposition 3.19]. □

The above Proposition 1.2.35 allows us to define a less naive verification method for the properties described in Definition 1.1.29.

**Proposition 1.2.36.** *Properties of Definition 1.1.29 can be discovered from the pruned transition graph $\overline{\mathcal{G}}_P$ of the program P as follows:*

* a position which is not reachable in $\overline{\mathcal{G}}_P$ from the beginning position is unreachable

* a position in $\overline{\mathcal{G}}_P \setminus \{t_P\}$ which is not unreachable and from which there is no transition is a deadlock

* a position from which there is a path to a potential deadlock is unsafe

* a position from which there is no path to $t_P$ is doomed

Proof. See [18, Proposition 3.19]. □

In the Proposition 1.2.36 we have to consider the position as “potential” candidates as they might be unreachable in the sense of Definition 1.1.29 (even though they might be reachable in $\overline{\mathcal{G}}_P$). Unreachable positions in $\overline{\mathcal{G}}_P$ are a subset of all unreachable positions, as shown in Remark 1.2.38, because of properties other than the structure of the program (i.e. how semaphores are used). This algorithm is still very inefficient, as it searches through all the vertices of the graph. Much of our focus in the thesis will be on methods of representing these valid positions in a more compact way.

*Example 1.2.37.* Let us consider the program P with two mutexes a, b of capacity $\kappa_a = \kappa_b = 1$:

$$ (P_a; P_b; V_b; V_a) \parallel (P_b; P_a; V_a; V_b) $$

On the left we see its transition graph, and on the right its pruned transition graph (only exterior edges are labelled for clarity). The transition $s_P \to x$ is labelled by $P_a$ which has the effect of increasing the consumption of a. Thus, $[[x]](a) = 1 = \kappa_a$. Similarly, the transition $x \to y$ is labelled by $P_b$ which increments the consumption of b. Then $[[y]](b) = 1 = \kappa_b = \kappa_a = [[y]](a)$. Then, by the same argument on the transition $y \to z$ we can see that $[[z]](a) = 2 > \kappa_a$, which implies that z is not valid. A similar argument may be used for the rest of the pruned vertices.

<figure><img src="image_37.png" /></figure>

<figure><img src="image_38.png" /></figure>
Then $y$ is a deadlock as it is not $t_P$ and there are no transitions from $y$. The points $x, w, s_P$ are unsafe as there is a path to $y$ from these vertices. The vertex $u$ is unreachable, and no positions, except for the deadlock, are doomed.

*Remark 1.2.38.* Not all undesirable positions are discovered by the Proposition 1.2.36. Indeed, let us consider the program $P = \text{while true do } x:=x+1$. Its pruned transition graph can be represented as:

<figure><img src="image_39.png" /></figure>

The position $t_p$ is unreachable because the condition $\neg true$ is never true. We could prune more by removing vertices following branching that are never satisfied, but it would make pruning our graph undecidable [18]. Furthermore, the non-reachability of these point does not come from concurrent program features, so we will not dwell on it more than necessary.

# 1.3 Directed geometric semantics

## 1.3.1 Asynchronous semantics

As explained in Section 1.1.3, the number of paths one has to check in order to verify a program might be exponential in the size of the program. To lower this number, we take an approach, historically called true concurrency, of considering schedulings of all actions up to a certain notion of commutation of these actions. Two actions commute when their effect on any state does not depend on the order in which they are executed.

**Definition 1.3.1.** We write $\mathfrak{S}_n$ for the symmetric group of order $n$ composed of all the permutations of the elements of the set $\{1, \dots, n\}$.

**Definition 1.3.2.** Given $n$ actions $A_1, \dots, A_n$, we say that $A_1, \dots, A_n$ commute if for any permutation $\sigma \in \mathfrak{S}_n$ we have:

$$[[A_1]] \circ \dots \circ [[A_n]] = [[A_{\sigma(1)}]] \circ \dots \circ [[A_{\sigma(n)}]]$$

When two actions commute, we indicate this on their transition graph in the following way, by writing $\sim$ in the centre of the square formed by these paths:

<figure><img src="image_40.png" /></figure>
**Example 1.3.3.** The two actions $x:=x+1, x:=x*2$ do not commute. Indeed, $[[x:=x+1] \circ [[x:=x*2]](\sigma_0)(x) = 1$ which is different from $[[x:=x*2]] \circ [[x:=x+1]](\sigma_0)(x) = 2$. On the contrary, it is easy to check that $y:=y+1$ and $x:=x+1$ commute.

<figure><img src="image_41.png" /></figure>

**Remark 1.3.4.** The only paths we are interested in verifying are the execution traces. Thus, the “correct” notion of commutation we would like to study would be a looser one: Two actions $A, B$ commute when for each path $\pi: s_P \to x$, we have:

$$[[B]] \circ [[A]] \circ [[\pi]](\sigma_0) = [[A]] \circ [[B]] \circ [[\pi]](\sigma_0)$$

Unfortunately, this notion of commutativity is undecidable ([36]). Moreover, commutation in the sense of Definition 1.3.2 implies this commutation, which makes it a suitable over-approximation.

In the following Section 1.3.1.1, we will enhance the transition graph model by filling in the cubes of the graph to take into account this notion of commutation as in the Example 1.3.5 below. To do this we introduce precubical sets and new semantics.

**Example 1.3.5.** Consider the following program

$$P = P_a; V_a \| P_a; V_a \| P_a; V_a$$

Depending on the capacity $\kappa_a$ of the resource $a$,

* If $\kappa_a = 0$ then, there are no transitions between states, and thus the semantics consists of 8 disjoint vertices.

* If $\kappa_a = 1$, then the transition graph is the skeletal cube, and there are no commutation/independence tiles.

* If $\kappa_a = 2$, then each smaller subdivided face has a commutation tile.

* If $\kappa_a = 3$ then we should fill the whole cube with commutation tiles.

<figure><img src="image_42.png" /></figure>

$\kappa_a = 0$

<figure><img src="image_43.png" /></figure>

<figure><img src="image_44.png" /></figure>

<figure><img src="image_45.png" /></figure>

<figure><img src="image_46.png" /></figure>

<figure><img src="image_47.png" /></figure>

$\kappa_a = 1$

<figure><img src="image_48.png" /></figure>

<figure><img src="image_49.png" /></figure>

<figure><img src="image_50.png" /></figure>

$\kappa_a = 2$

<figure><img src="image_51.png" /></figure>

<figure><img src="image_52.png" /></figure>

<figure><img src="image_53.png" /></figure>

$\kappa_a = 3$

<figure><img src="image_54.png" /></figure>
### 1.3.1.1 Cubical semantics

A precubical set consists of sets of $n$-dimensional cubes, for all $n \in \mathbb{N}$, together with the data of their faces (i.e. which $n-1$ dimensional cube of the precubical set corresponds to one of its face): each cube has two faces in each direction $i$ with $0 \le i < n$, a front face and a back face. We would also like these higher order cubes to encode notions of commutation presented in the start of this section.

**Definition 1.3.6.** A precubical set $C$ consists of a family $(C_n)_{n \in \mathbb{N}}$ of sets whose elements are called $n$-cubes together with maps

$$ \partial_{n,i}^{+} : C_n \to C_{n-1} \quad \text{and} \quad \partial_{n,i}^{-} : C_n \to C_{n-1} \qquad (1.2) $$

for all indices $n, i \in \mathbb{N}$ such that $0 \le i < n$. $\partial_{n,i}^{+}$ and $\partial_{n,i}^{-}$ respectively associate each $n$-cube to its back and front face in the $i$-th direction such that for $0 \le i \le j < n$ and $\alpha, \beta \in \{+, -\}$

$$ \partial_{n,j}^{\beta} \circ \partial_{n+1,i}^{\alpha} = \partial_{n,i}^{\alpha} \circ \partial_{n+1,j}^{\beta} \qquad (1.3) $$

The 0-cubes and 1-cubes of a precubical sets are often called its *vertices* and its *edges* respectively. Given a set $\mathcal{L}$ of labels, a labelled precubical set $(C, l)$ consists of a precubical set $C$ equipped with a function $l: C_1 \to \mathcal{L}$ associating to each 1-cube (edges) a label and such that

$$ l \circ \partial_{2,0}^{-} = l \circ \partial_{2,0}^{+} \quad \text{and} \quad l \circ \partial_{2,1}^{-} = l \circ \partial_{2,1}^{+} $$

**Example 1.3.7.** A labelled precubical set $C$, where $C_i = \emptyset$ for all $i \ge 2$, is equivalent to a labelled graph:

* $C_0$ can be seen as the set of its vertices,

* $C_1$ can be seen as the set of its edges,

* $\partial_{1,0}^{+}, \partial_{1,0}^{-}$ are respectively the source and target functions.

If we have 2-cubes, i.e. $C_2 \neq \emptyset$, then its elements are cells differentiating the empty square on the left (no 2-cubes) to the “filled” square on the right (corresponding to a 2-cube $\gamma$):

<figure><img src="image_55.png" /></figure>

All 2-cubes of our precubical sets are of this form by the conditions on the labelling function $l$. We will use $n$-cubes to indicate that the actions labelling the 1-cubes which are used in their construction commute.

There is a nice categorical structure that will be of technical interest later on.
**Definition 1.3.8.** If we define the precubical category □ to be the opposite of the category whose objects are natural numbers and whose morphisms are generated by morphisms of the form in Eq. (1.2) quotiented by the congruence relations Eq. (1.3). Then the category of precubical sets ⋄ can be defined as the category of presheaves over □, i.e. the category of functors □$^{op}$ → Set.

*Remark 1.3.9.* There is a full and faithful embedding of the category of transition graphs into the category of precubical sets [52] (cf Example 1.3.7).

**Definition 1.3.10.** Given two precubical sets $C$ and $D$, the operations previously defined on graphs can be extended to precubical sets, while coinciding with previous operations on the embedding of transition graphs.

* The disjoint union $C \sqcup D$ is the precubical set defined by

$$ (C \sqcup D)_n = C_n \sqcup D_n $$

with face maps induced by those of $C$ and $D$

* The tensor product $C \otimes D$ is the precubical set defined by

$$ (C \otimes D)_n = \coprod_{i+j=n} C_i \times D_j $$

with face maps $\partial_{n,k}^{\alpha}: (C \otimes D)_n \to (C \otimes D)_{n-1}$ defined on $(x, y) \in C_i \times D_j$ such that $i + j = n$ by:

$$ \partial_{n,k}^{\alpha}(x, y) = \begin{cases} (\partial_{n,k}^{\alpha}(x), y) & \text{if } 0 \le k < i \\ (x, \partial_{n,k-i}^{\alpha}(y)) & \text{if } i \le k < n \end{cases} $$

* The quotient $C[c = c']$ is the precubical sets obtained by identifying the 0-cubes $c$ and $c'$.

* The restriction $C|_{C'_0}$ of a precubical sets to a subset $C'_0 \subseteq C_0$ is defined as the precubical sets where we remove from each $C_n$ all cubes $c_n$ such that there exists $(\alpha_i)_{i \le n}$ and $(i_j)_{j \le n}$ such that $\partial_{1,i_1}^{\alpha_1} \cdots \partial_{n,i_n}^{\alpha_n}(c_n) \notin C'_0$

These operations naturally extend to labelled precubical sets.

*Example 1.3.11.* We write $I$ for the precubical set corresponding to the directed graph with a single edge $f$ between two vertices $x, y$. Then $S^1 = I[x = y]$ is the precubical set with a single vertex and edge i.e. $\partial_{1,0}^{-}(f) = \partial_{1,0}^{+}(f) = x$.

$$ I = x \xrightarrow{f} y \qquad S^1 = \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (0,0) circle (1); \node at (0,0) {$f$}; \node at (1,0) {$x$}; \node at (0,1) {$y$}; \node at (0,0) {$I$}; \end{tikzpicture} $$
Then the tensor product $I \otimes I$ correspond to the filled square (which differs from the underlying graph by the 2-cube in grey). $I \otimes I \otimes S^1$ on the right below is the filled torus where each arrow is a 1-cube, each face of the torus is a 2-cube and the interior is the only 3-cube.

<figure><img src="image_56.png" /></figure>

**Definition 1.3.12.** A *path* $\pi$ in a precubical set is either :

* a non-empty finite sequence $c_1, \dots, c_n$ of 1-cubes such that for every $1 \le i < n$.

$$ \partial_{1,0}^{+}(c_i) = \partial_{1,0}^{-}(c_{i+1}) $$

* the *empty path* $\varepsilon_x$ on a 0-cube $x$.

For the empty path $\varepsilon_x$, we define $\partial_{1,0}^{+}(\varepsilon_x) = \partial_{1,0}^{-}(\varepsilon_x) = x$. Given two paths $\pi = (c_i)_{1 \le i \le n}$ and $\tau = (d_j)_{1 \le j \le p}$ such that $\partial_{1,0}^{+}(c_n) = \partial_{1,0}^{-}(d_1)$ we write $\pi \cdot \tau$ for their concatenation defined as the sequence $c_1 \dots c_n d_1 \dots d_p$.

**Definition 1.3.13.** The precubical transition set associated to a command $c$ is the precubical set $G_c$ with labels in the set $\mathcal{L} = \mathcal{X} \mathcal{I} \mathcal{B}$, equipped with two distinguished 0-cubes $s_c, t_c \in E$ called the *start* and *end*. It is defined inductively as follows, similarly to Definition 1.2.2.

* $G_{\text{skip}}$ is the 0-cube.

* $G_A$ for $A \in \mathcal{X}$ is precubical set with the 1-cubes labelled $A$ with $\partial_{1,0}^{-}(A) = s_P$ and $\partial_{1,0}^{+}(A) = t_P$

$$ s_A \cdot \xrightarrow{A} \cdot t_A $$

* $G_{c_1;c_2} = G_{c_1} \sqcup G_{c_2} [t_{c_1} = s_{c_2}]$

$$ s_{c_1;c_2} = s_{c_1} \cdot \mathcal{G}_{c_1} t_{c_1} \cdot \mathcal{G}_{c_2} s_{c_2} \cdot \mathcal{G}_{c_2} t_{c_2} = t_{c_1;c_2} $$

* With $c = \text{if } b \text{ then } c_1 \text{ else } c_2$,

$$ G_c = (G_{c_1} \sqcup G_{c_2} \sqcup G_b \sqcup G_{\neg b}) [s_b = s_{\neg b}, t_b = s_{c_1}, t_{\neg b} = s_{c_2}, t_{c_1} = t_{c_2}] $$

where
$$G_b = s_b \cdot \dotsb \to \cdot t_b \qquad G_{\neg b} = s_{\neg b} \cdot \dotsb \to \cdot t_{\neg b}$$

Such that

$$G_c = s_c \cdot \begin{array}{@{}c@{\,}c@{}} \begin{tikzpicture}[baseline=-0.5ex, scale=0.3, every node/.style={font=\scriptsize}] 
  \node (b) at (0,0) {$b$};
  \node (c1) at (1,0) {$s_{c_1}$};
  \node (c2) at (2,0) {$s_{c_2}$};
  \node (t1) at (0,1) {$t_{c_1}$};
  \node (t2) at (2,1) {$t_{c_2}$};
  \draw[->] (b) -- (c1) node[left] {$\cdot$};
  \draw[->] (b) -- (c2) node[left] {$\cdot$};
  \draw[->] (c1) -- (c2) node[right] {$\cdot$};
  \node[below=0.25cm of b] {$\sim b$};
  \node[above=0.25cm of c1] {$s_{c_1}$};
  \node[above=0.25cm of c2] {$s_{c_2}$};
  \node[below=0.25cm of t1] {$t_{c_1}$};
  \node[below=0.25cm of t2] {$t_{c_2}$};
\end{tikzpicture} & G_{c_1} \\ 
\begin{tikzpicture}[baseline=-0.5ex, scale=0.3, every node/.style={font=\scriptsize}] 
  \node (b) at (0,0) {$b$};
  \node (c1) at (1,0) {$s_{c_1}$};
  \node (c2) at (2,0) {$s_{c_2}$};
  \node (t1) at (0,1) {$t_{c_1}$};
  \node (t2) at (2,1) {$t_{c_2}$};
  \draw[->] (b) -- (c1) node[left] {$\cdot$};
  \draw[->] (b) -- (c2) node[left] {$\cdot$};
  \draw[->] (c1) -- (c2) node[right] {$\cdot$};
  \node[below=0.25cm of b] {$\sim b$};
  \node[above=0.25cm of c1] {$t_{c_1}$};
  \node[above=0.25cm of c2] {$t_{c_2}$};
  \node[below=0.25cm of t1] {$t_{c_1}$};
  \node[below=0.25cm of t2] {$t_{c_2}$};
\end{tikzpicture} & G_{c_2} \\ 
\begin{tikzpicture}[baseline=-0.5ex, scale=0.3, every node/.style={font=\scriptsize}] 
  \node (b) at (0,0) {$b$};
  \node (c1) at (1,0) {$s_{c_1}$};
  \node (c2) at (2,0) {$s_{c_2}$};
  \node (t1) at (0,1) {$t_{c_1}$};
  \node (t2) at (2,1) {$t_{c_2}$};
  \draw[->] (b) -- (c1) node[left] {$\cdot$};
  \draw[->] (b) -- (c2) node[left] {$\cdot$};
  \draw[->] (c1) -- (c2) node[right] {$\cdot$};
  \node[below=0.25cm of b] {$\sim b$};
  \node[above=0.25cm of c1] {$t_{c_1}$};
  \node[above=0.25cm of c2] {$t_{c_2}$};
  \node[below=0.25cm of t1] {$t_{c_1}$};
  \node[below=0.25cm of t2] {$t_{c_2}$};
\end{tikzpicture} & G_{c_1} \cdot G_{c_2} \\ 
\end{array}$$

* With $c = \mathbf{while} \ b \ do \ c'$, $G_c$ is obtained similarly to the transition graph:

$$s_c = t_{c'} \cdot \begin{array}{@{}c@{\,}c@{}} \begin{tikzpicture}[baseline=-0.5ex, scale=0.3, every node/.style={font=\scriptsize}] 
  \node (b) at (0,0) {$b$};
  \node (c1) at (1,0) {$s_{c_1}$};
  \node (c2) at (2,0) {$s_{c_2}$};
  \node (t1) at (0,1) {$t_{c_1}$};
  \node (t2) at (2,1) {$t_{c_2}$};
  \draw[->] (b) -- (c1) node[left] {$\cdot$};
  \draw[->] (b) -- (c2) node[left] {$\cdot$};
  \draw[->] (c1) -- (c2) node[right] {$\cdot$};
  \node[below=0.25cm of b] {$\sim b$};
  \node[above=0.25cm of c1] {$s_{c_1}$};
  \node[above=0.25cm of c2] {$s_{c_2}$};
  \node[below=0.25cm of t1] {$t_{c_1}$};
  \node[below=0.25cm of t2] {$t_{c_2}$};
\end{tikzpicture} & G_{c'} \\ 
\begin{tikzpicture}[baseline=-0.5ex, scale=0.3, every node/.style={font=\scriptsize}] 
  \node (b) at (0,0) {$b$};
  \node (c1) at (1,0) {$s_{c_1}$};
  \node (c2) at (2,0) {$s_{c_2}$};
  \node (t1) at (0,1) {$t_{c_1}$};
  \node (t2) at (2,1) {$t_{c_2}$};
  \draw[->] (b) -- (c1) node[left] {$\cdot$};
  \draw[->] (b) -- (c2) node[left] {$\cdot$};
  \draw[->] (c1) -- (c2) node[right] {$\cdot$};
  \node[below=0.25cm of b] {$\sim b$};
  \node[above=0.25cm of c1] {$t_{c_1}$};
  \node[above=0.25cm of c2] {$t_{c_2}$};
  \node[below=0.25cm of t1] {$t_{c_1}$};
  \node[below=0.25cm of t2] {$t_{c_2}$};
\end{tikzpicture} & G_{c_1} \cdot G_{c_2} \\ 
\end{array}$$

* $G_{c_1 \parallel c_2} = G_{c_1} \otimes G_{c_2}$. where $s_{c_1 \parallel c_2} = (s_{c_1}, s_{c_2})$ and $t_{c_1 \parallel c_2} = (t_{c_1}, t_{c_2})$

The pruned precubical transition set $\overline{G}_c$ or cubical semantics of $c$ is then obtained by restricting to valid vertices (i.e. 0-cubes) in the sense of Definition 1.2.25.

**Example 1.3.14.** Consider the program $P = A \parallel B$ where $A$ and $B$ are arbitrary actions. Its asynchronous semantics is shown below:

$$\begin{tikzpicture}[baseline=-0.5ex, scale=0.3, every node/.style={font=\scriptsize}] 
  \node (A) at (0,0) {$A$};
  \node (B) at (0,1) {$B$};
  \draw[->] (A) -- (B); 
  \node[above=0.25cm of A] {$\sim$};
  \node[below=0.25cm of B] {$A$};
  \node[above=0.25cm of B] {$\sim$};
  \node[below=0.25cm of B] {$B$};
\end{tikzpicture}$$

Most of the two cubes of the precubical transition set are obtained by adding a 2-cube to each square of this form in the transition graph of the program. Notice that there is a 2-cube introduced by the tensor product $G_A \otimes G_B$ in the precubical transition set, even though the actions $A$ and $B$ might not commute. If the actions do not commute, these cubes will be pruned in the cubical semantics.

**Definition 1.3.15.** Given a precubical set $C$, the dihomotopy relation $\sim$ on paths is the smallest equivalence relation on path, which is a congruence w.r.t. concatenation and such that for all $h \in C_2$

$$(\partial_{2,1}^{+}(h) \cdot \partial_{2,0}^{-}(h)) \sim (\partial_{2,0}^{+}(h) \cdot \partial_{2,1}^{-}(h))$$

i.e. for any figure of the following form, the paths are dihomotopic.
<figure><img src="image_57.png" /></figure>

*Example 1.3.16.* Let us consider the program $P = p_1 \| \dots \| p_n$ with $n + 1$ resources $(a_i)_{0 \le i \le n}$, where $a_0 = a_n$ and $p_i = P_{a_i}; P_{a_{i+1}}; V_{a_i}; V_{a_{i+1}}$, commonly know as the “Dining Philosophers”. For $n = 2$ its semantics is given below. For $n$ philosophers there are more than $2^{2n}$ states and more than $2^{(n-1)^2}$ total traces. In comparison, there are only $2^n - 2$ maximal traces up to dihomotopy. Below we give the cubical semantics associated to the case of two philosophers:

<figure><img src="image_58.png" /></figure>

Another example is the program $P = p_1 \| \dots \| p_n$ where $p_i = P_{a_i}; V_{a_i}$, where all $a_i$ are distinct resources. There are $(2n)!$ maximal traces, but only a single dihomotopy class.

Since the dihomotopy relation is a congruence by definition, the following *fundamental category* can be associated to any precubical set.

**Definition 1.3.17.** The *fundamental category* $\bar{\Pi}_1(C)$ associated to a precubical set $C$ is the category whose objects are the vertices of $C$ and morphisms are paths up to dihomotopy.

This gives us a more compact representation, of all possible paths up to dihomotopy and will prove useful in Section 1.3 in relating our models.

### 1.3.1.2 Coherent programs

Although it was the case in most of the examples up to now, nothing guarantees that the dihomotopy in the cubical semantics as defined in Definition 1.3.15 corresponds to the semantic one in Definition 1.3.2, i.e. two paths are homotopic when they can be transformed into each other by permuting commuting actions as seen in Example 1.3.14. Programs for which this property holds are called coherent: in these programs, two dihomotopic paths have the same semantics.
**Definition 1.3.18.** A conservative program *P* is said to be *coherent* when for every pair of dihomotopic paths π, τ: *x* →* y in* $\bar{G}_P$, π is an execution trace if and only if τ is an execution trace.

*Remark 1.3.19.* Furthermore, for any pair of execution dihomotopic execution traces π, τ: *x* →* y, we have* [[π]] = [[τ]] ([18, 3.42]).

*Example 1.3.20.* The program *x*:=1||*x*:=2 whose cubical semantics is given below is not coherent.

<figure><img src="image_59.png" /></figure>

Indeed, the two paths $\pi = x:=1 \cdot x:=2$ and $\tau = x:=2 \cdot x:=1$ are related by a 2-cube and are thus dihomotopic, but their semantics are not the same $[[\pi]](\sigma_0)(x) = 1 \neq 2 = [[\tau]](\sigma_0)(x)$.

*Remark 1.3.21.* Every sequential program is coherent. Indeed, dihomotopic paths are generated by the constructor $||$, which gets interpreted as a tensor product of precubical sets. In sequential programs, the dihomotopy relation is reduced to equality.

Coherent programs have a very nice property: two dihomotopic paths in a coherent program have the same effect on the state. Thus, in order to verify the executions of the program, it is enough to check a single representative for each dihomotopy class. This allows us to reduce the space of traces to explore during verification, giving results comparable to partial order reduction techniques [23].

Even when compared up to dihomotopy, a program might generate an exponential number of maximal execution traces, for example the program $P = (P_a; V_a) \parallel \dots \parallel (P_a; V_a)$ of $n$ parallel threads, whose cubical semantics is the skeletal cube of dimension $n$ has $n!$ dihomotopy classes of execution traces.

In the following, we suppose that all programs are coherent. Following the POSIX philosophy, we leave to the programmer to make sure this assumption is verified. This is necessary as the property of being coherent is undecidable in general. Indeed, this property implies the ability to check if two pointers are referencing the same variable, also known as the *may-alias property*, which is undecidable when allowing arithmetic of pointers [46, Theorem 2.3] (based on work from [36]).

*Remark 1.3.22.* Given a program *P*, we can make it coherent by placing instructions $P_a$ and $V_a$, where *a* is a fresh mutex, around each action that is not locking or unlocking a resource as shown in the example below. This translation might seem naïve and particularly simple, but it is sometimes used in practical applications such as in the OCaml language [37]. Of course this translation is not optimal, and we refer to [18] for some possible optimizations.

*Example 1.3.23.* Let us consider the program *x*:=1||*x*:=2. It is not coherent since *x*:=1 and *x*:=2 do not commute. Its cubical semantics is shown on the left below and both maximal execution traces are dihomotopic.
<figure><img src="image_60.png" /></figure>

The transformed program is $(P_a; x:=1; V_a) \llbracket (P_a; x:=2; V_a) \rrbracket$. Its pruned cubical semantics is shown on the right above. As no two paths are dihomotopic, it is coherent.

## 1.3.2 Geometric semantics

In this section we will present our final model of concurrent programs of our introductory chapter. This model is based on representing programs by topological spaces, equipped with a notion of direction, that we call *directed spaces*. The aim of this model is to import tools and techniques from algebraic topology in order to simplify the verification of programs. In those models, execution of a program is naturally assimilated to a path in the associated space. The reason we add a notion of direction is to encompass the causality of a program, the order in which operations must be executed (paths should not go back in time). This is why we define a notion of *directed paths*, a subset of all paths, respecting this causality. Many variants of this notion have been proposed, but we will mainly focus here on d-spaces as introduced by Grandis [25], as they provide more tractable results and are more widely accepted.

### 1.3.2.1 Directed spaces

Let us first recall some standard notions of classical topology:

* The unit interval $I$ is the topological space $I = [0, 1]$ with the standard euclidean topology.

* A path $f$ in a topological space is a continuous map $f: I \to X$. $f(0)$ (resp. $f(1)$) is called the source (resp. target) of $f$.

* We sometimes write $f: x \to y$ when talking about the path $f$ when $x = f(0)$ and $y = f(1)$

* A loop is a path where $f(0) = f(1)$

* A path $\varepsilon_x$ is constant when its image is a single point $\{x\}$

A directed topological space is then a topological space in the usual sense of the term, endowed with a coherent set of paths we call its *directed paths*

**Definition 1.3.24.** A *d-space* $(X, dX)$ consists of a topological space $X$ together with a set $dX$ of paths of $X$ - the *directed paths*, or *d-paths* of $X$ - such that:
* All constant paths are in $dX$

* Given a directed path $f$ and a weakly increasing function $\gamma: I \to I$ called a partial reparametrization, then $f \circ \gamma$ is also a directed path

* Given $f, g$ two directed paths, such that $f(1) = g(0)$ the concatenation $f \cdot g$ defined as follows is also a directed path

$$f \cdot g(t) = \begin{cases} f(2t) & \text{if } 0 \le t \le 1/2 \\ g(2t - 1) & \text{otherwise} \end{cases}$$

A subspace $(Y, dY)$ of a d-space $(X, dX)$ is a subset $Y \subseteq X$ with the topology inherited from $X$ and where $dY = \{f \in dX | f(I) \subseteq Y\}$.

The second condition implies in particular that $dX$ is closed under taking sub-paths.

**Definition 1.3.25.** A morphism of d-spaces, or $d$-map, $h: (X, dX) \to (Y, dY)$ is a continuous map $h: X \to Y$ such that for each $f \in dX$, $h \circ f \in dY$. We write **dTop** for the category of d-spaces and d-maps between them.

*Example 1.3.26.* The first example of a directed space is the directed unit interval $\vec{I} = (I, dI)$, with $I = [0, 1]$ the unit interval and $dI$ the set of weakly increasing paths of $I$. This structure is of course not unique, for example, we could have equipped $I$ with the set of constant paths and still got a valid d-space.

*Example 1.3.27.* Many directed spaces can be generated from pospaces, that is, topological spaces $X$ equipped with a partial order, whose graph is a closed subspace of $X \times X$ i.e. that is compatible with the topology of the space. The set $dX$ for such a d-space will simply be the subset of weakly increasing paths. The directed interval from Example 1.3.26 is an example of such a d-space. Another example is the directed $n$-cube $\vec{I}^n$, generated by $I^n$, equipped with the product order.

An important property of **dTop** is that it has all limits and colimits [25, Section 1.4.1]. Furthermore, these should behave somewhat similarly to the (co)limits in the underlying category **Top** as shown by the following proposition.

**Proposition 1.3.28.** The category **dTop** is both complete and co-complete. It has all limits and colimits. Furthermore, the forgetful functor $U: \mathbf{dTop} \to \mathbf{Top}$ has both a left and a right adjoint. Thus, it preserves both limits and colimits.

*Proof.* See [18, Proposition 4.5]. □

<figure><img src="image_61.png" /></figure>

This allows us to give a concrete definition of some (co)limits on directed space, which will be useful constructors for the topological semantics.

**Definition 1.3.29.** By Proposition 1.3.28, we can construct some usual (co)limits, as topological analogues of the operations on graph, as follows:

* The terminal d-space **1** is the space containing a single point $\star$.

* The cartesian product $X \times Y$ of two d-space $X$ and $Y$ is defined as $(X \times Y, d(X \times Y))$ where $d(X \times Y)$ is the set of paths $h: I \to X \times Y$ such that the projection $\pi_1 \circ h$, $\pi_2 \circ h$ are respectively in $dX$ and $dY$.
* The disjoint union $X \sqcup Y$ of two d-space $X, Y$ is defined as $(X \sqcup Y, d(X \sqcup Y))$, where $d(X \sqcup Y)$ is the set of paths $h: I \to X \sqcup Y$ such that $h(I) \subseteq X$ (resp. $h(I) \subseteq Y$) and $h$ when considered as a function from $I$ to $X$ (resp. $Y$) is in $dX$ (resp. $dY$).

* The quotient $X[x = y]$ of a d-space $X$ is defined as $(X[x = y], dX[x = y])$, where $X[x = y]$ is the space obtained by identifying $x$ and $y$ and $dX[x = y]$ is the set of the concatenation (up to reparametrization) of finite sequences of directed paths $(f_i: s_i \to t_i)_{0 \le i \le n}$ in $X$ such that $s_i, t_i \in \{x, y\}$, except possibly for $s_1$ and $t_n$.

*Example 1.3.30.* The product $\vec{S}^1 \times \vec{I}$ of the directed circle and the directed interval gives the filled cylinder on the left. The product $\vec{S}^1 \times \vec{S}^1$ gives the empty torus on the right. The product $\vec{S}^1 \times \vec{I} \times \vec{I}$ would give a filled square toroid similarly to Example 1.3.11.

<figure><img src="image_62.png" /></figure>

### 1.3.2.2 Geometric semantics

The constructions of Section 1.3.2.1 allow us to define semantics of programs in directed topological spaces. These constructions are extremely similar to the constructions of the Definition 1.3.31 and Definition 1.2.2, adding a function to keep track of the consumption of resources.

**Definition 1.3.31.** Given an operational semantics, to any conservative program $P$, we associate a quadruple $(G_P, s_P, t_P, \llbracket P \rrbracket)$ consisting of a directed topological space $G_P$ equipped with two distinguished points $s_P, t_P \in G_P$, the beginning and the end, as well as a function $\llbracket - \rrbracket_P : G_P \to (\mathcal{R} \to \mathbb{Z})$, the *resource consumption*. This quadruple is defined inductively as follows:

* For skip, writing $1 = \{\star\}$ for the terminal d-space:

$$G_{\text{skip}} = 1 \qquad s_{\text{skip}} = \star \qquad t_{\text{skip}} = \star \qquad \llbracket x \rrbracket = 0$$

* For the locking $P_a$. Only 1 unit of $a$ is consumed and nothing else at the halfway point 0.5 of the segment

$$G_{P_a} = \vec{I} \qquad s_{P_a} = 0 \qquad t_{P_a} = 1 \qquad \llbracket x \rrbracket(b) = \mathbb{1}_{x>0.5} \mathbb{1}_{b=a}$$

* For the unlocking $V_a$. Similarly, 1 unit of $a$ is released at 0.5.

$$G_{V_a} = \vec{I} \qquad s_{V_a} = 0 \qquad t_{V_a} = 1 \qquad \llbracket x \rrbracket(b) = -\mathbb{1}_{x \ge 0.5} \mathbb{1}_{b=a}$$
* For any other action $A \in \mathcal{X}$,

$$ G_A = \vec{I} \qquad s_A = 0 \qquad t_A = 1 \qquad [[x]] = \underline{0} $$

* $P = p;q$.

$$ G_{p;q} = (G_p \sqcup G_q)[t_p = s_q] \qquad s_{p;q} = s_p \qquad t_{p;q} = t_q $$

$$ [[x]]_{p;q}(a) = \begin{cases} [[x]]_p(a) & \text{if } x \in G_p \\ [[x]]_p(t_p) + [[x]]_q(a) & \text{if } x \in G_q \end{cases} $$

* $P = \text{if } b \text{ then } p \text{ else } q$

$$ G_P = (G_p \sqcup G_q \sqcup G_b \sqcup G_{-b})[s_b = s_{-b}, t_b = s_p, t_{-b} = s_q, t_p = t_q] $$

Where given a condition $b$ we have $G_b = (\vec{I}, 0, 1, \underline{0})$.

<figure><img src="image_63.png" /></figure>

$$ s_P = s_b \qquad t_P = t_p \qquad [[x]]_P(a) = \begin{cases} 0 & \text{if } x \in G_b \cup G_{-b} \\ [[x]]_p(a) & \text{if } x \in G_p \\ [[x]]_q(a) & \text{if } x \in G_q \end{cases} $$

* $P = \text{while } b \text{ do } q$.

$$ G_P = (G_q \sqcup G_b \sqcup G_{-b})[s_q = t_b, t_q = s_{-b}, s_b = t_q] $$

Where given a condition $b$ we have $G_b = (\vec{I}, 0, 1, \underline{0})$.

<figure><img src="image_64.png" /></figure>

$$ s_P = s_b \qquad t_P = t_{-b} \qquad [[x]]_P(a) = \begin{cases} 0 & \text{if } x \in G_b \cup G_{-b} \\ [[x]]_q(a) & \text{if } x \in G_q \end{cases} $$
$$ \bullet \ P = p \parallel q $$

$$ G_{p \parallel q} = G_p \times G_q \quad s_{p \parallel q} = (s_p, s_q) \quad t_{p \parallel q} = (t_p, t_q) \quad [(x, y)]_{p \parallel q} = [[x]]_p + [[y]]_q $$

The *forbidden region* is defined as the subspace

$$ R_p = \{x \in G_P \mid \exists a \in \mathcal{R}, [[x]](a) > \kappa_a \text{ or } [[x]](a) < 0\} $$

The geometric semantics $\overline{G}_P$ of a program $P$ is the d-space defined as $\overline{G}_P = G_P \setminus R_P$

*Remark 1.3.32.* The resource consumption for all the above constructions is well-defined only because we suppose that we are working with conservative programs [18, Remark 4.14].

The geometric semantics of a program can be seen as a “continuous” counterpart to the semantics we have presented up to now. To each program, we associate a d-space whose directed paths are the executions of a program.

The commutation of the actions will be transposed as the equivalence of path up to continuous deformation, a version of “directed” homotopy, or *dihomotopy*. And we will prove that this notion of dihomotopy is actually equivalent to the one introduced in *Definition 1.3.15*.

*Example 1.3.33.* The geometric semantics of the dining philosophers from Example 1.3.16 is given below in dimension 2 and 3 respectively on the left and right. On each axis, the half-integer coordinates have been labelled by the corresponding action being performed.

<figure><img src="image_65.png" /></figure>

*Example 1.3.34.* Below we give an example of the geometric semantics for the slightly less intuitive case of a program with loops

$$ P = (P_a; \text{while } b \text{ do } (V_a; P_a)) \parallel (P_a; V_a) $$

<figure><img src="image_66.png" /></figure>
## 1.3.3 Homotopy in directed algebraic topology

### 1.3.3.1 Classical homotopy theory

The notion of homotopy is central to algebraic topology. Two maps with the same (co)domain are said to be homotopic when they can be continuously deformed into one another. We simply introduce basic notions to better introduce the study of dihomotopy, homotopy for directed spaces in the following section. We refer to the standard textbooks [4, 27] for more details.

**Definition 1.3.35.** Given two continuous maps between topological spaces $f, g: X \to Y$, a homotopy from $f$ to $g$ is a continuous map $h: I \times X \to Y$ such that $h(0, -) = f$ and $h(1, -) = g$. When such an $h$ exists, the maps $f$ and $g$ are said to be homotopic, written $f \sim g$.

*Remark 1.3.36.* If $X = I$, then $f, g: I \to Y$ are paths on $Y$. And we can thus talk of homotopy of paths. Such a homotopy is said to be *endpoint preserving* when $h(-, 0)$ is the constant function $f(0)$ and $h(-, 1) = f(1)$.

In the following homotopy between two paths is always assumed to be endpoint-preserving.

*Example 1.3.37.* Let us consider $X = I \times I$. Then for any two paths $f, g: x \to y$, if we define $h(t, x) = (1-t)f(x) + tg(x)$, then $h: I \times I \to X$ is an endpoint-preserving homotopy between $f$ and $g$

In directed spaces, the notion of endpoint preserving homotopy between directed paths still makes sense, and we could define homotopy classes of directed paths, and an equivalent of the fundamental category associated to a d-space. However, Example 1.3.38 suggests that when only considering directed paths, the notion of homotopy is not the right one.

*Example 1.3.38.* We give the respective geometric realization of the programs

$$P_a; V_a; P_b; V_b \parallel P_a; V_a; P_b; V_b \text{ and } P_a; V_a; P_b; V_b \parallel P_b; V_b; P_a; V_a$$

We consider all directed paths which are homotopic. This gives us on the left 4 homotopy classes, and on the right only 3 different directed paths up to homotopy. A representative from each class has been given on the semantics.

<figure><img src="image_67.png" /></figure>

<figure><img src="image_68.png" /></figure>

However, both underlying spaces are homeomorphic, and this implies that the homotopy types are similar, i.e. we should have the same homotopy classes.
1.3.3.2 Homotopy in directed spaces

Let us consider the program P = (P_a; V_a) || (P_a; V_a) || (P_a; V_a). Its cubical semantics is the empty cube, with each cube of dimension 2 “filled”, represented on the left of the figure below, while its geometric semantics is represented on the right.

<figure><img src="image_69.png" /></figure>

Now let us consider the two paths highlighted in the cubical and geometric semantics.
In the cubical semantics, they are not dihomotopic, whereas in the geometric semantics
there is a homotopy between both paths as shown in the following figures.

<figure><img src="image_70.png" /></figure>

Some paths used in the homotopy are not directed. And it would not be difficult to
prove that it is not possible to build a homotopy between the paths that would only go
through directed paths. In order for the relation to match the dihomotopy relation of
cubical semantics, we will need a *directed* version of homotopy from [24], that would be
restricted to directed paths, preserving the idea that we cannot go back in time during
execution.

**Definition 1.3.39.** Given a d-space X and two directed paths $f, g: \vec{I} \to X$, a *dihomotopy* between the two directed path $f, g$ is an endpoint-preserving homotopy $h: I \times \vec{I} \to X$ from $f$ to $g$ such that for every $t \in I$, the path $h(t, -)$ is directed. In this case, $f$ and $g$ are called *dihomotopic*, written $f \sim g$.

*Remark 1.3.40.* The set of directed paths *dX* of a d-space *X* is in bijection with d-maps from *Γ* to *X* i.e. *dX* ≈ *dTop*(*Γ*, *X*) similarly to how the set of (non-directed) maps in *X* is by definition *Top*(*I*, *X*). Thus, *f*, *g* in the definition above are indeed directed paths of *X*.

**Proposition 1.3.41.** The dihomotopy relation ~ satisfies the following properties:

• The relation ~ is an equivalence relation

* The relation ~ is compatible with concatenation of paths. Given f, f': x → y and g, g': y → z:

$$
f \sim f' \quad g \sim g' \quad \text{implies} \quad f \cdot g \sim f' \cdot g'
$$
* Up to dihomotopy, concatenation of paths is associative and admits the empty path $\varepsilon$ as identity. Given directed paths $f: w \to x, g: x \to y$ and $h: y \to z$ we have

$$f \cdot (g \cdot h) \sim (f \cdot g) \cdot h \quad \text{and} \quad \varepsilon_x \cdot f \sim f \cdot \varepsilon_y$$

*Proof.* See [18, Lemma 4.32]. □

We can define the category of directed paths up to dihomotopy in a given topological space. Indeed, Proposition 1.3.41 guarantees that composition (concatenation) is well-defined and that the categorical axioms are well-defined.

**Definition 1.3.42.** The fundamental category $\bar{\Pi}_1(X)$ of a directed space $X$ is the category whose objects are the points of $X$ and whose morphisms are the directed paths up to dihomotopy.

*Remark 1.3.43.* The same applies to the homotopy relation. Instead of having a category, we get a groupoid as the lack of direction allows us to define an inverse for each path.

### 1.3.3.3 Geometric realization

In this section, we will relate our geometric model with our precubical model presented in Section 1.3.1 by showing how these precubical sets can be seen as topological spaces obtained by gluing cubes according to the data in the face maps.

**Definition 1.3.44.** The topological space $I^n$ is called the *standard n-cube*.

<figure><img src="image_71.png" /></figure>

As seen in the Example 1.3.27, we have a similar notion for directed spaces, and we'll call $\bar{I}^n$, called the *standard directed n-cube*, whose underlying space is $I^n$ and directed paths are the weakly increasing maps.

Each standard $n$-cube has $2n$ faces, like $n$-cubes of precubical sets, a front and a back face in each direction, which are $(n-1)$-cubes included in $\bar{I}^n$ that can be described by the following inclusion maps:

$$\iota_{n,i}^{-} : I^{n-1} \to I^{n} \qquad \iota_{n,i}^{+} : I^{n-1} \to I^{n}$$

such that

$$\iota_{n,i}^{\alpha}(x_0, \dots, x_{n-1}) = (x_0, \dots, x_{i-1}, \mathbb{1}_{\alpha=+}, x_i, \dots, x_{n-1})$$

These face maps extend to directed standard $n$-cubes. It is thus natural to think of these directed standard $n$-cube as a directed topological counterpart of an $n$-cube. Then, a precubical set is simply a gluing of such cubes.

Formally, this means there is a functor $\bar{I}^{-} : \square \to \mathbf{dTop}$ associating to each element $n$ a standard directed $n$-cube $\bar{I}^n$, that can be extended to a functor $| - | : \square \to \mathbf{dTop}$ defined as follows:
**Definition 1.3.45.** The directed geometric realization functor $|-|: \Box \to \mathbf{dTop}$ is the functor associating a precubical set $C$ to

$$|C| = \coprod_{n \in \mathbb{N}} (C_n \times \bar{I}^n) / \approx$$

Where

* $C_n$ is equipped with the discrete topology and the discrete d-space structure (i.e. only constant paths are directed).

* $\approx$ is the equivalence relation generated by the relations $(\partial_{n,i}^{\alpha}(x), y) \approx (x, i_{n-1,i}^{\alpha}(y))$ for $n \in \mathbb{N}$, $x \in C_n$ and $y \in \bar{I}^{n-1}$.

Every 0-cube $x \in C_0$ is canonically associated to a point in $|C|$, denoted by $|x|$, elements of $C_1$ to segments... For further theoretical background on geometric realization we refer to [39, 22].

*Example 1.3.46.* The geometric realization of the precubical set corresponding to the cylinder and the torus given in Example 1.3.11 are the directed cylinder and directed torus described in Example 1.3.30.

This directed geometrical realization functor gives us a nice way of embedding precubical sets e.g. cubical semantics, in directed topological spaces, e.g. geometric semantic.

**Proposition 1.3.47.** *The directed geometric realization functor $|-|$ preserves all colimits and sends tensor products of finite precubical sets to cartesian products of their directed geometric realization.*

*Proof.* See [18, Proposition 4.12]. □

<figure><img src="image_72.png" /></figure>

**Proposition 1.3.48.** *Given a conservative program $P$ such that for each vertex $x$ of the associated precubical set $C_p$, $\llbracket x \rrbracket(a) \ge 0$ for all resources $a$. Then, the directed geometric realization of its cubical semantics $\bar{C}_P$ embeds as a topological space in $\bar{\mathcal{G}}_P$:*

$$|\bar{C}_P| \to \bar{\mathcal{G}}_P$$

*Proof.* See [18, Proposition 4.19]. □

<figure><img src="image_73.png" /></figure>

*Remark 1.3.49.* The condition $\llbracket x \rrbracket(a) \ge 0$ implies that no resources is released more than its capacity. This is in general good practice and can be considered to be enforced in practical cases.

*Remark 1.3.50.* By slightly modifying the definitions, the above embedding could be turned into an isomorphism, but would make it harder to understand. This can be safely assumed for the rest of the thesis.

*Example 1.3.51.* Consider the program $P = (P_a; P_b; V_b; V_a) \parallel (P_b; P_a; V_a; V_b)$. From left to right we show its cubical semantics, its directed geometric realization and its geometric semantics: the embedding of the realization into the geometric semantics is trivial.
<figure><img src="image_74.png" /></figure>

In Proposition 1.3.48, we saw that the geometric semantics $\overline{\mathcal{G}}_P$ corresponds to the cubical semantics $\overline{\mathcal{C}}_P$ via its directed geometric realization. Formally, $|\overline{\mathcal{C}}_P| = \overline{\mathcal{G}}_P$. In particular, we can associate to each vertex $x \in \overline{\mathcal{C}}_P$ a point $|x| \in \overline{\mathcal{G}}_P$. We will now show that both the geometric and cubical semantics model the execution of programs in the same way. That is to say, they have the same directed paths. This correspondence on paths will only hold up to dihomotopy (as they are much more paths on $\overline{\mathcal{G}}_P$ than $\overline{\mathcal{C}}_P$). This would not be true should we consider paths simply up to homotopy.

**Theorem 1.3.52.** Given a conservative program $P$ with $\overline{\mathcal{C}}_P$ (resp. $\overline{\mathcal{G}}_P$) as its cubical (resp. geometric) semantics. The functor induced by the directed geometric realization between the fundamental category of $\overline{\mathcal{C}}_P$ (Definition 1.3.17) and that of $\overline{\mathcal{G}}_P$ (Definition 1.3.42) is full and faithful:

$$ \Pi_1(\overline{\mathcal{C}}_P) \hookrightarrow \Pi_1(\overline{\mathcal{G}}_P) $$

This is equivalent to saying that for each vertex $x, y \in \overline{\mathcal{C}}_P$, there is a bijection between paths from $x$ to $y$ (in the cubical sense) and paths from $|x|$ to $|y|$ in $\overline{\mathcal{G}}_P$ (up to dihomotopy).

*Proof.* See [18, Theorem 4.38]. □

*Example 1.3.53.* Let us consider the program $P = P_a; V_a; P_b; V_b \parallel P_a; V_a; P_b; V_b$. Its cubical and geometrical semantics is respectively shown on the left and the right below.

<figure><img src="image_75.png" /></figure>

The dotted path in the geometric semantics is dihomotopic to the dashed path, which corresponds to the image of a path in the cubical semantics.
The embedding above cannot be directly extended to an equivalence of categories. Indeed, considering a portion of the dotted path in Example 1.3.53, no dihomotopic path which is the image of a cubical path can be found. However, it is always possible to extend a path in the geometric semantics so that it is dihomotopic to the realization of a cubical path.

**Proposition 1.3.54.** Given a conservative program *P*, for every path *f*: *x* → *y* in $\bar{G}_P$, there exists a path *g*: $v_1 \to v_2$ in $\bar{C}_P$ and paths $f_1$: $|v_1| \to *x$ and $f_2$: $*y \to |v_2|$ such that the paths $f_2 \cdot *f \cdot f_1$ and $|g|$ are dihomotopic:

<figure><img src="image_76.png" /></figure>

Moreover, if *x* (resp. *y*) is the realization of a point in $\bar{C}_P$ then $v_1$ (resp. $v_2$) can always be chosen to be that point.

*Proof.* See [18, Proposition 4.40]. □

<figure><img src="image_77.png" /></figure>

*Remark 1.3.55.* The extensions $f_1$ and $f_2$ provided in Proposition 1.3.54 are not canonical. For instance, consider the geometric semantics of the floating cube $P = P_a \times V_a \parallel P_a \times V_a$ depicted on the left. The path *f* can be extended in two different ways $f_2$ and $f_2'$:

<figure><img src="image_78.png" /></figure>

The path $f \cdot f_2$ and $f \cdot f_2'$ are respectively dihomotopic to each of the two maximal path of the geometric realization of $\bar{C}_P$.

We can now define the geometric semantics of a path by reusing the semantics developed in Section 1.3.1 as follows.

**Definition 1.3.56.** Given a coherent conservative program *P* and two vertices *x*, *y* ∈ $\bar{C}_P$, the *operational semantics* of a path *f*: $|x| \to |y|$ is the function $[[f]]$: $\Sigma \to \Sigma$ defined as $[[f]] = [[g]]$ for some path *g*: *x* → *y* in $\bar{C}_P$ such that $|g| = |f|$

The existence of *g* is guaranteed by Theorem 1.3.52. Furthermore, the definition does not depend on the choice of *g*. Indeed, two paths with the same realization are dihomotopic (in the cubical sense). As the program is coherent, their semantics are the same.
*Remark 1.3.57.* Extremal points such as deadlocks and the starting and ending points in the geometric realization of the cubical semantics are the geometric realization of a vertex in $\bar{C}_P$, so the above definition covers the majority of interesting paths. We refer to [18, Section 4.2.3] for more details.

*Remark 1.3.58.* If we consider a program of the form $P = A \llcorner B$. Its cubical and geometric semantics are respectively shown on the left and right below.

<figure><img src="image_79.png" /></figure>

The path *f* is dihomotopic to the geometric realization of both maximal paths in the cubical semantics $B \cdot A$ and $A \cdot B$. Then we could define $[f] = [A] \circ [B]$ or $[f] = [[B]] \circ [[A]]$. If the program is not coherent, then there is no guarantee that $[A] \circ [B] = [[B]] \circ [[A]]$ and that the semantics of *f* can be defined.

The Proposition 1.3.54 allows us to consider the geometric counterparts of the “undesirable positions” introduced in Definition 1.1.29 and Proposition 1.2.35.

**Definition 1.3.59.** Given a conservative program *P*, the points *x* of its geometric semantics $\bar{G}_P$ corresponding to Definition 1.1.29 can be identified as follows:

* If there is no directed path $f: s_p \to x$, then *x* is unreachable.

* If $x \neq t_P$ and the only directed path from *x* is the empty path $\varepsilon_x$, then *x* is a deadlock.

* If there exists a directed path $f: x \to y$, where *y* is a deadlock, then *x* is unsafe.

* If there is no dipath $f: x \to t_P$, then *x* is doomed.

The subspace of $\bar{G}_P$ consisting of unreachable (resp. unsafe, resp. doomed) points is called the unreachable (resp. unsafe, resp. doomed) region.

*Remark 1.3.60.* We remind that these are only potential deadlock, unsafe, doomed points as they might be unreachable (in the sense that they might correspond to state that might not be reached by the program).

## 1.4 The boolean algebra of cubical regions

We present here the work of [18], which exhibits an algorithm for detecting deadlocks, unsafe and doomed positions in parallel programs. We will restrict our presentation to the cases of simple programs (Definition 1.4.1) and refer to [18] for the extension to parallel composition of more complex threads. The idea of this section is to represent subspaces of the geometric semantics $\bar{G}_P$ by a set of “maximal” cubes that covers the underlying subspace. These sets of cubes give a finite representation with some nice properties of geometric realization of programs which is what we will be manipulating in the algorithms of Section 1.4.3 to find the deadlocks, unsafe and doomed regions.
### 1.4.1 Cubical cover of simple programs

**Definition 1.4.1.** A simple program is a program of the form $P = p_1 \| \dots \| p_n$, where the programs $p_i$ consists purely of sequences of actions (i.e. they do not contain any conditional branching, loops or parallel composition). In this case, the programs $p_i$ are called processes, and $n$ is called the dimension of the program.

Simple programs are nice and easy to use as their geometric semantics correspond to a standard directed $n$-cube, with some cubes carved out as shown in Proposition 1.4.2.

**Proposition 1.4.2.** The geometric semantics of a simple program $P$ of dimension $n$ is isomorphic to a $d$-space of the form

$$ \bar{\mathcal{G}}_P = I^n \setminus \bigcup_{0 \le i \le k} R^i \quad \text{with} \quad R^i = \prod_{j=1}^{n} |x_j^i, y_j^i| $$

with $l \in \mathbb{N}$ and for all $i \in [1:n]$, $x_j^i < y_j^i \in \{-\infty\} \cup \tilde{I}^n \cup \{\infty\}$.

*Proof.* See [18, Equation (5.1)]. □

<figure><img src="image_80.png" /></figure>

Furthermore, the regions $R^i$ in Proposition 1.4.2 can be chosen to correspond to a conflict on a particular resource $a_i$. For a program with two threads and mutexes, this means that the lower bound of $R^i$ will correspond to a thread trying to lock $a_i$ while it is already locked up to its capacity. Similarly, the upper bound of $R^i$ will correspond to an instruction $V_{a_i}$ from both threads as in Example 1.4.3 below.

*Example 1.4.3.* Let us consider the program $P = P_a; V_a \| P_a; V_a$. Its geometric semantics, shown below is clearly isomorphic to $\tilde{I}^2 \setminus \{\frac{1}{3}, \frac{2}{3}[\times]\frac{1}{3}, \frac{2}{3}[\times]\frac{1}{3}, \frac{2}{3}[\times]\frac{1}{3}\}$, where $\{\frac{1}{3}, \frac{2}{3}[\times]\frac{1}{3}, \frac{2}{3}[\times]\frac{1}{3}\}$ [clearly corresponds to the conflict on $a$]. The precise coordinates of the forbidden region do not matter as we always consider up to isomorphism of $d$-space.

<figure><img src="image_81.png" /></figure>

For the rest of Section 1.4, we will only consider simple programs for ease of presentation, but the algorithms could be adapted to any programs without loops. See [18, Section 5.1] for more details.

**Definition 1.4.4.** Given a space $X \subseteq \tilde{I}^n$, a cubical cover $R = (R^i)_{i \in I}$ of $X$ is a finite family of $n$-cubes with open or closed boundaries in $X$ such that $\bigcup_{i \in I} R^i = X$.

**Definition 1.4.5.** A space $X$ which admits a cubical cover is called a cubical region. We write $C_n$ (resp. $R_n$) for the set of cubical covers (resp. regions) included in $\tilde{I}^n$

*Remark 1.4.6.* The results presented in [18] and in this section are for cubes that can have both open and closed boundaries. This has some effects on computations that will not be detailed here.
Finite cubical covers provide a nice way of representing the associated cubical region and manipulating them algorithmically. In the next Chapter 3, we will give a more precise implementation of these operations on cubes.

**Proposition 1.4.7.** The set of cubical regions is closed under union, intersection and complement in $\overline{I}^n$. It is thus a boolean subalgebra of the power set $\mathfrak{P}(\overline{I}^n)$.

*Proof.* See [18, Proposition 5.3]. □

<figure><img src="image_82.png" /></figure>

## 1.4.2 Maximal cubical covers

A cubical region generally admits multiple cubical covers, however there is always a canonical one which represents the cubical region, and usual operations can be performed quite efficiently on this representation.

Intuitively, a cover that uses bigger intervals is “more economical” than one that uses smaller intervals, as it requires less of those intervals to cover the same region. This gives us a first criterion for finding a most economical region, by ordering regions by inclusion of their intervals.

**Definition 1.4.8.** Let $R$ and $S$ be two cubical covers of a space $X$. The relation $\preceq$ defined as follows is a preorder on the cubical covers of $X$

$$R \preceq S \iff \forall R^i \in R, \exists S^j \in S, R^i \subseteq S^j$$

*Example 1.4.9.* Let us consider the space $X \subseteq \overline{I}^2$ on the left. Both $R = \{R^1, R^2, R^3, R^4\}$ and $S = \{R^1, R^2\}$ are cubical covers of $X$, but $S \preceq R$, as we consider that $R$ carries more information about the region, as it has more of the maximal cubes included in $X$.

<figure><img src="image_83.png" /></figure>

This is not enough to define the normal form as a maximal element. Indeed, taking from the previous Example 1.4.9, adding any cube included in $R_1$ to our cover gives an equivalent cover w.r.t. $\preceq$. We not only need covers that contain all maximal cubes, but we need a way of identifying covers that are more economical than others.

**Definition 1.4.10.** For the finite cubical covers of a space $X$, we can define a partial order $\leq$ from the preorder $\preceq$ as follows. Given $R, S$ two cubical covers, we define

$$R \leq S \iff R \preceq S \preceq R \text{ and } S \subseteq R$$

It can be shown that the poset of cubical covers of $X$, equipped with $\leq$ defined above admits a maximum element. We will call this maximum element the *normal form* of the cubical region $X$, which consists of all the maximal $n$-cubes included in $X$. We will write $C_n^{\max} \subseteq C_n$ for the set of cubical covers in normal form.
**Proposition 1.4.11.** Let us consider the functions $U_n: C_n \to \mathbb{R}_n$ which associate to a cubical cover $R$ the region $U_n(R) = \bigcup_{R^i \in R} R^i$ and $C_n^{\max}$ which associate to a cubical region $X$, the finite set $C_n^{\max}(X)$ of its maximal cubes w.r.t. to inclusion. Then there is an adjunction of functors, between the posets $(C_n, \leq)$ and $(\mathbb{R}_n, \subseteq)$, called a Galois connection, written

$$ (C_n, \leq) \xrightarrow{\overleftarrow{C_n^{\max}}} (\mathbb{R}_n, \subseteq) $$

When restricting to $U_n$ to $C_n^{\max}$, this Galois connection induces a bijection between the cubical regions $\mathbb{R}_n$ and the cubical covers in normal form $C_n^{\max}$.

*Proof.* See [18, Proposition 5.6]. □

<figure><img src="image_84.png" /></figure>

Among other things, this implies that $C_n^{\max}(X)$ is the maximal cubical cover of a cubical region $X$ w.r.t. to $\leq$, which we will define as the normal form of the cubical region $X$. The Galois connection above extends the boolean algebra structure to the normal forms, but it is not very useful in practice because we do not have yet a way of computing the normal cover associated to a region. But as we will see, we can compute “pre-normal” covers of the complement of cubical covers.

**Definition 1.4.12.** Given two $n$-cubes $R^1 = \prod_{k=1}^n [x_k^1, y_k^1]$ and $R^2 = \prod_{i=1}^n [x_k^2, y_k^2]$ of $\vec{I}$, we define their intersection $R^1 \cap R^2$ as follows:

$$ R^1 \cap R^2 = \prod_{k=1}^{n} [\max(x_k^1, x_k^2), \min(y_k^1, y_k^2)] $$

**Definition 1.4.13.** Given two cubical covers $R = (R^i)_{i \in I}$, $S = (S^j)_{j \in J}$, we define their intersection $R \cap S$ as follows:

$$ R \cap S = \{R^i \cap S^j \mid R^i \in R, S^j \in S\} $$

**Proposition 1.4.14.** Given an $n$-cube $C = \prod_{j=1}^n [x_j, y_j]$ of $\vec{I}^n$. The maximal cubical cover of its complement is given by

$$ C^c = \{ \prod_{i=1}^{n} \mathbb{I}_{i,j}^{0} \mid 0 \leq j \leq n \} \cup \{ \prod_{i=1}^{n} \mathbb{I}_{i,j}^{1} \mid 0 \leq j \leq n \} $$

where

$$ \mathbb{I}_{i,j}^{0} = \begin{cases} I & \text{if } i \neq j \\ [0, x_j] & \text{if } i = j \end{cases} \qquad \mathbb{I}_{i,j}^{1} = \begin{cases} I & \text{if } i \neq j \\ [y_j, 1] & \text{if } i = j \end{cases} $$

*Proof.* It is trivial to check that all the cubes are in the complement. And by definition they can't be included in any other cube of the complement and any other cube will be included in such a cube. □

<figure><img src="image_85.png" /></figure>

**Remark 1.4.15.** A similar property holds in the case where some boundaries of $R$ are closed.
A cover is said to be *prenormal* if it contains the normal cover. This implies that we can obtain the normal cover by removing all the cubes that are included in another cube of the prenormal cover.

The intersection in Definition 1.4.13 of two prenormal region can be shown to still be prenormal. Then, a prenormal cover of the complement of any cubical cover $R = (R_i)_{i \in I}$ can be computed as the intersection of the normal (a fortiori prenormal) forms $R_i^c$ of the complements of $R_i$ of Proposition 1.4.14.

**Proposition 1.4.16.** The complement of a cubical cover $R$ of a cubical region $X$ as given in Proposition 1.4.14 is a pre-normal cover of the region $X^c$.

*Proof.* As discussed in the description of [18, Algorithm 5.7], it can be shown that intersection and complement of a prenormal cover are still prenormal. Thus, the complement of a cubical cover $R$ computed as the intersection of the normal (a fortiori prenormal) forms $R_i^c$ of the complements of $R_i$ of Proposition 1.4.14 is prenormal. □

*Example 1.4.17.* Let us apply this to the Swiss Cross, whose semantics has already been described in Example 1.3.51. The forbidden region has two maximal cubes, whose complement are respectively shown on the two figures on the right and left.

<figure><img src="image_86.png" /></figure>

By computing the intersections of all the cubes above in light grey, we get the following maximal cubes, as well as 4 unnecessary cubes shown on the right.

<figure><img src="image_87.png" /></figure>

Thus, by taking the twice complemented region $R^{cc}$, and removing all the cubes that are not maximal, we get the normal form $C_n^{max}(X)$ of the cubical region $X$.

Computing the normal cover of $X$ will allow us to compute the doomed and unsafe regions in Algorithm 1.4.33.

## 1.4.3 Computing deadlocks

### 1.4.3.1 Cubical partitions

The algorithm from [18, Section 5.1] works by first computing a suitable cubical partition of our allowed space $X$, then defining a relation between cubes of this partition corresponding to a notion of “directed connectedness”.
**Definition 1.4.18.** Let $R = (R_i)_{i \in I}$ be a cubical cover of $X$, such that the disjoint union $\coprod_{i \in I} R_i = X$. Then we say that $R$ is a *cubical partition of* $X$. We say that a partition $R$ is coarser than a partition $R'$ if $R \preceq R'$.

**Definition 1.4.19.** A partition $R$ is compatible with a cubical cover $C$ if for each $C_j \in C$, $R_i \subseteq C_j$ or $R_i \cap C_j = \emptyset$.

Let us suppose given a set $X$, and a subset $R = (R_i)_{i \in I}$ of $\mathfrak{P}(X)$, such that $R$ covers $X$. The coarsest partition of $X$ that is compatible with $R$ is obtained by the following method:

1. For each $i \in I$, we define $S_i = R_i$ or its complement $S_i = R_i^c$.

2. We perform the intersection of all $S_i$ for $i \in I$.

For each different choice of $R_i$'s, unless we chose the complement for each $R_i$, the intersection generates a subset of $X$. The set of all these intersections, where we exclude the case where only the complements have been chosen, then generates the coarsest partition of $X$ compatible with $R$.

*Example 1.4.20.* Let us consider the following subset of $[0, 1] \times [0, 1]$ in grey below, and the associated maximal cover:

<figure><img src="image_88.png" /><figcaption>The method described above gives us the following three subsets</figcaption></figure>

<figure><img src="image_89.png" /></figure>

In our case we are not actually dealing with a subset $Y$ of $\mathfrak{P}(X)$, but with its associated cubical cover $R$. We would like the partition we obtain, to be a cubical cover, that is
compatible with $R$ and that it remains a partition when we consider the cubes of the cover. As we have explained that the underlying region already form a partition, the only thing to check is that we can find a maximal cubical cover of each element of the partition with no overlapping cubes.

We define a first try at a cubical cover compatible with a given partition

**Definition 1.4.21.** Given a cubical cover $R$ of a set $X$, we define the *generic 1-dimensional cubical partition*:

$$ \Gamma_1^m(R) = \bigcup_{\substack{U \cup V = R \\ U \neq \emptyset}} C^{\max}(Z_{U,V}) $$

with $Z_{U,V} = \bigcap_{u \in U} [u] \bigcap_{v \in V} [v]^c$

*Example 1.4.22.* Let us consider the Example 1.4.20 above. Each of the subsets generated by the intersections does indeed admit a cubical cover, where none are overlapping.

*Example 1.4.23.* If the initial cover $R$ of $X$ was not maximal, this process does not give a proper cubical partition. Indeed, let us look at the region covered by $\{R_1, R_2\}$ below. The subsets of $X$ generated by the partition do admit a cubical cover, but their cubes overlap.

<figure><img src="image_90.png" /></figure>

*Remark 1.4.24.* It is important to find a partition as coarse as possible as the Algorithm 1.4.33 scales quadratically with the size of the cubical partition.

Unfortunately, this formula is not applicable beyond dimension 2. Indeed, even for maximal cubical covers of cubical regions of $\vec{I}^3$, the method above does not give a cubical partition as shown in Example 1.4.26 below.

*Remark 1.4.25.* In dimension 1, the method above does produce a cubical partition. Indeed, the complement of an interval $[x, y] \subseteq I$ is a region $[0, x[ \times ]y, 1]$, which is covered by two disconnected cubes. Then, the iterated intersection of cubes and their complements in dimension 1 will always lead to sets of disconnected cubes.

*Example 1.4.26.* Let us consider the program

$$ P = (\mathbf{P}_a; \mathbf{P}_b; \mathbf{V}_b; \mathbf{V}_a) \| (\mathbf{P}_a; \mathbf{P}_b; \mathbf{V}_b; \mathbf{V}_a) \| (\mathbf{P}_b; \mathbf{P}_a; \mathbf{V}_a; \mathbf{V}_b) $$

where $a, b$ are two semaphores of arity 2. The two cubes $R_1, R_2$ given below on the left form a cover of its forbidden region. Now, if we consider the intersection $R_1^c \cap R_2$ on the right, we can see that the two maximal cubes $S_1$ and $S_2$ overlap in the lower right corner.
<figure><img src="image_91.png" /></figure>

As we previously explained in Remark 1.4.24, it is important to find a partition as coarse as possible for efficiency, but actually computing the coarsest cubical partition is not necessary by any means, and any cubical partition will suffice.

For now, the best partition we can reasonably implement is the following “generic partition”. Let us suppose given a subset $X \subseteq \vec{I}^n$, and a cubical cover $R = (R_i)_{i \in I}$ of $X$. The *generic cubical partition* is obtained by the following steps:

1. For each axis $1 \le k \le n$, project each cube $R_i \in R$ on the axis $k$, i.e. for each cube $R_i = \prod_{j=1}^n [x_j^i, y_j^i]$, take the projection $[x_k^i, y_k^i]$.

2. For each axis $1 \le k \le n$, compute the coarsest cubical partition $\Gamma_1^m(( [x_k^i, y_k^i ] )_{i \in I})$ associated to the cover $([x_k^i, y_k^i])_{i \in I}$.

3. Compute cartesian product of all covers $\Gamma_1^m(( [x_k^i, y_k^i ] )_{i \in I})$.

4. Remove all the cubes that are not included in $X$.

**Definition 1.4.27.** Given a cubical cover $R$ of a region $X \subseteq \vec{I}^n$, we define the *generic cubical partition* $\Gamma^m(R)$ compatible with $R$ as:

$$ \Gamma^m(R) = \left( \prod_{i=1}^{n} \Gamma_1^m(\{c_i \mid \exists (r_k)_{1 \le k \le n} \in R, r_i = c_i\}) \right) \cap \mathcal{C}_n(R) $$

with $\Gamma_1^m$ the generic 1-dimensional generic partition defined in Definition 1.4.21.

It is clear that this gives a partition compatible with the cover, and is what is used in [18, Chapter 5].

*Example 1.4.28.* Let us consider the Swiss Cross $P = (P_a; P_b; V_b; V_a) \parallel (P_b; P_a; V_a; V_b)$, whose geometric semantics, and associated maximal cover $R$ are given below on the left. Then, in the middle, we get the projection $R^1$ and $R^2$ of the cubes of $R$ on both axes. Finally, on the right, the coarsest cubical partition $\Gamma_1^m(R^i)$, $i = 1, 2$ compatible with the projections.
<figure><img src="image_92.png" /></figure>

Computing the product $\Gamma_1^m(R^1) \times \Gamma_1^m(R^2)$, we obtain the partition on the left below. We see that this partition is not only a partition of the authorized region but of all $\bar{I}^2$. Then by removing the cubes whose associated cubical region is not in $X$, we get the partition of $X$ on the right.

<figure><img src="image_93.png" /></figure>

This method gives a cubical partition of the original subset $X$, which in practice, is quite close to the coarsest cubical partition. Of course some cubes might be partitioned too finely. One could think of trying to fuse cubes and see if the partition remains compatible. In practice the cost of the union and checking proves too great compared with simply executing Algorithm 1.4.33 on a suboptimal cover.

Furthermore, one can check that even for simple programs, the “coarsest cubical partition” might not be properly defined. In particular, going back to Example 1.4.26, there is no single maximal partition in terms of coarseness as shown below:

*Example 1.4.29.* Let us consider the Example 1.4.26, and more precisely, the region $R_1^c \cap R_2$, which is the square torus given below. In this case we have two maximal covers $S = (S_i)_{1 \le i \le 4}$ on the left and $S' = (S'_i)_{1 \le i \le 4}$ on the right. The two partitions given below are both local maximum in terms of coarseness.
<figure><img src="image_94.png" /><figcaption>Remark 1.4.30. As we have defined the intersection and complement of cubes and cubical covers, the computation can be performed directly on the cover for greater efficiency.</figcaption></figure>

### 1.4.3.2 Ordering elements of the partition

The algorithm is based on a “reachability” order defined on the cubes of the coarsest partition. We say that a cube $R_i$ is in the past of $R_j$, when every point of $R_i$ is the origin of a directed path of X that reaches $R_j$. “Being in the past of” is actually the reflexive and transitive closure of the following relation.

**Definition 1.4.31.** Let $R = (R_i)_{i \in I}$ be a cubical partition of the space X. We define the pre-order $\triangleleft^*$ on elements of R as the reflexive transitive closure of the following relation: $R_i \triangleleft R_j$ if and only if for all $x \in [R_i]$ there exists $y \in [R_j]$ and a path of $[R_i] \cup [R_j]$ from x to y.

The relation $\triangleleft$ can be algorithmically computed by suitably comparing the boundaries.

**Proposition 1.4.32.** Given a topological space X $\subseteq \tilde{I}^n$, and two cubes R and S of X:

$$R \triangleleft S \text{ if and only if } R \subseteq \downarrow ((\bar{R} \cap S) \cup (R \cap \bar{S}))$$

where, for any set Y, $\bar{Y}$ correspond to the topological closure of Y and $\downarrow Y = \{x \in X \mid \exists y \in Y, x \le y\}$ is the downwards closure of Y.

*Proof.* [30, Proposition 7.5] □

<figure><img src="image_95.png" /></figure>

In the case of simple programs, the condition for being in the past is even stronger. Indeed, if $R \triangleleft S$, we can even ask the upper bound of R to be in the set $(\bar{R} \cap S) \cup (R \cap \bar{S})$ [30, Corollary 7.1]. Then it is only a matter of computing intersection of cubes (being careful around open borders).

It is on this resulting graph that we find the deadlocks using [18, Algorithm 5.7]. Indeed, the upper corner of an n-cubes $R_i$ of this partition that is not the terminal cube of our program and such that there are no cubes $R_j$ such that $R_i \triangleleft R_j$ is a deadlock [18, Section 5.2].

**Algorithm 1.4.33.** Let $X^c$ be the forbidden region of a program P. $X \subseteq \tilde{I}^n$. We can compute:
1. The normal cubical cover $C_n^{\max}(X)$ of $X$ as maximal cubes of the complement of $X^c$.

2. The generic cubical partition $\Gamma^m(C_n^{\max}(X))$ that is compatible with $C_n^{\max}(X)$.

3. Deadlocks are the cubes of $\Gamma^m(C_n^{\max}(X)) \setminus R_{max}$ that are maximal (w.r.t. $\triangle^*$), where $R_{max}$ is the only cube of $\Gamma^m(C_n^{\max}(X))$ containing the maximal point of $\vec{I}^n$.

4. A cubical partition $\mathcal{U}(X)$ of the unsafe region as the downward closure (w.r.t. $\triangle^*$) of the deadlocks.

5. A cubical partition $\mathcal{D}(X)$ of the doomed region as $\mathcal{U}(X) \setminus \mathcal{E}(X)$, where $\mathcal{E}(X)$ is the downwards closure (w.r.t. $\triangle^*$) of $R_{max}$.

*Example 1.4.34.* Let us take the Swiss cross once more, $P = P_a; P_b; V_b; V_a \parallel P_b; P_a; V_a; V_b$ whose maximal cover has already been computed in Example 1.4.17. Then we can compute the coarsest partition of the allowed region, as shown on the left. From this we find the unsafe region $\mathcal{U}$ and doomed region $\mathcal{D}$.

<figure><img src="image_96.png" /></figure>

This algorithm works well for programs without loops, but is quite complicated to implement (because of all the edge cases for the open and closed boundaries). Furthermore, this algorithm does not handle loops, although another algorithm from [18, Section 5.2] can handle some simple cases with some trade-offs. This will be explored later in Section 4.1.1.2. In Chapter 3, we will develop a new model of programs, based directly on the syntax of our programs, in order to make it easier to implement. We will show that even though we forewent the topological tools, we can still get back similar results, such as the deadlock detection Algorithm 1.4.33, with much more tractable results.
# Chapter 2
## Factoring models of programs

> A coconut is just a nut.

> – Oliver Lugg, *27 Unhelpful Facts About Category Theory*

One way of reducing the size of the state space of a concurrent program is to split it into several groups of processes running independently of each other, i.e. the execution of each group has no effect on the execution of the others. In such situations, we can analyse the processes independently and thus reason modularly on those. This process is very similar to the factorization of integers as products of prime factors or of polynomials as products of monomials.

In order to address this question, Ninin [45, 5] has provided an algorithm in order to factorize isothetic regions (as products of smaller regions), which covers in particular the geometric semantics of concurrent programs as introduced in Chapter 1. From this, we can deduce a factorization of the original program as a product of independent processes. In this chapter, we adopt another point of view and consider factorization of the *category of components* (instead of the geometric semantics). Informally, this category describes all the possible executions of the program, in a very compact way, by trivializing all transitions which have no real impact on the control flow of the program. For loop-free programs, such categories have the property of being *loop-free*, which roughly means that there is no non-trivial endomorphism. This motivates our quest for the more general question of factorizing loop-free categories.

In the 50s, Hashimoto has proved a very strong refinement result for posets [26, 49]: any two decompositions of a connected poset as a cartesian product of posets have a common refinement. In this chapter, we generalize this and show that this result in fact holds more generally for connected loop-free categories. This thus provides us with another approach to the decomposition of the semantics of concurrent (loop-free) programs.

We will first present the existing factorization techniques and framework introduced for program verification. Then we will motivate our extension of Hashimoto's theorem by introducing the category of components, a directed topological invariant which preserves products, and whose factorization leads to the factorization of programs. Finally, we will detail the proof of our refinement theorem for loop-free categories and the larger implications of this property for these categories.
## 2.1 Factorisation à la Ninin

### 2.1.1 Independent processes

Two process are independent when their execution can be freely interleaved without any effect on their evaluation, i.e. when the geometric semantics of their parallel composition is equal to the product of their geometric semantics:

**Definition 2.1.1.** In a program $P \parallel Q$, the processes $P$ and $Q$ are *independent* when

$$ \bar{G}_{P \parallel Q} = \bar{G}_{P} \times \bar{G}_{Q}. $$

Once this notion has been introduced, it is natural to investigate decompositions of programs as products of independent processes, which are maximal in the sense they have the greatest number of non-trivial factors. For some special classes of programs (parallel compositions of conservative programs), such decompositions have been shown to exist [5]. Similar decompositions have also been investigated in various related formalisms such as CCS [41] or π-calculus [16]. Such decompositions are useful because we can show they provide normal forms for programs (up to reordering of processes), similar to the decomposition of integers as products of prime factors.

In some cases, it is very simple to determine when two processes are independent. For instance, a simple criterion is given in [5, 31]: two processes are independent when the sets of resources occurring in each of the two processes are disjoint.

**Example 2.1.2.** Consider the following program $P$:

$$ \begin{array}{l} P = \mathbf{P}_a; \mathbf{V}_a \\ \quad \parallel \mathbf{P}_b; \mathbf{V}_b \\ \quad \parallel \mathbf{P}_b; \mathbf{V}_b \\ \quad \parallel \mathbf{P}_a; \mathbf{V}_a \end{array} $$

It is easy to see that the program $P$ can be factorized in two minimal concurrent programs

$$ P = (\mathbf{P}_b; \mathbf{V}_b \parallel \mathbf{P}_b; \mathbf{V}_b) \parallel (\mathbf{P}_a; \mathbf{V}_a \parallel \mathbf{P}_a; \mathbf{V}_a) $$

Indeed, the two subprograms have no mutex in common (the first one uses only $b$ and the second one only $a$).

Of course, the above condition is sufficient but not necessary, as illustrated in the following example.

**Example 2.1.3.** Fix two mutexes $a, b$ and a semaphore $c$ of arity 2, and consider the program

$$ \begin{array}{l} P = \mathbf{P}_a; \mathbf{P}_c; \mathbf{V}_c; \mathbf{V}_a \\ \quad \parallel \mathbf{P}_a; \mathbf{P}_c; \mathbf{V}_c; \mathbf{V}_a \\ \quad \parallel \mathbf{P}_b; \mathbf{P}_c; \mathbf{V}_c; \mathbf{V}_b \\ \quad \parallel \mathbf{P}_b; \mathbf{P}_c; \mathbf{V}_c; \mathbf{V}_b \end{array} $$
This program can be factorized as

$$P = \left( \mathbf{P}_a; \mathbf{P}_c; \mathbf{V}_c; \mathbf{V}_a \parallel \mathbf{P}_b; \mathbf{P}_c; \mathbf{V}_c; \mathbf{V}_b \right) \parallel \left( \mathbf{P}_a; \mathbf{P}_c; \mathbf{V}_c; \mathbf{V}_a \parallel \mathbf{P}_b; \mathbf{P}_c; \mathbf{V}_c; \mathbf{V}_b \right)$$

since the mutexes a, b prevent c from being taken more than twice at the same time. We will study this example in more details below.

### 2.1.2 The free commutative monoid of cubical covers

The setting in which factorization properties are best studied is the one of free commutative monoids that we now recall.

**Definition 2.1.4.** A monoid $(M, \cdot, e)$ is a set $M$ equipped with an internal multiplication $\cdot : M \times M \to M$ and an element $e$ such that the following properties are satisfied:

* associativity: for any $x, y, z \in M$, $(x \cdot y) \cdot z = x \cdot (y \cdot z)$

* unitarity: for any $x \in M$, $x \cdot e = e \cdot x = x$

We say that the monoid is commutative when $x \cdot y = y \cdot x$ for every $x, y \in M$.

*Example 2.1.5.* $(\mathbb{N}, +, 0)$ is a commutative monoid.

*Example 2.1.6.* $(\{e, a, b\}, \cdot, e)$ with $\cdot$ defined as follows is a non-commutative monoid.

$$a \cdot b = a$$

$$b \cdot a = b$$

$$a \cdot a = a$$

$$b \cdot b = b$$

**Definition 2.1.7.** Let $(M, \cdot, e)$ a monoid. An element $x$ of $M$ is said to be *invertible* when there exists an element $x^{-1}$ of $M$ such that $x \cdot x^{-1} = x^{-1} \cdot x = e$. When such an element exists, it is unique and called the *inverse* of $x$.

**Definition 2.1.8.** Let $(M, \cdot, e)$ a monoid. A non-invertible element $x \in M$ is said to be *irreducible* if for all elements $y, z \in M$, $x = y \cdot z$ implies $y$ or $z$ is invertible.

We recall that a word $w$ on an alphabet $\mathcal{A}$ is a finite sequence of elements of $\mathcal{A}$ and that we write $\mathcal{A}^*$ for the set of all words over $\mathcal{A}$. The concatenation of two words $w = w_1 \dots w_p$ and $w' = w'_1 \dots w'_q$ is given by $w \cdot w' = w_1 \dots w_p w'_1 \dots w'_q$.

**Definition 2.1.9.** Given a set $S$, the free monoid over the set $S$ is the monoid $(S^*, \cdot, \varepsilon)$, where $S^*$ is the set of all words over $S$, equipped with concatenation.

The sets of $n$-cubes of the geometric semantics of a program as defined in Chapter 1 is a commutative monoid when we consider it as the set of homogenous (of the same size) words over the alphabet $\mathcal{A}$ consisting of the set of all sub-intervals of $\vec{I}$ [18, 31]. Indeed, let $\mathcal{A}$ be the set of subintervals of $\vec{I}$, then an $n$-cube is precisely a word of size $n$ on the alphabet $\mathcal{A}$. Furthermore, a cubical cover is a homogenous finite set of such words.

The concatenation operator Definition 1.1.20 induces a monoidal structure on cubical covers which is itself induced by the cartesian product (equivalent to parallel composition of processes).
**Example 2.1.10.** The cubes $[0, 1] \times [0, 1] \times [0, \frac{1}{2}]$ and $[\frac{1}{2}, 1] \times [0, 1]$ can be respectively seen as words of length 3 and 2 over the set of sub-intervals of $[0, 1]$. Their concatenation is simply given by the usual cartesian product

$$[0, 1] \times [0, 1] \times [0, \frac{1}{2}] \cdot [\frac{1}{2}, 1] \times [0, 1] = [0, 1] \times [0, 1] \times [0, \frac{1}{2}] \times [\frac{1}{2}, 1] \times [0, 1]$$

**Definition 2.1.11.** The group $\mathfrak{S}_n$ of all permutations of the set $[1:n]$ is equipped with the tensor product $\otimes$ defined, for all $\sigma \in \mathfrak{S}_p$ and $\tau \in \mathfrak{S}_q$ by $\sigma \otimes \tau \in \mathfrak{S}_{p+q}$ where:

$$(\sigma \otimes \tau)(i) = \begin{cases} \sigma(i) & \text{if } i \le p \\ \tau(i-p) + p & \text{if } p < i \le p+q \end{cases}$$

We have an action of $\mathfrak{S}_n$ on the set of $n$-cubes is given on an $n$-cube $c$ by

$$\sigma.c = (c_{\sigma^{-1}(1)}, \dots, c_{\sigma^{-1}(n)})$$

This action extends to all homogenous sets of cubes (i.e. cubical covers) $R$,

$$\sigma.R := \{\sigma.c \mid c \in R\}$$

The tensor product is compatible with the cartesian product of topological spaces:

**Lemma 2.1.12.** Given two spaces $X \subseteq \vec{I}^p$ and $Y \subseteq \vec{I}^q$, and two permutations $\sigma \in \mathfrak{S}_p, \tau \in \mathfrak{S}_q$ we have $(\sigma.X) \times (\tau.Y) = (\sigma \otimes \tau).(X \times Y)$.

*Proof.* See [18, Lemma 5.23]. □

We also have the expected analogous compatibility property for regions. First we recall the definition of a quotient.

**Definition 2.1.13.** Given a group $\mathfrak{S}$ acting over a set $X$, we define the *quotient* $X/\mathfrak{S}$ as the set of all orbits of elements of $X$ under the action of $\mathfrak{S}$:

$$X/\mathfrak{S} = \{\{\sigma.c \mid \sigma \in \mathfrak{S}_n\} \mid c \in X\}$$

We can then define the following monoids.

**Definition 2.1.14.** Let $\bar{\mathfrak{G}}_p$ be the geometric semantics of a program $P$ and $\mathcal{R}_n$ (resp. $\mathcal{C}_n$) be the set of all cubical regions (resp. cubical covers in normal forms) of $n$-cubes.

* Then $\mathcal{R}^{\mathfrak{S}} = \coprod_{n \in \mathbb{N}} \mathcal{R}_n/\mathfrak{S}_n$, equipped with the concatenation of Definition 1.1.20 (induced by the cartesian product) is the *monoid of cubical regions over* $\bar{\mathfrak{G}}_p$ (up to permutation). Its neutral element is the non-empty 0-dimensional cubical region.

* Similarly, $\mathcal{C}^{\mathfrak{S}} = \coprod_{n \in \mathbb{N}} \mathcal{C}_n^{\max}/\mathfrak{S}_n$ is the *monoid of cubical covers in normal form* (up to permutation) of $\bar{\mathfrak{G}}_p$.

**Proposition 2.1.15.** The monoid $\mathcal{R}^{\mathfrak{S}}$ is isomorphic to $\mathcal{C}^{\mathfrak{S}}$.

*Proof.* [18, Theorem 5.25] □
**Theorem 2.1.16.** In the commutative monoid $\mathcal{R}^{\mathcal{S}}$ of cubical regions, every element can be uniquely factored as a product of irreducible elements.

*Proof.* [18, Theorem 5.26] □

<figure><img src="image_97.png" /></figure>

Given a program $P$, Theorem 2.1.16 imply that every cubical region, and in particular $\bar{\mathcal{G}}_P$ can be factored as a product of irreducible elements. Furthermore, the fact that $\mathcal{R}^{\mathcal{S}}$ are isomorphic $\mathcal{C}^{\mathcal{S}}$ allows us to perform our computation on the maximal cover of $\bar{\mathcal{G}}_P$ instead.

### 2.1.3 Factorization and partition

We have seen above that cubical covers can be factored uniquely as products of irreducible elements. To make a use of this result in practice, we need to be able to compute this factorization.

For implementation matters, it is convenient to represent such factorizations as partitions of $[1:n]$, which are linked to factorization of a homogenous set of elements of a monoid by Lemma 2.1.19 below.

**Definition 2.1.17.** Given an alphabet $\mathcal{A}$ and a word $w = w_1...w_n \in \mathcal{A}^*$. Let $I$ be a subset of $[1:n]$, we write $w|_I$ for the subword of $w$ consisting of letters with indices in $I$. Given a set $R \subseteq \mathcal{A}^n$, we define $R|_I = \{w|_I | w \in R\}$.

**Definition 2.1.18.** Let $w = w_1...w_n \in \mathcal{A}^n$, let $I \subseteq [1:n]$. We write

$$ \pi_I : \mathcal{A}^n \to \mathcal{A}^{|I|} \\ w \mapsto w|_I $$

for the canonical projection.

**Lemma 2.1.19.** Given $I \subseteq [1:n]$, we write $I^c = [1:n] \setminus I$. For a homogenous set $R \subseteq \mathcal{A}^n$ of cubes, we have $R = R|_I \times R|_{I^c}$ if and only if for all $u, v \in R$ there exists $w \in R$ such that $w|_I = u|_I$ and $w|_{I^c} = v|_{I^c}$.

*Proof.* See [18, Lemma 5.27]. □

<figure><img src="image_98.png" /></figure>

In order to find a factorization of a cubical cover $R \subseteq \mathcal{A}^*$ it is enough to check all the subsets $I$ of $[1:n]$ of cardinality less than $n/2$ and, for each of those, check if there is a decomposition of $R$ as $R|_I \times R|_{I^c}$ using the characterization given by the above lemma. This gives us the following algorithm ([18, Algorithm 5.28]), with complexity exponential in the size of the program, which brutally checks all possible decomposition of a set of cubes $R$ as a product of $R|_I \times R|_{I^c}$ (up to permutation), for a given subset $I \subseteq [1:n]$.

**Algorithm 2.1.20.** Given $R \subseteq \mathcal{A}^n$ a cubical cover of the state space in normal form.

1. Choose a set $I \subseteq [1:n]$ such that its cardinal $p \le n/2$.

2. Compute $S_I = \{\pi_{I^c}(\pi_I^{-1}(w)) | w \in \pi_I(R)\}$.

3. If $S_I$ is a singleton then $R$ factorizes as $R|_I \times R|_{I^c}$. Otherwise, go back to the first step and pick another $I$.
4. Proceed recursively with the same algorithm on $R|_I$ and $R|_{I^c}$.

5. Once all sets $I$ are depleted, $R$ is no longer factorizable.

If $I = [1 : p]$, then the set $\pi_{I^c}(\pi_I^{-1}(w))$ associated to a prefix $w \in \pi_I(R)$ of size $p$, is the set of all suffixes of size $n - p$ of words starting by the prefix $w$. Then, the fact that $S_I$, which is a set of sets, is a singleton means that we get the same set $\pi_{I^c}(\pi_I^{-1}(w))$ for all words $w$, which correspond to the fact, that any concatenation $w \cdot w'$ of such a prefix and suffix is a cube of $R$.

*Example 2.1.21.* Let us consider the Example 2.1.3 once more. We remind ourselves that we have two mutexes $a, b$ and a semaphore $c$ of arity 2 and a program

$$P = \begin{array}{l} \pi_1 = P_a; P_c; V_c; V_a \\ \parallel \pi_2 = P_b; P_c; V_c; V_b \\ \parallel \pi_3 = P_a; P_c; V_c; V_a \\ \parallel \pi_4 = P_b; P_c; V_c; V_b \end{array}$$

As seen in Example 2.1.3, even though the independence criterion is not respected, it is possible to factorize this program. The normal cubical cover $R$ of the geometric semantics has the following 16 cubes, where we use $[0, 5]^4$ instead of $\bar{I}^4$ for readability:

$$\begin{array}{l} [0, 5] \times [4, 5] \times [0, 1] \times [0, 5] \qquad [4, 5] \times [0, 5] \times [0, 1] \times [0, 5] \\ [0, 5] \times [4, 5] \times [0, 5] \times [0, 1] \qquad [4, 5] \times [0, 5] \times [0, 5] \times [0, 1] \\ [0, 5] \times [4, 5] \times [0, 5] \times [4, 5] \qquad [4, 5] \times [0, 5] \times [0, 5] \times [4, 5] \\ [0, 5] \times [4, 5] \times [4, 5] \times [0, 5] \qquad [4, 5] \times [0, 5] \times [4, 5] \times [0, 5] \\ \\ [0, 5] \times [0, 1] \times [0, 1] \times [0, 5] \qquad [0, 1] \times [0, 5] \times [0, 1] \times [0, 5] \\ [0, 5] \times [0, 1] \times [0, 5] \times [0, 1] \qquad [0, 1] \times [0, 5] \times [0, 5] \times [0, 1] \\ [0, 5] \times [0, 1] \times [0, 5] \times [4, 5] \qquad [0, 1] \times [0, 5] \times [0, 5] \times [4, 5] \\ [0, 5] \times [0, 1] \times [4, 5] \times [0, 5] \qquad [0, 1] \times [0, 5] \times [4, 5] \times [0, 5] \end{array}$$

Now it is easy to see that independently of the first half of our cubes we consider, the set of associated suffixes will always be the following ones:

$$[0, 1] \times [0, 5] \qquad [0, 5] \times [0, 1] \qquad [0, 5] \times [4, 5] \qquad [4, 5] \times [0, 5]$$

This is precisely the condition $S_I = \{\pi_{I^c}(\pi_I^{-1}(w)) \mid w \in \pi_I(R)\}$ is a singleton for $I = \{1, 2\}$, i.e.

$$R = R|_{1,2} \times R|_{3,4}$$

And indeed, the subprograms $\pi_1 \parallel \pi_2$ and $\pi_3 \parallel \pi_4$ are independent. The algorithm, will then proceed recursively on subsets of $\{1, 2\}$ and $\{3, 4\}$ without finding suitable subsets as the program cannot be factorized further.

This algorithm is not limited to programs whose semantics are $n$-dimensional cubes, but can be extended to any simple program, i.e. any program of the form $P_1 \parallel P_2 \parallel \dots \parallel P_n$ where each $P_i$ does not contain parallel composition, but might contain branchings and even loops [18].
### 2.1.3.1 A more efficient factorization algorithm

Algorithm 2.1.20 can be further improved, thanks to a result by Haucourt and Ninin [31], by exploiting the fact that the n-dimensional cubical regions form a boolean algebra.

**Proposition 2.1.22.** Let $R \subseteq \mathbb{A}^n$ be the cubical cover in normal form of the complement of the state space $X \subseteq \tilde{I}^n$. The prime factorization of $X$ is

$$X = \pi|_{I_1}(X) \times \dots \times \pi|_{I_n}(X)$$

such that $I_1, \dots, I_n$ is the finest partition of $[1:n]$ whose elements are unions of subsets of the form $\{i | \pi_i(u) \neq \tilde{I}\}$.

*Proof.* See [45, Proposition 2.4.10]. □

We can then refine our Algorithm 2.1.20 to be used on the forbidden region which is generally much smaller.

*Example 2.1.23.* Let us restart Example 2.1.21. The forbidden region of the program is

$$\{1, 4[\times]1, 4[\times][0, 5] \times [0, 5], [0, 5] \times [0, 5] \times 1, 4[\times]1, 4[\times]\}$$

From Proposition 2.1.22, the factorization immediately follows. The associated partition of $[1:4]$ being $\{\{1, 2\}, \{3, 4\}\}$.

## 2.2 The category of components

### 2.2.1 Category of components of loop-free programs

A major contribution of algebraic topology is to provide invariants of topological spaces up to homotopy, such as homotopy groups or homology groups. One of the simplest such invariants is the set of connected components of a space. This is very coarse, as for example it does not distinguish between a disk and a circle, which are both connected.

As explained in [18, Section 6] we can refine this invariant by considering both the connected components, and the associated fundamental group for each of the connected components. More abstractly, this invariant can be obtained by taking the skeleton of the fundamental groupoid. The resulting category is often quite small compared to the fundamental groupoid, while retaining much information about the original groupoid. In the example of the disk, whose fundamental groupoid is infinite, the skeleton only has a single object, and a single morphism. For the circle, the skeleton of the fundamental groupoid is reduced to the fundamental group $\mathbb{Z}$.

For directed topological spaces, the notion of fundamental groupoid is replaced by the fundamental category, and the operation of taking the skeleton has to be replaced by the notion of category of components. This notion was introduced in [20] and is now well understood for loop-free categories [28]. Indeed, transposing the category of components in the directed setting is non-trivial: the fundamental category of a d-space often has no non-trivial isomorphisms, meaning that the category is isomorphic to its skeleton. This means that it is necessary to collapse a wider class of morphisms in order to obtain a more compact representation. Intuitively, we collapse all the morphisms which do not change the future or the past of other morphisms.
**Definition 2.2.1.** Given a category $\mathcal{C}$, we say that an object $y$ is in the *future* (resp. *past*) of an object $x$ if $\mathcal{C}(x, y) \neq \emptyset$ (resp. $\mathcal{C}(y, x) \neq \emptyset$).

Given a morphism $f: x \to y$ in a category $\mathcal{C}$, we write $f_*: \mathcal{C}(y, z) \to \mathcal{C}(x, z)$ (resp. $f^*: \mathcal{C}(z, x) \to (z, y)$) for the pre-composition (resp. post-composition) by the morphism $f$.

**Definition 2.2.2.** A morphism $f: x \to y$ is a weak isomorphism if

* for any $z \in \mathcal{C}$, such that $\mathcal{C}(y, z) \neq \emptyset$, $f_*: \mathcal{C}(y, z) \to \mathcal{C}(x, z)$ is a bijection,

* for any $z \in \mathcal{C}$, such that $\mathcal{C}(z, x) \neq \emptyset$, $f^*: \mathcal{C}(z, x) \to \mathcal{C}(z, y)$ is a bijection.

*Remark 2.2.3.* For any isomorphism $f$, both $f_*$ and $f^*$ are bijections: any isomorphism is a weak isomorphism.

*Example 2.2.4.* Let us consider the category $\mathcal{C} = \Pi_1(\bar{\mathcal{G}}_P)$ associated to the fundamental category of the directed semantics of the program

$$P = P_a; x:=1; V_a \| P_a; x:=2; V_a$$

Let us focus on the morphisms $f: x \to y$ and $f': x' \to y'$ given below.

<figure><img src="image_99.png" /></figure>

We can see that $f$ is not a weak isomorphism. Indeed, the morphism $f_*(g) = g \circ f \in \mathcal{C}(x, z)$ is not dihomotopic to the path $h \in \mathcal{C}(x, z)$. Thus, $f_*$ cannot be an isomorphism. It can be shown that the morphism on the right is a weak isomorphism.

Intuitively, the fact that $f$ is not a weak isomorphism corresponds to the fact that when “executing” $f$, we made an irreversible choice during our execution, namely here $x:=2$ will be executed first, changing the value of $x$ in the final state. Then $f'$ being a weak isomorphism could be interpreted from a computing point of view as being the only possible path, up to dihomotopy, between $x'$ and $y'$.

We have seen that programs with while loops are difficult to handle so that it makes sense to first discard them. A similar phenomenon also occurs for categories, motivating the introduction of the following definition of loop-free category [18, Section 6.2, p. 107].

**Definition 2.2.5.** A morphism $f: x \to y$ in a category $\mathcal{C}$ is said to be *without return* when the hom-set $\mathcal{C}(y, x)$ is empty. Otherwise, we say that $f$ admits a return. A category $\mathcal{C}$ is said to be *loop-free* when all its morphisms, except identities, are without return. We write **LFCat** for the category of all small loop-free categories.
**Lemma 2.2.6.** *Given a loop-free category *C*, a morphism *f*: *x* → *y* is a weak isomorphism implies that *C*(*x*, *y*) = {*f*}.*

*Proof.* See [18, Lemma 6.6]. □

However, this is not exactly what we want from this class of morphisms. Indeed, being
the only execution possible from a point to another is not the same as not having made
any irreversible choice, i.e. our notion of inessential transitions, as shown in the example
Example 2.2.7, from [18, Ex. 6.9].

*Example 2.2.7.* Let us revisit the Swiss Cross Example 1.3.51.

<figure><img src="image_100.png" /></figure>

The morphism *f* drawn above is a weak isomorphism, but should not be considered
as inessential. Indeed, executing along *f* makes an "irreversible choice": the terminal
position cannot be reached from *y* but can be from *x*.

In order to rule out morphisms that are weak isomorphisms, but do not correspond
to inessential transitions, we need to restrict the class of weak isomorphisms we are
considering by imposing further restrictions to make it closer to the class of isomorphisms.
One property of isomorphisms is that they are stable under pushouts and pullbacks, which
is not the case for weak isomorphisms in general. And indeed, the collections of weak
isomorphisms satisfying this property rule out the previous Example 2.2.7 and correspond
to our notion of "inessential executions".

**Definition 2.2.8.** Given a category *C*, a system of weak isomorphisms is a collection Σ of weak isomorphisms of *C*, which is stable under pushouts and pullbacks, and contains all isomorphisms. We write **SWI**(*C*) the collection of all such systems.

Since the composite of weak isomorphisms is still a weak isomorphism, it is easy to see
that given a system of weak isomorphisms, its closure under composition is still a system
of weak isomorphisms. We will therefore suppose that the systems we consider are closed
under composition.

*Example 2.2.9.* In the geometric semantics of the Swiss Cross in Example 2.2.7, the morphism *f* cannot be in a collection stable by pushout as there is no pushout with any path *g*: *x* → *t*<sub>*P*</sub>. For example, we can see that there is no possible pushout between *f* and the dotted path in Example 2.2.7

The set SWI(C) is partially ordered by inclusion. This gives rise to a complete lattice
structure, where greatest lower bound is the set-theoretic intersection and the greatest
upper bound is the smallest system w.r.t. inclusion containing the set-theoretic union.
**Proposition 2.2.10.** Given a loop-free category (*C*), the set SWI(*C*) forms a complete lattice, with maximal element noted Σ<sup>*m*</sup>.

*Proof.* [18, Proposition 6.12] □

<figure><img src="image_101.png" /></figure>

For loop-free categories which are finitely presented, such as fundamental categories of loop-free programs, this maximal system can be computed algorithmically by computing the pushouts from the coarsest cubical partition compatible with the normal cover. This is discussed in more details in [18, Section 6.1.4].

This maximal class of weak isomorphisms is precisely what we are aiming to “remove” out of our fundamental category: morphisms that preserve past and future while not interfering with “choices” (i.e. pullback and pushouts). This operation is done by taking the quotient of our category by this maximal class.

**Definition 2.2.11.** The quotient of a category *C* by a set of morphisms Σ is a category *C*/*Σ* together with a quotient functor *Q*: *C* → *C*/*Σ* sending all morphisms in *Σ* to identities and such that any functor *F*: *C* → *D* factors uniquely through *Q* if and only if it sends all morphisms in *Σ* to identities.

<figure><img src="image_102.png" /></figure>

Such a category always exists, see [6], but the resulting category does not necessarily preserve the properties we care about.

*Example 2.2.12.* Let us consider the two following categories. On the left we have a category *G* with two objects *E*, *V* and two arrows *s*, *t* from *E* to *V*. Taking the quotient *G*/{*t*} gives us the category the free category over the graph on the right, which has a countable number of arrows.

<figure><img src="image_103.png" /></figure>

**Definition 2.2.13.** The category of components $\vec{\Pi}_0(C)$ of a loop-free category $C$ is the quotient category $C/\Sigma^m$, where $\Sigma_m$ is the greatest system of weak isomorphisms of SWI($C$). Given a directed topological space $X$, we write $\vec{\Pi}_0(X)$ for $\vec{\Pi}_0(\vec{\Pi}_1(X))$.

When $\Sigma$ is not maximal, the category $C/\Sigma$ can be thought of an over-approximation of the category of components $\vec{\Pi}_0(C)$, in the sense that the latter is a quotient of the former.

*Example 2.2.14.* Below are figured three directed spaces corresponding to geometric realizations of programs, together with the generators of their category of components in superimposition.