Directed algebraic topology and concurrency. With a foreword by Maurice Herlihy and a preface by Samuel Mimram (Q2515156): Difference between revisions

From the foreword by Maurice Herlihy: ``Computer science has a rugged tradition of appropriating concepts and mechanisms from classical mathematics, concepts once proudly considered pure and useless, and adapting those concepts to describe and analyze phenomena that once could not have been imagined.'' The papers and works of the authors of this monograph as well as the book under review are oriented towards the adaptation of some concepts and methods from classical algebraic topology to models of concurrent processes in computer science and their analysis. The authors are among the initiators of this branch on the borderline of mathematics, which is directed algebraic topology in computer science. Out of the exhaustive list of references containing 172 titles (published between 1941 (S. Eilenberg) and 2015), about 40 articles belong to the authors of this monograph. From the introduction (Chapter 1): ``Concurrent programs consist of multiple processes running in parallel. Their use has become more and more widespread in order to efficiently exploit recent architectures (processors with many cores, clouds, etc.), but they are notoriously difficult to design and to reason about: one has to ensure that the program will not go wrong, regardless of the way the different processes constituting the program are scheduled. In principle, in order to achieve this task with the help of a computer, we could apply traditional verification techniques for sequential programs on each of the possible executions of the program. But this is not feasible in practice because the number of those executions, or \textit{schedulings}, may grow exponentially with the size of the program. Fortunately, it can be observed that many of the schedulings are equivalent in the sense that one can be obtained from the other by permuting independent instructions: such equivalent executions will always lead to the same result. Hence, if one of those executions can be shown not to lead to an error, neither will any other execution which is equivalent to it. This suggests that a model for concurrent programs should incorporate not only the possible executions of the program (as in traditional interleaving semantics), but also the commutations between instructions, following the principle of what is now called \textit{true concurrency}. Interestingly, the resulting models are algebraic structures which can be interpreted \textit{geometrically}: roughly as topological spaces in which paths correspond to executions and two executions are equivalent when the corresponding paths are homotopic, i.e., connected by a continuous deformation from one to the other. In order to make this connection precise, it turns out that topological spaces are not exactly the notion for our purpose. One needs to use a \textit{directed} variant, i.e., to incorporate a notion of irreversible time. Mutatis mutandis, starting from very practical motivations (the verification of concurrent programs), questions of a more theoretical nature arise. What is a good notion of a directed space, and how do classical techniques from algebraic topology apply to this setting? What is the geometry of concurrent programs? How can a geometrically refined understanding of concurrency be used in order to design new and more efficient algorithms for studying concurrent programs? The goal of this book is to give a general overview of our current understanding, regarding these questions.'' Chapters 2 and 3 include standard material on concurrent languages and their semantics. These chapters are recommended by the authors to be studied especially by the mathematicians not accustomed to computer science. Chapter 2, entitled ``A toy language for concurrency'', has the following sections: 2.1 ``A toy language'' (parallel IMP, concurrent programs, sequential consistency), 2.2 ``Semantics of programs'' (graphs, the transition graph \(G_p=(G_p,\ell_p,s_p,t_p)\) associated to a program \(p\), operational semantics \(\mathcal{A}\), \(\mathcal{B}\), \(\mathcal{C}^{\ast}_{\mathrm{act}}\)) and 2.3 ``Verifying programs'' (correctness properties, reachability in concurrent programs). PIMP is a variant of the IMP language extended with a parallel composition operator. Chapter 3, entitled ``Truly concurrent models of programs with resources'', has the following content: 3.1 ``Modeling resources in the language'' (taming concurrency, extending the language with resources), 3.2 ``State spaces for conservative resources'' (conservative programs, transition graphs for conservative programs), 3.3 ``Asynchronous semantics'' (toward true concurrency, asynchronous semantics, coherent programs, programs with mutexes only), 3.4 ``Cubical semantics'' (precubical sets, the geometric realization) and 3.5 ``Historical notes''. From this part, for computer scientists the authors recommend only Section 3.4. A precubical set \(C\) consists of a family \((C_n)_{n\in \mathbb{N}}\) of sets whose elements are called \(n\)-\textit{cubes} together with, for all indices \(n,i\in \mathbb{N}\) with \(0\leq i<n\), maps \(\partial_{n,i}^{\pm}:C_n\rightarrow C_{n-1}\), respectively, associating to an \(n\)-cube its back and front face in the \(i\)th direction such that \(\partial^\beta_{n,j}\partial^\alpha_{n+1,i}= \partial^\alpha_{n,i}\partial^\beta_{n+1,j+1}\), for \(0\leq i\leq j<n\) and \(\alpha,\beta\in \{-,+\}\). A morphism \(f:C\rightarrow D\) of precubical sets consists of a family \((f_n:C_n\rightarrow D_n)_{n\in \mathbb{N}}\) of functions such that for all integers \(n,i\in \mathbb{N}\) with \(0\leq i<n\) and \(\alpha\in \{-,+\}\), \(\partial^\alpha_{n,i}\circ f_n=f_{n-1}\circ \partial^\alpha_{n,i}\). The 0-cubes and 1-cubes are called \textit{vertices }and \textit{edges}, respectively. A precubical set \(C\) is called \textit{labeled} if there is given a set \(\mathcal{L}\) of labels and a function \(\ell:C_1\rightarrow \mathcal{L}\) such that \(\ell\circ \partial^{-}_{2,i}=\ell\circ \partial^{+}_{2,i}\), \(i\in \{0,1\}\). A \textit{path} in a precubical set is a finite sequence \(e_1,\ldots,e_n\) of 1-cubes such that \(\partial^{+}_{1,0}(e_i)=\partial^{-}_{1,0}(e_{i+1})\) for every index \(1\leq i<n\). The \textit{dihomotopy} relation \(\sim\) on paths is the smallest equivalence relation that is a congruence w.r.t. concatenation and such that \((e_1.e'_2)\sim (e_2.e'_1)\) whenever there is a 2-cube \(h\in C_2\) satisfying the following relations: \(\partial^{-}_{2,i-1}(h)=e_i\), \(\partial^{+}_{2,i-1}(h)=e'_i\), \(i\in \{1,2\}\). The \textit{fundamental category} \(\overrightarrow{\Pi}_1(C)\) associated to a precubical set \(C\) is the category whose objects are the vertices of \(C\) and morphisms from \(x\) to \(y\) are paths from \(x\) to \(y\) up to dihomotopy. The \textit{geometric realization} of a precubical set \(C\) is the topological space \(|C|=\coprod_{n\in \mathbb{N}}(C_n\times I^n)/\approx \), where \(C_n\) is equipped with the discrete toplogy, \(I^n\) is the standard \(n\)-cube and \(\approx\) is the equivalence relation generated by the relations \((\partial^\alpha_{n,i}(x),p)\approx (x,i^\alpha_{n-1,i}(p))\), \(n\in \mathbb{N}\), \(x\in C_n\), \(p\in I^{n-1}\), and \(i^{\pm}_{n,i}:I^{n-1}\rightarrow I^n\) are the usual inclusions. All these notions are used in the subsequent chapters. Chapter 4 is entitled ``Directed topological models of concurrency''. In the first part of this chapter, directed spaces (d-spaces) and directed maps (d-maps) are defined and their category \textbf{dTop} is studied. The usual examples are given: \(\overrightarrow{\mathbb{ C }}\), \(\overrightarrow{S^1}\), \(\overrightarrow{D^2}\). A directed geometric semantics is defined. If an operational semantics is given, then to any conservative program \(p\) a quadruple \((G_p,s_p,t_p,r_p)\) is associated consisting of a d-space \(G_p\) with two points \(s_p,t_p\in G_p\), the \textit{beginning} and \textit{end}, and a function \(r_p:G_p\rightarrow (\mathcal{R}\rightarrow \mathbb{Z})\), the \textit{resource potential}. Then, the \textit{geometric semantics} \(\check{G}_p \) is defined as the d-subspace of \(G_p\) complementary to \(R_p=\{x\in G_p\mid\exists a\in R,r_p(x)(a)+\kappa_a<0 \text{ or } r_p(x)(a)>0\}\). Given a conservative program \(p\), the following points in its geometric semantics \(\check{G}_p\) can be identified. A point \(x\) is: \textit{unreachable} if there is no dipath \(t:s_p\twoheadrightarrow x\), \textit{deadlock} if \(x\) is different from \(t_p\) and the only dipath from \(x\) is the constant dipath \(\varepsilon_x\), \textit{unsafe} if there is a dipath \(t:x\twoheadrightarrow y\) for some deadlock \(y\), \textit{doomed} if there is no dipath \(t:x\twoheadrightarrow t_p\). For d-paths, the relation of \textit{directed homotopy} (d-homotopy or dihomotopy) is defined. The fundamental category \(\overrightarrow{\Pi}_1(X)\) of a d-space \(X\) is defined as the category whose objects are points of \(X\) and whose morphisms are directed paths up to dihomotopy. For this category, a Seifert-van Kampen-type theorem is proved. The subsection 4.3.2 is dedicated to the definition and study of so-called \textit{dicoverings} and \textit{universal dicoverings}. A d-map \(g:Y_1\rightarrow Y_2\) has the \textit{unique right lifting property} w.r.t. a d-map \(f:X_1\rightarrow X_2\), if for each d-map \(h_i:X_i\rightarrow Y_i\), \(i=1,2\), satisfying \(g\circ h_1=h_2\circ f\), there exists a unique d-map \(h:X_2\rightarrow Y_1\) such that \(h\circ f=h_1\) and \(g\circ h=h_2\). Then, a d-map \(p:Y\rightarrow X\) is a \textit{dicovering} if it has the unique right lifting property w.r.t. the inclusion d-maps \(\{0\}\hookrightarrow \overrightarrow{I}\), \(\{(0,0)\}\hookrightarrow (I\times \overrightarrow{I})/\approx_0\), \(\{(0,0)\}\hookrightarrow (I\times \overrightarrow{I})/(\approx_0\cup \approx_1)\), where \(I\) is equipped with only constant paths as dipaths, and the equivalence relations \(\approx_t\) are defined by \((s_1,t_1)\approx_t(s_2,t_2)\) if and only if \(t_1=t=t_2\). The \textit{universal dicovering} of a pointed d-space \((X,x)\) is a pointed dicovering \(p:(\widetilde{X},\widetilde{x})\rightarrow (X,x)\) such that for every dicovering \(q:(Y,y)\rightarrow (X,x)\) there exists a unique pointed morphism \(r:(\widetilde{X},\widetilde{x})\rightarrow (Y,y)\) satisfying \(p=q\circ r\). This is an important notion for directed algebraic topology since the dicoverings have some properties similar to the properties of the covering spaces from usual algebraic topology. More importantly, in the context of the book, this structure provides a geometrical approach to some programs that are not loop-free. The aim of Chapter 5, entitled ``Algorithmics on directed spaces'', is to explain algorithms that are based on the geometric semantics of programs. This chapter includes the following sections. 5.1 ``The Boolean algebra of cubical regions'', 5.2 ``Computing deadlocks'' and 5.3 ``Factorizing programs''. Given a d-space \(X\subseteq \overrightarrow{I}^n\), a \textit{cubical cover} \(R=(R^i)_{1\leq i\leq \ell}\) of \(X\) is a finite family of \(n\)-cubes (with open or closed boundaries) in \(X\) such that \(\bigcup R=X\). A space that admits a cubical cover is called a \textit{cubical region}. Denote by \(\mathcal{C}_n\) (respectively \(\mathcal{R}_n\)) the set of cubical covers (respectively regions) of dimension \(n\). It is proved that the set of cubical regions is a Boolean subalgebra of the powerset \(\mathfrak{B}(\overrightarrow{I}^n)\) and there is a bijection between \(\mathcal{R}_n\) and the subset \(\overline{\mathcal{C}}_n\) of \(\mathcal{C}_n\) whose elements are covers in \textit{normal forms}. In Section 5.2, the authors provide an algorithm to detect deadlocks in simple programs and, more generally, doomed regions. Section 5.3 refers to the important question, whether a concurrent program be can be decomposed as several processes that are running concurrently and are completely independent. The result is presented as a general theorem (Theorem 5.26): In the commutative monoid \(\mathcal{R}^{\mathfrak{C}}\) of cubical regions, every element can be uniquely factorized as a product of irreducible elements. In Chapter 6, entitled ``The category of components'', the notion of connected components is introduced to directed topology, which can be used to obtain a compact representation of the category of directed paths up to homotopy. A category \(\mathcal{C}\) is \textit{loop-free} if for every pair of objects \(x,y\in \mathcal{C}\), \(\mathcal{C}(x,y)\neq \emptyset\) and \(\mathcal{C}(y,x)\neq \emptyset\) implies \(x=y\) and \(\mathcal{C}(x,x)=\{\mathrm{id}_x\}\). A morphism \(f\in \mathcal{C}(x,y)\) is a \textit{weak isomorphism} if for every object \(z\in \mathcal{C}\) such that \(\mathcal{C}(y,z)\neq \emptyset\), the function \(f^{\ast}:=\mathcal{C}(.,z):\mathcal{C}(y,z)\rightarrow \mathcal{C}(x,z)\) is a bijection, and if \(\mathcal{C}(z,x)\neq \emptyset \), the function \(f_{\ast}=\mathcal{C}(z,.):\mathcal{C}(z,x)\rightarrow \mathcal{C}(z,y)\) is a bijection. The \textit{category of components} \(\overrightarrow{\Pi}_0(\mathcal{C})\) associated to a loop-free category \(\mathcal{C}\) is the quotient category \(\mathcal{C}/\Sigma\), where \(\Sigma\) is the greatest \textit{system} of weak isomorphisms of \(\mathcal{C}\). If \(X\) is a d-space, then the category \(\overrightarrow{\Pi}_0(\overrightarrow{\Pi}_1(X))\) is denoted by \(\overrightarrow{\Pi}_0(X)\). The category of components provides a tool which is able to identify, in concurrent programs, actions that really have an impact on the execution of the program and neglect the others. This is done using the following theorem (Theorem 6.23): Given two objects \(x\) and \(y\) of \(\mathcal{C}\) such that \(\mathcal{C}(x,y)\neq\emptyset\), and \(\Sigma\) a system of weak isomorphisms, the function \(\mathcal{C}(x,y)\rightarrow \mathcal{C}/\Sigma([x],[y])\), induced by the quotient functor, is a bijection. The authors investigate the categories of components associated to the fundamental categories of trees, cubical regions in dimension 2 and a ``floating cube'' \(\check{G}_p=\overrightarrow{I}^3\backslash ]1/3,2/3[^3\). A generalized Seifert-van Kampen theorem is proved (Theorem 6.41). In the last section of this chapter (6.4), the authors discuss other extensions of the notion of component that were or can be investigated. Chapter 7 is entitled ``Path spaces''. For a d-space \(X\) and two points \(x,y\in X\), \(X(x,y)\) denotes the subspace of \(X^{\overrightarrow{I}}\) consisting of all dipaths from \(x\) to \(y\), equipped with the compact-open topology, and called the \textit{path space} from \(x\) to \(y\). The authors start from the remark that the space of dipaths in the geometric semantics of a program is generally very large, even for the most simple programs. But a space of dipaths has a docomposition into subspaces of particular shapes, called restricted spaces, which are either empty or contractible. In addition, every restricted space can be coded by a certain Boolean matrix, where inclusion of subspaces corresponds to the natural order of matrices, and this gives rise to efficient computations. A \textit{prod-simplicial complex} is a topological space obtained by gluing products of geometric simplices. It is proved that if \(X=\check{G}_p\), then the path space \(X(0,1)\), of paths from the begining point \(0=(0,\dots,0)\) to the end point \(1=(1,\dots,1)\), is homotopy equivalent to a prod-simplicial complex. Then the homology groups of the path spaces \(\check{G}_p(0,1)\), corresponding to some parallel programs, can be calculated. And very interesting is that using this technique, for an arbitrary finite-dimensional simplicial complex \(P\) on \(n\) vertices, there exists a simple program \(p\) with \(n\) threads, hence with a geometric semantics \(X=\check{G}_p\subseteq \overrightarrow{I}^n\), such that \(X(0,1)\) is homotopy equivalent to the disjoint union \(P\sqcup S^{n-2}\). In particular, if \(P\) is \(P\mathbb{R}^2\), with the usual triangulation with 6 vertices, then \(X(0,1)\) is homotopy-equivalent to \(P\mathbb{R}^2\sqcup S^4\) [\textit{A. Zomorodian} and \textit{G. Carlsson}, Discrete Comput. Geom. 33, No. 2, 249--274 (2005; Zbl 1069.55003)]. The book ends (Chapter 8) with the enunciation of a few perspective issues. First, the authors make a short self-evaluation of the content of the previous chapters of the book: ``We hope that this panorama of relationships between directed algebraic topology and concurrency has given the reader an impression of the profound links between the two fields. Even though most computational processes are intrinsically discrete, adopting a geometric point of view to this investigation has brought many new insights, and we believe that this is only a beginning. This book can only serve as a relatively short introduction to the subject. Many related results and approaches were not presented, and we would like to point the reader to some of these in this final chapter''. The aforementioned issues that are not approached in the book, of which some are already extensively covered and others are still in an incipient and perspective form, are the following: concurrency control in distributed databases, fault-tolerant protocols for distributed systems, higher-dimensional automata and semantic equivalences, rewriting techniques, homotopy type theory. The authors support this list of perspective issues with bibliographical references and indications of practical necessity in computer science, and even by initiating new development directions in algebraic topology.