nano_o

29 ms·

1.
by nano_o 2mo ago
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
2.
by nano_o 2mo ago
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 i
3.
by nano_o 2y ago
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:/&#x
4.
by nano_o 3y ago
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
5.
by nano_o 4y ago
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:/&#x2
6.
by nano_o 5y ago
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 issu
7.
by nano_o 6y ago
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-shel
8.
by nano_o 7y ago
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
9.
by nano_o 7y ago
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
10.
by nano_o 10y ago
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 t
11.
by nano_o 10y ago
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
12.
by nano_o 11y ago
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
13.
by nano_o 11y ago
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
14.
by nano_o 12y ago
Is it comfortable ? Doesn't it cause itch on the neck or make you sweat ?
15.
by nano_o 13y ago
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 o
16.
by nano_o 13y ago
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?
17.
by nano_o 13y ago
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 a
18.
by nano_o 13y ago
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. W
19.
by nano_o 13y ago
Yes, I have just tried and it does not work.
20.
by nano_o 13y ago
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
21.
by nano_o 13y ago
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
22.
by nano_o 13y ago
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?
23.
by nano_o 13y ago
But, to be pedantic, 1000 times zero is still zero, so you are saying that any income will be worth zero.
24.
by nano_o 13y ago
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 implemen
25.
by nano_o 13y ago
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-chec
26.
by nano_o 13y ago
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
27.
by nano_o 13y ago
There is btdigg.org, which builds its database by crawling the bittorrent distributed hash table.
28.
by nano_o 13y ago
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 examp
29.
by nano_o 13y ago
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.
30.
by nano_o 13y ago
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

More ›