Directed Algebraic Topology and Concurrency | springerprofessional.de

Springer Professional

nach oben

2016 | Buch

Kapitel lesen Erstes Kapitel lesen

Directed Algebraic Topology and Concurrency

verfasst von: Lisbeth Fajstrup, Eric Goubault, Emmanuel Haucourt, Samuel Mimram, Martin Raussen

Verlag: Springer International Publishing

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This monograph presents an application of concepts and methods from algebraic topology to models of concurrent processes in computer science and their analysis.

Taking well-known discrete models for concurrent processes in resource management as a point of departure, the book goes on to refine combinatorial and topological models. In the process, it develops tools and invariants for the new discipline directed algebraic topology, which is driven by fundamental research interests as well as by applications, primarily in the static analysis of concurrent programs.

The state space of a concurrent program is described as a higher-dimensional space, the topology of which encodes the essential properties of the system. In order to analyse all possible executions in the state space, more than “just” the topological properties have to be considered: Execution paths need to respect a partial order given by the time flow. As a result, tools and concepts from topology have to be extended to take privileged directions into account.

The target audience for this book consists of graduate students, researchers and practitioners in the field, mathematicians and computer scientists alike.

Anzeige

Inhaltsverzeichnis

Frontmatter

Chapter 1. Introduction

Abstract

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 composing 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 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.

Lisbeth Fajstrup, Eric Goubault, Emmanuel Haucourt, Samuel Mimram, Martin Raussen

Chapter 2. A Toy Language for Concurrency

Abstract

Since the aim of this book is to introduce models and verification techniques for programming languages, our first task is to introduce the programming language through which we demonstrate the main ideas of this book. We begin by introducing the language. We then describe its operational semantics, which formalizes the way programs are to be executed. Finally, we describe the correctness properties that we will be interested in.

Lisbeth Fajstrup, Eric Goubault, Emmanuel Haucourt, Samuel Mimram, Martin Raussen

Chapter 3. Truly Concurrent Models of Programs with Resources

Abstract

The graph-based semantics introduced in the previous chapter is often not informative enough, because it does not take into account whether two actions commute or not. In this chapter, we introduce truly concurrent models which incorporate this information. We begin by extending our programming languages with resources and restrict ourselves to conservative programs, in which resource consumption only depends on the current state. We then generalize the semantics to asynchronous graphs, which explicitly describe the commutation of two actions and to precubical sets, which can more generally express the commutation of n actions. Finally, links with other classical models for concurrency are mentioned.

Lisbeth Fajstrup, Eric Goubault, Emmanuel Haucourt, Samuel Mimram, Martin Raussen

Chapter 4. Directed Topological Models of Concurrency

Abstract

We study topological models for concurrent programs with the aim of importing tools and techniques coming from algebraic topology to ease verification of concurrent programs. In those models, the state space of a program is described as a topological space, and an execution corresponds naturally to a path in this space. To rensure that models reflect order properties, we are led to enrich the concept of a topological space so that it takes causality into account. We shall focus our attention on directed paths, i.e., the ones respecting causality.

Lisbeth Fajstrup, Eric Goubault, Emmanuel Haucourt, Samuel Mimram, Martin Raussen

Chapter 5. Algorithmics on Directed Spaces

Abstract

In this section, we explain algorithms which are based on the geometric semantics of programs. In order to ease the presentation, those algorithms are formulated for simple programs, and we only hint at generalizations: programs with branchings can generally be handled by adapting the algorithms, and loops can be handled up to a finite depth by unrolling the programs. We illustrate the wide variety of applications of the geometric point of view by presenting a compact way of representing regions in the geometric semantics, an algorithm for detecting deadlocks, and an algorithm for factoring programs into independent parallel processes.

Lisbeth Fajstrup, Eric Goubault, Emmanuel Haucourt, Samuel Mimram, Martin Raussen

Chapter 6. The Category of Components

Abstract

The components of a directed space are not easy to define. We explain what the problem is and why some obvious ideas fail. Then the components of a d-space without loops is defined. It is a quotient of the fundamental category. It is defined for a general category without non-trivial isomorphisms. The component category is the quotient under a system of morphisms, the weak isomorphisms. Another construction, which gives an isomorphic fundamental category, is obtained by inverting the weak isomorphisms. An algorithm which determines a less “quotiented” category, precomponents, for simple programs is given, as well as several examples.

Lisbeth Fajstrup, Eric Goubault, Emmanuel Haucourt, Samuel Mimram, Martin Raussen

Chapter 7. Path Spaces

Abstract

The space of dipaths in the geometric semantics of a program is generally very large, even for the most simple programs. In this chapter, we describe a method that allows one to “compress” this space in the case of simple programs, and to provide a finite combinatorial description of it which retains its essential topological characteristics: we compute a combinatorial model of this space, whose geometric realization is homotopy equivalent to it.

Lisbeth Fajstrup, Eric Goubault, Emmanuel Haucourt, Samuel Mimram, Martin Raussen

Chapter 8. Perspectives

Abstract

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.

Lisbeth Fajstrup, Eric Goubault, Emmanuel Haucourt, Samuel Mimram, Martin Raussen

Backmatter

Titel: Directed Algebraic Topology and Concurrency
verfasst von: Lisbeth Fajstrup
Eric Goubault
Emmanuel Haucourt
Samuel Mimram
Martin Raussen
Copyright-Jahr: 2016
Verlag: Springer International Publishing
Electronic ISBN: 978-3-319-15398-8
Print ISBN: 978-3-319-15397-1
DOI: https://doi.org/10.1007/978-3-319-15398-8