Consensus Potpourri: Locally Solvable Tasks and the Limitations of Valency Arguments
CC Attribution 4.0 International:
You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Attiya, Hagit
Castañeda, Armando
Rajsbaum, Sergio
An elegant strategy for proving impossibility results in distributed computing was introduced in the celebrated FLP consensus impossibility proof. This strategy is *local* in nature, as at each stage, one configuration of an hypothetical protocol for consensus is considered, together with future valencies of possible extensions. This proof strategy has been used in numerous situations related to *consensus*, leading one to wonder why it has not been used in impossibility results of the two other well-known tasks: *set agreement* and *renaming*. This paper provide an explanation why the proof strategies for showing the impossibility of these tasks have a global nature. We show that *a protocol can always solve such tasks locally*, in the following sense. Given a configuration and all its future valencies, if a single successor configuration is selected, then the protocol can reveal all decisions in this branch of executions, satisfying the task specification. This result is shown for both set agreement and renaming.
 Hello, I'm Sergio Rashbaum. I will present the joint work with Haggitatiya and Armando Castagnela, titled Locally Solvable Tax and the Limitations of Valency Arguments. Already in the early times of Bozzi in 1989, Nancy Lynch presented a paper describing 100 impossibility proofs for distributed computing. And she observed that the limitations imposed by local knowledge are actually behind all of the arguments that she described. That is, that to prove an impossibility result, one needs to analyze the indistinguishability structure imposed by the local knowledge. And since there have been many impossibility proofs for consensus since then, but actually there are of two styles, a local style and a global style. The global style is the classic FLPA synchronous, one failure impossibility proof. And the global style was used to show that in a synchronous system, one is T plus one runs to solve consensus if T processes can crash. The local proof style, which started with FLP, has been since then used many times for various tasks like approximate agreement, randomized consensus, concurrent data structures, and so on. In different models of computation like message passing, shared memory, both with read-write operations and with more powerful communication primitives, in synchronous, asynchronous, partially synchronous models, and so on. Remember how the local FLP style proof works? At each state, a single configuration of an hypothetical protocol solving a task, consensus in the original FLP case, that holds some property. Then an indistinguishability analysis is performed of the successors of this configuration to derive some local structural properties of the successors determined by the model of computation. And then we use model properties, plus the task properties, to pick a successor configuration based on the valencies, on the future decisions of that configuration. The new variant is preserved in the FLP case by valency from one configuration to the next one, and so on. And this prevents a decision to be reached because a by valent configuration cannot be final. Instead, in the global proof style, what we do is to consider right from the start a set of final configurations of the hypothetical protocol, the set P of final configuration. You do the indistinguishability analysis right there to understand the structure of that set of configuration P. Typically, you show that these configurations are connected. And then using this global property connectivity plus the task specification, consensus, then one finds that there has to be a configuration in P where decisions are incorrect. So this global proof style, which was used, started to use early on, became very successfully in 1993, where in these three famous stuff papers that show that there is no weight-free, read-write-share-memory protocol for case set agreement. Remember that case set agreement is a generalization of consensus where at most k different values can be decided. So consensus is the case where k equal to 1. And that was the first time that topological properties other than just graph connectivity were used to derive an impossibility result. And since then, the area of using topology to derive impossibilities has presented many results for many other tasks. So if we compare the local style versus the global style, the global style is very powerful because it can be used to determine solvability and complexity of any task as a function of the topological properties of the final configurations P of the protocol. But the difficulty is how to identify a set of final configurations P where the impossibility is forced. Somehow you need to assume a canonical universal protocol that terminates after a bounded number of steps. In contrast, the local approach is very flexible because at each moment one needs to analyze only interactions of pending operations in a given configuration. So that's why this approach has been used in many different models. For example, consider a model where processes communicate by reading and writing a shared memory and also applying test and set operations. How do you define what is a canonical protocol in the system? So the local approach doesn't need to define a local canonical protocol just as it has to analyze the possible interactions among these operations. So the questions we ask are the following. The local style is very flexible, so we would like to use it for any task, but are local structural properties of the successor of a configuration sufficient to prove an impossibility for any task? Or maybe there are tasks for which they are not sufficient, like set agreement and renaming. Nobody has found yet a local impossibility proof for set agreement and renaming. And if global structural analysis is unavoidable for some tasks, why can we explain what are the reasons for this? In fact, the very question of what is a local impossibility proof needs to be answered. So this is precisely what we do first to provide a formal definition of a local impossibility proof notion. And based on this notion, we prove that nobody has defined local impossibility proofs for set agreement and renaming because it is impossible to do so. It will concentrate a little bit more for this talk, for the case of set agreement, but in the paper we also derive the impossibility for renaming. So to do so, we need to define a model of computation. We need to use a weight-free model where processes communicate by reading and writing a shared memory. And we would also like the model to have a round structure, which also is a uniform regular structure that can be easily analyzed. We need to be round-based because we want to consider the successors of a configuration after some number of rounds. The model that we selected is the iterated immediate snapshot model, which has these properties. And we show that there is no local impossibility proof for n-1 set agreement, nor for 2n-2 renaming in the IIS model. The other paper that we know of that considers these questions was published in stock of last year by Alistair Aspen, Selim, Gelashvili and Zuhl. And they define a different notion of local impossibility proof through a game between a prover and a verifier. In a model that is a non-uniform version of our iterated immediate snapshot model, which means that processes can take different number of steps. This leads to subdivisions which are not uniform. And they show that in this game there is no local impossibility proof for a case set agreement. In our approach, we can also prove the same for renaming. That's one difference. And the other difference is that dealing with uniforms of divisions, with executions, where always processes take the same number of steps, simplifies both the technical presentation and the definitions. And this is what is usually done when one proves a task impossibility result, because we can always assume that the protocols terminate after the same number of rounds are provided that the number of possible inputs to the task is finite, such as in set agreement. To get a little bit more detail into the model that we use, we assume a full information, wait-free protocol, that terminates after our rounds. Each process gets an input value to the task, set agreement, or renaming, and executes our rounds. And in each round, each process executes an immediate snapshot to a fresh memory. So it's not very important for this talk, but I will illustrate it with the figures now. What is important to remember is that this model is equivalent to the standard wait-free read-write-share memory model, with respect to task solvability, a task is solvable in the iterated immediate snapshot model, if and only if it is solvable in the usual wait-free model. So we need to consider configurations that is global states, which a configuration is simply a set of local states, which we will call it a simplex following the traditional topology notation. And in the case of three processes, so you have three configurations, one consists of three local states, which are represented by a triangle, where the vertices of the triangle are the local states of each of the three processes, that we draw by black, gray, and white in this example. One thing that is nice of this view is that you can consider partial configurations. Sigma prime consists of the local states of only the black and the gray process. And then you can consider many configurations, sets of configurations, which we call a simplex complex. And if you have two configurations where the local states of say the gray and the white process are the same, then you identify the two configurations and you can draw them nicely as two triangles sharing a nature. This is the example of the initial configurations for two process binary consensus, where the IDs, you have a black and a white process. The successes of the R rounds of an R illustrated in the video, when you have a simplex, an initial simplex sigma, the successors of the one round are three configurations, depending on the interleaving, so who takes the first immediate snapshot, then the successor of the two rounds, and so on. And you can consider also successors of partial configurations, which in this example would be solve executions, where a process sees only itself. For three processes, these pictures look like this. You have a simplex and you can consider the successors where only the black and the white processes see themselves, or you can consider all these successors. Here you can see from one round how the successes of two rounds are obtained for each one of the triangles. So the idea is the following, consider an R round full information protocol, the successor operator after one round, and after I rounds you can consider what are all configurations extending after I rounds, a given configuration. So for a J round simplex sigma prime, you can consider the successor after R minus J rounds, are the final configurations in the future of sigma prime, and the important notion is the valency of sigma prime, which is the set consisting of all decisions in the final configurations extending sigma prime. So a local proof consists of picking a sequence of simplexes starting with sigma 0, each time that we have selected a simplex of sigma i minus 1 in the simplex, you analyze the successors after one round of sigma i, and based on the valencies of those simplexes, you pick a new simplex sigma i plus 1 in the next round, and it continues in this way until the last round R minus 1, where once you selected the simplex sigma R minus 1, the protocol is supposed to reveal correct decisions only in this region. In consensus, in fact, we know that the protocol is unable to reveal correct decisions, this is the FLPR window, but we show that for set agreement, actually the protocol can reveal correct decisions, provided the valencies are properly defined. So here is the illustration of the FLP, impossibility resolved for two processes, you can select the sequence of sigma 0, sigma 1, after two rounds, if the protocol has to reveal these decisions in this region, and there will be at least one configuration where the decisions are wrong, processes decide different values, but can you do the same for set agreements, in this example three processes should decide at most two different values, can you pick a sequence of simplexes so that in the end the protocol must reveal a triangle with three different decisions, where in that region what we show is actually that there is no local proof for set agreement, which means that since set agreement is impossible, there must be mistakes, there must be a triangle with three different values, decision values, but the protocol can always hide its mistakes locally, no matter which sequence of simplexes sigma i are selected, the protocol is able to reveal correct decisions in the region that you selected, so this is what is illustrated in this figure, where for two rounds we select a simplex sigma prime, and then the protocol reveals decisions which are consistent with these valencies of sigma prime, and all of the triangles inside that region decide on at most two different values, there is an error because set agreement is impossible, but the error will always be pushed outside of the region that we are locally inspecting, to conclude we have provided a simple formalization of local style proof in the weight-free round-based iterated Begat snapshot model, we have defined new notions of valency task, which is what the protocol has to do to reveal decisions locally, and local solvability means that the protocol is actually able to reveal decisions that are consistent with the valencies, we showed that there are locally solvable valency tasks for set agreement, and this implies that there is no local impossibility proof for set agreement, and we do the same for 2n-2 renaming, and technically we do it through weak symmetry breaking, which is the problem that is equivalent to 2n-2 renaming, and this implies that there is no local impossibility proof for renaming, and in future work we would like to do the same for other tasks besides renaming and set agreement, in other weight-free shared memory models, and of course in models that are not weight-free, like T-resilient model, where it is not clear how to define bounded termination, and in fact it's models where it is not clear how to define round structure. Thanks for your attention. Thank you.
 Hello, I'm Sergio Rashbaum.  I will present the joint work with Haggitatiya and Armando Castagnela,  titled Locally Solvable Tax and the Limitations of Valency Arguments.  Already in the early times of Bozzi in 1989,  Nancy Lynch presented a paper describing 100 impossibility proofs for distributed computing.  And she observed that the limitations imposed by local knowledge  are actually behind all of the arguments that she described.  That is, that to prove an impossibility result,  one needs to analyze the indistinguishability structure imposed by the local knowledge.  And since there have been many impossibility proofs for consensus since then,  but actually there are of two styles, a local style and a global style.  The global style is the classic FLPA synchronous, one failure impossibility proof.  And the global style was used to show that in a synchronous system,  one is T plus one runs to solve consensus if T processes can crash.  The local proof style, which started with FLP, has been since then used many times  for various tasks like approximate agreement, randomized consensus, concurrent data structures, and so on.  In different models of computation like message passing, shared memory,  both with read-write operations and with more powerful communication primitives,  in synchronous, asynchronous, partially synchronous models, and so on.  Remember how the local FLP style proof works?  At each state, a single configuration of an hypothetical protocol solving a task,  consensus in the original FLP case, that holds some property.  Then an indistinguishability analysis is performed of the successors of this configuration  to derive some local structural properties of the successors determined by the model of computation.  And then we use model properties, plus the task properties, to pick a successor configuration  based on the valencies, on the future decisions of that configuration.  The new variant is preserved in the FLP case by valency from one configuration to the next one, and so on.  And this prevents a decision to be reached because a by valent configuration cannot be final.  Instead, in the global proof style, what we do is to consider right from the start  a set of final configurations of the hypothetical protocol, the set P of final configuration.  You do the indistinguishability analysis right there to understand the structure of that set of configuration P.  Typically, you show that these configurations are connected.  And then using this global property connectivity plus the task specification, consensus,  then one finds that there has to be a configuration in P where decisions are incorrect.  So this global proof style, which was used, started to use early on, became very successfully in 1993,  where in these three famous stuff papers that show that there is no weight-free,  read-write-share-memory protocol for case set agreement.  Remember that case set agreement is a generalization of consensus where at most k different values can be decided.  So consensus is the case where k equal to 1.  And that was the first time that topological properties other than just graph connectivity were used to derive an impossibility result.  And since then, the area of using topology to derive impossibilities has presented many results for many other tasks.  So if we compare the local style versus the global style, the global style is very powerful  because it can be used to determine solvability and complexity of any task as a function of the topological properties  of the final configurations P of the protocol.  But the difficulty is how to identify a set of final configurations P where the impossibility is forced.  Somehow you need to assume a canonical universal protocol that terminates after a bounded number of steps.  In contrast, the local approach is very flexible because at each moment one needs to analyze only interactions of pending operations in a given configuration.  So that's why this approach has been used in many different models.  For example, consider a model where processes communicate by reading and writing a shared memory and also applying test and set operations.  How do you define what is a canonical protocol in the system?  So the local approach doesn't need to define a local canonical protocol just as it has to analyze the possible interactions among these operations.  So the questions we ask are the following.  The local style is very flexible, so we would like to use it for any task,  but are local structural properties of the successor of a configuration sufficient to prove an impossibility for any task?  Or maybe there are tasks for which they are not sufficient, like set agreement and renaming.  Nobody has found yet a local impossibility proof for set agreement and renaming.  And if global structural analysis is unavoidable for some tasks, why can we explain what are the reasons for this?  In fact, the very question of what is a local impossibility proof needs to be answered.  So this is precisely what we do first to provide a formal definition of a local impossibility proof notion.  And based on this notion, we prove that nobody has defined local impossibility proofs for set agreement and renaming because it is impossible to do so.  It will concentrate a little bit more for this talk, for the case of set agreement,  but in the paper we also derive the impossibility for renaming.  So to do so, we need to define a model of computation.  We need to use a weight-free model where processes communicate by reading and writing a shared memory.  And we would also like the model to have a round structure, which also is a uniform regular structure that can be easily analyzed.  We need to be round-based because we want to consider the successors of a configuration after some number of rounds.  The model that we selected is the iterated immediate snapshot model, which has these properties.  And we show that there is no local impossibility proof for n-1 set agreement,  nor for 2n-2 renaming in the IIS model.  The other paper that we know of that considers these questions was published in stock of last year by Alistair Aspen, Selim, Gelashvili and Zuhl.  And they define a different notion of local impossibility proof through a game between a prover and a verifier.  In a model that is a non-uniform version of our iterated immediate snapshot model,  which means that processes can take different number of steps.  This leads to subdivisions which are not uniform.  And they show that in this game there is no local impossibility proof for a case set agreement.  In our approach, we can also prove the same for renaming.  That's one difference.  And the other difference is that dealing with uniforms of divisions, with executions,  where always processes take the same number of steps,  simplifies both the technical presentation and the definitions.  And this is what is usually done when one proves a task impossibility result,  because we can always assume that the protocols terminate after the same number of rounds are provided that the number of possible inputs to the task is finite,  such as in set agreement.  To get a little bit more detail into the model that we use,  we assume a full information, wait-free protocol, that terminates after our rounds.  Each process gets an input value to the task, set agreement, or renaming, and executes our rounds.  And in each round, each process executes an immediate snapshot to a fresh memory.  So it's not very important for this talk, but I will illustrate it with the figures now.  What is important to remember is that this model is equivalent to the standard wait-free read-write-share memory model,  with respect to task solvability, a task is solvable in the iterated immediate snapshot model,  if and only if it is solvable in the usual wait-free model.  So we need to consider configurations that is global states,  which a configuration is simply a set of local states,  which we will call it a simplex following the traditional topology notation.  And in the case of three processes, so you have three configurations,  one consists of three local states, which are represented by a triangle, where the vertices of the triangle are the local states of each of the three processes,  that we draw by black, gray, and white in this example.  One thing that is nice of this view is that you can consider partial configurations.  Sigma prime consists of the local states of only the black and the gray process.  And then you can consider many configurations, sets of configurations, which we call a simplex complex.  And if you have two configurations where the local states of say the gray and the white process are the same,  then you identify the two configurations and you can draw them nicely as two triangles sharing a nature.  This is the example of the initial configurations for two process binary consensus,  where the IDs, you have a black and a white process.  The successes of the R rounds of an R illustrated in the video, when you have a simplex, an initial simplex sigma,  the successors of the one round are three configurations, depending on the interleaving,  so who takes the first immediate snapshot, then the successor of the two rounds, and so on.  And you can consider also successors of partial configurations, which in this example would be solve executions,  where a process sees only itself.  For three processes, these pictures look like this.  You have a simplex and you can consider the successors where only the black and the white processes see themselves,  or you can consider all these successors.  Here you can see from one round how the successes of two rounds are obtained for each one of the triangles.  So the idea is the following, consider an R round full information protocol, the successor operator after one round,  and after I rounds you can consider what are all configurations extending after I rounds, a given configuration.  So for a J round simplex sigma prime, you can consider the successor after R minus J rounds,  are the final configurations in the future of sigma prime, and the important notion is the valency of sigma prime,  which is the set consisting of all decisions in the final configurations extending sigma prime.  So a local proof consists of picking a sequence of simplexes starting with sigma 0,  each time that we have selected a simplex of sigma i minus 1 in the simplex,  you analyze the successors after one round of sigma i,  and based on the valencies of those simplexes, you pick a new simplex sigma i plus 1 in the next round,  and it continues in this way until the last round R minus 1, where once you selected the simplex sigma R minus 1,  the protocol is supposed to reveal correct decisions only in this region.  In consensus, in fact, we know that the protocol is unable to reveal correct decisions, this is the FLPR window,  but we show that for set agreement, actually the protocol can reveal correct decisions, provided the valencies are properly defined.  So here is the illustration of the FLP, impossibility resolved for two processes,  you can select the sequence of sigma 0, sigma 1, after two rounds,  if the protocol has to reveal these decisions in this region,  and there will be at least one configuration where the decisions are wrong, processes decide different values,  but can you do the same for set agreements, in this example three processes should decide at most two different values,  can you pick a sequence of simplexes so that in the end the protocol must reveal a triangle with three different decisions,  where in that region what we show is actually that there is no local proof for set agreement,  which means that since set agreement is impossible, there must be mistakes, there must be a triangle with three different values, decision values,  but the protocol can always hide its mistakes locally, no matter which sequence of simplexes sigma i are selected,  the protocol is able to reveal correct decisions in the region that you selected,  so this is what is illustrated in this figure, where for two rounds we select a simplex sigma prime,  and then the protocol reveals decisions which are consistent with these valencies of sigma prime,  and all of the triangles inside that region decide on at most two different values,  there is an error because set agreement is impossible, but the error will always be pushed outside of the region that we are locally inspecting,  to conclude we have provided a simple formalization of local style proof in the weight-free round-based iterated Begat snapshot model,  we have defined new notions of valency task, which is what the protocol has to do to reveal decisions locally,  and local solvability means that the protocol is actually able to reveal decisions that are consistent with the valencies,  we showed that there are locally solvable valency tasks for set agreement,  and this implies that there is no local impossibility proof for set agreement,  and we do the same for 2n-2 renaming, and technically we do it through weak symmetry breaking,  which is the problem that is equivalent to 2n-2 renaming,  and this implies that there is no local impossibility proof for renaming,  and in future work we would like to do the same for other tasks besides renaming and set agreement,  in other weight-free shared memory models,  and of course in models that are not weight-free, like T-resilient model,  where it is not clear how to define bounded termination,  and in fact it's models where it is not clear how to define round structure.  Thanks for your attention.  Thank you.
session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_0_359.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_360_743.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_744_1127.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_1128_1451.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_1452_2423.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_2424_3227.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_3228_5183.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_5184_6455.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_6456_8015.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_8016_10211.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_10212_11555.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_11556_11735.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_11736_12131.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_12132_12395.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_12396_13511.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_13512_13787.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_13788_16223.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_16224_16271.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_16272_17615.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_17616_18911.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_18912_19103.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_19104_19487.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_19488_19847.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_19848_20771.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_20772_21119.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_21120_21359.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_21360_23387.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_23388_24383.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_24384_24887.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_24888_25451.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_25452_26447.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_26448_28031.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_28032_28787.png session3_4_Locally_Solvable_Tasks_and_the_Limitations_of_Valency_Arguments_28788_29558.png