On: Notes on Paxos

[lxe]

I find using set, TLA, or other mathematical notation cumbersome to explain these things. Would a visualization would make it more approachable?

I know Raft is easier to understand, at least to me, probably due in part to its visual explanation that's front and center: https://raft.github.io/

EDIT: Turns out it's harder to find a paxos visualization. Here's one: https://www.scs.stanford.edu/17au-cs244b/labs/projects/vimbe... https://jivimberg.io/paxos-playground/src/main/html/

[inaseer → lxe]

Shameless plug: http://imnaseer.net/paxos-from-the-ground-up.html

I worked on an explanation of Paxos where we start with a simple but incorrect implementation of the protocol. The bug is then fixed and the protocol refined. Which leads to another bug. Interestingly, after fixing 6 or 7 bugs we arrive at the actual working implementation of Paxos. The reader, having walked the path of arriving at the protocol (hopefully) understands the nuances better than just reading the description of the protocol from the get-go.

Bonus: The explanation uses simulated visual runs as well, eg. http://imnaseer.net/paxos-from-the-ground-up.html?section=3&...

[lalwanivikas → lxe]

Raft is understandable because that was one of it's key design goals.

[sillysaurusx → lxe]

Set / TLA / etc tends to fail when a system is only probabilistically stable, doesn't it?

(Not strictly about paxos; more of a general observation.)

[rantwasp → sillysaurusx]

nope. it’s not about probabilities. if it is it’s incorrectly modeled

[sillysaurusx → rantwasp]

There are probabilistic systems.