It's impossible to do it deterministically (that's the famous FLP impossibility result), but if you accept to have liveness only with probability 1 then it's possible (for example, an early randomized asynchronous protocol is Ben-Or's protocol from 1983).
What's interesting here is that this would be the first production implementation of an asynchronous consensus algorithm (QuePaxa). Paxos, Raft, etc. are all partially synchronous, meaning they rely on timeouts and only make progress if message delay is sufficiently small compared to timeout durations. QuePaxa doesn't rely on timeouts and makes progress even under wild fluctuations in message delay. The question is whether performance is competitive enough in the normal case, when message delay is small and doesn't vary much, and historically the answer has been "no" and that's why asynchronous protocols weren't used.
The bug in the Paxos Made Simple paper is that Lamport forgot to mention that, upon accepting a proposal, an acceptor also implicitly promises not to accept any proposal in lower ballots. It's discussed at length here: https://stackoverflow.com/questions/29880949/contradiction-i...
In your example, you can just add a variable that is incremented at every step and then use it to state your invariant that convergence must happen within 5 steps.
Sometimes you can encode properties that might initially seem hard to state in TLA+ in a similar way. Lamport has a recent paper explaining how to do that for hyperproperties such as information-flow security: http://lamport.azurewebsites.net/pubs/pubs.html?from=https:/...
With fancy cryptography (e.g. zero-knowledge proofs), you can allow the public to verify that the tally is correct while keeping votes secret. It's called end-to-end verifiable voting, and this is a good introduction: https://www.microsoft.com/en-us/research/publication/end-end...
The idea is that people post their votes publicly, but encrypted, and there's a procedure (based on zero-knowledge proofs) that allows to check that an encrypted vote is correctly accounted for in the tally without decrypting said vote. If sufficiently many voters post their encrypted votes (and if it's not too predictable who will do so), a wrong tally will be detected with high probability.
The Stellar Network relies on nodes declaring quorum slices, which can be understood as trust relationships, but it implements a single global blockchain. So I don't think it's very similar.
Edit: one similarity is that token issuers in Stellar can remain authoritative on their token.
You might find the Sledgehammer tool for Isabelle quite interesting. It has been using machine learning techniques to find proofs automatically since at least 2013. It uses previous proof to learn how to select facts to send to off-the-shelf automated provers in order to discharge a goal.
See e.g. http://isabelle.in.tum.de/~blanchet/mash2.pdf
On issue I have with it, and that automated proof tools based on ML are going to have to solve, is that it's quite unpredictable. Even if it finds stunning proofs from time to time, it is hard to use an unpredictable tool efficiently.
Yes, it's a nitpick. The comparison to Multi-Paxos seems fair because it makes similar assumptions (unless re-configuring the relay network after a leader failure is somehow difficult, but I wouldn't expect that).
My point is that it would be nice to benchmark protocols that take into account the issues I brought up, and measure what happens in the worst failure scenarios they are supposed to tolerate. Otherwise we get a false sense of what performance can be achieved if one really cares about fault-tolerance.
This small issue does not diminish the main contribution of the paper in any way.
A couple nitpicks: it would be nice to see what happens when the leader fails. Optimizing for the case of a stable leader might have impact on recovery time.
Another important aspect for fault-tolerance is whether you can really survive any minority crashing. For example, if only the strictly necessary number of nodes keep up with the leader, then if most of those crash the system will have a really hard time recovering due to the backlog accumulated at slow nodes which now need to catch up for the system to continue operating.
A performance number that does not take those things into account may not be very realistic. Nevertheless the idea is pretty good.
Also, it seems they proved a behavioral equivalence property: any user-space program has exactly the same behaviors when running on the C+assembly implementation of the OS (6500 lines) and when running on the abstract machine specified by the high-level specification of the OS (450 lines). Their specification also includes liveness properties (e.g. no deadlocks or livelocks).
For comparison, seL4 has verified behavioral refinement between implementation and specification, termination of all syscalls, and several security properties (non-interference and information-flow properties among threads), worst case execution times, and other things; but, seL4 does not support fined-grained concurrency.
The article seems to be based on the following paper, published in 2012:
"Cosmic Rays Don't Strike Twice: Understanding the Nature of DRAM Errors and the Implications for System Design".
Newer research on the topic has since been published, for example this year: "Revisiting Memory Errors in Large-Scale Production Data Centers: Analysis and Modeling of New Trends from the Field" (from Facebook) and "Memory Errors in Modern Systems: The Good, The Bad, and The Ugly".
It seems similar to the primary-backup instance of the Vertical Paxos family. In the primary-backup Vertical Paxos, one can tolerate f faults with f+1 replicas as long as a reliable external reconfiguration master is there to replace failed replicas and make sure everyone agrees on the configuration.
Here the external reconfiguration master would be ZooKeeper and the primary-backup protocol the ISR protocol.
Have a look at the documentary "Growing up in America".
It is about the activists of the 60s, how they thought they could change the world, and what had happened by the 80s.
There was also this idea that everything would improve once the old generation would be dead, but it did not happen.
Ok, so it is relatively easy to obtain a safe implementation and from there you can use a heuristic to prevent a thread from looping forever trying to find an available slot. Would that sum up the issue in practice?
I'm a bit skeptical about the code: it seems that it's using only the atomic fetch-and-add synchronization instruction, and not compare-and-swap.
However, I think that whether queues are implementable with only fetch-and-add is an open problem in distributed computing (in technical terms, whether queues are in the Common2 family. See for example Afek et al., "Common2 Extended to Stacks and Unbounded Concurrency".)
I think that they would not be able to do that: only one of the two transactions could be in the longest correct block-chain. That's because it is easy for the clients to detect and reject a block-chain that contains double spending.
What they can do is pay for goods or services and revert the transaction after the goods or services have been delivered.
I am running OpenWRT on a Buffalo WBMR-HP-G300H without any issues. This model has an integrated ADSL modem and has a few USB ports. I have a USB hard disk attached and I use it as a media and bittorrent server. Over LAN it can stream an HD movie from the disk, but over wifi it seems too slow for that.