1 Department of Mathematical Sciences, The Faculty of Engineering and Science, Aalborg University, VBN2 The Faculty of Engineering and Science, Aalborg University, VBN3 CEA, Gif-sur-Yvette Cedex, France
We show in this article that some concepts from homotopy theory, in algebraic topology,are relevant for studying concurrent programs. We exhibit a natural semantics of semaphore programs, based on partially ordered topological spaces, which are studied up to “elastic deformation” or homotopy, giving information about important properties of the program, such as deadlocks, unreachables, serializability, essential schedules, etc. In fact, it is not quite ordinary homotopy that has to be used, but rather a “directed homotopy” that does not reverse the flow of time. We show some of the essential differences between ordinary and directed homotopy through examples. We also relate the topological view to a combinatorial view of concurrent programs closer to transition systems, through the notion of a cubical set. Finally we apply some of these concepts to the proof of the safeness of a two-phase protocol, well-known and used in concurrent database theory. We end up with a list of problems from both a mathematical and a computer-scientific point of view.
Theoretical Computer Science, 2006, Vol 357, Issue 1-3, p. 241-278