From January 27 to January 31 at the Université Lyon 1, room Fokko du Cloux of the Braconnier building, tramway T1 or T4, stop at Université Lyon 1.
People interested in assisting to the week should register here.
Participants are encouraged to submit talk proposals before November 30, 2013 by sending a mail to Samuel Mimram (samuel.mimram@cea.fr). Slots have been allowed for those, however we might have to do some selection depending on the number and quality of the propsals.
Over the past decades there has been an increasing interest in the potential applications of algebraic topology to study concurrency. This new field at the intersection of topology and computer science was started by a series of works which introduced semantics of concurrent programs based on topological spaces, whose points model the states of programs and paths model executions of the program. Since executions of programs always go forward in time, these topological spaces should be equipped with a notion of direction for paths, which requires adapting the usual tools in algebraic topology to this new setting. Two paths which are homotopic (in a directed sense) correspond to two schedulings of a concurrent program which are equivalent in the sense that they give rise to the same results. Starting from this observation, the study of the space of paths up to homotopy in a directed space provides compact representations of the possible schedulings of concurrent programs, in the same way that homotopy (or homology) groups describe in a concise way the essential characteristics of classical topological spaces. This point of view has provided new tools in order to efficiently verify concurrent programs. Another major application of algebraic topology in the study of concurrent programs can be found in the classification of tasks which can be performed by asynchronous concurrent programs, by modeling coherent states of threads using simplicial complexes and drawing conclusions from the study of their geometrical properties.
The goal of this thematic week is to present the latest developments resulting from the interaction between algebraic topology and concurrency theory:
Monday 27 | ||
---|---|---|
10h30 | Opening | |
11h00 - 12h30 | Rob van Glabbeek | Higher Dimensional Automata and Other Models of Concurrency |
Lunch | ||
14h00 - 15h30 | Emmanuel Haucourt | Introduction to Directed Algebraic Topology with a view towards modelling Concurrency |
Coffee break | ||
16h00 - 17h00 | Lisbeth Fajstrup | Cut-Off-theorems from a geometric viewpoint |
Tuesday 28 | ||
9h45 - 11h15 | Rob van Glabbeek | Higher Dimensional Automata and Other Models of Concurrency |
Coffee break | ||
11h45 - 12h45 | Éric Goubault | The Geometry of Mutual Exclusion |
Lunch | ||
14h30 - 15h30 | Uli Fahrenberg | History-Preserving Bisimilarity for Higher-Dimensional Automata via Open Maps |
15h45 - 16h45 | Martin Raussen | Combinatorial and topological models for spaces of schedules |
Coffee break | ||
17h15 - 18h15 | Krzysztof Ziemianski | Computing trace spaces of PV-programs |
Wednesday 29 | ||
9h15 - 10h45 | Emmanuel Haucourt | Introduction to Directed Algebraic Topology with a view towards modelling Concurrency |
Coffee break | ||
11h15 - 12h45 | Dmitry Feichtner-Kozlov | Simplicial methods in theoretical distributed computing |
Lunch | ||
Thursday 30 | ||
9h15 - 10h45 | Rob van Glabbeek | Higher Dimensional Automata and Other Models of Concurrency |
Coffee break | ||
11h15 - 12h45 | Dmitry Feichtner-Kozlov | Simplicial methods in theoretical distributed computing |
Lunch | ||
14h30 - 15h30 | Marco Grandis | A categorical approach to directed algebraic topology |
Coffee break | ||
16h00 - 17h00 | Christine Tasson | A Geometrical Interpretation of Asynchronous Computability |
17h15 - 17h45 | Thomas Kahl | On topological abstraction of higher dimensional automata |
17h45 - 18h30 | students session | |
20h | Dinner | |
Friday 31 | ||
9h15 - 10h45 | Dmitry Feichtner-Kozlov | Simplicial methods in theoretical distributed computing |
Coffee break | ||
11h15 - 12h45 | Emmanuel Haucourt | Introduction to Directed Algebraic Topology with a view towards modelling Concurrency |
Lunch | ||
14h30 - 15h30 | Sanjeevi Krishnan | Directed Poincare Duality |
Uli Fahrenberg
History-Preserving Bisimilarity for Higher-Dimensional Automata via Open Maps
We show that history-preserving bisimilarity for higher-dimensional automata has a simple characterization directly in terms of higher-dimensional transitions. This implies that it is decidable for finite higher-dimensional automata. To arrive at our characterization, we apply the open-maps framework of Joyal, Nielsen and Winskel in the category of unfoldings of precubical sets.
Lisbeth Fajstrup
Cut-Off-theorems from a geometric viewpoint
Launching a thread a number of times in parallel with itself may lead to conflicts. Considering this as a PV-problem, a thread T is a PV-program without the parallel operator and T^{n} is n copies of T in parallel. A cut-off theorem states that a certain property holds for all n if and only if it holds for some M (or for all n less than M). A geometric approach allows the proof of a cut off theorem for deadlocks. T^{n} is deadlock free for all n if and only if T^{M} is deadlock free, where M is the sum of the capacities of all the shared objects called by T. Moreover, the bound M is sharp in the sense that for any given set of resources with given capacities, there is a PV-thread such that T^{n} has no deadlocks for n<M, but T^{n} has deadlocks for all n greater than or equal to M.
Another result of the geometric approach is a cut-off theorem for serializability. T^{n} is serializable if all executions are equivalent to one of the n! serial executions. For resources all with capacity 1, the cut-off is 2: T^{n} is serializable for all n if and only if T^{2} is serializable. For capacities greater than 1, there are some partial results on serializability, e.g., that all serial executions are equivalent, so T^{n} is serializable if and only if the trace space is connected.
Dmitry Feichtner-Kozlov
Simplicial methods in theoretical distributed computing
In this series of talks I will discuss the application of methods of combinatorial algebraic topology to theoretical distributed computing.
In the first talk I will introduce the formal simplicial concepts of a task and a protocol and illustrate it on some of the central tasks of distributed computing. I will present several theorems which connect topological properties of the associated structures with the computability issues of the related tasks. This will follow an outline of the recently published book “Distributed Computing through Combinatorial Topology” written jointly with Maurice Herlihy and Sergio Rajsbaum.
The second talk will be devoted to topology of protocol complexes. Based on 3 research papers of myself, I will investigate the topology of the protocol complex in 3 different computational models: read/write, immediate snapshot, and layered immediate snapshot.
In the third, and the last talk, I will talk about topology of the Weak Symmetry Breaking task. Specifically I will be concentrating on the combinatorial theory of abstract simplicial path subdivisions. This will be based on the work of Castaneda, Rajsbaum and myself.
Éric Goubault
The Geometry of Mutual Exclusion
This talk will mostly consist of an assembly of some known, but scattered, results, both in computer science and in topology, and some of their (simple) consequences. A striking fact is the existence of relatively efficient methods for analyzing concurrent models with mutual exclusion (binary semaphores only), based on (safe) Petri nets or (prime) event structures, whereas things seem to be much more intricate in classical approaches to concurrency, when it comes to dealing with more subtle synchronization primitives, such as, for instance, counting semaphores. In the directed topological approach to these concurrent models, this difference is apparent since trace spaces in the “mutual exclusion only” model appear to be very simple. In fact even, in the latter case, the state space is geometrically a non-positive curvature (NPC) space (or cubical complex, in the discrete setting). As observed by Ghrist et al., the L^infty geodesics are then discrete up to homotopy (for finite NPC cubical complexes), and in fact they correspond to traces, up to dihomotopy. Also, as a direct consequence of work by Chepoi, Santocanale, Ardila and other authors, NPC cubical complexes are the same as prime event structures introduced to model, precisely, concurrent processes with mutual exclusion some 25 years before, and equivalent to safe Petri nets, introduced and heavily studied even before. We explore some of the consequences of these facts in the rest of the talk, if time permits.
Marco Grandis
A categorical approach to directed algebraic topology
Starting from the usual domains of directed algebraic topology (like preordered spaces, d-spaces, etc.) I shall present a formal setting for directed algebraic topology in a category C, based on an abstract cylinder endofunctor of C and natural transformations between its powers. The setting can be easily extended to categories of diagrams in C, or categories of algebras over C (of a given type, in both cases). Moreover, it has strong analogies with the structure of a monad over C, a standard basis of categorical algebra.
Emmanuel Haucourt
Introduction to Directed Algebraic Topology with a view towards modelling Concurrency
Concurrency is an ubiquitous question in computer science which actually dates back to the early ages of the discipline. The most spread model in hardware architectures is the so-called shared memory. In other words several sequential processes can simultaneously read/write a vast area of memory. If no care is taken in writing concurrent programs one can observe erratic behaviour running them. The fact that such errors due to concurrency are nondeterministic make them much harder to treat. While graphs are widely recognized as a good framework for representing sequential programs there is no consensus about the nature of their counterpart in parallel programming. Plethora of models for concurrency have been proposed. The specificity of the ones we are about to describe is that they make use of topology to formalize the fact that the actions performed along an execution trace can be locally performed in another order.
We introduce the notion of control flow graph for sequential processes then remark that parallel composition of process should corresponds to cartesian product. However the cartesian product in the category of graphs in the category if graphs do not fit, so topological models are introduced and compared. The directed geometric realization and generalized cubical areas, from which all the relevant examples can be obtained, are described. The invariants of directed algebraic topology are then presented. The fundamental category arises as as straightforward generalization of the notion of fundamental groupoid, some examples of computations are given. The category of components, which is used to reduce the size of the description of the fundamental categories, is built in the case of loop-free categories. Some perspectives beyond the loop-free case are given. Then we come to the question of factorization, which was raised by R. Milner in the early 90's.
Thomas Kahl
On topological abstraction of higher dimensional automata
In this talk, I will discuss topological abstraction of HDAs, i.e. the replacement of HDAs by more abstract and smaller ones that can be considered equivalent from a topological point of view. I will introduce two preorder relations for HDAs, called homeomorphic abstraction and topological abstraction. These preorder relations are defined using certain label preserving d-maps called weak morphisms. Roughly speaking, a weak morphism between two HDAs is a continuous map between their geometric realisations that sends subdivided cubes to subdivided cubes and that preserves labels of paths. An HDA A is said to be a homeomorphic abstraction of an HDA B if there exists a weak morphism from A to B that is a homeomorphism. Homeomorphic abstraction may be seen as a labelled version of T-homotopy equivalence in the sense of Gaucher and Goubault. The main result on homeomorphic abstraction is that it preserves the trace category, which is a variant of Bubenik’s fundamental bipartite graph, and the homology graph. The homology graph of an HDA is a directed graph whose nodes are the homology classes of the HDA. The preorder relation of topological abstraction is then defined as the existence of a weak morphism that is a homotopy equivalence, an isomorphism of trace categories and an isomorphism of homology graphs.
Sanjeevi Krishnan
Directed Poincare Duality
Spaces in nature often come equipped with dynamical structure, such as distinguished vector fields; examples include directed graphs and spacetimes. Constraints on dynamical behavior often take the form of semimodule-valued sheaves over such spaces; examples include capacity constraints on flows.
This talk will describe a (co)homology theory, taking values and local coefficients in semimodules, for spaces equipped with dynamical structure. Such directed (co)homology semimodules, generalizing Abelian sheaf (co)homology modules in a principled manner, capture certain global behavior subject to local constraints. For an example of a calculation, the first directed natural homology of a Klein (1+1)-spacetime is a group-free semimodule with two generators and one relation.
A generalization of Poincare Duality for the directed setting holds for spaces whose local dynamics exhibits bifurcations in top dimensions only. For example, the Max-Flow Min-Cut theorem (MFMC) admits an interpretation and generalization as an instance of Directed Poincare Duality. For another example, a recent robust algorithm for target-tracking (joint work with Rob Ghrist, Dave Lipsky, Mike Stein, and Hank Owen), loosely exploits such a duality in its fusion of disparate sensor data.
The talk will describe constructions, calculations, and sketch some of these applications in optimization and video analysis
Martin Raussen
Combinatorial and topological models for spaces of schedules
In topological models for concurrent computations, a schedule corresponds to a directed path (d-path), and d-homotopies (preserving the directions) of such d-paths preserve the results of a computation. I shall discuss particular classical examples of directed spaces, a class of Higher Dimensional Automata (HDA). For such a state space, I shall describe a (nerve lemma) method that determines the homotopy type of the space of traces (schedules) as a prodsimplicial complex – with products of simplices as building blocks. A description of that complex opens up for (machine) calculations of homology groups and other topological invariants of the trace space. The determination of the path components of trace space is particularly important for applications.
Unfortunately, the resulting prodsimplicial complexes grow quickly in both dimension and the occurences of shared resources. I shall sketch ongoing work with K. Ziemianski that attempts to find smaller homotopy equivalent simplicial complexes via suitable homotopy decompositions of trace spaces.
Christine Tasson
A Geometrical Interpretation of Asynchronous Computability
The purpose of this talk will be to present comparison between different models of computation in distributed computing. Starting from the operational semantics of asynchronous scan/update computations, I will introduce well known models such as the protocol complexes, used by Herlihy and Shavit to show impossibility results or the directed algebraic approach, used for studying deadlocks and scheduling. I will then explain how to establish a bridge between these approaches.
This is a joint ongoing work with Éric Goubault and Samuel Mimram.
Rob van Glabbeek
Higher Dimensional Automata and Other Models of Concurrency
I will compare the expressiveness of several models of concurrency that could be thought of as formalisations of higher dimensional automata: cubical sets, presheaves over a category of bipointed sets, automata with a predicate on hypercube-shaped subgraphs, labelled step transition systems, and higher dimensional transition systems. A series of counterexamples will illustrate the limitations of each of these models.
Additionally I present results relating higher dimensional automata to ordinary automata, Petri nets, and various kinds of event structures. I compare the expressive power of these models of concurrency based on their ability to represent causal dependence. To this end, I translate these models, in behaviour preserving ways, into a model of higher dimensional automata. In particular, I propose four different translations of Petri nets, corresponding to the four different computational interpretations of nets found in the literature.
I also review various equivalence relations for concurrent systems on higher dimensional automata. These include the history preserving bisimulation, which is the coarsest equivalence that fully respects branching time, causality and their interplay, as well as the ST-bisimulation, a branching time respecting equivalence that takes causality into account to the extent that it is expressible by actions overlapping in time. Through their embeddings in higher dimensional automata, it is well-defined whether members of different models of concurrency are equivalent.
Krzysztof Ziemianski
Computing trace spaces of PV-programs
PV-programs are models for parallel computing, where semaphores are used for synchronization of processes. They are a small and simple subclass of higher dimensional automata. I will show that the class of PV-programs is in fact very general - one can realize any finite simplical complex as the execution space of a PV-program. The main technique used in the construction are homotopy decompositions, i.e. presentations of executions spaces of PV-programs as homotopy colimits of simpler spaces, usually the execution spaces of shorter PV-programs. I will present calculations in specific cases, as some programs with a single resource.