There is a recurring trend of interpreting democracy to mean "leaderless consensus-based decision-making", which really doesn't work and never has. That's why Occupy and pretty much every other similar bottom-up movement failed: leaders are necessary. People follow other people, not algorithms or groups.
"Making democracy work" should be about training better leaders and getting them into the system.
A cited paper's title is "There is more consensus in Egalitarian parliaments."
Are terms like "democracy" and "parliament" common terms in distributed computing theory? Or are these intentionally clickbaity/humorous paper titles?
otrack et al.: Thank you and congratulations! It's gratifying seeing the wheels of research make progress.
My appreciation of formal and machine-checked proofs has grown since we wrote the original EPaxos paper; I was delighted at the time at the degree to which Iulian was able to specify the protocol in TLA+, but now in hindsight wish we (or a later student) had made the push to get the recovery part formalized as well, so perhaps we'd have found these issues a decade ago. Kudos for finding and fixing it.
Have you yourselves considered formalizing your changes to the protocol in TLA+? I wonder if the advances the formal folks have made over the last decade or so would ease this task. Or, perhaps better yet -- one could imagine a joint protocol+implementation verification in a system like Ironfleet or Verus, which would be tremendously cool and also probably a person-year of work. :)
Edited to add: This would probably make a great masters thesis project. If y'all are not already planning on going there, I might drop the idea to Bryan Parno and see if we find someone one of these years who would be interested in verifying/implementing your fixed version in Verus. Let me know (or if we start down the path I'll reach out).
Thank you, dgacmu! We are currently working on a TLA+ specification with master's students, and we plan to verify it with TLC and Apalache. I discovered that Iulian's TLA+ specification was missing a ballot variable [1] by injecting a trace, because exhaustive exploration was not tractable. Therefore, state-space explosion is likely to become a problem (systems of interest contain 7–9 processes with non‑transitive conflicts). In that case, intermediate abstractions will be necessary, which may naturally lead us to theorem proving.
Once the specification is ready, I'll post about it here. :)
* As others have pointed out, Paxos is leaderless. Electing a leader is a performance trick (reduce contention/retries), not a correctness trick - if you want to order your events.
* EPaxos appears to relax ordering as long as the clients can declare their event-dependencies.
Q1) If I withdraw from ATM 1 and someone else withdraws from ATM 2, we are independent consumers - so how do we possibly coordinate which withdrawal depends on the other?
Q2) Assuming that's not a problem, how do I get the ability to replay events? If the nodes don't care about order (beyond constraints), how can I re-read events 1-100, suffer a node outage, and resume reading events 101-200 from a replacement node?
One of the big gaps in Raft is that it’s hard to manage leader election on a heterogenous network. Everyone has or knows a story about the tiny branch office we keep for the CTO’s nephew or that engineer who decided to move to Colorado and quit if he couldn’t work from there, getting elected leader and the whole system limping to a halt.
In the case of Raft it would benefit I think from having an instant runoff election process. Where three nodes are nominated and everyone votes on which one has the best visibility.
At the very least I can see a way to use latency to determine who to vote for, to manage a fast election instead of timeouts and retries.
I'm struggling to grasp this paper. The title makes it sound like its talking about democratic processes in the real world but then reading makes me think its a technical paper on computing. Then the comments talk about a mix.
Is anyone able to provide a simple overview of whats being covered here? To me it seems impossible to run a government with no leader and humans having to vote on everything and trust each other. It would be very inefficient not having someone to break ties and make executive choices.
10 comments
[ 4.4 ms ] story [ 37.3 ms ] threadThis is exactly how bitcoin works.
Every 10 minutes the network elects a leader to assort & order transactions and also throw out fraudulent transactions.
If he fails to do this, he is not allow to claim his block reward (technically the "coinbase" transaction)
I keep telling people the future of politics is markets & Blockchains.
Its hard to explain comprehensively and what's strange is that no one has written a thorough book on the topic.
I am happy there are people actually writing such material on this topic.
Albeit its a bit too technical.
Computer science is the future of politics & governance. (I don't think AI is any useful but rather distributed systems)
"Making democracy work" should be about training better leaders and getting them into the system.
Isn’t that multi-Paxos? Paxos is leaderless.
Very odd opening sentence.
My appreciation of formal and machine-checked proofs has grown since we wrote the original EPaxos paper; I was delighted at the time at the degree to which Iulian was able to specify the protocol in TLA+, but now in hindsight wish we (or a later student) had made the push to get the recovery part formalized as well, so perhaps we'd have found these issues a decade ago. Kudos for finding and fixing it.
Have you yourselves considered formalizing your changes to the protocol in TLA+? I wonder if the advances the formal folks have made over the last decade or so would ease this task. Or, perhaps better yet -- one could imagine a joint protocol+implementation verification in a system like Ironfleet or Verus, which would be tremendously cool and also probably a person-year of work. :)
Edited to add: This would probably make a great masters thesis project. If y'all are not already planning on going there, I might drop the idea to Bryan Parno and see if we find someone one of these years who would be interested in verifying/implementing your fixed version in Verus. Let me know (or if we start down the path I'll reach out).
can you share more?
Once the specification is ready, I'll post about it here. :)
[1] https://arxiv.org/abs/1906.10917
* EPaxos appears to relax ordering as long as the clients can declare their event-dependencies.
Q1) If I withdraw from ATM 1 and someone else withdraws from ATM 2, we are independent consumers - so how do we possibly coordinate which withdrawal depends on the other?
Q2) Assuming that's not a problem, how do I get the ability to replay events? If the nodes don't care about order (beyond constraints), how can I re-read events 1-100, suffer a node outage, and resume reading events 101-200 from a replacement node?
In the case of Raft it would benefit I think from having an instant runoff election process. Where three nodes are nominated and everyone votes on which one has the best visibility.
At the very least I can see a way to use latency to determine who to vote for, to manage a fast election instead of timeouts and retries.
Is anyone able to provide a simple overview of whats being covered here? To me it seems impossible to run a government with no leader and humans having to vote on everything and trust each other. It would be very inefficient not having someone to break ties and make executive choices.