TY - GEN
T1 - A sound foundation for the topological approach to task solvability
AU - Ledent, Jérémy
AU - Mimram, Samuel
N1 - Publisher Copyright:
© Jérémy Ledent and Samuel Mimram.
PY - 2019/8/1
Y1 - 2019/8/1
N2 - The area of fault-tolerant distributed computability is concerned with the solvability of decision tasks in various computational models where the processes might crash. A very successful approach to prove impossibility results in this context is that of combinatorial topology, started by Herlihy and Shavit’s paper in 1999. They proved that, for wait-free protocols where the processes communicate through read/write registers, a task is solvable if and only if there exists some map between simplicial complexes satisfying some properties. This approach was then extended to many different contexts, where the processes have access to various synchronization and communication primitives. Usually, in those cases, the existence of a simplicial map from the protocol complex to the output complex is taken as the definition of what it means to solve a task. In particular, no proof is provided of the fact that this abstract topological definition agrees with a more concrete operational definition of task solvability. In this paper, we bridge this gap by proving a version of Herlihy and Shavit’s theorem that applies to any kind of object. First, we start with a very general way of specifying concurrent objects, and we define what it means to implement an object B in a computational model where the processes are allowed to communicate through shared objects A1, . . ., Ak. Then, we derive the notion of a decision task as a special case of concurrent object. Finally, we prove an analogue of Herlihy and Shavit’s theorem in this context. In particular, our version of the theorem subsumes all the uses of the combinatorial topology approach that we are aware of.
AB - The area of fault-tolerant distributed computability is concerned with the solvability of decision tasks in various computational models where the processes might crash. A very successful approach to prove impossibility results in this context is that of combinatorial topology, started by Herlihy and Shavit’s paper in 1999. They proved that, for wait-free protocols where the processes communicate through read/write registers, a task is solvable if and only if there exists some map between simplicial complexes satisfying some properties. This approach was then extended to many different contexts, where the processes have access to various synchronization and communication primitives. Usually, in those cases, the existence of a simplicial map from the protocol complex to the output complex is taken as the definition of what it means to solve a task. In particular, no proof is provided of the fact that this abstract topological definition agrees with a more concrete operational definition of task solvability. In this paper, we bridge this gap by proving a version of Herlihy and Shavit’s theorem that applies to any kind of object. First, we start with a very general way of specifying concurrent objects, and we define what it means to implement an object B in a computational model where the processes are allowed to communicate through shared objects A1, . . ., Ak. Then, we derive the notion of a decision task as a special case of concurrent object. Finally, we prove an analogue of Herlihy and Shavit’s theorem in this context. In particular, our version of the theorem subsumes all the uses of the combinatorial topology approach that we are aware of.
KW - Asynchronous computability
KW - Combinatorial topology
KW - Distributed task
KW - Fault-tolerant protocols
KW - Protocol complex
U2 - 10.4230/LIPIcs.CONCUR.2019.34
DO - 10.4230/LIPIcs.CONCUR.2019.34
M3 - Conference contribution
AN - SCOPUS:85071606118
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 30th International Conference on Concurrency Theory, CONCUR 2019
A2 - Fokkink, Wan
A2 - van Glabbeek, Rob
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 30th International Conference on Concurrency Theory, CONCUR 2019
Y2 - 27 August 2019 through 30 August 2019
ER -