/* Consensus: Raft's leader election and log replication, and nothing else. * * Ongaro and Ousterhout, In Search of an Understandable Consensus Algorithm, * USENIX ATC, June 2014. Every rule below is a line of the paper's Figure 2, * and the comment beside it says which one. Membership changes, snapshots, * clients and the state machine itself are not here, because the page is about * two mechanisms and a partition. * * The model is atomic. A message is either delivered whole, with its reply, * in one step, or it is never delivered at all. There are no clocks: a * timeout is something the reader makes happen, and the paper's randomised * 150 to 300 ms is the reason one server usually gets there first, not a * number this engine measures. Both simplifications are on the page's ledger. * * The same step() that the buttons call is the one the checker explores. So * the states a reader can reach by pressing buttons are a subset of the states * the checker has already examined, and the claims in the checks table are * about the machine the reader is driving rather than about a second copy of * it. * * Servers are numbered from 0 inside the engine and printed from S1. Terms * start at 0 with every log empty and nobody in charge. */ (function () { "use strict"; /* ---- a cluster -------------------------------------------------------- */ function server() { return { term: 0, // currentTerm, persistent role: "F", // F follower, C candidate, L leader voted: -1, // votedFor in this term, persistent; -1 is null log: [], // the term of each entry; an entry is (index, term) commit: 0, // commitIndex, the highest entry known committed votes: 0, // a candidate's granted votes, as a bit per server match: null // a leader's matchIndex[], one per server }; } function fresh(n) { var s = []; for (var i = 0; i < n; i += 1) s.push(server()); // The ghost is not part of any server. It is the history the safety // properties are stated over: who was elected in which term, and which // entry was committed at which index in which term. A real cluster has no // such record; the checker needs one because two of the five properties // are about the past. return { n: n, s: s, cut: 0, ghost: { elected: [], committed: [] } }; } function copyServer(x) { return { term: x.term, role: x.role, voted: x.voted, log: x.log.slice(), commit: x.commit, votes: x.votes, match: x.match ? x.match.slice() : null }; } function copy(st) { return { n: st.n, s: st.s.map(copyServer), cut: st.cut, ghost: { elected: st.ghost.elected.slice(), committed: st.ghost.committed.map(function (c) { return c ? { et: c.et, ct: c.ct } : c; }) } }; } function majority(n) { return Math.floor(n / 2) + 1; } function bits(mask) { var c = 0; while (mask) { c += mask & 1; mask >>>= 1; } return c; } function lastTerm(log) { return log.length ? log[log.length - 1] : 0; } /* Section 5.4.1: "If the logs have last entries with different terms, then * the log with the later term is more up-to-date. If the logs end with the * same term, then whichever log is longer is more up-to-date." */ function atLeastAsUpToDate(cand, voter) { var a = lastTerm(cand), b = lastTerm(voter); if (a !== b) return a > b; return cand.length >= voter.length; } /* A cut puts some servers on side B; a message crosses only within a side. */ function reachable(st, i, j) { return ((st.cut >> i) & 1) === ((st.cut >> j) & 1); } /* "If RPC request or response contains term T > currentTerm: set * currentTerm = T, convert to follower." Figure 2, all servers. */ function adopt(x, term) { x.term = term; x.role = "F"; x.voted = -1; x.votes = 0; x.match = null; } /* ---- the two decisions a server makes on someone else's behalf ---------- */ /* What j answers if candidate i asks it for a vote now, and why. This is * RequestVote's receiver implementation, read in the state j would be in * after adopting i's term. */ function voteAnswer(st, i, j) { var c = st.s[i], v = st.s[j]; // A late request comes from a server that has already won, and the // sentence has to say leader, not candidate, for it to be true. var who = c.role === "L" ? "leader" : "candidate"; var vTerm = Math.max(v.term, c.term); var vVoted = c.term > v.term ? -1 : v.voted; if (c.term < v.term) { return { grant: false, code: "stale", why: "its own term is " + v.term + ", newer than the " + who + "'s " + c.term }; } if (vVoted !== -1 && vVoted !== i) { return { grant: false, code: "voted", why: "it has already voted for S" + (vVoted + 1) + " in term " + vTerm }; } if (!atLeastAsUpToDate(c.log, v.log)) { var a = lastTerm(c.log), b = lastTerm(v.log); return { grant: false, code: "log", why: a !== b ? "its last entry is from term " + b + " and the " + who + "'s is from term " + a : "both logs end in term " + a + " and its own is longer, " + v.log.length + " entries against " + c.log.length }; } return { grant: true, code: "yes", why: vVoted === i ? "it has already voted for this " + who + " in this term" : "the " + who + "'s log is at least as up to date as its own" }; } /* ---- the actions ------------------------------------------------------ */ /* * Four, and they are all the checker explores: * T i server i's election timer runs out * V i j candidate i asks j for a vote, and hears the answer * W i a client write reaches leader i * A i j leader i sends j everything j is missing, and hears the answer * plus two that only the page uses, because the checker already considers * every message that might never arrive: * P mask cut the network, servers in the mask on one side * H heal it * * step() returns the next state and what happened, or a refusal saying why * the action is not possible. It never changes its argument. */ var RULES = ["raft", "majority"]; function refuse(why) { return { ok: false, why: why }; } function step(st, act, rule, quick) { rule = rule || "raft"; var k = act.k, i = act.i, j = act.j; var nx, me, you, ev = []; if (k === "P") { var mask = act.mask & ((1 << st.n) - 1); if (mask === 0 || mask === (1 << st.n) - 1) return refuse("a cut needs a server on each side"); nx = copy(st); nx.cut = mask; return done(st, nx, act, rule, ["the network is cut in two"], null, quick); } if (k === "H") { if (!st.cut) return refuse("the network is already whole"); nx = copy(st); nx.cut = 0; return done(st, nx, act, rule, ["the network is whole again"], null, quick); } if (!(i >= 0 && i < st.n)) return refuse("there is no such server"); if ((k === "V" || k === "A") && !(j >= 0 && j < st.n && j !== i)) { return refuse("a server does not send to itself"); } me = st.s[i]; if (k === "T") { // Followers and candidates time out; a leader has no election timer. if (me.role === "L") return refuse("S" + (i + 1) + " is the leader and has no election timer running"); nx = copy(st); me = nx.s[i]; // "On conversion to candidate, start election: Increment currentTerm, // Vote for self." me.term += 1; me.role = "C"; me.voted = i; me.votes = 1 << i; me.match = null; ev.push("S" + (i + 1) + " times out and stands for term " + me.term); // A cluster of one would win on the spot; with three or more it cannot. won(nx, i, ev); return done(st, nx, act, rule, ev, null, quick); } if (k === "V") { // A candidate sends its requests "in parallel to each of the other // servers", so one can still arrive after the candidate has won. That // late request is the only way a leader appears here: the voter answers // it as it would any other, and the leader has no use for the reply // unless it carries a newer term. if (me.role !== "C" && me.role !== "L") return refuse("S" + (i + 1) + " is not standing for election"); if (me.role === "L" && me.term === st.s[j].term && st.s[j].voted !== -1) { return refuse("S" + (j + 1) + " has already voted in term " + me.term); } if (!reachable(st, i, j)) return refuse("S" + (i + 1) + " cannot reach S" + (j + 1) + " across the cut"); if ((me.votes >> j) & 1) return refuse("S" + (j + 1) + " has already given S" + (i + 1) + " its vote"); var answer = voteAnswer(st, i, j); nx = copy(st); me = nx.s[i]; you = nx.s[j]; if (me.term > you.term) { if (you.role !== "F") ev.push("S" + (j + 1) + " hears term " + me.term + " and steps down"); adopt(you, me.term); } if (answer.grant) { you.voted = i; ev.push("S" + (j + 1) + " votes for S" + (i + 1) + " in term " + me.term); if (me.role === "C") { me.votes |= 1 << j; won(nx, i, ev); } } else { ev.push("S" + (j + 1) + " refuses S" + (i + 1) + ": " + answer.why); if (you.term > me.term) { ev.push(me.role === "L" ? "S" + (i + 1) + ", which leads term " + me.term + ", hears term " + you.term + " and steps down" : "S" + (i + 1) + " learns of term " + you.term + " and stops standing"); adopt(me, you.term); } } return done(st, nx, act, rule, ev, { answer: answer }, quick); } if (k === "W") { if (me.role !== "L") return refuse("only the leader takes writes, and S" + (i + 1) + " is not the leader"); nx = copy(st); me = nx.s[i]; // "If command received from client: append entry to local log." me.log.push(me.term); ev.push("S" + (i + 1) + " appends an entry from term " + me.term + " at index " + me.log.length); return done(st, nx, act, rule, ev, null, quick); } if (k === "A") { if (me.role !== "L") return refuse("S" + (i + 1) + " is not the leader"); if (!reachable(st, i, j)) return refuse("S" + (i + 1) + " cannot reach S" + (j + 1) + " across the cut"); nx = copy(st); me = nx.s[i]; you = nx.s[j]; // Receiver rule 1: "Reply false if term < currentTerm", and the leader, // seeing the newer term in the reply, converts to follower. if (me.term < you.term) { ev.push("S" + (j + 1) + " is in term " + you.term + ", so S" + (i + 1) + " learns it is no longer the leader"); adopt(me, you.term); return done(st, nx, act, rule, ev, { stale: true }, quick); } if (me.term > you.term) adopt(you, me.term); // A candidate that hears from a leader of its own term steps down. if (you.role !== "F") { ev.push("S" + (j + 1) + " stops standing and follows S" + (i + 1)); } you.role = "F"; you.votes = 0; you.match = null; // Receiver rule 2 and the leader's retry loop, collapsed into one step: // the leader backs nextIndex off until prevLogIndex matches, which is // the latest index at which both logs hold an entry of the same term. var p = Math.min(me.log.length, you.log.length); while (p > 0 && you.log[p - 1] !== me.log[p - 1]) p -= 1; // Rules 3 and 4: delete from the first conflict, append what is missing. var removed = []; for (var x = p; x < me.log.length; x += 1) { if (x < you.log.length) { if (you.log[x] === me.log[x]) continue; for (var y = x; y < you.log.length; y += 1) removed.push({ index: y + 1, term: you.log[y] }); you.log.length = x; } you.log.push(me.log[x]); } if (removed.length) { ev.push("S" + (j + 1) + " deletes " + removed.map(function (r) { return "index " + r.index + " (term " + r.term + ")"; }).join(", ") + ", which conflicted with S" + (i + 1)); } // Rule 5: "If leaderCommit > commitIndex, set commitIndex = // min(leaderCommit, index of last new entry)". Every entry after the // match point was sent, so the last new entry is the leader's last. if (me.commit > you.commit) you.commit = Math.min(me.commit, me.log.length); // The reply: "If successful: update nextIndex and matchIndex". me.match[j] = Math.max(me.match[j], me.log.length); ev.push("S" + (j + 1) + " now matches S" + (i + 1) + " up to index " + me.log.length); advance(nx, i, rule, ev); return done(st, nx, act, rule, ev, { removed: removed, from: p }, quick); } return refuse("there is no such action"); } /* A candidate with a majority of the full cluster becomes leader, with * matchIndex "initialized to 0". */ function won(st, i, ev) { var me = st.s[i]; if (me.role !== "C" || bits(me.votes) < majority(st.n)) return; me.role = "L"; me.votes = 0; me.match = []; for (var j = 0; j < st.n; j += 1) me.match.push(0); var prior = st.ghost.elected[me.term]; if (prior === undefined) st.ghost.elected[me.term] = i; else if (prior !== i) st.ghost.elected[me.term] = -2; // two leaders: Election Safety ev.push("S" + (i + 1) + " has a majority and leads term " + me.term); } /* The commit rule, which is the whole of Figure 8. Raft's: "If there exists * an N such that N > commitIndex, a majority of matchIndex[i] >= N, and * log[N].term == currentTerm: set commitIndex = N". The other rule drops the * last clause, which is what a reader would write first. */ function advance(st, i, rule, ev) { var me = st.s[i]; for (var N = me.log.length; N > me.commit; N -= 1) { var have = 1; for (var j = 0; j < st.n; j += 1) if (j !== i && me.match[j] >= N) have += 1; if (have < majority(st.n)) continue; if (rule === "raft" && me.log[N - 1] !== me.term) continue; for (var x = me.commit + 1; x <= N; x += 1) { var c = st.ghost.committed[x]; if (!c) st.ghost.committed[x] = { et: me.log[x - 1], ct: me.term }; else if (c.et !== me.log[x - 1]) c.et = -1; // a second, different entry at x } ev.push("S" + (i + 1) + " commits up to index " + N); me.commit = N; return; } } /* quick leaves the five properties unchecked, for the checker, which checks * them itself once per state rather than once per way of arriving there. */ function done(prev, nx, act, rule, ev, extra, quick) { var r = { ok: true, state: nx, events: ev, broken: quick ? null : broken(nx, prev) }; if (extra) for (var key in extra) r[key] = extra[key]; return r; } /* ---- the five properties of Figure 3 ----------------------------------- */ /* Every property the paper says holds at all times, checked on one state * (and, for Leader Append-Only, against the state before). Returns a list * of {prop, text}; empty means all five hold here. */ function broken(st, prev) { var out = [], a, b, x, i; // Election Safety: at most one leader can be elected in a given term. st.ghost.elected.forEach(function (who, t) { if (who === -2) out.push({ prop: "election", text: "two servers were elected in term " + t }); }); // Log Matching: same index and term means identical up through it. for (a = 0; a < st.n; a += 1) { for (b = a + 1; b < st.n; b += 1) { var A = st.s[a].log, B = st.s[b].log, top = Math.min(A.length, B.length); for (x = top; x > 0; x -= 1) { if (A[x - 1] !== B[x - 1]) continue; for (var y = 0; y < x; y += 1) { if (A[y] !== B[y]) { out.push({ prop: "matching", text: "S" + (a + 1) + " and S" + (b + 1) + " agree at index " + x + " but differ at index " + (y + 1) }); break; } } break; } } } if (prev) appendOnly(prev, st, out); // Leader Completeness: an entry committed in a term is in the log of // every leader of a later term. for (i = 0; i < st.n; i += 1) { var L = st.s[i]; if (L.role !== "L") continue; st.ghost.committed.forEach(function (c, idx) { if (c && c.ct < L.term && L.log[idx - 1] !== c.et) { out.push({ prop: "completeness", text: "S" + (i + 1) + " leads term " + L.term + " without the entry committed at index " + idx + " in term " + c.ct }); } }); } // State Machine Safety: once a server has applied an entry at an index, // no server applies a different one there. Applying is taken to happen // the moment an entry is known committed. st.ghost.committed.forEach(function (c, idx) { if (c && c.et === -1) { out.push({ prop: "machine", text: "two different entries were committed at index " + idx }); } }); for (i = 0; i < st.n; i += 1) { var S = st.s[i]; for (x = 1; x <= S.commit; x += 1) { var c = st.ghost.committed[x]; if (!c || S.log[x - 1] !== c.et) { out.push({ prop: "machine", text: "S" + (i + 1) + " has applied index " + x + " as " + (S.log[x - 1] === undefined ? "an entry it no longer has" : "an entry from term " + S.log[x - 1]) + (c && c.et > 0 ? ", where term " + c.et + " was committed first" : "") }); break; } } } return out; } /* Leader Append-Only: a leader never overwrites or deletes its entries. A * property of a step rather than of a state, so it needs the one before. */ function appendOnly(prev, st, out) { for (var i = 0; i < st.n; i += 1) { var was = prev.s[i], now = st.s[i]; if (was.role !== "L" || now.role !== "L" || was.term !== now.term) continue; var kept = now.log.length >= was.log.length; for (var z = 0; kept && z < was.log.length; z += 1) kept = now.log[z] === was.log[z]; if (!kept) out.push({ prop: "append", text: "leader S" + (i + 1) + " changed an entry it already had" }); } return out; } /* Whether a step changed the log of a server that leads the same term before * and after it. Those are the only steps Leader Append-Only can fail on, so * they are what its row counts, rather than every write and send. */ function leaderWrote(prev, st) { for (var i = 0; i < st.n; i += 1) { var was = prev.s[i], now = st.s[i]; if (was.role !== "L" || now.role !== "L" || was.term !== now.term) continue; if (now.log.length !== was.log.length) return true; for (var z = 0; z < was.log.length; z += 1) if (now.log[z] !== was.log[z]) return true; } return false; } var PROPS = [ { id: "election", name: "Election Safety" }, { id: "append", name: "Leader Append-Only" }, { id: "matching", name: "Log Matching" }, { id: "completeness", name: "Leader Completeness" }, { id: "machine", name: "State Machine Safety" } ]; /* ---- the actions available in a state ----------------------------------- */ function actions(st, bounds) { var out = [], i, j, n = st.n; var maxTerm = bounds && bounds.maxTerm, maxLog = bounds && bounds.maxLog; for (i = 0; i < n; i += 1) { var me = st.s[i]; if (me.role !== "L" && !(maxTerm && me.term >= maxTerm)) out.push({ k: "T", i: i }); if (me.role === "C" || me.role === "L") { for (j = 0; j < n; j += 1) { if (j === i || ((me.votes >> j) & 1) || !reachable(st, i, j)) continue; if (me.role === "L" && me.term === st.s[j].term && st.s[j].voted !== -1) continue; out.push({ k: "V", i: i, j: j }); } } if (me.role === "L") { if (!(maxLog && me.log.length >= maxLog)) out.push({ k: "W", i: i }); for (j = 0; j < n; j += 1) if (j !== i && reachable(st, i, j)) out.push({ k: "A", i: i, j: j }); } } return out; } /* ---- names for actions, so a history is a string ------------------------ */ function name(act) { if (act.k === "T" || act.k === "W") return act.k + (act.i + 1); if (act.k === "V" || act.k === "A") return act.k + (act.i + 1) + (act.j + 1); if (act.k === "P") { var side = ""; for (var z = 0; z < 9; z += 1) if ((act.mask >> z) & 1) side += String(z + 1); return "P" + side; } return act.k; } function parse(text) { var m = /^([TW])([1-9])$/.exec(text); if (m) return { k: m[1], i: Number(m[2]) - 1 }; m = /^([VA])([1-9])([1-9])$/.exec(text); if (m) return { k: m[1], i: Number(m[2]) - 1, j: Number(m[3]) - 1 }; m = /^P([1-9]{1,8})$/.exec(text); if (m) { var mask = 0; m[1].split("").forEach(function (d) { mask |= 1 << (Number(d) - 1); }); return { k: "P", mask: mask }; } if (text === "H") return { k: "H" }; return null; } /* Run a history from an empty cluster. Stops at the first refusal and says * where, rather than skipping it: a history that cannot be replayed is not * the history it claims to be. */ function replay(n, names, rule) { var st = fresh(n), trail = [], firstBroken = null; for (var z = 0; z < names.length; z += 1) { var act = parse(names[z]); if (!act) return { ok: false, at: z, why: "not an action: " + names[z], state: st, trail: trail }; var r = step(st, act, rule); if (!r.ok) return { ok: false, at: z, why: r.why, state: st, trail: trail }; trail.push({ act: names[z], events: r.events, broken: r.broken, removed: r.removed || [], before: st, state: r.state }); st = r.state; if (r.broken.length && firstBroken === null) firstBroken = z; } return { ok: true, state: st, trail: trail, firstBroken: firstBroken }; } /* ---- Figure 8 ----------------------------------------------------------- */ /* The paper's Figure 8 as a history of the four actions, from an empty * five-server cluster. In term 1, S2 puts the entry at index 1 on everyone * and commits it, which is where the figure starts; the figure does not say * who led term 1. A crash is drawn here as a server cut off * from the rest; the ledger says what that does and does not cover. * * The logs below are the five panels of the figure, read from the page at * 300 dots per inch. Index 0 is S1. Leader is the server drawn with the * heavy border. verify() replays the history and compares. */ var FIG8_START = ["T2", "V21", "V23", "W2", "A21", "A23", "A24", "A25", "A21", "A23"]; var FIG8 = [ { panel: "a", // S1 wins term 2 and writes index 2, which reaches S2 only. The figure // names no voters for (a); S2 and S3 are the fewest that will do. steps: ["T1", "V12", "V13", "W1", "A12"], logs: [[1, 2], [1, 2], [1], [1], [1]], leader: 0 }, { panel: "b", // "S1 crashes; S5 is elected leader for term 3 with votes from S3, S4, // and itself, and accepts a different entry at log index 2." // S3 voted for S1 in term 2, so S5's first try, in term 2, gets S4 // and not S3, and it has to stand again. steps: ["P1", "T5", "V53", "V54", "T5", "V53", "V54", "W5"], logs: [[1, 2], [1, 2], [1], [1], [1, 3]], leader: 4 }, { panel: "c", // "S5 crashes; S1 restarts, is elected leader, and continues // replication." S1 is still the leader of term 2 in its own mind, so // the first reply carrying term 3 is what takes that away from it. steps: ["P5", "A13", "T1", "V12", "V13", "A12", "A13", "W1"], logs: [[1, 2, 4], [1, 2], [1, 2], [1], [1, 3]], leader: 0 }, { panel: "d", from: "c", // "If S1 crashes as in (d), S5 could be elected leader (with votes // from S2, S3, and S4) and overwrite the entry with its own entry from // term 3." // S5 is in the same position S1 was in (c): leader of term 3 in its own // mind until a reply carrying term 4 reaches it. steps: ["P1", "A52", "T5", "V52", "V53", "V54", "A52", "A53", "A54", "H", "A51"], logs: [[1, 3], [1, 3], [1, 3], [1, 3], [1, 3]], leader: 4 }, { panel: "e", from: "c", // "if S1 replicates an entry from its current term on a majority of the // servers before crashing, as in (e), then this entry is committed". steps: ["A12", "A13"], logs: [[1, 2, 4], [1, 2, 4], [1, 2, 4], [1], [1, 3]], leader: 0 } ]; /* From (c): S1 copies its term-4 entry to S2 only, is cut off, and S5 wins * term 5 with S3 and S4 and sends to each. verify() uses it to tell the * clause apart from a test of the leader's newest entry. */ var NEWEST = ["A12", "P1", "A52", "T5", "V53", "V54", "A53", "A54", "A52"]; /* The history that reaches one panel. (d) and (e) both branch from (c). */ function figure8(panel) { var by = {}, out; FIG8.forEach(function (p) { by[p.panel] = p; }); var chain = [], p = by[panel]; if (!p) return null; while (p) { chain.unshift(p); p = p.from ? by[p.from] : (p.panel === "a" ? null : by[String.fromCharCode(p.panel.charCodeAt(0) - 1)]); } out = FIG8_START.slice(); chain.forEach(function (q) { out = out.concat(q.steps); }); return out; } /* The leader a reader would point at: of the servers that believe they * lead, the one with the newest term. A leader cut off from the rest keeps * believing it until a reply with a newer term reaches it, and the figure * draws the crashed one without its border. */ function leaderOf(st) { var best = -1; st.s.forEach(function (x, i) { if (x.role === "L" && (best < 0 || x.term > st.s[best].term)) best = i; }); return best; } /* ---- the checker -------------------------------------------------------- */ /* A state as a string, with the servers renamed by perm. Two states that * differ only in which server is called what are the same state, and * checking both would only check the same thing twice. * * The string is in two halves: what each server holds that names nobody * (term, role, log, commit), then what names somebody (the vote, the votes * a candidate holds, a leader's matchIndex, the ghost's record of who led). * The first half alone fixes most of the order, so only orders that sort it * have to be tried. */ function localPart(x) { return x.term + x.role + x.log.join(".") + ":" + x.commit; } function keyOf(st, perm, locals) { var inv = [], i, n = st.n, head = "", tail = ""; for (i = 0; i < n; i += 1) inv[perm[i]] = i; for (var p = 0; p < n; p += 1) { var x = st.s[inv[p]]; head += (locals ? locals[inv[p]] : localPart(x)) + "!"; tail += x.voted < 0 ? "-" : perm[x.voted]; if (x.role === "C") { var vm = 0; for (i = 0; i < n; i += 1) if ((x.votes >> i) & 1) vm |= 1 << perm[i]; tail += "v" + vm; } else if (x.role === "L") { tail += "m"; for (var q = 0; q < n; q += 1) tail += x.match[inv[q]] + ","; } tail += "|"; } tail += "e"; st.ghost.elected.forEach(function (w, t) { if (w !== undefined) tail += t + "=" + (w < 0 ? w : perm[w]) + ","; }); tail += "c"; st.ghost.committed.forEach(function (c, idx) { if (c) tail += idx + "=" + c.et + "/" + c.ct + ","; }); return head + "#" + tail; } /* The smallest key over every renaming that puts the servers' own halves in * sorted order. Any renaming outside that set has a larger first half, so * the minimum over the set is the minimum over all of them, and it does * not depend on how the state was named to begin with. */ function canonical(st) { var n = st.n, locals = st.s.map(localPart); var order = locals.map(function (_, z) { return z; }).sort(function (a, b) { return locals[a] < locals[b] ? -1 : locals[a] > locals[b] ? 1 : 0; }); // Runs of equal halves can be renamed among themselves freely. var groups = [], start = 0; for (var z = 1; z <= n; z += 1) { if (z === n || locals[order[z]] !== locals[order[start]]) { groups.push(order.slice(start, z)); start = z; } } var best = null, perm = []; (function go(g, pos) { if (g === groups.length) { var k = keyOf(st, perm, locals); if (best === null || k < best) best = k; return; } eachOrder(groups[g], function (arr) { for (var y = 0; y < arr.length; y += 1) perm[arr[y]] = pos + y; go(g + 1, pos + arr.length); }); })(0, 0); return best; } function eachOrder(list, fn) { if (list.length <= 1) { fn(list); return; } (function go(prefix, rest) { if (!rest.length) { fn(prefix); return; } for (var z = 0; z < rest.length; z += 1) { go(prefix.concat([rest[z]]), rest.slice(0, z).concat(rest.slice(z + 1))); } })([], list); } /* Identity naming only, for checking the reduction against no reduction. */ function plainKey(st) { return keyOf(st, st.s.map(function (_, z) { return z; })); } /* Breadth first over every state reachable within the bounds. Breadth first * because the first broken state it meets is then one of the shortest * histories that break anything, which is the one worth showing. * * Returns counts, and for each property how many states it was checked in * with something to check: Leader Completeness says nothing about a state * with no leader or nothing committed, and a property that was never put to * the test has not held. */ function check(opts) { var n = opts.n, rule = opts.rule || "raft"; var bounds = { maxTerm: opts.maxTerm, maxLog: opts.maxLog }; var keyFn = opts.symmetry === false ? plainKey : canonical; var start = fresh(n); var seen = new Map(); var startKey = keyFn(start); seen.set(startKey, null); var queue = [{ st: start, key: startKey, depth: 0 }]; var head = 0, edges = 0, maxDepth = 0; var tested = { election: 0, append: 0, matching: 0, completeness: 0, machine: 0 }; var failed = null, brokenStates = 0, limit = opts.limit || Infinity; var deletions = 0; // steps in which a follower deleted entries var writes = 0; // of the steps that changed a leader's log, client writes var kept = opts.collect ? [start] : null; while (head < queue.length) { var node = queue[head]; head += 1; var st = node.st; tally(st, tested); var acts = actions(st, bounds); for (var z = 0; z < acts.length; z += 1) { var r = step(st, acts[z], rule, true); if (!r.ok) continue; edges += 1; if (leaderWrote(st, r.state)) { tested.append += 1; if (acts[z].k === "W") writes += 1; } if (r.removed && r.removed.length) deletions += 1; var key = keyFn(r.state); var bad = appendOnly(st, r.state, []); if (seen.has(key) && !bad.length) continue; if (!seen.has(key)) { seen.set(key, { from: node.key, act: name(acts[z]) }); if (kept) kept.push(r.state); } bad = bad.concat(broken(r.state, null)); if (bad.length) { brokenStates += 1; if (!failed) failed = { key: key, broken: bad, depth: node.depth + 1 }; continue; // a broken state is a counterexample, not somewhere to go next } if (seen.size > limit) return { n: n, rule: rule, aborted: true, states: seen.size }; queue.push({ st: r.state, key: key, depth: node.depth + 1 }); if (node.depth + 1 > maxDepth) maxDepth = node.depth + 1; } } var trace = null; if (failed) { trace = []; var at = seen.get(failed.key); while (at) { trace.unshift(at.act); at = seen.get(at.from); } // The names in the trace are of the states as they were reached, not // of their canonical forms, so the trace replays as it stands. } return { n: n, rule: rule, maxTerm: opts.maxTerm, maxLog: opts.maxLog, states: seen.size, edges: edges, depth: maxDepth, tested: tested, brokenStates: brokenStates, failed: failed, trace: trace, deletions: deletions, writes: writes, kept: kept }; } /* Counts, per property, the states in which the property had something to * say. A leader with nothing committed before its term is a state Leader * Completeness cannot fail in. Log Matching can fail only where two logs * hold the same term at some index after the first, because only then is * there an earlier entry for them to disagree on; two logs of one entry * each are not a test of it. */ function tally(st, t) { var leaders = 0, i; t.election += st.ghost.elected.some(function (w) { return w !== undefined; }) ? 1 : 0; var pairs = 0; for (i = 0; i < st.n; i += 1) for (var j = i + 1; j < st.n; j += 1) { var A = st.s[i].log, B = st.s[j].log; for (var x = Math.min(A.length, B.length); x >= 2; x -= 1) { if (A[x - 1] === B[x - 1]) { pairs += 1; break; } } } t.matching += pairs ? 1 : 0; for (i = 0; i < st.n; i += 1) { var L = st.s[i]; if (L.role !== "L") continue; if (st.ghost.committed.some(function (c) { return c && c.ct < L.term; })) leaders += 1; } t.completeness += leaders ? 1 : 0; t.machine += st.s.some(function (x) { return x.commit > 0; }) ? 1 : 0; } /* The bounds the page checks at load. Three servers, terms up to four, one * entry per log. Four because the other commit rule fails there and not * below, which verify() measures rather than this comment asserting it. */ var LOAD = { n: 3, maxTerm: 4, maxLog: 1 }; /* A second box, for the two properties one entry per log cannot test. Log * Matching is about the entries before one two logs share, and a log of one * entry has none before it. Leader Append-Only is about a leader that holds * an entry and takes another, and with one entry per log a leader only ever * writes into an empty log. Two entries and two terms are enough for a wrong * send or a wrong write to show, and the test suite proves it by breaking * each on purpose. It costs about a tenth of the first box. */ var LOAD2 = { n: 3, maxTerm: 2, maxLog: 2 }; /* A ceiling on the search, because a bug can make the box unbounded: a * follower that never deletes a conflicting entry grows its log on every * send, and the search would run until the tab dies. The box has tens of * thousands of states; one that passes a quarter of a million has stopped * being the search this page describes, and verify() says it did not * finish rather than reporting on part of it. */ var CEILING = 250000; var cache = {}; function checked(rule, maxTerm, maxLog) { var t = maxTerm || LOAD.maxTerm, m = maxLog || LOAD.maxLog, key = rule + "/" + t + "/" + m; if (!(key in cache)) { var r = check({ n: LOAD.n, maxTerm: t, maxLog: m, rule: rule, limit: CEILING }); cache[key] = r.aborted ? null : r; } return cache[key]; } /* How many indexes the ghost has ever seen committed. */ function committedAt(st) { return st.ghost.committed.reduce(function (t, c) { return t + (c ? 1 : 0); }, 0); } /* ---- verify ------------------------------------------------------------- */ var ENTRIES = ["no entries", "one entry", "two entries", "three entries"]; function verify() { var out = []; var good, bad, wide; try { good = checked("raft"); } catch (e) { good = null; } try { bad = checked("majority"); } catch (e) { bad = null; } try { wide = checked("raft", LOAD2.maxTerm, LOAD2.maxLog); } catch (e) { wide = null; } // Log Matching and Leader Append-Only are read off the second box, the // other three off the first; see LOAD2 for why. PROPS.forEach(function (p) { var two = p.id === "matching" || p.id === "append", box = two ? wide : good; if (!box) { out.push({ claim: p.name + " was checked in every state three servers can reach", ok: false, detail: "the search did not finish inside " + CEILING.toLocaleString("en-US") + " states" }); return; } var seen = box.tested[p.id] || 0; var held = !box.failed || !box.failed.broken.some(function (b) { return b.prop === p.id; }); var detail; if (seen === 0) detail = "no state put it to the test"; else if (p.id === "append") { detail = seen.toLocaleString("en-US") + " steps changed a leader's own log and each was checked" + (box.writes === seen ? "; every one was a client write, which appends, and no other step " + "touched a leader's log" : "; " + box.writes.toLocaleString("en-US") + " of them were client writes"); } else if (p.id === "matching") { detail = seen.toLocaleString("en-US") + " of those states had two logs agreeing at index 2 or later, " + "the only place it can fail" + (good ? "; the first box, with one entry per log, has " + good.tested.matching.toLocaleString("en-US") + " such states" : ""); } else detail = seen.toLocaleString("en-US") + " of those states had something for it to check"; out.push({ claim: p.name + " holds in every state three servers can reach, terms up to " + box.maxTerm + " and " + ENTRIES[box.maxLog] + " per log: " + box.states.toLocaleString("en-US") + " states, counting a renaming of the servers as the same state", ok: seen > 0 && held && !box.failed, untested: seen === 0, detail: detail }); }); if (!bad) { out.push({ claim: "counting replicas of any entry breaks the cluster", ok: false, detail: "the checker did not finish" }); } else { var props = bad.failed ? bad.failed.broken.map(function (b) { return b.prop; }) : []; out.push({ claim: "with the term check removed from the commit rule, the same search finds a " + "history that breaks it, " + (bad.trace ? bad.trace.length : 0) + " steps long", ok: !!bad.failed && !!bad.trace && bad.trace.length > 0, detail: bad.failed ? PROPS.filter(function (p) { return props.indexOf(p.id) >= 0; }) .map(function (p) { return p.name; }).join(" and ") + " fail: " + bad.failed.broken[0].text : "nothing failed, so the term check would be doing no work" }); // And that history really is one: replayed through step() from empty. var again = bad.trace ? replay(LOAD.n, bad.trace, "majority") : null; var underRaft = bad.trace ? replay(LOAD.n, bad.trace, "raft") : null; out.push({ claim: "replayed with Raft's rule, the same history breaks nothing", ok: !!again && again.ok && again.firstBroken === bad.trace.length - 1 && !!underRaft && underRaft.ok && underRaft.firstBroken === null, untested: !bad.trace, detail: !bad.trace ? "there was no history to replay" : underRaft && underRaft.ok ? committedAt(underRaft.state) === 0 ? "nothing was committed: the one entry on a majority came from an earlier term than its leader" : committedAt(underRaft.state) + " entries were committed, and every later leader holds them" : "it did not replay: " + (underRaft ? underRaft.why : "") }); } // And why four terms: one fewer and the other rule has nothing to break. var lower; try { lower = checked("majority", LOAD.maxTerm - 1); } catch (e) { lower = null; } out.push({ claim: "with terms only up to " + (LOAD.maxTerm - 1) + ", the other rule breaks nothing in " + (lower ? lower.states.toLocaleString("en-US") : "any") + " states, so its failure " + "needs a fourth term", ok: !!lower && !lower.failed && lower.states > 0 && !!bad && !!bad.failed, untested: !lower || lower.states === 0, detail: lower && lower.failed ? "it fails there too: " + lower.failed.broken[0].text : bad && bad.trace ? "the shortest failure ends in term " + replay(LOAD.n, bad.trace, "majority") .state.s.reduce(function (m, x) { return Math.max(m, x.term); }, 0) : "there is no failure to compare it with" }); // Figure 8, all five panels, under Raft's rule. var panelsRight = 0, panelsSeen = 0, why = ""; FIG8.forEach(function (p) { var h = figure8(p.panel), r = replay(5, h, "raft"); panelsSeen += 1; if (!r.ok) { why = why || "(" + p.panel + ") did not replay: " + r.why; return; } var logs = r.state.s.map(function (x) { return x.log; }); var leader = leaderOf(r.state); var same = JSON.stringify(logs) === JSON.stringify(p.logs) && leader === p.leader && r.firstBroken === null; if (same) panelsRight += 1; else why = why || "(" + p.panel + ") came out as " + JSON.stringify(logs); }); out.push({ claim: "the five panels of the paper's Figure 8 are reached exactly, by the same " + "four actions the buttons press", ok: panelsSeen === 5 && panelsRight === 5, detail: why || "every log and every leader as printed, and nothing broken on the way" }); // And (d) under the other rule is the failure the figure warns about. var dBad = replay(5, figure8("d"), "majority"); var dProps = []; if (dBad.ok) dBad.trail.forEach(function (t) { t.broken.forEach(function (b) { if (dProps.indexOf(b.prop) < 0) dProps.push(b.prop); }); }); out.push({ claim: "counting replicas of any entry, the same history breaks Leader Completeness " + "and State Machine Safety on the way to (d)", ok: dBad.ok && dProps.indexOf("completeness") >= 0 && dProps.indexOf("machine") >= 0, detail: dBad.ok && dBad.firstBroken !== null ? "first at step " + (dBad.firstBroken + 1) + " of " + dBad.trail.length + ": " + dBad.trail[dBad.firstBroken].broken[0].text : "nothing broke" }); // (c) has the old entry on a majority and not committed; (e) commits it. var c = replay(5, figure8("c"), "raft"), e = replay(5, figure8("e"), "raft"); var onC = c.ok ? c.state.s.filter(function (x) { return x.log[1] === 2; }).length : 0; out.push({ claim: "in (c) the term-2 entry is on " + onC + " of 5 servers and the leader has not " + "committed it; in (e) it is committed by the entry from term 4 after it", ok: c.ok && e.ok && onC >= majority(5) && c.state.s[0].commit < 2 && e.state.s[0].commit === 3, detail: c.ok && e.ok ? "S1's commit index is " + c.state.s[0].commit + " in (c) and " + e.state.s[0].commit + " in (e)" : "a panel did not replay" }); // The clause names log[N], the entry being counted, and not the leader's // newest entry. Three servers cannot tell those apart: any send after a // write puts the newest entry on a majority of three. Five can. From (c), // S1's term-4 entry at index 3 reaches S2 only, so it is on 2 of 5, while // index 2 from term 2 is on 3. Testing the newest entry's term would // commit index 2 here, and S5 then deletes it. var cN = figure8("c").length, lastN = replay(5, figure8("c").concat(NEWEST), "raft"); var lostN = 0; if (lastN.ok) lastN.trail.forEach(function (t) { t.removed.forEach(function (x) { if (x.index === 2 && x.term === 2) lostN += 1; }); }); var atN = lastN.ok ? lastN.trail[cN].state : null, s1At = atN ? atN.s[0] : null; var on = function (idx, term) { return atN ? atN.s.filter(function (x) { return x.log[idx - 1] === term; }).length : 0; }; out.push({ claim: "the clause tests the term of the entry being counted, not of the leader's newest: " + "from (c), with index 3 from term 4 on " + on(3, 4) + " of 5 servers and index 2 from term 2 on " + on(2, 2) + ", S1 commits neither, and S5 can then delete index 2 with nothing broken", ok: lastN.ok && lastN.firstBroken === null && !!s1At && s1At.log.length === 3 && on(3, 4) < majority(5) && on(2, 2) >= majority(5) && s1At.commit < 2 && leaderOf(lastN.state) === 4 && lostN > 0, detail: lastN.ok ? "S1's commit index stays at " + (s1At ? s1At.commit : "?") + "; " + lostN + " servers delete index 2" + (lastN.firstBroken === null ? ", and nothing breaks" : ", and " + lastN.trail[lastN.firstBroken].broken[0].text) : "it did not replay: " + lastN.why }); // (e): S5 cannot win. Cut S1 off, let S5 hear term 4, stand, and ask // everyone it can reach. var tryS5 = replay(5, figure8("e").concat(["P1", "A52", "T5", "V52", "V53", "V54"]), "raft"); if (tryS5.ok) { var asked = tryS5.trail.slice(-3), got = []; asked.forEach(function (t, z) { if (t.events.some(function (w) { return /votes for S5/.test(w); })) got.push("S" + (z + 2)); }); out.push({ claim: "and from (e), S5 cannot win: it gets " + (got.length + 1) + " votes of the " + majority(5) + " it needs", ok: tryS5.state.s[4].role !== "L" && got.length + 1 < majority(5), detail: "only " + (got.length ? got.join(", ") + " and itself" : "itself") + "; S2 and S3 hold an entry from term 4 and S5's log ends in term 3" }); } else { out.push({ claim: "and from (e), S5 cannot win", ok: false, untested: true, detail: "it did not replay: " + tryS5.why }); } return out; } window.Consensus = { RULES: RULES, PROPS: PROPS, FIG8: FIG8, LOAD: LOAD, LOAD2: LOAD2, NEWEST: NEWEST, fresh: fresh, copy: copy, majority: majority, atLeastAsUpToDate: atLeastAsUpToDate, reachable: reachable, voteAnswer: voteAnswer, step: step, actions: actions, broken: broken, name: name, parse: parse, replay: replay, leaderOf: leaderOf, figure8: figure8, check: check, checked: checked, keyOf: keyOf, canonical: canonical, committedAt: committedAt, verify: verify }; })();