Thus

$$
\begin{align*}
[w] \cap [x]^c \cap [y] \cap [z]^c &= [p^*, \bar{\tau}_p^*] \cap [\bar{\vec{\ell}}_q^*, q]^c \\
[w] \cap [x]^c \cap [y] \cap [z]^c &= [p^*, \bar{\tau}_p^*] \cap [\perp^*, \perp^*]^c \cap [\bar{\vec{\ell}}_q^*, q]^c \cap [\perp, \perp]^c \cap [\top, \top]^c
\end{align*}
$$

* Dually, if $U_j = \{x, y\}$ then we have $U_j^\Omega = \{(\vec{\ell}_q^*, q)\}$. Indeed, by the same arguments

$$
\begin{align*}
[w]^c \cap [x] \cap [y] \cap [z]^c &= [p^*, \bar{\tau}_p^*]^c \cap [\vec{\ell}_q^*, q] \\
[w]^c \cap [x] \cap [y] \cap [z]^c &= [p^*, \bar{\tau}_p^*] \cap [\perp^*, \perp^*]^c \cap [\vec{\ell}_q^*, q]^c \cap [\perp, \perp]^c \cap [\top, \top]^c
\end{align*}
$$

* If $U_j = \{w, x, y\}$ then we have $U_j^\Omega = \{(p^*, \bar{\tau}_p^*), (\vec{\ell}_q^*, q)\}$. Indeed,

$$
\begin{align*}
[w] \cap [x] &= ([p^*, \bar{\tau}_p^*] \sqcup [\perp^*, \perp^*] \sqcup [\top, \top]) \cap ([\vec{\ell}_q^*, q] \sqcup [\perp^*, \perp^*] \sqcup [\perp, \perp]) \\
[w] \cap [x] &= ([p^*, \bar{\tau}_p^*] \cap [\vec{\ell}_q^*, q]) \sqcup [\perp^*, \perp^*]
\end{align*}
$$

By Proposition 4.4.18, $[z] = [\top, \top] \sqcup [\perp^*, \perp^*] \sqcup [\perp, \perp]$ i.e. $[z]^c = [\perp^*, \perp^*]^c \cap ([\top, \top] \sqcup [\perp, \perp])^c$, such that

$$
[\perp^*, \perp^*] \cap [z]^c = \emptyset
$$

Additionally $[p^*, \bar{\tau}_p^*] \subseteq [z]^c$ and $[\vec{\ell}_q^*, q] \subseteq [z]^c$. Thus,

$$
[w] \cap [x] \cap [z]^c = [p^*, \bar{\tau}_p^*] \cap [\vec{\ell}_q^*, q]
$$

And once again by Proposition 4.4.18, $[p^*, \bar{\tau}_p^*]$, $[\vec{\ell}_q^*, q] \subseteq [y]$. This implies

$$
\begin{align*}
[w] \cap [x] \cap [z]^c \cap [y] &= [p^*, \bar{\tau}_p^*] \cap [\vec{\ell}_q^*, q] \\
[w] \cap [x] \cap [z]^c \cap [y] &= [p^*, \bar{\tau}_p^*] \cap [\perp^*, \perp^*] \cap [\vec{\ell}_q^*, q]^c \cap [\perp, \perp]^c \cap [\top, \top]^c
\end{align*}
$$

* For all other $U_j$ or $U_j^\Omega$, the intersections of the supports are empty.

Thus, we have for all $j \in J_2$, a partition $U_j^\Omega \amalg V_j^\Omega = \omega(R_j)$ such that

$$
Z_{U_j, V_j} = Z U_j^\Omega, V_j^\Omega
$$

We define for all $j \in J_2$,

$$
U_1^\Omega = \Omega(R_{J_1}) \cap U \qquad U_2 = \bigcup_{j \in J_2} U_j^\Omega \qquad U^\Omega = U_1^\Omega \cup U_2^\Omega
$$

$$
V_1^\Omega = \Omega(R_{J_1}) \cap V \qquad V_2 = R_{J_2} \cap V \qquad V^\Omega = V_1^\Omega \cup V_2^\Omega
$$

By the result above

$$
Z_{U_2, V_2} = \bigcap_{j \in J} Z_{U_j, V_j} = \bigcap_{j \in J} Z_{U_j^\Omega, V_j^\Omega} = Z_{U_2^\Omega, V_2^\Omega}
$$
By Proposition 4.4.18, this implies $\Omega(R_{J_1}) = R_{J_1} = \chi(R_{J_1})$, i.e. $U_1 = U_1^\Omega$ and $V_1 = V_1^\Omega$, which implies a fortiori

$$Z_{U_1, V_1} = Z_{U_1^\Omega, V_1^\Omega}$$

Furthermore, it also implies $U_1^\Omega \amalg V_1^\Omega = \Omega(R_{J_1})$ and by construction $U_2^\Omega \amalg V_2 = \Omega(R_{J_2})$. Thus, we have

$$Z_{U,V} = Z_{U_1,V_1} \cap Z_{U_1,V_1} = Z_{U_1^\Omega,V_1^\Omega} \cap Z_{U_2^\Omega,V_2^\Omega} = Z_{U^\Omega,V^\Omega}$$

This concludes the proof.

□

**Corollary 4.4.42.** Let $P \in \mathbf{Prcs}^*$, $X \subseteq \mathcal{P}(P)$ and $R$ a cover on $P$, such that there exists a family $(R_i)_{i \in I}$ of conservative maximal covers such that $R = \bigcup_{i \in I} R_i$. Then, the existence of a partition $U \amalg V = R$ such that

$$X = \bigcap_{u \in U} [u] \bigcap_{v \in V} [v]^c$$

is equivalent to the existence of a partition $U_\Omega \amalg V_\Omega = \Omega(R)$ such that

$$X = \bigcap_{u_\Omega \in U_\Omega} [u_\Omega] \bigcap_{v_\Omega \in V_\Omega} [v_\Omega]^c$$

*Proof.* Let us suppose given $U \amalg V = R$. Then if we define

$$U_i = U \cap R_i$$

$$V_i = V \cap R_i$$

Then $U_i \amalg V_i = R_i$ and

$$U = \bigcup_{i \in I} U_i$$

$$V = \bigcup_{i \in I} V_i$$

Then by definition,

$$Z_{U,V} = \bigcap_{i \in I} Z_{U_i, V_i}$$

By Proposition 4.4.41, applied to all $U_i \amalg V_i = R_i$ with $R_i$ conservative maximal, this is equivalent to the existence of a partition $U_i^\Omega \amalg V_i^\omega = \Omega(R_i)$ such that

$$Z_{U_i, V_i} = Z_{U_i^\Omega, V_i^\omega}$$

Furthermore, $\Omega(R) = \bigcup_{i \in I} R_i$ implies

$$\bigcup_{i \in I} U_i^\Omega \amalg \bigcup_{i \in I} V_i^\Omega = \Omega(R)$$

Hence by defining $U_\Omega = \bigcup_{i \in I} U_i^\Omega$ and $v_\omega = \bigcup_{i \in I} V_i^\Omega$ we get

$$Z_{U_\Omega, V_\omega} = \bigcap_{i \in I} Z_{U_i^\Omega, V_i^\omega} = \bigcap_{i \in I} Z_{U_i, V_i} = Z_{U,V}$$

This concludes the proof.

□
**Proposition 4.4.43.** Let $P \in \mathbf{Pgrm}$, let $R$ a conservative maximal cover of $P$. Then

$$ \Gamma^m(\Omega(R)) = \Gamma^m(R) $$

*Proof.* As always, we will need to differentiate $P \in \mathbf{Prcs}^*$ and $P = P_1\|\dots\|P_n$.

* $P \in \mathbf{Prcs}^*$. Given a cover $R$ on $P$, such that $R = \bigcup_{i \in I} R_i$ with $R_i$ conservative maximal. We get

$$ \begin{aligned} \Gamma^m(\Omega(R)) &= \bigcup_{U_\Omega \cap V_\Omega = \Omega(R)} \mathcal{C}^{\max}(Z_{U_\Omega, V_\Omega}) \\ &= \bigcup_{U \cap V = \chi(R)} \mathcal{C}^{\max}(Z_{U,V}) \qquad \text{Corollary 4.4.42} \\ \Gamma^m(\Omega(R)) &= \Gamma^m(\chi(R)) \end{aligned} $$

* $P = P_1\|\dots\|P_n$, $P_i \in \mathbf{Prcs}^*$ for all $1 \le i \le n$. Then for any cover $S$ on $P$, we have

$$ \Gamma^m(S) = \left( \prod_{1 \le k \le n} \Gamma^m(\mathcal{P}_k(S)) \right) \cap \mathcal{C}[S] $$

where $\mathcal{P}_k(S) = \{c_k \mid c_1\|\dots\|c_n \in S\}$, which is by Corollary 4.3.8 a union of conservative maximal covers. We have for any $1 \le k \le n$,

$$ \Gamma^m \circ \Omega(\mathcal{P}_k(R)) = \Gamma^m(\chi(\mathcal{P}_k(R))) \qquad \text{by the case above} $$

This is true for all $1 \le k \le n$, then as $\Omega$ distributes over products, we get:

$$ \begin{aligned} \Gamma^m \circ \Omega(R) &= \left( \prod_{1 \le k \le n} \Gamma^m(\mathcal{P}_k(\Omega(R))) \right) \cap \mathcal{C}(\Omega(R)) \\ &= \left( \prod_{1 \le k \le n} \Gamma^m(\mathcal{P}_k(\Omega(R))) \right) \cap \mathcal{C}(R) \\ &= \left( \prod_{1 \le k \le n} \Gamma^m(\Omega(\mathcal{P}_k(R))) \right) \cap \mathcal{C}(R) \\ &= \left( \prod_{1 \le k \le n} \Gamma^m(\mathcal{P}_k(R)) \right) \cap \mathcal{C}(\chi(R)) \\ \Theta \circ \Gamma^m(R) &= \Gamma^m(\chi(R)) \end{aligned} $$

□

**Proposition 4.4.44.** Let $P \in \mathbf{Pgrm}$, let $R$ a conservative maximal cover of $P$. Then

$$ \Gamma^*(\Omega(R)) = \Gamma^*(\chi(R)) $$
Proof.

$$ \Gamma^*(\Omega(R)) = \Gamma^m \circ \Gamma^m(\Omega(R)) \qquad \text{Proposition 3.3.22} $$

$$ = \Gamma^m \circ \Gamma^m(\chi(R)) \qquad \text{Proposition 4.4.43} $$

$$ \Gamma^*(\Omega(R)) = \Gamma^*(\chi(R)) \qquad \text{Proposition 3.3.22} $$

□

### 4.4.2.5 Final Theorem

Finally, we can prove our main theorem on the commutation of the generic cubical partition operator and the lifting of cubes.

**Theorem 4.4.45.** Given a program $P \in \mathbf{Pgrm}$ and a maximal conservative cover $R$ on $P$ we have

$$ \Theta \circ \Gamma^* \circ \Psi^{-1}(R) = \Psi^{-1} \circ \Gamma^*(\chi(R)) $$

*Proof.* By Proposition 4.4.38, we have for any maximal conservative cover

$$ \Theta \circ \Gamma^* \circ \Psi^{-1}(R) = \Psi^{-1} \circ \Gamma^*(\Omega(R)) $$

By Proposition 4.4.44, this implies

$$ \Theta \circ \Gamma^* \circ \Psi^{-1}(R) = \Psi^{-1} \circ \Gamma^*(\chi(R)) $$

□

*Remark 4.4.46.* As $\Psi^{-1}(R^c) = C^{\max}([R]^c)$ (Theorem 4.3.28) the Theorem 4.4.45 also works when taking the complement.

### 4.4.3 Deadlock computation for programs with loops

We now have all the tools required to compute unsafe and doomed covers for programs with loops using the previous algorithm of [18] on the finite unfolding of programs. This algorithm is based on a “reachability” order defined on the cubes of the coarsest partition. Once again, 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 4.4.47.** Let $R = (R_i)_{i \in I}$ be a cubical partition of a preorder $\mathcal{P}$. We define the preorder $\triangleleft$ on elements of $R$ as 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$

Here is the moment where we need to stop seeing $\mathcal{U}(P)$ as a program in and of itself but more as a lens in which we observe its underlying program $P$. When moving across the cubical partition of $\mathcal{U}(P)$, we should really be thinking of being in both copies of $P$ at the same time. And naturally, when seen in this light, it makes sense to jump from any member of an equivalence class to the other when thinking of “being in one’s past”.
**Definition 4.4.48.** Let $P \in \mathbf{Pgrm}$, let $R$ be a conservative cover on $P$. Let $u, v \in \Gamma^m(C_P^m \setminus R)$, then we define $\trianglelefteq$ on the quotient of $\Theta_P(\Gamma^m(C_{\mathcal{U}(P)}^m \setminus \Psi^{-1}(R)))$ by $\approx$ as

$$ \Psi^{-1}(u) \trianglelefteq \Psi^{-1}(v) \iff \exists c, d \in \Psi^{-1}(u) \times \Psi^{-1}(v), c \triangleleft d $$

We define $\trianglelefteq$ as the reflexive, transitive closure of $\trianglelefteq$

*Remark 4.4.49.* For conservative programs, loops have no global effect on the consumption of resources, if one can reach one iteration of the loop, then one can reach it in any further iteration of the loop, one simply needs to execute all the parallel loops sequentially, skirting along the edges of the state space.

As an example, let us consider the program $P = (P_a; P_b; V_b; V_a)^* \parallel (P_b; P_a; V_a; V_b)$. Its unfolding is given by the program

$$ \mathcal{U}(P) = (P_a; P_b; V_b; V_a); (P_a; P_b; V_b; V_a) \parallel (P_b; P_a; V_a; V_b) $$

Looking at its generic partition, the two cubes in grey are equivalent, and indeed, if the first one can be reached, so can be the second one. Paths to each cube are given by the line of cubes on the lower side of the semantics.

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

That is why we consider, with our definition, that a cube is, in a sense, both in the past and in the future of any member of its equivalence class.

Now we can finally prove the intuition we have presented at the beginning of this section. Indeed, the following Theorem 4.4.50 tells us precisely that a cube of the looped program is in the past of another if and only if its equivalence class is in the past of the equivalence class of the other.

**Theorem 4.4.50.** Let $P \in \mathbf{Pgrm}$, let $R$ be a conservative cover on $P$. Let $u, v \in \Gamma^m(C_{\max}^m(R))$, the following properties are equivalent

* $u \triangleleft v$

* $\Psi^{-1}(u) \trianglelefteq \Psi^{-1}(v)$

* There exists $c, d \in \Psi^{-1}(u) \times \Psi^{-1}(v)$ such that $c \triangleleft d$

*Proof.* $P \in \mathbf{Prcs}$. As usual $\Psi$ is the identity, so everything works out.
* $P = S \| T$. Let $c = s \times t, d = u \times v$ in $\Theta_P(\Gamma^m(C_{\mathcal{U}(P)}^m \setminus \Psi^{-1}(R)))$ By Definition 4.1.22, a path from $a \| b \to p \| q$ is a path from $a \to p$ and a path from $b \to q$ such that

$$s \times t \triangleleft u \times v \iff s \triangleleft u \text{ and } t \triangleleft v$$

Similarly

$$\Psi(s \times t) \triangleleft \Psi(u \times v) \iff \Psi(s) \triangleleft \Psi(u) \text{ and } \Psi(t) \triangleleft \Psi(v)$$

Then by applying the induction hypothesis to $\Psi(s) \triangleleft \Psi(u)$ and $\Psi(t) \triangleleft \Psi(v)$. This is equivalent to the existence of $s' \approx s, u' \approx u$ and $t' \approx t, v' \approx v$ such that

$$s' \triangleleft u' \text{ and } t' \triangleleft v'$$

Thus by the remark above it is equivalent to

$$c = s \times t \approx s' \times t' \triangleleft u' \times v' \approx u \times v = d$$

* $P = Q^*$. First let us remark that $x \in \Theta_P(\Gamma^m(C_{\mathcal{U}(P)}^m \setminus \Psi^{-1}(R)))$ implies by definition of $\Theta$

$$- x \in C_0 \cup C_0$$

$$- \text{ or } x = (s; \perp, t; \perp) \in C_5, \perp < s \leq t < \top$$

$$- \text{ or } x = (\top; s, \top; t), \perp < s \leq t < \top$$

And by Theorem 4.4.45, $x \in \Gamma^m(C_P^m \setminus R)$ implies $x \in \Psi \circ \Theta_P \circ \Gamma^m(C_{\mathcal{U}(P)}^m \setminus \Psi^{-1}(R))$ i.e.

$$- x \in \{(\perp, \perp), (\top, \top), (\perp^*, \perp^*)\}$$

$$- \text{ or } x = (s^*, t^*) \in \mathcal{L}_5 \text{ such that } \perp < s \leq t < \top$$

By reduction rules Definition 4.1.22 and by definition of `pred` and `succ`. The only reduction rules possible involving $\perp_P, \perp^*, \top_P$ are

$$- \perp \to \perp^* \text{ and } \perp^* \to \top$$

$$- t^* \to \perp^*, \text{ with } t \in \text{pred}\perp.$$

$$- \perp^* \to s^*, \text{ with } s \in \text{succ}\perp.$$

Similarly, the only reduction rules involving $\perp_{P;P}, \top_{P;P}, \perp;\perp, \top;\perp, \top;\top$ are

$$- \perp \to \perp;\perp \text{ and } \top;\perp \to \top$$

$$- t;\perp \to \top;\perp, \text{ with } t \in \text{pred}\perp.$$

$$- \top; t \to \top;\top, \text{ with } t \in \text{pred}\perp.$$

$$- \perp;\perp \to s;\perp, \text{ with } s \in \text{succ}\perp.$$

$$- \top;\perp \to \top;s, \text{ with } s \in \text{succ}\perp.$$

Such that the only transition by $\triangleleft$ involving cubes of $\{(\perp, \perp), (\top, \top), (\perp^*, \perp^*)\}$ and $C_0 \cup C_0$ are the following (or transition on cubes in the same equivalence class)
$$- (\perp^*, \perp^*) \triangleleft (\top, \top) \text{ and } \Psi^{-1}((\perp^*, \perp^*)) \ni (\top; \top, \top; \top) \triangleleft (\top, \top) \in \Psi^{-1}(\top, \top)$$

$$- (\perp, \perp) \triangleleft (\perp^*, \perp^*) \text{ and } \Psi^{-1}(\perp, \perp) \ni (\perp, \perp) \triangleleft (\perp; \perp, \top; \top) \in \Psi^{-1}((\perp^*, \perp^*))$$

$$- (\perp^*, \perp^*) \triangleleft (s^*, t^*) \text{ with } s \in \text{succ}\perp \text{ and}$$

$$\Psi^{-1}(\perp^*, \perp^*) \ni (\perp; \perp, \perp; \perp) \triangleleft (s; \perp, t; \perp) \in \Psi^{-1}(s^*, t^*)$$

$$- (s^*, t^*) \triangleleft (\perp^*, \perp^*) \text{ with } t \in \text{pred}\perp \text{ and}$$

$$\Psi^{-1}(\perp^*, \perp^*) \ni (\perp; \perp, \perp; \perp) \triangleleft (s; \perp, t; \perp) \in \Psi^{-1}(s^*, t^*)$$

Thus for all these cubes

$$u \triangleleft v \iff \exists c, d \in \Psi^{-1}(u) \times \Psi^{-1}(v), c \triangleleft d$$

Now let $c, d$ such that $\Psi(c) \triangleleft \Psi(d)$. The only case left are when $\Psi(c) = (s^*, t^*)$ and $\Psi(d) = (u^*, v^*)$, such that

$$\Psi^{-1}(\Psi(c)) = \{(s; \perp, t; \perp), (\top; s, \top; t)\}$$

$$\Psi^{-1}(\Psi(d)) = \{(u; \perp, v; \perp), (\top; u, \top; v)\}$$

Then $\Psi(c) \triangleleft \Psi(d)$ implies for all $x^* \in [\Psi(c)]$ there exists $y^* \in [\Psi(d)]$ and a directed path

$$\pi = (z_i^*)_{i \in I}: x^* \to y^* \subseteq [\Psi(c)] \cup [\Psi(d)]$$

Then by Lemma 4.2.14 $\top^* \notin [\Psi(c)] \cup [\Psi(d)]$, i.e. $\top^* \notin \pi$. Thus, we can apply Definition 4.2.13 which gives $z_i^* \in [s^*, t^*]$ is equivalent to $z_i \in [s, t]$ which is equivalent by reduction rule to

$$z_i; \perp \in [s; \perp, t; \perp]$$

Similarly $z_i^* \in [u^*, v^*]$ is equivalent to

$$z_i; \perp \in [u; \perp, v; \perp]$$

Thus $(z_i; \perp)_{i \in I}$ is a directed path of $[s; \perp, t; \perp] \cup [u; \perp, v; \perp]$ from $x; \perp \in (s; \perp, t; \perp) \approx c$ to $y; \perp \in (u; \perp, v; \perp) \approx d$. Similarly, $(\top; z_i)_{i \in I}$ is a directed path of $[\top; s, \top; t] \cup [\top; u, \top; v]$ from $x; \perp \in (\top; s, \top; t) \approx c$ to $y; \perp \in (\top; u, \top; v) \approx d$

□

Now to compute the unsafe and doomed regions of our programs with loops, we simply need to apply Algorithm 3.3.23 to the partition of the unfolding ordered with $\triangleleft$ as in Section 1.4.3 and adding arrows in between all elements of a same equivalence class. From this result, applying $\Psi$ one last time will yield the doomed and unsafe regions.

**Algorithm 4.4.51.** Given a maximal cover $R$ of the forbidden region of the program $P$.

1. We obtain the maximal cover of the forbidden region of the unfolding as $\Psi^{-1}(R)$. Otherwise, compute $\Phi^{-1}[R]$.

2. We obtain a cover of the maximal cubes of the authorized region in the same way as in Algorithm 3.3.23.
3. Compute the generic partition of the forbidden region as $\Theta \circ \Gamma^m(\Psi^{-1}(R)^c)$.

4. Compute $\triangleleft \approx$ using Remark 3.3.26.

5. Compute the deadlocks/unsafe/doomed regions using Algorithm 1.4.33 with the altered order

6. The deadlocks of the base programs are obtained by projecting the obtained deadlocks by $\Phi$. Similarly, for the cubes of the unsafe/doomed region we project using $\Psi$ the cubes obtained in the previous step.

An important thing to understand is that the program actually works in the quotient of the unfolding, where each execution is simultaneously in both copies of the loop, that is why the cubes that are equivalent are reachable from each other, we consider that if we have reached one of the cubes, then we can reach the equivalent cube only in a matter of considering a shift in the iteration we are looking at. This of course only works as we are not considering any variables or boolean test for the programs. This method might be possible to adapt to still work with the addition of these feature, but it would require some efforts.

As an addition, our work not only produces the Algorithm 4.4.51 but also transmits an equivalence between the cubical partition, that we hope in later works to carry further, maybe to an eventual notion of category of components from Chapter 2.

Unfortunately visualization of this algorithm is quite complicated, as the simplest of programs with deadlocks and loops necessitates 3D graphs (at least 2 dimensions for the parallel compositions and one for the loops) which makes it very hard to actually represent what is going on in a “real” conservative programs. An attempt has been made in Example 4.4.52. This method is actually implemented in the tool Sparkling [42] made in collaboration with Samuel Mimram, through the form of textual output.

*Example 4.4.52.* Let us consider the program

$$P = (P_a; P_b; V_b; V_a)^* \| (P_b; P_a; V_a; V_b)$$

Its unfolding is given by the program

$$\mathcal{U}(P) = (P_a; P_b; V_b; V_a); (P_a; P_b; V_b; V_a) \| (P_b; P_a; V_a; V_b)$$

Now let us try to see what our algorithm would give on such a program. To make the illustration more clear some transitions have been omitted. They do not change the fundamental results. First and foremost, if we compute the maximal cubes of P we obtain the following cubes.
<figure><img src="image_205.png" /></figure>
<figure><img src="image_206.png" /></figure>

One can see that the generic partition on the base program will separate each position in its own interval. Indeed, if we look at the projection on $(P_a; P_b; V_b; V_a)^*$ we obtain the following partition.

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

Now if we look at the unfolding of the maximal cubes, we get the following cubes.

<figure><img src="image_208.png" /></figure>
<figure><img src="image_209.png" /></figure>

Now, if we apply the generic cubical partition, we get the following cubes.

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

Then, applying $\Theta$, we obtain the following partition.

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

We recall that the order is different from Algorithm 3.3.23. The two cubes in grey are equivalent for $\trianglelefteq$, meaning we can jump from one to the other, which is the case for any other cube that projects to the same cube on the base program.

The deadlock are easily obtained as the cubes with no transition other than equiva-
lences. Now if we compute the downwards closure of our deadlocks, only taking a single
deadlock would give us the “correct” unsafe region to project, using the aforementioned
equivalence of cubes.

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

Finally, projecting back we get the correct deadlocks and unsafe region for our program
with loops.

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

*Remark 4.4.53.* In the examples we have that the generic partition separates all positions into their own cubes. This is an artefact due to the fact that we are identifying a lot of positions that would get grouped in the same cube for the sake of presentation.
# Chapter 5
## Perspectives

> *Scientists have calculated that the chances of something so patently absurd actually existing are millions to one. But magicians have calculated that million-to-one chances crop up nine times out of ten.*

> — Sir Terry Pratchett, *Mort*

In this thesis we have provided an extension of Hashimoto's theorem about refining product decompositions of partial orders to the case of loop-free categories. Many of the useful topological invariants associated to loop-free programs are naturally expressed in this larger setting. The factorization properties associated to this theorem can now be used for the purpose of studying independent processes in concurrent programs.

We have also provided a new model of programs, based directly on the syntax of programs, which imports powerful theoretical results from the directed topological models, such as Algorithm 1.4.33, in a setting where implementation is much more natural.

We also provide an extension of the aforementioned algorithm in the case of simple programs with non-nested loops, which offers greater theoretical complexity than the previously known Algorithm 4.1.6 on programs with loops for the computation of doomed and unsafe region, while also being easier to implement per our new setting.

### Extension of the deadlock detection algorithm to more general programs

Extending Algorithm 3.3.23 to more than simple programs of **NPIMP** only requires two small steps to be effectively implemented.

The first would be to extend the definition of the generic partition $\Gamma^*$ to handle programs whose semantics is not defined as a product. This could be done by calculating these partitions locally for each $n$-dimensional product of semantics and gluing them at the lower dimension cubes at the frontier. The algorithm could then, through iterated computation, partition the space, starting from the most nested parallel composition and reassemble the cubes.

The second step required would be to give an inductive characterization of cubes, more particularly maximal cubes, in order to perform the separation. Indeed, for now, the characterization of the cubes of a specific constructor, especially in the case of cubes
of loops and unfolding is done through the inductive nature of positions. We feel, that is instead possible of defining cubes of programs inductively from cubes of their subprograms. Results from Lemma 3.3.15, Lemma 3.3.16 and Lemma 4.4.22 even hint at the fact that a certain notion of maximality could be preserved by these constructions.

For programs with nested loops, there is still much work to be done. While most of the proofs are independent (or could easily be extended from the case) of nesting loops, some properties (Definition 4.2.13, Lemma 4.3.16) would need some work to get right. The notion of trivial loop is already defined with this extension in mind and should prove useful in an eventual extension.

## Abstracting properties of syntactic semantics

As announced before, most of the work in Chapter 4 is still in its early stages and the proofs could benefit from some refining. For now, we quite brutally apply the inductive nature of our programs to the proofs and manage to extract the results, with very few results exploiting known facts in graph theory. However, we do believe that there is a nice general setting in which the graphs associated to state space of programs exists.

Indeed, as already hinted at by Lemma 4.4.16 and the proof of Lemma 4.2.14, there is a certain notion of “well-bracketedness” to the graphs of sequential programs: given a main path $\pi$, any pair of paths that split from a vertex must wait for any pair of paths that split further along $\pi$ to rejoin before they can rejoin themselves. Furthermore, paths are confluent (i.e. they always rejoin). On the left below we have an example of a “well-bracketed” graph and on the right, one that does not have such a property.

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

This is due to the fact that we do not have jump instructions in our language, so that when going through a conditional branching we cannot reach the other branches. One can notice that this also extends to loops, and is what gives us the nice characterization of maximal covers (Proposition 4.3.21) and the cutting properties than ensue from it.

## Conservative regions and Alexandroff topology

In our works we had a lot of trouble in how to deal with the core of the loop. We had to force intervals to somehow spread inside the loop, as we feel it is very important to differentiate the different states near the core of the loop (being able to enter, being inside, being able to leave, having left...). We dealt with this problem by forcibly separating these positions through the consideration of conservative regions. This forced the existence of some states ($\perp$ for $P$; $Q$ that should not differ from $\perp$; $\perp$ in principle but whose distinction is important in our proofs when considering loops).

Alexandroff spaces [3] are topological space such that every point has a minimal neighbourhood. For graphs, if we define the subset of its set of vertices $E$ to be the opens,
we define an Alexandroff space, where the minimal neighbourhoods are the edges and stars (a vertex with all initial and terminal edges for that vertex). The fact that minimal neighbourhoods are stars and that we mostly consider edges might solve our problem of discretization around the core of the loops.

Instead of considering positions as we did, one could also look at this topology, which can be defined inductively on programs and could join some nice tools from directed topological spaces and the implementability of our methods.

## Equivalence between topological and syntactic models

Most tools developed in the case of syntactic models were heavily inspired from tools of the directed topological models of concurrent programs. It is then natural to ask if there exists an equivalence between the resulting objects it generates. One good candidate is the category of components associated to a program.

This topological invariant can be constructed from the data of the maximal cover of the topological space, a cubical partition compatible with this cover and the relation $\prec$ (Definition 1.4.31) (see [18, Section 6], [28] for more details). All of which have an equivalent in our syntactic models. It is very reasonable to then ask ourselves if the notion already defined have the same properties and can be used to define a “category of components”. Furthermore, we would also need to know if this “category of components” correspond to the classical notion.

We believe that the links we have stipulated above with the Alexandroff topology on graphs might play an important part, in the equivalences between these models, as a point where these different approach converge.

## Extending lifting property to category of components

In Chapter 4, we have seen that maximal cubes of the base program can be seen as a quotient of the 2-unfolding. The same was also proven for the generic cubical partition (the use of the operator $\Theta$ when considering the generic partitions might complicate our affairs) and the relation $\prec$.

If we can define a notion of category of components for syntactic semantics, it would be interesting to see how this property translates. Even though we don't expect it to work with our current definitions, we have high hopes that many insights can be gained from the attempt.

As previously stated it is still unknown what is the correct definition of the category of components of a program with loops, so there is still much to learn in this direction. Thus considering the quotient, or localization of the category of the 2-unfolding might prove itself insightful in finding the correct way to go about this particular problem.
# Chapter A
## Technical Background

### A.1 Category theory

Here we give an informal primer and reminder on the categorical notion used throughout this thesis. For a more in depth explanation on category theory we refer the reader to the wealth of resources available [38], [21]. As we always deal with small categories in the verification of programs, we have limited our presentation to this case.

**Definition A.1.1 (Category).** A (small) category $\mathcal{C}$ consists of the following data:

* A set $\text{Obj}(\mathcal{C})$ of objects

* For each pair $x, y \in \text{Obj}(\mathcal{C})$ a collection $\text{Hom}_{\mathcal{C}}(x, y)$, alternatively written $\mathcal{C}(x, y)$, of morphisms (or arrows) from $x$ to $y$, called a hom-set.

* For each object $x$ a morphism $\text{id}_x \in \text{Hom}_{\mathcal{C}}(x, x)$ called the identity morphism on $x$

* For each pair $f, g \in \mathcal{C}(y, z) \times \mathcal{C}(x, y)$, a morphism $f \circ g \in \mathcal{C}(x, z)$ called the composite (or composition) of $f$ and $g$ such that:

- Composition is associative i.e. for any triplet $f, g, h \in \mathcal{C}(y, z) \times \mathcal{C}(x, y) \times \mathcal{C}(w, x)$, we have: $f \circ (g \circ h) = (f \circ g) \circ h$

- For any $f \in \text{Hom}_{\mathcal{C}}(x, y)$, $f \circ \text{id}_x = f = \text{id}_y \circ f$

We sometimes write $f: x \to y$ for $f \in \text{Hom}_{\mathcal{C}}(x, y)$.

**Definition A.1.2.** Given a morphism $f: x \to y$, in a category $\mathcal{C}$. We call $x$ (resp. $y$) the *source* (resp. *target*) of $f$

Let $g$ be a second morphism in $\mathcal{C}$, we say that $g$ and $f$ are *co-initial* (resp. *co-final*) if they have the same source (resp. target).

**Definition A.1.3.** Given the four morphisms $f: A \to C$, $g: C \to D$, $h: A \to B$, $k: B \to D$, we say that the following diagram commutes when every path (representing composition of morphism) on the diagram is equal, i.e. $g \circ f = k \circ h$
<figure><img src="image_215.png" /></figure>

**Definition A.1.4.** (Opposite Category) Given a category $\mathcal{C}$, the opposite category $\mathcal{C}^{\text{op}}$ has the same objects as $\mathcal{C}$, but a morphism $f: x \to y$ in $\mathcal{C}^{\text{op}}$ is the same as a morphism $f: y \to x$ in $\mathcal{C}$, and a composite of morphism $g \circ f$ in $\mathcal{C}^{\text{op}}$ is defined to be the composite $f \circ g \in \mathcal{C}$

**Definition A.1.5 (Isomorphism).** Given a category $\mathcal{C}$, and $f \in \mathcal{C}(x, y)$. $f$ is called an isomorphism if there exists a morphism $f^{-1}$ such that

$$f \circ f^{-1} = \mathrm{id}_y$$

$$f^{-1} \circ f = \mathrm{id}_x$$

In this case, $f^{-1}$ is unique and called the inverse of $f$.

**Definition A.1.6 (Groupoid).** A groupoid is a (small) category in which all morphisms are isomorphism

**Definition A.1.7 (Functor).** A functor $F$ from a category $\mathcal{C}$ to a category $\mathcal{D}$ is a map sending each object $x \in \mathcal{C}$ to an object $F(x) \in \mathcal{D}$ and each morphism $f: x \to y$ in $\mathcal{C}$ to morphism $F(f): F(x) \to F(y)$ in $\mathcal{D}$, such that:

* $F$ preserves composition: $F(g \circ f) = F(g) \circ F(f)$ whenever the left-hand side is well-defined

* $F$ preserves identity morphisms: for each object $x \in \mathcal{C}$, $F(\mathrm{id}_x) = \mathrm{id}_x$.

Alternatively, a functor $f: \mathcal{C} \to \mathcal{D}$ sends commutative diagrams in $\mathcal{C}$ to commutative diagrams in $\mathcal{D}$

**Definition A.1.8.** The category **Cat** is the category which has:

* As objects, all (small) categories

* As arrows of $\mathrm{Hom}_{\mathrm{Cat}}(\mathcal{C}, \mathcal{D})$ all functors $F: \mathcal{C} \to \mathcal{D}$

* As composition the evident composition of functors

**Definition A.1.9 (Natural transformation).** Given two categories $\mathcal{C}, \mathcal{D}$ and two functors $F, G: \mathcal{C} \to \mathcal{D}$, a natural transformation $\alpha: F \Rightarrow G$ is a family of maps $(\eta_x: F(x) \to G(x))_{x \in \mathrm{Obj}(\mathcal{C})}$ such that for any morphism $f: x \to y$, the following diagram commutes:

<figure><img src="image_216.png" /></figure>
If each $\eta_{a}: F(x) \to G(x)$ is an isomorphism in $D$, $\eta$ is a natural isomorphism, and we write $F \simeq G$.

**Definition A.1.10 (Presheaves).** Given a small category $\mathcal{S}$, a *presheaf* on $\mathcal{C}$ is a functor

$$F: \mathcal{C}^{\text{op}} \to \mathbf{Set}$$

The category of presheaves on $\mathcal{C}$, denoted $[\mathcal{C}^{\text{op}}, \mathbf{Set}]$, $\mathbf{Set}^{\mathcal{C}^{\text{op}}}$, or simply $\hat{\mathcal{C}}$ has:

* functors $F: \mathcal{C}^{\text{op}} \to \mathbf{Set}$ as objects,

* natural transformations between such functors as morphisms

**Definition A.1.11 (Pullback, pushout).** Given a category $\mathcal{C}$, with $f: a \to c$ and $g: b \to c$, two co-terminal arrows of $\mathcal{C}$. A *pullback* of $f$ and $g$ consists of an object $x$, together with arrows $p_a: x \to a$ and $p_b: x \to b$ such that:

* The following diagram commutes:

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

* For any object $y$ together with a pair of arrows $q_a^y, q_b^y$ verifying the first condition, there exists a unique $h: x \to y$ making the following diagram commute:

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

A *pushout* in $\mathcal{C}$ is a pullback in $\mathcal{C}^{\text{op}}$

**Definition A.1.12 (Product Category).** Given a category $\mathcal{C}$ and any set of its objects $\{X_i\}_{i \in I}$, the *product* of $\{X_i\}_{i \in I}$ is, if it exists an object denoted

$$\prod_{i \in I} X_i \in \mathcal{C}$$

and equipped with morphisms

$$\pi_j: \prod_{i \in I} X_i \to X_j$$
called projections for all $j \in I$, such that for any family of morphisms $\{f_i: Q \to X_i\}_{i \in I}$, there exists a unique morphism

$$ (f_i)_{i \in I}: Q \to \prod_{i \in I} X_i $$

such that all the following diagrams commutes:

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

*Example A.1.13.* In **Cat**, all products are defined (we say that **Cat** has all products). The product of two categories $\mathcal{C}, \mathcal{D}$ is the category $\mathcal{C} \times \mathcal{D}$ which has:

* as set of objects the cartesian product $\text{Obj}(\mathcal{C}) \times \text{Obj}(\mathcal{D})$

* as hom-sets $\text{Hom}_{\mathcal{C} \times \mathcal{D}}(X \times U, Y \times V) = \text{Hom}_{\mathcal{C}}(X, Y) \times \text{Hom}_{\mathcal{D}}(U, V)$

* as composition, the natural composition on pairs i.e. $(g, k) \circ (f, h) = (g \circ f, k \circ h)$

**Definition A.1.14** (Product Preserving Functor). Given a functor $F: \mathcal{C} \to \mathcal{D}$ and $(X_i)_{i \in I}$ a set of objects in $\mathcal{C}$ which admits a product $\prod_{i \in I} X_i$, equipped with projections $\pi_i: \prod_{i \in I} X_i \to X_i$. We say that $F$ preserves this product if $F(\prod_{i \in I} X_i)$, with projections $F(\pi_i)$ is the product of the objects $(F(X_i)_{i \in I})$

**Definition A.1.15** (Hom-Functor). Given a small category, its hom-functor is the functor $\text{Hom}_{\mathcal{C}}(-, -): \mathcal{C}^{op} \times \mathcal{C} \to \text{Set}$ from the product category of $\mathcal{C}^{op}$ and $\mathcal{C}$ to the category of sets, which sends:

* each object $(x, y) \in \mathcal{C}^{op} \times \mathcal{C}$ to the hom-set $\text{Hom}_{\mathcal{C}}(x, y)$

* each morphism $(x, y) \to (w, z)$ of $\mathcal{C}^{op} \times \mathcal{C}$, i.e. each pair of morphism $f^{op}: x \to w$, $g: y \to z$ to the function

$$ \begin{gathered} \text{Hom}_{\mathcal{C}}(x, y) \to \text{Hom}_{\mathcal{C}}(w, z) \\ \{q: x \to y\} \mapsto \{g \circ q \circ f: w \to z\} \end{gathered} $$

**Definition A.1.16** (Adjoint Functors). Given two categories $\mathcal{C}, \mathcal{D}$ and two functors $L: \mathcal{C} \to \mathcal{D}$ and $R: \mathcal{D} \to \mathcal{C}$ We say that $L$ is left adjoint to $R$ (or $R$ right adjoint to $L$) when there exists a natural isomorphism between the hom-functors of the following form:

$$ \text{Hom}_{\mathcal{D}}(L(-), -) \simeq \text{Hom}_{\mathcal{C}}(-, R(-)) $$

Meaning that for all objects $c \in \mathcal{C}$ and all objects $d \in \mathcal{D}$, there is a bijection of hom-sets:

$$ \text{Hom}_{\mathcal{D}}(L(c), d) \stackrel{\sim}{\to} \text{Hom}_{\mathcal{C}}(c, R(d)) $$

which is natural in $c$ and $d$.
**Definition A.1.17** (Full, Faithful, Essentially Surjective). A functor $F: \mathcal{C} \to \mathcal{D}$ is called:

* full if for each pair of objects $x, y \in \mathcal{C}$, the function $F: \mathcal{C}(x, y) \to \mathcal{D}(F(x), F(y))$ between hom-sets is surjective

* faithful if for each pair of objects $x, y \in \mathcal{C}$, the function $F: \mathcal{C}(x, y) \to \mathcal{D}(F(x), F(y))$ between hom-sets is surjective

* fully faithful if it is both full and faithful

* essentially surjective if for every object $y$ of $\mathcal{D}$, there is an object $x$ of $\mathcal{C}$ such that $F(x)$ is isomorphic to $y$.

**Definition A.1.18** (Subcategory). Given a category $\mathcal{C}$, a *subcategory* $\mathcal{D}$ of $\mathcal{C}$ is a subset of the objects of $\mathcal{C}$ and a subset of the set of morphisms of $\mathcal{C}$ such that

* If $f: x \to y$ is in $\mathcal{D}$ so are $x$ and $y$

* If $f: x \to y$ and $g: y \to z$ are in $\mathcal{D}$, so is their composite $g \circ f$.

* If $x$ is an object of $\mathcal{D}$, then $\mathrm{id}_x$ is in $\mathcal{D}$

Then $\mathcal{D}$ is a category in its own right and the inclusion $\mathcal{D} \hookrightarrow \mathcal{C}$ is a functor, called the *inclusion functor*.

**Definition A.1.19** (Skeleton). The *skeleton* of a category $\mathcal{C}$ is the unique subcategory $\mathcal{D}$ of $\mathcal{C}$ such that:

* The inclusion functor $\iota: \mathcal{D} \to \mathcal{C}$ is full,

* The inclusion functor $\iota$ is essentially surjective,

* $\mathcal{D}$ is skeletal, i.e. no two distinct objects of $\mathcal{D}$ are isomorphic.

**Definition A.1.20** (Discrete Fibration). A functor $F: \mathcal{C} \to \mathcal{B}$ is a *discrete fibration* if for every object $c$ in $\mathcal{C}$, and every morphism of the form $g: b \to F(c)$ in $\mathcal{B}$ there is a unique morphism $h: d \to c$ such that $F(h) = g$.

## A.2 Order theory

**Definition A.2.1** (Pre-order). A pre-order $(X, \preceq)$ is a set $X$ equipped with a relation $\preceq$ defined on $X \times X$ such that:

* $\preceq$ is transitive i.e. for any $x, y, z \in X$, $x \preceq y$ and $y \preceq z$ implies $x \preceq z$

* $\preceq$ is reflexive i.e. $x \preceq x$ for all $x \in X$

**Definition A.2.2** (Partial order). A *partial order* $(X, \leq)$ is a set $X$ equipped with a relation $\leq$ defined on $X \times X$ such that:

* $(X, \leq)$ is a pre-order

* $\leq$ is antisymmetric i.e. for any $x, y \in X$, $x \leq y$ and $y \leq x$ implies $x = y$.
We say that $X$ is a partially ordered set, or poset.

**Definition A.2.3 (Bounded Preorder).** A bounded pre-order $(X, \perp, \top)$ is a pre-order $X$ equipped with two distinguished elements $\perp, \top$ such that

* For any $x \in X$, $\perp \leq x$ and $x \not\leq \perp$

* For any $x \in L$, $x \leq \top$ and $\top \not\leq x$

$\perp, \top$ can be seen respectively as the smallest and greatest element of the set $X$.

**Definition A.2.4 (Lattice).** A lattice $(L, \leq, \wedge, \vee)$ is a poset $(L, \leq)$ such that each two-element subset $\{a, b\} \subseteq L$ has:

* a least upper bound (or join) in $L$, denoted $a \vee b$,

* and a greatest lower bound (or meet) in $L$, denoted $a \wedge b$

This is equivalent to requiring that every finite subset $X \subseteq L$ has a join (resp. meet) denoted $\bigvee X$ (resp. $\bigwedge X$)

**Definition A.2.5 (Bounded lattice).** A bounded lattice $(L, \perp, \top)$ is a lattice equipped with two distinguished elements $\perp, \top$ such that

* For any $x \in L$, $x \wedge \perp = \perp$

* For any $x \in L$, $x \vee \top = \top$

Equivalently, $(L, \perp, \top)$ is a bounded lattice if and only if $(L, \perp, \top)$ is a bounded pre-order, where $\perp$ and $\top$ are respectively the smallest and greatest elements.

**Definition A.2.6 (Complete lattice).** A complete lattice $L$ is a lattice where any subset $X \subseteq L$ has a meet $\bigvee X$ and join $\bigwedge X$

By definition, a complete lattice $L$ is bounded, with $\perp = \bigwedge L$, $\top = \bigvee L$

**Definition A.2.7 (Monotone functions).** Given two posets $(C, \leq_C)$, $(D, leq_D)$ a function $f: C \to D$ is monotone when for every $x, y \in C$, $x \leq_C y$ implies $f(x) \leq_D f(y)$

**Definition A.2.8.** Every preorder $X$ can be seen as a category, with $Obj(X) = X$ and each $Hom_X(x, y)$ defined to contain a single element if $x \leq y$, and otherwise it is empty. We write **Pos** for the category of partially ordered sets.

With this definition, a monotone function $f: C \to D$ is a functor from $C$ to $D$, i.e. a morphism in **Pos**

**Definition A.2.9 (Adjunction in posets).** Given two posets $C$, $D$ and a pair of monotone functions $l: CatC \to D$, $r: D \to CatC$, then $l$ is left adjoint to $r$ if and only if for any $c, d \in C \times D$

$$l(x) \leq y \iff x \leq r(y)$$

Alternatively, we say that there is a monotone Galois connection between $C$ and $D$.
**Theorem A.2.10** (Adjunct functor theorem). Given two posets C, D and a pair of monotone functions l: CatC → D, r: D → CatC such that l is left-adjoint to r, then

$$l(c) = \bigvee \{d \in D \mid r(d) = c\}$$

$$r(d) = \bigwedge \{c \in C \mid l(c) = d\}$$

**Definition A.2.11** (Boolean algebra). A Boolean algebra (B, ∧, ∨) is a bounded lattice (B, ∧, ∨) where ∧ and ∨ verify the following additional properties:

* ∧ and ∨ distribute over each other i.e. for any elements x, y, z ∈ B:

$$x \wedge (y \vee z) = (x \wedge y) \vee (x \wedge z)$$

$$x \vee (y \wedge z) = (x \vee y) \wedge (x \vee z)$$

* any element x ∈ B has a complement i.e. there exists x^c ∈ B such that:

$$x \wedge x^c = \perp$$

$$x \vee x^c = \top$$

**Definition A.2.12** (Atomic boolean algebra). Given a Boolean algebra B, an atom is an element a ∈ B, such that for any b ∈ B, b ≤ a implies b = ⊥ or b = a.

A Boolean algebra is atomic if for any element b ∈ B, there exists a set {a_i}_{i∈I_b} of atoms of B such that b = ∨{a_i}_{i∈I_b}.

## A.3 Topology

**Definition A.3.1** (Topological space). Given a set X, a topology τ on X is a collection τ ⊆ P(X) of subset of X called the open subsets of X, such that:

* τ is closed under finite intersections,

* τ is closed under arbitrary union.

A topological space (X, τ) is a set X equipped with a topology τ

**Definition A.3.2** (Metric space). A metric space (X, d_X) is a set X equipped with a distance function d: X × X → [0, +∞[ such that for all x, y, z ∈ X:

* d(x, y) = 0 if and only if x = y

* d(x, y) = d(y, x)

* d(x, z) ≤ d(x, y) + d(y, z)

To any metric space X, we can assign a topology where the open sets of X are the open balls $B_r(x) = \{y \in X \mid d(x, y) < r\}$ for all $x \in X$ and all $r \in \mathbb{R}^+$

**Definition A.3.3** (Euclidian topology). The euclidean topology on $\mathbb{R}^n$, is the topology associated to the metric space ($\mathbb{R}^n$, d), where $d(x, y) = \|x - y\|$, with $\| \cdot \|$ the standard euclidean norm:

$$\|(x_1, \dots, x_n)\| = \sqrt{x_1^2 + \dots + x_n^2}$$
**Definition A.3.4 (Continuous map).** A continuous function $f: (X, \tau_X) \to (Y, \tau_Y)$ between topological spaces is a function $f: X \to Y$ between the underlying sets, such that for every open $V$, the inverse image by $f$ is an open of $X$ i.e. for all $V \subseteq Y$

$$V \in \tau_Y \text{ implies } f^{-1}(V) \in \tau_X$$

**Definition A.3.5 (Paths).** We write $I$ for the unit interval $[0, 1] \subseteq \mathbb{R}$ equipped with the euclidean topology. A path on $X$ is a continuous map $f: I \to X$.

**Definition A.3.6 (Concatenation of maps).** Given $f, g$ two paths on a topological space $X$, such that $f(1) = g(0)$ we call concatenation of $g$ and $f$, the path $g \cdot f$ on $X$, defined as follows:

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

**Definition A.3.7 (Homotopy).** 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$.

The homotopy relation $\sim$ defines an equivalence relation

**Definition A.3.8 (Fundamental groupoid).** The fundamental groupoid $\Pi_1(X)$ associated to the topological space $X$ is the groupoid:

* whose objects are the points of $X$,

* whose morphisms are the equivalence classes of endpoint preserving homotopy on paths of $X$,

* whose composition is defined by concatenation of paths.
Bibliography

[1] Frances E Allen. Control flow analysis. *ACM Sigplan Notices*, 5(7):1–19, 1970.

[2] Bowen Alpern and Fred B Schneider. Recognizing safety and liveness. *Distributed computing*, 2:117–126, 1987.

[3] Francisco G Arenas. Alexandroff spaces. *Acta Math. Univ. Comenianae*, 68(1):17–25, 1999.

[4] Martin Arkowitz. *Introduction to homotopy theory*. Springer Science & Business Media, 2011.

[5] Thibaut Balabonski and Emmanuel Haucourt. A geometric approach to the problem of unique decomposition of processes. *CoRR*, abs/1004.2780, 2010. arXiv:1004.2780.

[6] Marek A. Bednarczyk, Andrzej M. Borzyszkowski, and Wiesław Pawlowski. Generalized congruences-epimorphisms in cat. *Theory and Applications of Categories*, 5(11):266–280, 1999.

[7] Edmund M Clarke. Model checking–my 27-year quest to overcome the state explosion problem. In *International Conference on Logic for Programming Artificial Intelligence and Reasoning*, pages 182–182. Springer, 2008.

[8] Edmund M Clarke, E Allen Emerson, and A Prasad Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. *ACM Transactions on Programming Languages and Systems (TOPLAS)*, 8(2):244–263, 1986.

[9] Cosynus. Alcool, 2018. Available at http://www.lix.polytechnique.fr/cosynus/alcool/.

[10] Patrick Cousot and Radhia Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In *International Symposium on Programming Language Implementation and Logic Programming*, pages 269–295. Springer, 1992.

[11] Edsger W Dijkstra. The structure of the “THE”-multiprogramming system. *Communications of the ACM*, 11(5):341–346, 1968.

[12] Edsger W. Dijkstra. Hierarchical ordering of sequential processes. *Acta informatica*, 1:115–138, 1971.
[13] Edsger W. Dijkstra. *Cooperating Sequential Processes*, pages 65–138. Springer New York, New York, NY, 2002. doi:10.1007/978-1-4757-3472-0_2.

[14] E.W. Dijkstra. Co-operating sequential processes. In *Programming languages : NATO Advanced Study Institute : lectures given at a three weeks Summer School held in Villard-le-Lans, 1966 / ed. by F. Genuys*, pages 43–112, United States, 1968. Academic Press Inc.

[15] Allen B Downey. *The little book of semaphores*. 2005.

[16] Jannik Dreier, Cristian Ene, Pascal Lafourcade, and Yassine Lakhnech. On Unique Decomposition of Processes in the Applied π-Calculus. In *16th International Conference on Foundations of Software Science and Computational Structures (FOS-SACS 2013), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2013)*, Rome, Italy, March 2013. URL: https://inria.hal.science/hal-01338002, doi:10.1007/978-3-642-37075-5_4.

[17] Lisbeth Fajstrup. Loops, ditopology and deadlocks. *Mathematical Structures in Computer Science*, 10(4):459–480, 2000. doi:10.1017/S0960129500003157.

[18] Lisbeth Fajstrup, Éric Goubault, Emmanuel Haucourt, Samuel Mimram, and Martin Raussen. *Directed Algebraic Topology and Concurrency*. Springer International Publishing, 2016. doi:10.1007/978-3-319-15398-8.

[19] Lisbeth Fajstrup, Eric Goubault, and Martin Raußen. Detecting deadlocks in concurrent systems. In Davide Sangiorgi and Robert de Simone, editors, *CONCUR'98 Concurrency Theory*, pages 332–347, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg.

[20] Lisbeth Fajstrup, Martin Raussen, Éric Goubault, and Emmanuel Haucourt. Components of the fundamental category. *Applied Categorical Structures*, 12:81–108, 2004.

[21] Brendan Fong and David I Spivak. *An invitation to applied category theory: seven sketches in compositionality*. Cambridge University Press, 2019.

[22] Peter Gabriel and Michel Zisman. *Calculus of fractions and homotopy theory*, volume 35. Springer Science & Business Media, 2012.

[23] Patrice Godefroid. *Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem*. Springer, 1996.

[24] Marco Grandis. Directed homotopy theory, i. *Cahiers de Topologie et Géométrie Différentielle Catégoriques*, 44(4):281–316, 2003.

[25] Marco Grandis. *Directed algebraic topology: models of non-reversible worlds*, volume 13. Cambridge University Press, 2009.

[26] Junji Hashimoto. On direct product decomposition of partially ordered sets. *Annals of Mathematics*, pages 315–318, 1951.

[27] Allen Hatcher. *Algebraic topology*. Cambridge University Press, 2005.
[28] Emmanuel Haucourt. Categories of components and loop-free categories. *Theory and Applications of Categories*, 16(27):736-770, 2006.

[29] Emmanuel Haucourt. *Some Invariants of Directed Topology towards a Theoretical Base for a Static Analyzer Dealing with Fine-Grain Concurrency*. PhD thesis, Université Paris 7-Denis Diderot, 2016.

[30] Emmanuel Haucourt. The geometry of conservative programs. *Mathematical Structures in Computer Science*, 28(10):1723-1769, 2018. doi:10.1017/S0960129517000226.

[31] Emmanuel Haucourt and Nicolas Ninin. Unique decomposition of homogeneous languages and application to isothetic regions. *Mathematical Structures in Computer Science*, 29(5):681-730, 2019. doi:10.1017/S0960129518000294.

[32] Dexter Kozen. Lower bounds for natural proof systems. In *18th Annual Symposium on Foundations of Computer Science (sfcs 1977)*, pages 254-266. IEEE, 1977.

[33] Joseph B Kruskal. Well-quasi-ordering, the tree theorem, and vazsonyi's conjecture. *Transactions of the American mathematical society*, 95(2):210-225, 1960.

[34] Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. *IEEE transactions on computers*, 100(9):690-691, 1979.

[35] Leslie Lamport. Proving the correctness of multiprocess programs. *IEEE transactions on software engineering*, (2):125-143, 1977.

[36] William Landi. Undecidability of static analysis. *ACM Letters on Programming Languages and Systems (LOPLAS)*, 1(4):323-337, 1992.

[37] Xavier Leroy, Damien Doligez, Alain Frisch, Jacques Garrigue, Didier Rémy, Jérôme Vouillon, et al. OCaml system release 4.02: Documentation and user's manual (2014), 2017.

[38] Saunders Mac Lane. *Categories for the working mathematician*, volume 5. Springer Science & Business Media, 2013.

[39] Saunders MacLane and Ieke Moerdijk. *Sheaves in geometry and logic: A first introduction to topos theory*. Springer Science & Business Media, 2012.

[40] Robin Milner. *Communication and concurrency*, volume 84. Prentice hall Englewood Cliffs, 1989.

[41] Robin Milner and Faron Moller. Unique decomposition of processes. *Theoretical Computer Science*, 107(2):357-363, 1993. URL: https://www.sciencedirect.com/science/article/pii/030439759390176T, doi:10.1016/0304-3975(93)90176-T.

[42] Samuel Mimram and Aly-Bora Ulusoy. Sparkling, 2021. Available at https://smimram.github.io/sparkling/.

[43] Samuel Mimram and Aly-Bora Ulusoy. Syntactic regions for concurrent programs. In *MFPS*, 2021.
[44] Antoine Miné. Static analysis of run-time errors in embedded critical parallel c programs. In *Programming Languages and Systems: 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings* 20, pages 398–418. Springer, 2011.

[45] Nicolas Ninin. *Factorisation des régions cubiques et application à la concurrence*. PhD thesis, École polytechnique, 12 2017.

[46] Ganesan Ramalingam. The undecidability of aliasing. *ACM Transactions on Programming Languages and Systems (TOPLAS)*, 16(5):1467–1471, 1994.

[47] Ganesan Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. *ACM Transactions on Programming Languages and Systems (TOPLAS)*, 22(2):416–430, 2000.

[48] Sylvain Schmitz and Philippe Schnoebelen. Algorithmic aspects of WQO theory. 2012.

[49] Bernd S.W. Schröder. Ordered sets. *Springer*, 29:30, 2003.

[50] Jaroslav Ševčik, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, and Peter Sewell. Relaxed-memory concurrency and verified compilation. In *Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages*, pages 43–54, 2011.

[51] Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, and Francesco Zappa Nardelli. Common compiler optimisations are invalid in the C11 memory model and what we can do about it. In *Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, pages 209–220, 2015.

[52] Rob J. van Glabbeek. On the expressiveness of higher dimensional automata. *Theoretical computer science*, 356(3):265–290, 2006.

[53] Glynn Winskel. *The formal semantics of programming languages: an introduction*. MIT press, 1993.
Titre : Une approche syntactique à la sémantique dirigée des programmes concurrents

Mots clés : Concurrence, Réalisation géométrique, Algèbre

Résumé : La vérification des programmes des systèmes critiques est cruciale pour garantir qu'ils exécutent avec précision les tâches désignées. Les programmes concurrents, fonctionnant en parallèle avec un accès mémoire partagé, présentent des défis uniques. Des verrous sont utilisés pour prévenir les comportements non déterministes, mais cela peut entraîner des deadlocks dans les systèmes critiques. Pour étudier ces programmes, il faut vérifier toutes les exécutions possibles, ce qui devient exponentiellement complexe.

Nous nous intéressons à un modèle récent où les programmes sont représentés par des espaces topologiques, équipés d'une notion de direction correspondant à l'exécution du programme. Dans ces modèles, déterminer la commutation des actions équivaut à déterminer les classes d'équivalence d'homotopie. Cette perspective géométrique introduit de nouveaux algorithmes de détection de deadlock, ainsi qu'une représentation efficace de ces espaces à l'aide d'ensembles

de cubes maximaux.

Les algorithmes de détection de deadlock dans les modèles topologiques et la représentation efficace de la région autorisée par des cubes ne résultent pas de l'approche topologique, mais uniquement de la structure dirigée sous-jacente. C'est pourquoi nous introduisons un nouveau modèle syntaxique de programmes dans lequel nous réimplémentons les représentations et algorithmes de l'approche topologique. Cette approche offre des résultats beaucoup plus facilement utilisables et implémentables, même dans le cas de programmes avec des boucles, où nous proposons un nouvel algorithme de détection d'états condamnés.

Nous fournissons également de nouveaux outils pour la factorisation des programmes grâce à une extension du théorème de Hashimoto au cas des catégories sans boucles, qui constitue un cadre naturel pour de nombreuses invariants topologiques dans la sémantique dirigée des programmes.

Title : A syntactic approach to the directed semantics of concurrent programs

Keywords : Concurrency, Geometric Realization, Algebra

Abstract : Verification of critical systems' programs is crucial to ensure they perform designated tasks accurately. Concurrent programs, operating in parallel with shared memory access, present unique challenges. Locks are used to prevent non-deterministic behavior, but this can lead to deadlocks in critical systems. To study these programs, one must verify all possible executions, which becomes exponentially complex.

We are interested in a recent model where programs are represented by topological spaces, equipped with a notion of direction corresponding to program execution. In these models, determining the commutation of actions is equivalent to determining homotopy equivalence classes. This perspective introduces new deadlock detection algorithms, as well as an efficient representation of these spaces using sets of maximal cubes.

The deadlock detection algorithms in topological models and the efficient representation of the authorized region by cubes do not result from the topological approach but only from the underlying directed structure. This is why we introduce a new syntactic model of programs in which we re-implement the representations and algorithms of the topological approach. This approach offers much more readily usable and implementable results, even in the case of programs with loops, where we provide a new algorithm for detecting doomed states.

We also provide new tools for factorization of programs through an extension of Hashimoto's theorem to the case of loop-free categories, which is a natural setting for many topological invariants in the directed semantics of programs.