A much easier but pathological proof is simply that Eve burns all messages and therefore Alice and Bob can never communicate a single bit to each other.
This is probably naive but if we already know Alice and Bob will win by both retreating, can't we simply say that if there is no acknowledgement by a pre agreed timeout, it means we both retreat?
Yes, either start with always attack, or always retreat.
Another (practical) solution could be to spoof a message, making it appear as if from Eve. Some kind of steganography might work as well (or alternative forms of communication such as pigeons or smoke signals). And if all communications between Alice and Bob is discarded, this would worry either one of them to send a personal messenger who is human. This person could be captured and tortured, sure. But if they get "burned" as well, that'd be an act of war. Plus, if they are able to predetermine that if they don't hear from each other after X time, they attack after X + Y time (e.g. 3 months and 1 month [to prepare]) then the problem can be solved. If they cannot create a clear way of predetermined action based on actions then they'll always retreat.
Actually now that I gave it some further thought this "two general problem" can be observed in the cold war as well via (the nuclear threat of both parties). The nuclear threat from both sides created an equilibrium akin to what could happen in the described situation.
The point of the Two Generals problem is that it's impossible to solve. No matter how many acknowledgements you send or receive over a lossy medium you can never be sure that both parties will agree on whether to attack. It's a fairly infamous restriction on distributed system design.
Working distributed systems have to work around this (and other) restrictions that are implicit to the properties of a distributed system. So TCP still works perfectly fine even though a perfect version of TCP (that didn't have timeouts) would be mathematically impossible to implement.
Ok. Say timeout is one hour. Alice sends message to Bob saying attack. Bob acknowledges, Alice receives message at T+:10 minutes. Alice acknowledges, but Eve drops Alice's acknowledgement.
Now, as far as Alice is concerned, both Alice and Bob acknowledged. However, Bob never got Alice's acknowledgement, so he won't attack.
You misunderstand the Two Generals problem, which is that regardless of how many messages Eve burns, the two generals can never be certain of shared knowledge.
Normally in the two generals problem you assume that if you send a message repeatedly for an indefinite amount of time it will eventually be delivered. This assumption makes the problem the author described possible, but the actual two generals problem is still impossible. See my explanation here: https://news.ycombinator.com/item?id=17536337
For such generic statement of the problem, it's certainly unsolvable.
But with encryption, timeouts and defaults it can be - as seen by many the distributed systems on the Internet
Timeouts and defaults can be considered as part of the algorithm. The problem is that you may be unable to determine a reasonable timeout beforehand. The timeout as a practical solution is also described under 'engineering approaches': https://en.wikipedia.org/wiki/Two_Generals'_Problem#Engineer...
I cannot reconcile your claim with my understanding of the formal proof. We are asking for a guaranteed consensus, perhaps you are merely asking for arbitrarily high probability of consensus.
Can you point me at an algorithm that guarantees consensus? Your claim seems to be at odds with the formal proof in the article. I particular, the article already allows for encryption, timeouts, and defaults.
So I can't see how you are right, and would appreciate some additional information as to why you think the article is wrong.
The whole point of the problem is that you're not allowed to use timeouts and stuff to get a work around. Adding timeouts etc fundamentally changes the situation. The distributed systems on the Internet you see do not solve the problem - they work around it, basically by adding failure modes not present in the original.
I think I'm being more pragmatic and immediately jumping to what needs to change to make this situation treatable. An abstract statement of a problem like this is probably great for teaching people concepts about consensus, but hopefully no one knowingly designs stuff that way (except Mongo perhaps)
If you don't understand what's impossible, you run the risk of trying for something you'll never be able to accomplish. You'll never know why you don't succeed. It's precisely about teaching and learning the limits beyond which it's pointless to even try to go.
If it's pragmatic to dismiss impossibility results, perhaps revisit pragmatism.
(Note: this is based on the informal description of the problem in the article and on Wikipedia, not the formal model given in the article)
What is consensus [1]?
As oh_sign noted in an earlier comment here, if Eve blocks all messages there is obviously no way to achieve consensus, so if there are no constraints on Eve's ability to interfere this is a trivial problem, so I'm going to assume that Eve is not able to block everything.
Suppose each general does this:
1. Generate a random 128 bit integer, P.
2. Decide the action they are going to take, A (attack or retreat).
3. Repeatedly send the message: "I will do A with priority P". (To be clear, P is only generated once. That single P is used in all messages).
4. They take action A unless they receive a message from the other general that states a different action, A', AND the other general's message has a lower P. In that case, they take action A'.
Without loss of generality, assume Alice has the lower P.
With the above procedure, as long as a single message from Alice to Bob makes it through, the generals will take the same action, which will be the action Alice picked.
Although they take the same action, only Bob knows that they are going to do so. He knows this because since a message from Alice got through to him, he knows she has a lower P so will stick with her original action regardless of whether or not his messages got through, and he will match her action because he knows she has a lower P.
Is that consensus, or to count as consensus do they both have to know before they act that they will be taking the same action?
Let's say that they do both have to know. Modify the above procedure so that if a general finds out they have the higher P, they change the message they are repeatedly sending to "I will do action A', following your lead", where A' is the action from the other general's message.
With this modified procedure, if Eve lets one message through from Alice, and after that lets one message through from Bob, then (1) the two generals take the same action, (2) Bob knows they will be taking the same action, and (3) Alice knows they will be taking the same action.
Is that now consensus? They are taking the same action and they both know they are doing so. Furthermore Alice knows that Bob knows. Bob, however, does not know that Alice knows. Do we need not only agreement, but each knowing that there is agreement, and knowing that they each know, and knowing that they each know that they each know, ad infinitum?
[1] Are consensus problems usually stated in terms of agreements between generals because the definition of consensus is literally, at least in Oxford, "A general agreement"?
> They take action A unless they receive a message from the other general
The missing piece in your algorithm is how long do they wait to receive a message from each other and how they can know that it's long enough? If they don't wait long enough they will not receive a message and will make wrong assumptions about the other general, will not reach consensus and will take each their own action. To fix this each has to wait as long as it takes to receive a message from the other general and know about this (which in itself requires more messages).
But what if one of the generals dies in the meantime and stops sending messages? Or what if both Bob and Alice got the same random integer? There are other issues too.
But the important thing is it's all about time. You can always wait out uncertainty, but of course you won't be able to make progress waiting.
If you know that at least one message from Alice goes through, and Alice says "do this with priority 0", then yes, you can solve the problem.
The issue here is different to what you are modelling; imagine this payoff table for A
B attacks B holds
A attacks +1 -∞
A holds 0 0
The question is, knowing nothing about the reliability of the connection, is possible to have a strategy that has a positive expectation? B is only going to attack if they are absolutely certain you will, and vice-versa.
The issue with your strategy is that even if Eve never interfered with the connection once, Alice does not know that, so will hold.
I see this annoying mistake everywhere, but it's important to point out in the context of computer science (more so than in mathematics) because it relates to one of its core components: in the context of logic and proofs, "formal" does not mean precise or mathematical (and certainly not official), but rather mechanical. A formal description is one with a precise syntax and semantics, whose truth can (at least in principle) be judged directly from its form. A formal proof is one carried out through pure syntactic (i.e., formal, in the sense of "pertaining to form") manipulation, and does not rely on any informal arguments, namely ones that do not appear in the form.
As a rule of thumb, if you could replace the word "formal" with "mechanical" and your sentence would still be true, then you can use the word formal (this is the case, say, with formal software verification, which is simply mechanical software verification, or formal proofs in a proof assistant, that are mechanical proofs). So, a formal description is one that could be directly mechanically interpreted by a simple computer program as written, and a formal proof is one that could be mechanically checked. If this is not the case -- use the word "precise" (or "mathematical" if you prefer). It's both simpler and more accurate.
As the description given here makes heavy use of natural language that is not easily interpretable by a computer, it is not formal, and since the proof makes use of a notion of a time machine, as well as others, not given a formal definition, it is very much informal, even if sufficiently precise to be acceptable as a mathematical proof.
welcome to writing? i don't understand this kind of pedantry: it is very clear from context that is not going to be a formal spec or formal proof and therefore the word formal here is being used informally... or just ya know according to its conventional understanding. did you really get to the end of article before you realized this wasn't going to be about formal proofs/specs?
>Did you really get to the end of the first paragraph before you decided this wasn't going to be about formal proofs/specs?
yes because i have heard of the word juxtaposition
>This guide will introduce the Two Generals' Problem and give an [INTUITIVE] explanation for why finding a solution to the problem is impossible. It will then formalize the Two Generals' Problem and formally prove the impossibility.
It's like writing "pusillanimous" when you want to say "nice" -- the chosen word is both unnecessarily fancy and wrong. I'm not aware that this has become the conventional understanding just because some people here and there make this mistake. It's fine for words to acquire new meaning, sometimes even an opposite one like in the case of "literally," but even in that case the word serves some purpose (that of emphasis). So if you tell me that the word "formal" has acquired the meaning informal, I would still ask what purpose does "formal" serve here? What's wrong with just saying proof? And yes, I did need to scroll to the section about the proof to see that the article does not, in fact, provide a formal proof. I agree that this is pedantry, but in this case the article emphasizes formalization so much that it seems like it's a central point, and yet no formalization is to be found. To me this suggests that some people may simply not know what "formal" means in this context, which is fine, but since this is an important concept in computer science, I thought it is worth pointing out.
The meaning of 'formal' really depends on the context and is a matter of degree. This is readily apparent from your identification of formal with mechanical.
That immediately forces the question: which machine?
> a formal description is one that could be directly mechanically interpreted by a simple computer program as written
Outside of automated theorem proving and checking, very little done in math or theoretical CS actually meets the definition you gave for 'formal'. E.g. the proof of FLT is clearly not 'formal', it has not been reduced to steps that are all machine-checkable. The proof of, say, the Halting Problem as is normally given is also not formal.
If you relax your definition of 'machine' to include 'humans with mathematical context following a sequence of steps', then most proofs can be 'formal', depending on how much context the proof assumes of the reader.
Anyway, I think the distinction you make is useful to think about, but in this context (where the audience is mostly non-mathematicians, of which CS theorists are a variety), the better definition of formal is not mechanical, but are we attempting to abstract the problem down into a collection of fixed rules, and it's clear the author has done so.
The principle of charity would ask of us to ask, 'Is there another definition of 'formal' that would be reasonable, even if it's not the definition that I am most accustomed to?'
> The meaning of 'formal' really depends on the context
Yes, I say, "in the context of proofs."
> That immediately forces the question: which machine?
From Aristotle and up until Turing (exclusive) the answer was no machine, but the mechanical application of formal -- i.e., "of form" -- inference rules. That this mechanical process could actually be carried out by a machine was only realized later. Today we know what "mechanical" means, and the word is better understood than "formal" in this context, so it's easier to explain that formal just means mechanical.
> Outside of automated theorem proving and checking, very little done in math or theoretical CS actually meets the definition you gave for 'formal'.
That's right, but mathematicians know they're working informally. It is true that on occasion you do see a mathematician use the word formal for an informal presentation and proof, but I think that mostly happens because they hear the word from logicians and computer scientists and may not know what it means. Given that the word in this context originated together with the concept of computation, computer scientists should know better.
> If you relax your definition of 'machine' to include 'humans with mathematical context following a sequence of steps', then most proofs can be 'formal', depending on how much context the proof assumes of the reader.
If the derivations are not done formally then they are not formal even if a human does them. We certainly do hope that most mathematical proofs have formal counterparts, but unless you provide the formal proof, or make the relationship of your proof to a formal one obvious, then you are not providing a formal proof.
> the better definition of formal is not mechanical, but are we attempting to abstract the problem down into a collection of fixed rules, and it's clear the author has done so.
I don't know if it's better or not, but it is not the one that has been used for centuries. For example, in the book Formal Logic (1847) by Augustus de Morgan, he writes, "This logical truth depends upon the structure of the sentence and not upon the particular matters spoken of." In this particular case, the discussion of time machines in the construction of the proof clearly was not related to the structure (form) of the presentation but on the particular matters spoken-of, hence it is informal.
> 'Is there another definition of 'formal' that would be reasonable, even if it's not the definition that I am most accustomed to?'
I don't think it would qualify as a defintion, but clearly some people mean precise or mathematical when they say formal. This mistake is merely annoying and not serious. The reason that's annoying is that the words precise and mathematical are both more accurate and simpler/more familiar.
I like to say 'semiformal' of arguments meant for humans which could also be turned into a formal argument without calling on too much cleverness. (That's of course a matter of opinion or judgement.) Like pseudocode for programs.
If the author had simply written 'It will then formalize the Two Generals' Problem and f̶o̶r̶m̶a̶l̶l̶y̶ prove the impossibility', would you be fine with their statement?
I like this definition because it explicitly shows formal is really a continuum—since in the limit, you should go all the way down to ZF, but in practice nobody actually does this. A hard, black-and-white definition for formal is simply less useful.
It seems that your objection can be summarized as: 'formally prove' has only a single meaning in the context of a proof, the mathematical one.
IMHO is uncharitable to the author, since there are other, looser definitions of 'formal' in the context of algorithm analysis and software engineering.
> If the author had simply written 'It will then formalize the Two Generals' Problem and f̶o̶r̶m̶a̶l̶l̶y̶ prove the impossibility', would you be fine with their statement?
Not really, because he doesn't formalize the problem (i.e. write it in a formal system). But I may not have commented if the term "formal" wasn't so emphasized and used so often. This emphasis and repetition means that people simply don't know what formal means, and so I thought it was an opportunity to point out this rather common mistake.
> Note that 'formal' has another common definition in the context of software engineering
It's the very same definition. At all levels, the word "formal" actually means formal -- i.e., stated in a formal language.
> but in practice nobody actually does this.
100% of whatever it is that you do in formal methods is actually formal. You don't necessarily need a deductive formal proof, but in order to say formal you need to be formal. Static analyzers are 100% formal, as are model checkers. Even tests are 100% formal (although they don't fall under the umbrella term "formal verification" for unrelated reasons).
> there are other, looser definitions of 'formal' in the context of algorithm analysis and software engineering.
Not to my knowledge. I am not aware of any use of "formal" in the context of logic, proofs, computer science or software where it does not mean "mechanical".
>With the help of my time machine, I'll switch Alice's input from 1 to 0. This execution,
E
k
+
1
, is indistinguishable to
E
k
for Alice, so she still outputs 1, as does Bob. Next, I'll switch Bob's input to 0. Again, this execution,
E
k
+
2
, is indistinguishable to the previous execution,
E
k
+
1
, for Bob, so both Bob and Alice output 1.
I assume they must meet to discuss the algorithm beforehand.
So they could choose as algorithm: never attack
(Even if they cannot meet beforehand, the above is a strategy they can figure out on their own assuming the other is also choosing an optimal solution. Never attack is better than always attack because it doesn't depend on timing)
Then they need no communication yet know what to do and what the other does.
So problem is solvable, and something is wrong in the proof? Or alternatively I missed something in the problem statement preventing the above.
I had the same confusion until I read the proof, though maybe I missed something earlier too. This corresponds to the validity condition in the last section.
Both generals start with either 0 or 1, and the condition is that if both started with 0 (i.e., initially wanted to individually retreat), they should both output 0. Likewise for 1. The thing about Eve deciding which value the generals start with may also be confusing; a better way to think of it is that 'no matter what both generals start with, this validity condition holds'.
The problem could be formulated better, basically it's about reaching consensus about what the state is right now through a lossy medium. Your suggestion is to have a default, which is a good idea, but it doesn't really solve the problem if you want both processes to react to the state (there's an opportunity for an attack now, let's attack).
What also makes it unsolvable is that you do not want to endanger more messengers than necessary, i.e you don't want to send the another messenger with a message already sent. It's impossible to always know whether or not the receiver really did get the last message.
While I have not seen this problem before, I agree that a better formulation would have been helpful in thinking about it. For example, I (and it looks like some others in the thread) got caught up on the idea that Eve should just burn all of the messages and obviously you couldn't have consensus. This is because the article says Eve has the ability to burn all of the messages. I think it would be better stated as something like, "Bob/Alice is sending a messenger past the enemy to the other and the messenger may or may not be caught by Eve and killed." Or maybe I am still misunderstanding?
Two ships on the ocean of two different civilizations (who don't have shared traffic rules, and they also cannot communicate) are by accident on a head-on collision course towards each other. To avoid collision, they each need to turn a different direction, not the same direction. So each needs to quickly decide which direction to turn.
(Actually, more recognizable: walking on a sidewalk in a different country where people appear to have a different, or no, convention about which side people should cross each other)
It already assumes private communication and doesn't involve an attacker reading the messages, so no.
FTA:
> Eve receives every message and decides whether she wants to deliver the message or burn the message. She does not, however, get to open the enveloped message.
Most of the time, people deal with this by noting that the network sometimes has problems and expecting success anyway.
This is guaranteed to fail eventually, but if you can characterize the likelihood of dropping messages, you can set up agreed-upon sequences to improve the probability of eventual cooperation -- but you can never guarantee it.
For example: you can put checksums or hashes on your message to help detect corruption. You can put sequence numbers on your messages to help detect message loss. You can run an isochronous stream of very short messages to help decide on a base error rate, or to increase the likelihood of detecting a major loss. You can set up N different networks and hope that they don't all have losses at the same time.
All of these techniques help identify and remediate some degree of message loss, but cannot guarantee to solve it given a cantankerous enough -- or evil enough -- message killer.
Could this be solved by sending lots of messages to synchronize between the two parties.
Even if most messages are lost, its possible to have a state where you have both the same goal: if both receive the same message they sent they're on the same page.
A sends "Attack?Send your plan"
B sends "Retreat,Send your plan"
A sends "Retreat,Send your plan"
B sends "Retreat,Send your plan"
A sends "Retreat,Send your plan"
B sends "Retreat,Send your plan"
Then the network isn't lossy, but it's droppy. If all messages are dropped, one of the conditions of the theorem are invalidated; then it becomes a different problem.
I had a similar comment re. eventual consistency; and I think this is a case of eventual consistency.
I think it doesn't work because the problem becomes "when to retreat". It actually introduces a third state (attack; retreat; do nothing), where I might retreat today, and you do nothing.
Out of interest, if you set a time/date on when to retreat, how would the message look like, and how would you define confirmation for both parties?
It's possible to have a state where both reach consensus, but not possible to guarantee such state to happen in bounded time.
Here's another example: Alice asks Bob to attack in the morning. Bob accepts. But Eve doesn't let Bob's acceptance message to get to Alice. Alice waits for some time and asks Bob again to attack in the morning. Bob accepts. But message still doesn't reach Alice. If message does reach Alice before the attack, it's a win. If not, i.e. Eve holds messages past the attack time, only Bob attacks, as Alice won't know if he will.
A sends "Attack at 5:00, send your plan"
B sends "Attack at 5:00, send your plan"
A sends "Attack at 5:00, send your plan"
B sends "Attack at 5:00, send your plan"
A sends "Attack at 5:00, send your plan"
B sends "Attack at 5:00, send your plan"
Repeat until you got 3-4 confirmations of same data being sent back to you and the plan will work.
Given the Two Generals problem, I wanted to frame "eventual consistency" as the below, (but it doesn't work):
Alice sends a message saying "Attack on XX:XX on the nth day", and sends that message each day, with nth changing to (n - days)th. If the network (Eve) is lossy, it means she doesn't automatically burn all messages, so eventually, Bob will receive Alice's message.
Bob then responds with the same message back to Alice, until Alice receives it.
I initially thought this would work, but the extra round-trip from Bob to Alice makes it a problem.
I suppose with a long enough 'n', one only needs 2 round-trips, but with a state beyond {0;1}, it's probably impossible to reach "eventual consistency"
Reaching consensus is the definition of strong consistency. Eventual consistency would be something like: "Alice: I don't care when Bob attacks, as long as he attacks sometime in the future."
The article incorrectly defines the two generals problem.
The problem states that the two generals have decided to attack but need to coordinate on when. Failure to attack at the same time will result in defeat.
Does the semantics of the message matter to the fundamental problem? What's the difference between coordinating a time and coordinating an action? Notice that in either case, you're assuming the other component.
Deciding between a time and an action does matter. The big difference is when deciding on an action, each general only needs to eventually learn the action to take. When learning a time, each general needs to know the time to attack and they need to need to know the other general knows the time to attack before the time to attack has arrived. Here's a more thorough explanation:
Normally for the two generals problem, you assume if you retry a message indefinitely, the message will eventually be delivered. If this isn't the case, the problem is trivially impossible. If every message is dropped, the two generals cannot communicate with each other at all.
With this assumption, deciding on an action eventually becomes possible. Let's say the two generals strategy is the following. Each general individually decides to attack or retreat, then communicates their plan to the other general. If both general's agree they will execute that plan. Otherwise they will both retreat. To execute this strategy, the generals can use a protocol like TCP.
Each general repeatedly sends their plan to the other general until they receive an acknowledgement. Whenever a general receives a plan from the other general they send an acknowledgement, even if they have acknowledgement before. Based on the assumption above, if the first general keeps sending their plan, the second general will eventually receive it. When this happens the second general sends an acknowledgment. If the acknowledgement gets dropped, this cycle repeats. This is because the first general keeps sending the plan and the second general acknowledges it every time they receive it. Since the second general repeatedly sends the acknowledgement indefinitely, the first general will eventually receive it. Since both generals eventually receive the acknowledgement from the other general, using this algorithm will eventually finish.
This algorithm allows the generals to eventually agree an action. To see why the algorithm doesn't work for deciding on a time to attack, you can notice that in the above algorithm that each general never actually learns when both general's agree on an action. If a general doesn't know if the other general knows the plan, they cannot attack. If one general learns they are going to attack at 2pm, but the other general hasn't yet learned the time to attack, the first general will attack at 2pm, but the second general won't. Not only do you have to decide on a time, but each general needs to know that the other general has agreed with the time.
Doing this is impossible. The proof from Wikipedia looks something like the following. If the two generals eventually reach a point where they both know that "we will attack at 2pm" and "both generals know to attack at 2pm", there must have been some specific message where that statement became true. Without loss of generality, let's say that message was a message sent from the first general to the second. If that message was dropped, everything appears the same to the first general, but not to the second. The first general is now thinking "both generals will attack at 2pm", but the other general doesn't think that yet. This means that its impossible to construct any algorithm that works.
> The big difference is when deciding on an action, each general only needs to eventually learn the action to take.
This is implicitly dropping the requirement that the actions be coordinated.
When the message is what to do, the when must have been previously agreed upon (e.g. "dawn of the day after we figure out what we're going to do").
> using this algorithm will eventually finish
No, the same problem exists as in the other scenario: neither general knows when the other learned the correct action to take, and cannot schedule it correctly.
I agree. The author of the post didn't require that the general's attack at the same time. They only had to reach consensus on whether to attack or retreat. That's what spooneybarger meant by:
> The article incorrectly defines the two generals problem.
> The [actual] problem states that the two generals have decided to attack but need to coordinate on when. Failure to attack at the same time will result in defeat.
What if you said that Bob and Alice have an agreement to send letters every 2 minutes (taking turns one after another). If Eve were to drop a message, Bob or Alice would know that the message was discarded because the next sent message would not arrive in that 2-minute frame. Therefore, they do not update their state. If a state change is requested by either party, if and only if, simultaneous/consecutive messages go through (a total time of 4 minutes: one send and acknowledge) - states are updated: except the catch is that the send note contains the future time both Alice and Bob need to perform the update - which is constant in this entire exchange.
67 comments
[ 1.7 ms ] story [ 130 ms ] threadBut if we don't know that the other army is in position, and if Eve burns every message, then the problem is clearly unsolvable.
Another (practical) solution could be to spoof a message, making it appear as if from Eve. Some kind of steganography might work as well (or alternative forms of communication such as pigeons or smoke signals). And if all communications between Alice and Bob is discarded, this would worry either one of them to send a personal messenger who is human. This person could be captured and tortured, sure. But if they get "burned" as well, that'd be an act of war. Plus, if they are able to predetermine that if they don't hear from each other after X time, they attack after X + Y time (e.g. 3 months and 1 month [to prepare]) then the problem can be solved. If they cannot create a clear way of predetermined action based on actions then they'll always retreat.
Actually now that I gave it some further thought this "two general problem" can be observed in the cold war as well via (the nuclear threat of both parties). The nuclear threat from both sides created an equilibrium akin to what could happen in the described situation.
Working distributed systems have to work around this (and other) restrictions that are implicit to the properties of a distributed system. So TCP still works perfectly fine even though a perfect version of TCP (that didn't have timeouts) would be mathematically impossible to implement.
Now, as far as Alice is concerned, both Alice and Bob acknowledged. However, Bob never got Alice's acknowledgement, so he won't attack.
That has been accounted for.
" [Eve] does not, however, get to open the enveloped message."
> timeouts and defaults it can be
These time-outs and defaults would have to be negotiated between the generals over the postal system and wouldn't help them.
> as seen by many the distributed systems on the Internet
Those would have implemented a form of fault-tolerance for the more general "Byzantine Generals Problem."
Can you point me at an algorithm that guarantees consensus? Your claim seems to be at odds with the formal proof in the article. I particular, the article already allows for encryption, timeouts, and defaults.
So I can't see how you are right, and would appreciate some additional information as to why you think the article is wrong.
If it's pragmatic to dismiss impossibility results, perhaps revisit pragmatism.
What is consensus [1]?
As oh_sign noted in an earlier comment here, if Eve blocks all messages there is obviously no way to achieve consensus, so if there are no constraints on Eve's ability to interfere this is a trivial problem, so I'm going to assume that Eve is not able to block everything.
Suppose each general does this:
1. Generate a random 128 bit integer, P.
2. Decide the action they are going to take, A (attack or retreat).
3. Repeatedly send the message: "I will do A with priority P". (To be clear, P is only generated once. That single P is used in all messages).
4. They take action A unless they receive a message from the other general that states a different action, A', AND the other general's message has a lower P. In that case, they take action A'.
Without loss of generality, assume Alice has the lower P.
With the above procedure, as long as a single message from Alice to Bob makes it through, the generals will take the same action, which will be the action Alice picked.
Although they take the same action, only Bob knows that they are going to do so. He knows this because since a message from Alice got through to him, he knows she has a lower P so will stick with her original action regardless of whether or not his messages got through, and he will match her action because he knows she has a lower P.
Is that consensus, or to count as consensus do they both have to know before they act that they will be taking the same action?
Let's say that they do both have to know. Modify the above procedure so that if a general finds out they have the higher P, they change the message they are repeatedly sending to "I will do action A', following your lead", where A' is the action from the other general's message.
With this modified procedure, if Eve lets one message through from Alice, and after that lets one message through from Bob, then (1) the two generals take the same action, (2) Bob knows they will be taking the same action, and (3) Alice knows they will be taking the same action.
Is that now consensus? They are taking the same action and they both know they are doing so. Furthermore Alice knows that Bob knows. Bob, however, does not know that Alice knows. Do we need not only agreement, but each knowing that there is agreement, and knowing that they each know, and knowing that they each know that they each know, ad infinitum?
[1] Are consensus problems usually stated in terms of agreements between generals because the definition of consensus is literally, at least in Oxford, "A general agreement"?
The missing piece in your algorithm is how long do they wait to receive a message from each other and how they can know that it's long enough? If they don't wait long enough they will not receive a message and will make wrong assumptions about the other general, will not reach consensus and will take each their own action. To fix this each has to wait as long as it takes to receive a message from the other general and know about this (which in itself requires more messages).
But what if one of the generals dies in the meantime and stops sending messages? Or what if both Bob and Alice got the same random integer? There are other issues too.
But the important thing is it's all about time. You can always wait out uncertainty, but of course you won't be able to make progress waiting.
This problem keeps coming up in distributes systems and sadly, a full breakdown of internal communication is also possible.
I.e. internet routing works, switch for lan/cluster communication broke.
The issue here is different to what you are modelling; imagine this payoff table for A
The question is, knowing nothing about the reliability of the connection, is possible to have a strategy that has a positive expectation? B is only going to attack if they are absolutely certain you will, and vice-versa.The issue with your strategy is that even if Eve never interfered with the connection once, Alice does not know that, so will hold.
As a rule of thumb, if you could replace the word "formal" with "mechanical" and your sentence would still be true, then you can use the word formal (this is the case, say, with formal software verification, which is simply mechanical software verification, or formal proofs in a proof assistant, that are mechanical proofs). So, a formal description is one that could be directly mechanically interpreted by a simple computer program as written, and a formal proof is one that could be mechanically checked. If this is not the case -- use the word "precise" (or "mathematical" if you prefer). It's both simpler and more accurate.
As the description given here makes heavy use of natural language that is not easily interpretable by a computer, it is not formal, and since the proof makes use of a notion of a time machine, as well as others, not given a formal definition, it is very much informal, even if sufficiently precise to be acceptable as a mathematical proof.
"It will then formalize the Two Generals' Problem and formally prove the impossibility."
yes because i have heard of the word juxtaposition
>This guide will introduce the Two Generals' Problem and give an [INTUITIVE] explanation for why finding a solution to the problem is impossible. It will then formalize the Two Generals' Problem and formally prove the impossibility.
That immediately forces the question: which machine?
> a formal description is one that could be directly mechanically interpreted by a simple computer program as written
Outside of automated theorem proving and checking, very little done in math or theoretical CS actually meets the definition you gave for 'formal'. E.g. the proof of FLT is clearly not 'formal', it has not been reduced to steps that are all machine-checkable. The proof of, say, the Halting Problem as is normally given is also not formal.
If you relax your definition of 'machine' to include 'humans with mathematical context following a sequence of steps', then most proofs can be 'formal', depending on how much context the proof assumes of the reader.
Anyway, I think the distinction you make is useful to think about, but in this context (where the audience is mostly non-mathematicians, of which CS theorists are a variety), the better definition of formal is not mechanical, but are we attempting to abstract the problem down into a collection of fixed rules, and it's clear the author has done so.
The principle of charity would ask of us to ask, 'Is there another definition of 'formal' that would be reasonable, even if it's not the definition that I am most accustomed to?'
Yes, I say, "in the context of proofs."
> That immediately forces the question: which machine?
From Aristotle and up until Turing (exclusive) the answer was no machine, but the mechanical application of formal -- i.e., "of form" -- inference rules. That this mechanical process could actually be carried out by a machine was only realized later. Today we know what "mechanical" means, and the word is better understood than "formal" in this context, so it's easier to explain that formal just means mechanical.
> Outside of automated theorem proving and checking, very little done in math or theoretical CS actually meets the definition you gave for 'formal'.
That's right, but mathematicians know they're working informally. It is true that on occasion you do see a mathematician use the word formal for an informal presentation and proof, but I think that mostly happens because they hear the word from logicians and computer scientists and may not know what it means. Given that the word in this context originated together with the concept of computation, computer scientists should know better.
> If you relax your definition of 'machine' to include 'humans with mathematical context following a sequence of steps', then most proofs can be 'formal', depending on how much context the proof assumes of the reader.
If the derivations are not done formally then they are not formal even if a human does them. We certainly do hope that most mathematical proofs have formal counterparts, but unless you provide the formal proof, or make the relationship of your proof to a formal one obvious, then you are not providing a formal proof.
> the better definition of formal is not mechanical, but are we attempting to abstract the problem down into a collection of fixed rules, and it's clear the author has done so.
I don't know if it's better or not, but it is not the one that has been used for centuries. For example, in the book Formal Logic (1847) by Augustus de Morgan, he writes, "This logical truth depends upon the structure of the sentence and not upon the particular matters spoken of." In this particular case, the discussion of time machines in the construction of the proof clearly was not related to the structure (form) of the presentation but on the particular matters spoken-of, hence it is informal.
See https://en.wikipedia.org/wiki/Logic#Logical_form and https://en.wikipedia.org/wiki/Logical_form
> 'Is there another definition of 'formal' that would be reasonable, even if it's not the definition that I am most accustomed to?'
I don't think it would qualify as a defintion, but clearly some people mean precise or mathematical when they say formal. This mistake is merely annoying and not serious. The reason that's annoying is that the words precise and mathematical are both more accurate and simpler/more familiar.
Note that 'formal' has another common definition in the context of software engineering: https://en.wikipedia.org/wiki/Formal_methods#Taxonomy
I like this definition because it explicitly shows formal is really a continuum—since in the limit, you should go all the way down to ZF, but in practice nobody actually does this. A hard, black-and-white definition for formal is simply less useful.
It seems that your objection can be summarized as: 'formally prove' has only a single meaning in the context of a proof, the mathematical one.
IMHO is uncharitable to the author, since there are other, looser definitions of 'formal' in the context of algorithm analysis and software engineering.
Not really, because he doesn't formalize the problem (i.e. write it in a formal system). But I may not have commented if the term "formal" wasn't so emphasized and used so often. This emphasis and repetition means that people simply don't know what formal means, and so I thought it was an opportunity to point out this rather common mistake.
> Note that 'formal' has another common definition in the context of software engineering
It's the very same definition. At all levels, the word "formal" actually means formal -- i.e., stated in a formal language.
> but in practice nobody actually does this.
100% of whatever it is that you do in formal methods is actually formal. You don't necessarily need a deductive formal proof, but in order to say formal you need to be formal. Static analyzers are 100% formal, as are model checkers. Even tests are 100% formal (although they don't fall under the umbrella term "formal verification" for unrelated reasons).
> there are other, looser definitions of 'formal' in the context of algorithm analysis and software engineering.
Not to my knowledge. I am not aware of any use of "formal" in the context of logic, proofs, computer science or software where it does not mean "mechanical".
This is wrong. Alice and Bob should be switched.
So they could choose as algorithm: never attack
(Even if they cannot meet beforehand, the above is a strategy they can figure out on their own assuming the other is also choosing an optimal solution. Never attack is better than always attack because it doesn't depend on timing)
Then they need no communication yet know what to do and what the other does.
So problem is solvable, and something is wrong in the proof? Or alternatively I missed something in the problem statement preventing the above.
Both generals start with either 0 or 1, and the condition is that if both started with 0 (i.e., initially wanted to individually retreat), they should both output 0. Likewise for 1. The thing about Eve deciding which value the generals start with may also be confusing; a better way to think of it is that 'no matter what both generals start with, this validity condition holds'.
What also makes it unsolvable is that you do not want to endanger more messengers than necessary, i.e you don't want to send the another messenger with a message already sent. It's impossible to always know whether or not the receiver really did get the last message.
Two ships on the ocean of two different civilizations (who don't have shared traffic rules, and they also cannot communicate) are by accident on a head-on collision course towards each other. To avoid collision, they each need to turn a different direction, not the same direction. So each needs to quickly decide which direction to turn.
(Actually, more recognizable: walking on a sidewalk in a different country where people appear to have a different, or no, convention about which side people should cross each other)
FTA:
> Eve receives every message and decides whether she wants to deliver the message or burn the message. She does not, however, get to open the enveloped message.
This is guaranteed to fail eventually, but if you can characterize the likelihood of dropping messages, you can set up agreed-upon sequences to improve the probability of eventual cooperation -- but you can never guarantee it.
For example: you can put checksums or hashes on your message to help detect corruption. You can put sequence numbers on your messages to help detect message loss. You can run an isochronous stream of very short messages to help decide on a base error rate, or to increase the likelihood of detecting a major loss. You can set up N different networks and hope that they don't all have losses at the same time.
All of these techniques help identify and remediate some degree of message loss, but cannot guarantee to solve it given a cantankerous enough -- or evil enough -- message killer.
I think it doesn't work because the problem becomes "when to retreat". It actually introduces a third state (attack; retreat; do nothing), where I might retreat today, and you do nothing.
Out of interest, if you set a time/date on when to retreat, how would the message look like, and how would you define confirmation for both parties?
Here's another example: Alice asks Bob to attack in the morning. Bob accepts. But Eve doesn't let Bob's acceptance message to get to Alice. Alice waits for some time and asks Bob again to attack in the morning. Bob accepts. But message still doesn't reach Alice. If message does reach Alice before the attack, it's a win. If not, i.e. Eve holds messages past the attack time, only Bob attacks, as Alice won't know if he will.
Let’s say the last message in your example is dropped
B would have 3 acks from A while A only has 2 acks from B.
Will A attack? If not, B is left attacking on their own.
Similarly, what if none of Bs messages make it back to A? How does B know to attack?
Alice sends a message saying "Attack on XX:XX on the nth day", and sends that message each day, with nth changing to (n - days)th. If the network (Eve) is lossy, it means she doesn't automatically burn all messages, so eventually, Bob will receive Alice's message. Bob then responds with the same message back to Alice, until Alice receives it.
I initially thought this would work, but the extra round-trip from Bob to Alice makes it a problem.
I suppose with a long enough 'n', one only needs 2 round-trips, but with a state beyond {0;1}, it's probably impossible to reach "eventual consistency"
So, I agree re. strong consistency; as the problem was about that, and not eventual consistency.
https://en.m.wikipedia.org/wiki/Two_Generals'_Problem
The problem states that the two generals have decided to attack but need to coordinate on when. Failure to attack at the same time will result in defeat.
Full details are available on Wikipedia:
https://en.m.wikipedia.org/wiki/Two_Generals'_Problem
Normally for the two generals problem, you assume if you retry a message indefinitely, the message will eventually be delivered. If this isn't the case, the problem is trivially impossible. If every message is dropped, the two generals cannot communicate with each other at all.
With this assumption, deciding on an action eventually becomes possible. Let's say the two generals strategy is the following. Each general individually decides to attack or retreat, then communicates their plan to the other general. If both general's agree they will execute that plan. Otherwise they will both retreat. To execute this strategy, the generals can use a protocol like TCP.
Each general repeatedly sends their plan to the other general until they receive an acknowledgement. Whenever a general receives a plan from the other general they send an acknowledgement, even if they have acknowledgement before. Based on the assumption above, if the first general keeps sending their plan, the second general will eventually receive it. When this happens the second general sends an acknowledgment. If the acknowledgement gets dropped, this cycle repeats. This is because the first general keeps sending the plan and the second general acknowledges it every time they receive it. Since the second general repeatedly sends the acknowledgement indefinitely, the first general will eventually receive it. Since both generals eventually receive the acknowledgement from the other general, using this algorithm will eventually finish.
This algorithm allows the generals to eventually agree an action. To see why the algorithm doesn't work for deciding on a time to attack, you can notice that in the above algorithm that each general never actually learns when both general's agree on an action. If a general doesn't know if the other general knows the plan, they cannot attack. If one general learns they are going to attack at 2pm, but the other general hasn't yet learned the time to attack, the first general will attack at 2pm, but the second general won't. Not only do you have to decide on a time, but each general needs to know that the other general has agreed with the time.
Doing this is impossible. The proof from Wikipedia looks something like the following. If the two generals eventually reach a point where they both know that "we will attack at 2pm" and "both generals know to attack at 2pm", there must have been some specific message where that statement became true. Without loss of generality, let's say that message was a message sent from the first general to the second. If that message was dropped, everything appears the same to the first general, but not to the second. The first general is now thinking "both generals will attack at 2pm", but the other general doesn't think that yet. This means that its impossible to construct any algorithm that works.
This is implicitly dropping the requirement that the actions be coordinated.
When the message is what to do, the when must have been previously agreed upon (e.g. "dawn of the day after we figure out what we're going to do").
> using this algorithm will eventually finish
No, the same problem exists as in the other scenario: neither general knows when the other learned the correct action to take, and cannot schedule it correctly.
> The article incorrectly defines the two generals problem.
> The [actual] problem states that the two generals have decided to attack but need to coordinate on when. Failure to attack at the same time will result in defeat.