HN user
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.
Great idea and great work!
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.
There is an interesting paper that recently explored the de-facto C standard: Into the Depths of C: Elaborating the De Facto Standards, by Memarian et al. http://www.cl.cam.ac.uk/~km569/into_the_depths_of_C.pdf
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.
http://research.microsoft.com/en-us/um/people/lamport/pubs/v...
Is it comfortable ? Doesn't it cause itch on the neck or make you sweat ?
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.
Yes, I have just tried and it does not work.
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.
How would you find clothes that have not been manufactured by slaves ? In Switzerland I can buy from Switcher (switcher.ch), which markets clothes "made with respect", and I just found out about the Fair Wear Foundation, which has a short list of member brands (www.fairwear.org). As pointed out in this thread, just buying more expensive clothes may not make a difference.
Not really, if the total amount of money does not change, then the worth of the basic income would not converge to zero. Am I missing something obvious?
But, to be pedantic, 1000 times zero is still zero, so you are saying that any income will be worth zero.
I think that the "infinite, streaming structures" that you are referring to can be modelled in ZFC or HOL using Tarski's fixed-point theorem. See for example the paper by L. C. Paulson, "A fixedpoint approach to implementing (co)inductive definitions".
So the point of this anti-foundation axiom probably lies somewhere else.
Great work. Do you have a link to the machine-checked proof? In the technical report there is only a formal specification and a detailed but not machine-checkable proof. It would be really great to see systems researchers write machine-checked proofs :)
There is some very interesting work in the area of "choosing the right data structures".
For example "An introduction to data representation synthesis" (http://theory.stanford.edu/~aiken/publications/papers/cacm13...) presents a technique to do the following:
1) specify what the data structure should do using relational algebra (like for data bases)
2) automatically generate a data structure that is optimized for your specific hardware and workload.
A big advantage is that you can optimize for different hardware and workloads without changing your code. Also, the relational specification is much easier to get right than an optimized implementation.
It has also been extended to concurrent data structures: http://theory.stanford.edu/~hawkinsp/papers/pldi12concurrent...
There is btdigg.org, which builds its database by crawling the bittorrent distributed hash table.
From what I see on the front page, the course seems to be based on the notion of refinement, i.e. transforming a high-level specification into a concrete implementation by refining the specification in several steps. There is a recent example [1] of a software development process based on refinement. The authors build a fully verified model-checker using Isabelle/HOL. The code has a non-trivial size (4900 lines of ML) and implements complex functionality (model-checking algorithms) in an efficient way. Roughly speaking, it is proved that the model-checker reports the violation of a property if and only if the system under scrutiny does violate the property.
[1] http://cava.in.tum.de/templates/publications/CAV2013.pdf
I like your analysis, but why throw the 4 million estimate on the number of people killed in your Avenue 2 scenario? To give a number like that for such a speculative scenario seems ridiculous to me.
Here is a talk by moot, founder of 4chan, about identity online. I think that he argues that having multiple identities is part of human nature, that it makes us richer, and that forcing users of a web-site to use their official identity is misled. https://www.youtube.com/watch?v=e3Zs74IH0mc