/* The Futex: three mutexes, every interleaving, and the system calls each one * makes. * * Ulrich Drepper's "Futexes Are Tricky" builds a mutex on the futex system * call three times. The first is wrong in a way that took, by his account, * many months to find in a real thread library. The second fixes it and pays * for the fix in atomic operations. The third gets some of that back on * processors with an exchange instruction. He prints a table of what each one * costs, in atomic operations and in system calls, uncontended and contended. * * This is those three programs, transcribed line for line, run by a model * checker. A state is the futex word, each thread's place in its program, the * one value each thread is holding in a register, and whether the kernel has * it asleep. Every step one thread can take from every state is taken, so a * number here is a count over every schedule the model allows, not a sample * of one. What the model allows is said in the honesty ledger: memory is * sequentially consistent, each atomic instruction and each system call is one * indivisible step, and a sleeping thread wakes only when another thread's * futex_wake picks it. * * Nothing here is timed. A system call is counted, not measured. */ (function () { "use strict"; /* The kernel's side, which is the whole of what a futex is. * * wait(expected) if the word still holds `expected`, go to sleep on it; * otherwise return at once with EWOULDBLOCK. The check * and the sleep are one step: nothing can change the * word between them. That one fact is why a futex works. * wake(1) wake one sleeper, if there is any. Which one is not * promised, so every choice is a separate branch. * * The user's side is the program: four kinds of instruction, each one * indivisible. * * rmw an atomic read-modify-write: atomic_inc, atomic_dec, cmpxchg or * xchg. Returns the old value, which the thread keeps in `c`. * store a plain store of nought, which Drepper does not count as atomic. * wait futex_wait, a system call. * wake futex_wake, a system call. * * `to` picks the next step from the value the instruction returned, which is * how the C's ifs and loops are folded into the steps themselves: a branch * on a register is not a separate moment anyone else can observe. */ var CS = "cs", REM = "rem"; function inc(v, c, w) { return { v: (v + 1) % w, old: v }; } function dec(v) { return { v: v - 1, old: v }; } function cmpxchg(o, n) { return function (v) { return { v: v === o ? n : v, old: v }; }; } function xchg(n) { return function (v) { return { v: n, old: v }; }; } /* Every program ends its lock() in CS and its unlock() in REM, and loops. */ var PROGRAMS = { mutex: { name: "the first mutex", section: "4", listing: "void lock () {\n int c;\n while ((c = atomic_inc (val)) != 0)\n futex_wait (&val, c + 1); }\nvoid unlock () {\n val = 0; futex_wake (&val, 1); }", lock: 0, unlock: 2, steps: [ { k: "rmw", f: inc, op: "atomic_inc", keep: true, to: function (old) { return old === 0 ? CS : 1; } }, { k: "wait", expect: function (c, w) { return (c + 1) % w; }, then: 0 }, { k: "store", then: 3 }, { k: "wake", then: REM } ] }, mutex2: { name: "the second mutex", section: "5", listing: "void lock () {\n int c;\n if ((c = cmpxchg (val, 0, 1)) != 0)\n do {\n if (c == 2\n || cmpxchg (val, 1, 2) != 0)\n futex_wait (&val, 2);\n } while ((c = cmpxchg (val, 0, 2))\n != 0);\n}\nvoid unlock () {\n if (atomic_dec (val) != 1) {\n val = 0;\n futex_wake (&val, 1);\n }\n}", lock: 0, unlock: 4, steps: [ { k: "rmw", f: cmpxchg(0, 1), op: "cmpxchg (val, 0, 1)", to: function (old) { return old === 0 ? CS : old === 2 ? 2 : 1; } }, // The short circuit's other branch. The C tests its result and drops it. { k: "rmw", f: cmpxchg(1, 2), op: "cmpxchg (val, 1, 2)", to: function (old) { return old !== 0 ? 2 : 3; } }, { k: "wait", expect: function () { return 2; }, then: 3 }, { k: "rmw", f: cmpxchg(0, 2), op: "cmpxchg (val, 0, 2)", to: function (old) { return old === 0 ? CS : old === 2 ? 2 : 1; } }, { k: "rmw", f: dec, op: "atomic_dec", unlock: true, to: function (old) { return old !== 1 ? 5 : REM; } }, { k: "store", then: 6 }, { k: "wake", then: REM } ] }, mutex3: { name: "the third mutex", section: "6", listing: "void lock () {\n int c;\n if ((c = cmpxchg (val, 0, 1)) != 0) {\n if (c != 2)\n c = xchg (val, 2);\n while (c != 0) {\n futex_wait (&val, 2);\n c = xchg (val, 2);\n }\n }\n}\nvoid unlock () {\n if (atomic_dec (val) != 1) {\n val = 0;\n futex_wake (&val, 1);\n }\n}", lock: 0, unlock: 4, steps: [ { k: "rmw", f: cmpxchg(0, 1), op: "cmpxchg (val, 0, 1)", to: function (old) { return old === 0 ? CS : old !== 2 ? 1 : 2; } }, { k: "rmw", f: xchg(2), op: "xchg (val, 2)", to: function (old) { return old === 0 ? CS : 2; } }, { k: "wait", expect: function () { return 2; }, then: 3 }, { k: "rmw", f: xchg(2), op: "xchg (val, 2)", to: function (old) { return old === 0 ? CS : 2; } }, { k: "rmw", f: dec, op: "atomic_dec", unlock: true, to: function (old) { return old !== 1 ? 5 : REM; } }, { k: "store", then: 6 }, { k: "wake", then: REM } ] } }; /* The change Drepper warns against in section 5: retake the lock with 1, * "locked, no waiters", instead of 2. He says being wrong in that guess * "sooner or later means running into a deadlock". This is the second * mutex with that one constant changed, and nothing else. */ PROGRAMS.mutex2one = (function () { var base = PROGRAMS.mutex2, steps = base.steps.slice(); steps[3] = { k: "rmw", f: cmpxchg(0, 1), op: "cmpxchg (val, 0, 1)", to: steps[3].to }; return { name: "the second mutex, retaking with 1", section: "5", listing: base.listing.replace("cmpxchg (val, 0, 2))", "cmpxchg (val, 0, 1))"), lock: 0, unlock: base.unlock, steps: steps }; })(); var ORDER = ["mutex", "mutex2", "mutex3"]; /* The counter's modulus when nobody asks for another: a four-bit word. * Only the first mutex counts upwards, and a counter as wide as the real * one is far too wide to enumerate here, so its width is a control and a stated limit. * The other two never leave 0, 1 and 2 at any width, which verify() checks * rather than assumes. */ var WIDE = 16; function keyOf(s) { var out = String(s.val); for (var i = 0; i < s.pc.length; i += 1) { out += "|" + s.pc[i] + "," + s.c[i] + (s.sleep[i] ? "z" : ""); } return out; } function copy(s) { return { val: s.val, pc: s.pc.slice(), c: s.c.slice(), sleep: s.sleep.slice() }; } function startState(prog, n) { var s = { val: 0, pc: [], c: [], sleep: [] }; for (var i = 0; i < n; i += 1) { s.pc.push(prog.lock); s.c.push(0); s.sleep.push(false); } return s; } /* Every successor of one state, each labelled with who moved and what kind * of thing happened. `opts.freeze` holds one thread still; `opts.width` is * the counter's modulus; `opts.noWrap` refuses the increment that would * wrap it, which is how "before the counter has wrapped" is asked. */ function successors(prog, s, opts) { var out = [], w = opts.width || WIDE; for (var i = 0; i < s.pc.length; i += 1) { if (s.sleep[i] || i === opts.freeze) continue; var pc = s.pc[i], n; if (pc === CS) { n = copy(s); n.pc[i] = prog.unlock; out.push({ to: n, by: i, kind: "leave" }); continue; } if (pc === REM) { n = copy(s); n.pc[i] = prog.lock; out.push({ to: n, by: i, kind: "again" }); continue; } var st = prog.steps[pc]; if (st.k === "rmw") { if (opts.noWrap && st.f === inc && s.val === w - 1) continue; var r = st.f(s.val, s.c[i], w); n = copy(s); n.val = r.v; n.pc[i] = st.to(r.old); // A register is part of the state only while something will read it. // In the first mutex, c is read by the futex_wait after the increment; // in the other two every branch on c is folded into `to`, so c is never // live across a step, and keeping its dead value would count one state // several times. n.c[i] = st.keep ? r.old : 0; out.push({ to: n, by: i, kind: "atomic", old: r.old, unlock: !!st.unlock }); } else if (st.k === "store") { n = copy(s); n.val = 0; n.pc[i] = st.then; out.push({ to: n, by: i, kind: "store" }); } else if (st.k === "wait") { var want = st.expect(s.c[i], w); n = copy(s); if (s.val === want) { n.sleep[i] = true; n.pc[i] = st.then; n.c[i] = 0; out.push({ to: n, by: i, kind: "sleep" }); } else { n.pc[i] = st.then; n.c[i] = 0; out.push({ to: n, by: i, kind: "ewouldblock" }); } } else { // wake(1): one branch per sleeper, or a call that wakes nobody. var any = false; for (var j = 0; j < s.pc.length; j += 1) { if (!s.sleep[j]) continue; any = true; n = copy(s); n.pc[i] = st.then; n.sleep[j] = false; out.push({ to: n, by: i, kind: "wake", woke: j }); } if (!any) { n = copy(s); n.pc[i] = st.then; out.push({ to: n, by: i, kind: "wake-nobody" }); } } } return out; } /* The whole reachable graph. Breadth first, so the parent links it keeps * give a shortest schedule to any state, which is what the page prints. */ function explore(id, n, opts) { opts = opts || {}; var prog = PROGRAMS[id]; var start = opts.start || startState(prog, n); var k0 = keyOf(start); var seen = {}, edges = {}, parent = {}, order = [k0], head = 0; seen[k0] = start; parent[k0] = null; while (head < order.length) { var k = order[head++], s = seen[k]; var succ = successors(prog, s, opts), list = []; for (var e = 0; e < succ.length; e += 1) { var t = succ[e], tk = keyOf(t.to); list.push({ to: tk, by: t.by, kind: t.kind }); if (seen[tk] === undefined) { seen[tk] = t.to; parent[tk] = { from: k, by: t.by, kind: t.kind }; order.push(tk); } } edges[k] = list; } return { id: id, prog: prog, start: k0, keys: order, seen: seen, edges: edges, parent: parent, width: opts.width || WIDE }; } function inside(s) { var m = 0; for (var i = 0; i < s.pc.length; i += 1) if (s.pc[i] === CS) m += 1; return m; } /* Drepper's second requirement for a mutex, negated: somebody is asleep in * the kernel, and every other thread has left the lock alone -- nobody holds * it, nobody is releasing it, nobody is on the way in. From such a state * nothing that is already running will ever wake the sleeper. */ function forgotten(g) { var bad = []; g.keys.forEach(function (k) { var s = g.seen[k], asleep = 0, idle = true; for (var i = 0; i < s.pc.length; i += 1) { if (s.sleep[i]) asleep += 1; else if (s.pc[i] !== REM) idle = false; } if (asleep > 0 && idle) bad.push(k); }); return bad; } /* A schedule, read back along the breadth-first parent links, with each * step said in the paper's own vocabulary. The words are worked out from * the two states either side of the step rather than stored on every edge: * an atomic returned whatever the word held before it, and a wake woke * whichever thread stopped sleeping. */ function describe(g, from, by, kind, to) { var pc = from.pc[by]; if (kind === "leave") return "leaves the critical section and calls unlock ()"; if (kind === "again") return "calls lock () again"; var st = g.prog.steps[pc]; if (kind === "atomic") return st.op + " returns " + from.val; if (kind === "store") return "val = 0"; if (kind === "sleep" || kind === "ewouldblock") { var want = st.expect(from.c[by], g.width); return "futex_wait (&val, " + want + ") " + (kind === "sleep" ? "goes to sleep" : "returns EWOULDBLOCK"); } if (kind === "wake") { for (var j = 0; j < to.sleep.length; j += 1) { if (from.sleep[j] && !to.sleep[j]) return "futex_wake wakes thread " + (j + 1); } } return "futex_wake wakes nobody"; } function schedule(g, key) { var out = []; while (key && g.parent[key]) { var p = g.parent[key], to = g.seen[key], from = g.seen[p.from]; out.push({ thread: p.by + 1, kind: p.kind, val: to.val, what: describe(g, from, p.by, p.kind, to) }); key = p.from; } return out.reverse(); } /* One mutex at N threads: the census the page's tables are made of. */ function census(id, n, opts) { opts = opts || {}; var g = explore(id, n, opts); var two = g.keys.filter(function (k) { return inside(g.seen[k]) > 1; }); var lost = forgotten(g); var values = {}; g.keys.forEach(function (k) { values[g.seen[k].val] = true; }); var vals = Object.keys(values).map(Number).sort(function (a, b) { return a - b; }); // A wake with two sleepers is two edges from one place, so the places an // unlock calls futex_wake -- a state and the thread making the call -- are // counted on their own, and they are what the page prints. var wakesNobody = 0, wakes = 0, fails = 0, places = 0; g.keys.forEach(function (k) { var callers = {}; g.edges[k].forEach(function (e) { if (e.kind === "wake-nobody") wakesNobody += 1; if (e.kind === "wake") wakes += 1; if (e.kind === "ewouldblock") fails += 1; if (e.kind === "wake" || e.kind === "wake-nobody") callers[e.by] = true; }); places += Object.keys(callers).length; }); return { id: id, n: n, states: g.keys.length, twoInside: two.length, firstTwo: two[0] || null, forgotten: lost.length, firstForgotten: lost[0] || null, values: vals, wakeNobodyEdges: wakesNobody, wakeEdges: wakes, wakePlaces: places, failedWaitEdges: fails, graph: g }; } /* Strongly connected components, iteratively. */ function components(nodes, out) { var index = {}, low = {}, on = {}, stack = [], counter = 0, comps = []; nodes.forEach(function (root) { if (index[root] !== undefined) return; var work = [{ v: root, i: 0 }]; index[root] = low[root] = counter++; stack.push(root); on[root] = true; while (work.length) { var frame = work[work.length - 1], succ = out(frame.v); if (frame.i < succ.length) { var w = succ[frame.i]; frame.i += 1; if (index[w] === undefined) { index[w] = low[w] = counter++; stack.push(w); on[w] = true; work.push({ v: w, i: 0 }); } else if (on[w]) { low[frame.v] = Math.min(low[frame.v], index[w]); } continue; } work.pop(); if (work.length) { var u = work[work.length - 1].v; low[u] = Math.min(low[u], low[frame.v]); } if (low[frame.v] === index[frame.v]) { var comp = [], x; do { x = stack.pop(); on[x] = false; comp.push(x); } while (x !== frame.v); comps.push(comp); } } }); return comps; } /* The first mutex's bug, as a number. * * Thread 1 takes the lock and is held still inside it. Nobody can release * it. The others try to take it, and each futex_wait that comes straight * back with EWOULDBLOCK is a system call that achieved nothing: the waste * Drepper describes as continuing "ad infinitum". This asks for the longest * run of those the model allows while the lock stays held by one thread. * `null` means a cycle contains one, so there is no longest. */ function failedRun(id, n, width) { var prog = PROGRAMS[id]; var start = startState(prog, n); start.pc[0] = CS; start.val = 1; var g = explore(id, n, { width: width, freeze: 0, start: start }); var region = {}; g.keys.forEach(function (k) { if (inside(g.seen[k]) === 1) region[k] = true; }); var inner = function (k) { return g.edges[k].filter(function (e) { return region[e.to]; }) .map(function (e) { return e.to; }); }; var keys = g.keys.filter(function (k) { return region[k]; }); var comps = components(keys, inner), cid = {}; comps.forEach(function (c, i) { c.forEach(function (k) { cid[k] = i; }); }); var cyclic = comps.some(function (c, i) { return c.some(function (k) { return g.edges[k].some(function (e) { return e.kind === "ewouldblock" && region[e.to] && cid[e.to] === i; }); }); }); var best = []; // Tarjan finishes a component only after every component it reaches, so // walking them in the order found is walking sinks first. comps.forEach(function (c, i) { var b = 0; c.forEach(function (k) { g.edges[k].forEach(function (e) { if (!region[e.to] || cid[e.to] === i) return; var v = best[cid[e.to]] + (e.kind === "ewouldblock" ? 1 : 0); if (v > b) b = v; }); }); best[i] = b; }); var escaped = g.keys.filter(function (k) { return !region[k]; }); return { id: id, n: n, width: width, states: g.keys.length, longest: cyclic ? null : best[cid[g.start]], twoInside: escaped.length, firstTwo: escaped[0] || null, graph: g }; } /* What one lock() and one unlock() cost, over every schedule. * * Thread 1 is followed through every call it makes. For a lock() the record * is what its first atomic operation found -- free, taken, or taken with * waiters -- and the atomic operations it made in each stretch between two * futex_wait calls. That is enough to count the cost either way the paper * might mean it, which turns out to matter. A call that waits more than * `cap.waits` times, or spins more than `cap.spin` atomics between two * waits, stops being followed, and the number of calls that stopped is * returned rather than hidden. */ function costs(id, n, opts) { opts = opts || {}; var cap = { waits: opts.waits || 3, spin: opts.spin || 4 }; // Costs are counted for the programs as designed, so the first mutex's // counter is not allowed to wrap here. What wrapping does is stage 2. opts = { width: opts.width, noWrap: true }; var prog = PROGRAMS[id]; var start = startState(prog, n); var NONE = "-"; var startKey = keyOf(start) + "#L" + NONE; var seen = {}, queue = [{ s: start, a: { mode: "L", found: null, segs: [0], sys: 0, gone: false } }]; seen[startKey] = true; var locks = {}, unlocks = {}, dropped = 0; function accKey(a) { return a.mode + (a.gone ? "x" : (a.found === null ? "?" : a.found) + ":" + a.segs.join(".") + ":" + a.sys); } function fresh(mode) { return { mode: mode, found: null, segs: [0], sys: 0, gone: false }; } var head = 0; while (head < queue.length) { var item = queue[head++], s = item.s, a = item.a; var succ = successors(prog, s, opts); for (var e = 0; e < succ.length; e += 1) { var t = succ[e], na = a; if (t.by === 0) { na = { mode: a.mode, found: a.found, segs: a.segs.slice(), sys: a.sys, gone: a.gone }; if (t.kind === "again") na = fresh("L"); else if (t.kind === "leave") na = fresh("U"); else if (!na.gone) { if (t.kind === "atomic") { if (na.mode === "L" && na.found === null) na.found = Math.min(t.old, 2); if (na.mode === "U" && na.found === null) na.found = t.old; na.segs[na.segs.length - 1] += 1; if (na.segs[na.segs.length - 1] > cap.spin) na.gone = true; } else if (t.kind === "sleep" || t.kind === "ewouldblock") { na.sys += 1; na.segs.push(0); if (na.segs.length - 1 > cap.waits) na.gone = true; } else if (t.kind === "wake" || t.kind === "wake-nobody") { na.sys += 1; na.woke = t.kind === "wake"; } } var nowPc = t.to.pc[0]; if (na.mode === "L" && nowPc === CS) { if (na.gone) dropped += 1; else locks[na.found + ":" + na.segs.join(".") + ":" + na.sys] = true; } if (na.mode === "U" && nowPc === REM) { var found = na.found === null ? NONE : na.found; unlocks[found + ":" + na.segs[0] + ":" + na.sys + ":" + (na.sys ? (na.woke ? "woke" : "nobody") : "none")] = true; } } var key = keyOf(t.to) + "#" + accKey(na); if (!seen[key]) { seen[key] = true; queue.push({ s: t.to, a: na }); } } } var lockList = Object.keys(locks).map(function (k) { var p = k.split(":"), segs = p[1].split(".").map(Number); var total = 0; segs.forEach(function (x) { total += x; }); return { found: Number(p[0]), segs: segs, atomics: total, waits: segs.length - 1, syscalls: Number(p[2]) }; }); var unlockList = Object.keys(unlocks).map(function (k) { var p = k.split(":"); return { found: p[0] === NONE ? null : Number(p[0]), atomics: Number(p[1]), syscalls: Number(p[2]), woke: p[3] }; }); return { id: id, n: n, locks: lockList, unlocks: unlockList, explored: queue.length, dropped: dropped, cap: cap }; } /* Drepper's tables, transcribed. The only typed numbers on the page, and * the test reads them back out of the archived paper rather than trusting * this copy. A stacked cell -- his "upper number" when there are already * waiters, "otherwise the lower number" -- is written {upper, lower}. */ var PRINTED = { uncontended: { mutex: { lock: { atomic: 1, syscall: 0 }, unlock: { atomic: 0, syscall: 1 } }, mutex2: { lock: { atomic: 1, syscall: 0 }, unlock: { atomic: 1, syscall: 0 } } }, contended: { mutex: { lock: { atomic: [1, 1], syscall: [1, 1] }, unlock: { atomic: 0, syscall: 1 } }, mutex2: { lock: { atomic: [{ upper: 2, lower: 3 }, { upper: 1, lower: 2 }], syscall: [1, 1] }, unlock: { atomic: 1, syscall: 1 } }, mutex3: { lock: { atomic: [{ upper: 1, lower: 2 }, 1], syscall: [1, 1] }, unlock: { atomic: 1, syscall: 1 } } } }; /* The uncontended row: one thread, nothing to wait for, so one schedule. */ function uncontended(id) { var c = costs(id, 1); var lock = c.locks[0] || null, unlock = c.unlocks[0] || null; return { lock: lock ? { atomic: lock.atomics, syscall: lock.syscalls } : null, unlock: unlock ? { atomic: unlock.atomics, syscall: unlock.syscalls } : null, calls: c.locks.length + c.unlocks.length }; } function minOf(list, f) { return list.reduce(function (m, x) { var v = f(x); return m === null || v < m ? v : m; }, null); } function setOf(list, f) { var s = {}; list.forEach(function (x) { s[f(x)] = true; }); return Object.keys(s).map(Number).sort(function (a, b) { return a - b; }); } /* The contended row, counted two ways, for one value of what the first * atomic found (1 taken, 2 taken with waiters). * * before the atomics a lock() makes before its first futex_wait * whole the atomics in a lock() that waits exactly once, start to finish, * including the one that finally takes the lock * extra what one more trip through the loop adds: the atomics between * one futex_wait and the next, when no thread spins between them * * Drepper's note under the table defines the +N as the extra cost "if the * futex_wait system call returns but the thread cannot get the mutex and is * going back to sleep", which is `extra`. He does not define the number * before the plus on its own, but "for the function call" makes the call * the unit, which points to `whole`. Only the second mutex's column fits * `whole`; the other two fit `before`. Which of those he meant -- two * columns one short, or two counts -- the arithmetic cannot say. */ function contended(id, found, census) { var c = census || costs(id, 3); var mine = c.locks.filter(function (x) { return x.found === found && x.waits >= 1; }); var once = mine.filter(function (x) { return x.waits === 1; }); var twice = mine.filter(function (x) { return x.waits === 2; }); var unl = c.unlocks.filter(function (x) { return x.syscalls > 0; }); return { id: id, found: found, before: minOf(mine, function (x) { return x.segs[0]; }), whole: minOf(once, function (x) { return x.atomics; }), extra: setOf(twice, function (x) { return x.segs[1]; }), extraMin: minOf(twice, function (x) { return x.segs[1]; }), syscallsOnce: minOf(once, function (x) { return x.syscalls; }), syscallsExtra: minOf(twice, function (x) { return x.syscalls; }) - minOf(once, function (x) { return x.syscalls; }), noWaitTaken: c.locks.filter(function (x) { return x.found === found && x.waits === 0; }).length, unlock: unl.length ? { atomic: minOf(unl, function (x) { return x.atomics; }), syscall: minOf(unl, function (x) { return x.syscalls; }) } : null, calls: mine.length }; } /* The printed cell for one mutex and one case, as a number. */ function printedFirst(id, found) { var cell = PRINTED.contended[id].lock.atomic[0]; return typeof cell === "number" ? cell : (found === 2 ? cell.upper : cell.lower); } function printedExtra(id, found) { var cell = PRINTED.contended[id].lock.atomic[1]; return typeof cell === "number" ? cell : (found === 2 ? cell.upper : cell.lower); } /* Which counting each printed cell agrees with. The first mutex has no * "waiters already" case of its own -- any non-zero value means taken -- so * it is read in the taken case. */ function readings(cache) { var out = []; ORDER.forEach(function (id) { var cases = id === "mutex" ? [1] : [2, 1]; cases.forEach(function (found) { var m = contended(id, found, cache && cache[id]); var p = printedFirst(id, found); out.push({ id: id, found: found, printed: p, before: m.before, whole: m.whole, extra: m.extra, printedExtra: printedExtra(id, found), matches: (p === m.before ? ["before"] : []).concat(p === m.whole ? ["whole"] : []) }); }); }); return out; } /* 2 to the W, minus 2: what the failed run should be for a W-bit counter, * by arithmetic rather than by search. The test and verify() both hold the * search against it; neither the engine's count nor this formula is * trusted on its own. */ function runFormula(width) { return Math.pow(2, width) - 2; } function verify() { var out = []; var cache = {}; // 1. The uncontended table, all eight printed cells. var unc = {}, ubad = []; ORDER.forEach(function (id) { unc[id] = uncontended(id); }); ["mutex", "mutex2"].forEach(function (id) { ["lock", "unlock"].forEach(function (op) { ["atomic", "syscall"].forEach(function (what) { var got = unc[id][op] ? unc[id][op][what] : null; if (got !== PRINTED.uncontended[id][op][what]) ubad.push(id + " " + op + " " + what); }); }); }); out.push({ claim: "uncontended, every cell of the paper's first table comes out of the model: " + "the first mutex's unlock makes " + (unc.mutex.unlock ? unc.mutex.unlock.syscall : "?") + " system call and the second's makes " + (unc.mutex2.unlock ? unc.mutex2.unlock.syscall : "?"), ok: ubad.length === 0 && unc.mutex.unlock !== null, detail: ubad.length ? ubad.join(", ") + " disagreed" : "eight cells of eight" }); // 2. The third mutex's uncontended path is the second's, as the paper says. out.push({ claim: "the third mutex's uncontended lock and unlock cost exactly what the second's do", ok: unc.mutex3.lock !== null && unc.mutex2.lock !== null && unc.mutex3.lock.atomic === unc.mutex2.lock.atomic && unc.mutex3.lock.syscall === unc.mutex2.lock.syscall && unc.mutex3.unlock.atomic === unc.mutex2.unlock.atomic && unc.mutex3.unlock.syscall === unc.mutex2.unlock.syscall, detail: unc.mutex3.lock ? "lock " + unc.mutex3.lock.atomic + " atomic, unlock " + unc.mutex3.unlock.atomic + " atomic, no system call" : "no uncontended call was seen" }); // 3. Mutual exclusion holds for the second and third at every N tried. var safe = [], tried = 0; ["mutex2", "mutex3"].forEach(function (id) { for (var n = 2; n <= 4; n += 1) { var c = census(id, n); tried += 1; if (c.twoInside || c.forgotten || c.values.some(function (v) { return v < 0 || v > 2; })) { safe.push(id + " N=" + n); } } }); out.push({ claim: "the second and third mutexes never let two threads in, never strand a " + "sleeper, and never leave the values 0, 1 and 2, with two, three or four threads", ok: tried === 6 && safe.length === 0, detail: safe.length ? safe.join(", ") + " failed" : tried + " state spaces enumerated" }); // 4. The first mutex's failed run is 2^W - 2, and it ends with two inside. var rbad = [], widths = 0; for (var w = 2; w <= 6; w += 1) { var r = failedRun("mutex", 3, 1 << w); widths += 1; if (r.longest !== runFormula(w) || r.twoInside === 0) rbad.push("W=" + w + " gave " + r.longest); } out.push({ claim: "with the lock held and two threads trying, the first mutex can fail " + "2 to the W minus 2 futex_waits in a row on a W-bit counter, and then two threads are inside", ok: widths === 5 && rbad.length === 0, detail: rbad.length ? rbad.join(", ") : "every width from 2 to 6 bits; at 32 bits the formula gives " + runFormula(32).toLocaleString("en-US") }); // 5. And with the lock held, the second and third fail none. var held = ["mutex2", "mutex3"].map(function (id) { return failedRun(id, 4, WIDE); }); out.push({ claim: "with the lock held and three threads trying, the second and third mutexes fail no futex_wait at all", ok: held.every(function (r) { return r.longest === 0 && r.twoInside === 0; }), detail: held.map(function (r) { return r.id + ": " + r.longest + " over " + r.states + " states"; }).join("; ") }); // 6. Two threads are not enough to show the first mutex's bug: one // waiter's failed wait means the holder has already let go. var twoBad = [], twoTried = 0, twoStates = 0; for (var tw = 2; tw <= 6; tw += 1) { var two = census("mutex", 2, { width: 1 << tw }); twoTried += 1; twoStates = two.states; if (two.twoInside || Math.max.apply(null, two.values) > 2) twoBad.push("W=" + tw); } out.push({ claim: "with only two threads the first mutex never counts past 2 and never lets two in, at any width tried", ok: twoTried === 5 && twoBad.length === 0, detail: twoBad.length ? twoBad.join(", ") + " failed" : "2 to 6 bits, " + twoStates + " states each: it takes a second waiter to keep the first awake" }); // 7. The constant Drepper warns about: retake with 1 and a sleeper is lost. var one = census("mutex2one", 3), right = census("mutex2", 3); out.push({ claim: "retaking the lock with 1 instead of 2 strands a sleeper in " + one.forgotten + " states with three threads; retaking with 2 strands none", ok: one.forgotten > 0 && right.forgotten === 0 && one.twoInside === 0, detail: "and with two threads the change strands nobody: " + census("mutex2one", 2).forgotten + " states" }); // 8. The contended table. Syscalls first, which the paper and the model // count the same way. ORDER.forEach(function (id) { cache[id] = costs(id, 3); }); var sbad = []; ORDER.forEach(function (id) { (id === "mutex" ? [1] : [2, 1]).forEach(function (found) { var m = contended(id, found, cache[id]); if (m.syscallsOnce !== PRINTED.contended[id].lock.syscall[0] || m.syscallsExtra !== PRINTED.contended[id].lock.syscall[1]) sbad.push(id); if (!m.unlock || m.unlock.atomic !== PRINTED.contended[id].unlock.atomic || m.unlock.syscall !== PRINTED.contended[id].unlock.syscall) sbad.push(id + " unlock"); }); }); out.push({ claim: "contended, every system-call cell of the paper's tables comes out of the model, " + "and so does every unlock", ok: sbad.length === 0 && ORDER.every(function (id) { return cache[id].locks.length > 0; }), detail: sbad.length ? sbad.join(", ") + " disagreed" : "one futex_wait per trip, one futex_wake per contended unlock" }); // 9. The atomic-operation cells, and the two ways they were counted. var rd = readings(cache); var firstAgree = rd.filter(function (x) { return x.id === "mutex2"; }) .every(function (x) { return x.matches.indexOf("whole") >= 0 && x.matches.indexOf("before") < 0; }); var otherAgree = rd.filter(function (x) { return x.id !== "mutex2"; }) .every(function (x) { return x.matches.indexOf("before") >= 0 && x.matches.indexOf("whole") < 0; }); out.push({ claim: "every contended atomic-operation cell is a number the model produces, but not under one count: " + "the second mutex's column equals the whole call, the other two equal the count up to the first futex_wait", ok: rd.length === 5 && firstAgree && otherAgree, detail: rd.map(function (x) { return x.id + (x.id === "mutex" ? "" : x.found === 2 ? " upper" : " lower") + " printed " + x.printed + ", before " + x.before + ", whole " + x.whole; }).join("; ") }); // 9b. What the third mutex's table appears to save in the first trip. var same = [2, 1].map(function (f) { var a = contended("mutex2", f, cache.mutex2), b = contended("mutex3", f, cache.mutex3); return { f: f, ok: a.before === b.before && a.whole === b.whole, a: a, b: b }; }); out.push({ claim: "counted either way, a contended lock's first trip costs the third mutex exactly " + "what it costs the second, with or without waiters already", ok: same.every(function (x) { return x.ok && x.a.whole !== null; }), detail: same.map(function (x) { return (x.f === 2 ? "waiters already" : "no waiters yet") + ": before the wait " + x.a.before + " and " + x.b.before + ", whole call " + x.a.whole + " and " + x.b.whole; }).join("; ") }); // 10. The +N. The third mutex's extra trip is always one. The second's is // one or two whatever the first atomic found, and more when another // thread keeps taking and dropping the lock between its compares. var e2 = [2, 1].map(function (f) { return contended("mutex2", f, cache.mutex2); }); var e3 = [2, 1].map(function (f) { return contended("mutex3", f, cache.mutex3); }); out.push({ claim: "an extra trip round the loop costs the third mutex exactly one atomic; " + "the second one or two in either case, and more while other threads keep slipping in", ok: e3.every(function (m) { return m.extra.length === 1 && m.extra[0] === 1; }) && e2.every(function (m) { return m.extra[0] === 1 && m.extra.indexOf(2) >= 0 && m.extra[m.extra.length - 1] > 2; }), untested: e3.concat(e2).some(function (m) { return m.extra.length === 0; }), detail: "second: " + e2.map(function (m) { return "{" + m.extra.join(", ") + "}"; }).join(" and ") + "; third: " + e3.map(function (m) { return "{" + m.extra.join(", ") + "}"; }).join(" and ") }); // 11. The cost census has a horizon, and it says where. var dropped = ORDER.map(function (id) { return cache[id].dropped; }); var kinds = ORDER.map(function (id) { return cache[id].locks.length; }); out.push({ claim: "the cost census followed thread 1 through every lock call of up to " + cache.mutex.cap.waits + " futex_waits and " + cache.mutex.cap.spin + " atomics between two of them, with three threads, and counts the calls that went past", ok: kinds.every(function (k) { return k > 0; }), untested: kinds.some(function (k) { return k === 0; }), detail: ORDER.map(function (id, i) { return id + ": " + kinds[i] + " different costs, " + dropped[i] + " ways for a call past the caps to finish"; }).join("; ") }); return out; } window.Futex = { PROGRAMS: PROGRAMS, ORDER: ORDER, PRINTED: PRINTED, CS: CS, REM: REM, explore: explore, census: census, schedule: schedule, failedRun: failedRun, runFormula: runFormula, costs: costs, uncontended: uncontended, contended: contended, readings: readings, printedFirst: printedFirst, printedExtra: printedExtra, verify: verify }; })();