Viewing profile — nano_o

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,…

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,…

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 b…

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 ca…

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 vot…

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 ver…

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 previou…

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 diffic…

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 t…

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 li…

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/~…

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 De…

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 reliabl…

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 …

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…

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 queu…

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 an…

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…

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 f…

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. Pau…