// The Futex, held against things that are not its engine.
//
//   1. A second model checker, tests/futex_oracle.py, written from the C in
//      another language with another traversal. Every state count, every
//      failed-wait run and every cost the page prints is compared, exactly.
//   2. Drepper's paper itself, archived. His three tables are parsed out of
//      the text and compared with the engine's transcription, cell by cell.
//   3. The kernel. A C program runs the same three mutexes against the real
//      futex system call; its own counts and strace's log of every futex call
//      are committed in tests/fixtures/futex, and every real lock call has to
//      cost something the model can reach.
//   4. The engine, broken on purpose, which has to turn its own table red.
//
// Sources are read from the archive (docs/sources, through its manifest). For
// development before the archive exists, LA_SOURCES_DIR may point at a scratch
// copy in the archive's own format, one <sha256(url)[:12]>.txt per source.

import { readFileSync, existsSync, readdirSync } from 'node:fs';
import { execFileSync } from 'node:child_process';
import { gunzipSync } from 'node:zlib';
import { createHash } from 'node:crypto';
import { fileURLToPath } from 'node:url';
import { dirname, join } from 'node:path';
import { homedir } from 'node:os';

const HERE = dirname(fileURLToPath(import.meta.url));
const ROOT = join(HERE, '..');
const SITE = process.env.LA_SITE || join(ROOT, 'site');
let p = 0;
let f = 0;
const check = (label, ok, detail = '') => {
  if (ok) { p += 1; console.log(`  ok   ${label}${detail ? `  [${String(detail).slice(0, 160)}]` : ''}`); }
  else { f += 1; console.error(`  FAIL ${label}${detail ? `\n       ${detail}` : ''}`); }
};

const ENGINE = join(ROOT, 'site/js/futex.js');
function engine(src = readFileSync(ENGINE, 'utf8')) {
  const window = {};
  new Function('window', src)(window);
  return window.Futex;
}
const F = engine();

/* ---- the archive ----------------------------------------------------------- */
const URL = {
  drepper: 'https://www.akkadia.org/drepper/futex.pdf',
  ols: 'https://www.kernel.org/doc/ols/2002/ols2002-pages-479-495.pdf',
  listing: 'https://www.kernel.org/pub/linux/kernel/v2.5/',
  cl257: 'https://www.kernel.org/pub/linux/kernel/v2.5/ChangeLog-2.5.7',
  cl2518: 'https://www.kernel.org/pub/linux/kernel/v2.5/ChangeLog-2.5.18',
  src257: 'https://git.kernel.org/pub/scm/linux/kernel/git/tglx/history.git/plain/kernel/futex.c?h=v2.5.7',
  src2518: 'https://git.kernel.org/pub/scm/linux/kernel/git/tglx/history.git/plain/kernel/futex.c?h=v2.5.18',
  man: 'https://man7.org/linux/man-pages/man2/futex.2.html',
};
const manifestPath = join(ROOT, 'docs/sources/manifest.json');
const manifest = existsSync(manifestPath)
  ? JSON.parse(readFileSync(manifestPath, 'utf8')).sources : [];
function source(url) {
  const e = manifest.find((m) => m.url === url && m.status !== 'unfetchable' && m.file);
  if (e && existsSync(join(ROOT, 'docs/sources', e.file))) {
    return readFileSync(join(ROOT, 'docs/sources', e.file), 'utf8');
  }
  const dev = process.env.LA_SOURCES_DIR;
  if (dev) {
    const file = join(dev, createHash('sha256').update(url).digest('hex').slice(0, 12) + '.txt');
    if (existsSync(file)) return readFileSync(file, 'utf8');
  }
  return null;
}
const SMART = { '’': "'", '‘': "'", '“': '"', '”': '"', '—': '-', '–': '-' };
const unentity = (t) => t.replace(/&quot;/g, '"').replace(/&#39;|&#x27;|&rsquo;|&lsquo;/g, "'")
  .replace(/&ldquo;|&rdquo;/g, '"').replace(/&amp;/g, '&').replace(/&lt;/g, '<').replace(/&gt;/g, '>')
  .replace(/&nbsp;/g, ' ');
const flat = (t) => unentity(t).replace(/[‘’“”–—]/g, (c) => SMART[c])
  .replace(/\s+/g, ' ');
const SRC = {};
for (const [k, url] of Object.entries(URL)) {
  const t = source(url);
  check(`archived: ${url}`, t !== null,
    t === null ? 'archive missing: run la-source-audit --archive' : '');
  SRC[k] = t === null ? null : flat(t);
}
const RAW_DREPPER = source(URL.drepper);

/* ---- 1. the engine's own claims -------------------------------------------- */
const notes = F.verify();
check('the page makes at least twelve checks at load', notes.length >= 12, String(notes.length));
notes.forEach((n) => check(`load-time: ${n.claim.slice(0, 70)}`, n.ok && !n.untested, n.detail));

/* ---- 2. a second model checker, in another language ------------------------ */
const oracle = JSON.parse(execFileSync('python3', [join(HERE, 'futex_oracle.py')],
  { encoding: 'utf8', maxBuffer: 1 << 26 }));
{
  const keys = Object.keys(oracle.census);
  check('the oracle enumerated at least fifteen state spaces', keys.length >= 15, String(keys.length));
  let bad = 0;
  for (const key of keys) {
    const [id, n, bits] = key.split('/');
    const theirs = F.census(id, Number(n), { width: 1 << Number(bits) });
    const mine = oracle.census[key];
    const same = theirs.states === mine.states && theirs.twoInside === mine.two
      && theirs.forgotten === mine.forgotten
      && Math.max(...theirs.values) === mine.maxword && Math.min(...theirs.values) === mine.minword
      && theirs.wakeEdges === mine.wake && theirs.wakeNobodyEdges === mine.wakenobody
      && theirs.wakePlaces === mine.wakeplaces;
    if (!same) bad += 1;
    check(`${key}: both models reach ${mine.states} states, ${mine.two} with two inside, ${mine.forgotten} stranded, `
      + `${mine.wakeplaces} futex_wake places`,
      same, `engine ${theirs.states}/${theirs.twoInside}/${theirs.forgotten} wakes ${theirs.wakeEdges}/`
        + `${theirs.wakeNobodyEdges}/${theirs.wakePlaces}, oracle ${mine.wake}/${mine.wakenobody}/${mine.wakeplaces}`);
  }
  check('and no state space disagreed', bad === 0, `${bad} of ${keys.length}`);

  // Step 1's own numbers: the first mutex with its counter stopped below 16,
  // which no comparison above passes. The wake counts are the page's 14 and
  // 12, and at three threads its 777 and 648; nothing else grades them.
  const nowrap = Object.entries(oracle.nowrap || {});
  check('the oracle counted step 1 at one, two and three threads', nowrap.length === 3, String(nowrap.length));
  for (const [key, mine] of nowrap) {
    const [id, n, bits] = key.split('/');
    const theirs = F.census(id, Number(n), { noWrap: true, width: 1 << Number(bits) });
    const shown = F.census(id, Number(n), { noWrap: true });
    check(`${key} unwrapped: ${mine.states} states, futex_wake at ${mine.wakeplaces} places, ${mine.wakenobody} waking nobody`,
      theirs.states === mine.states && theirs.wakeEdges === mine.wake
        && theirs.wakeNobodyEdges === mine.wakenobody && theirs.wakePlaces === mine.wakeplaces
        && shown.states === theirs.states && shown.wakePlaces === theirs.wakePlaces
        && shown.wakeNobodyEdges === theirs.wakeNobodyEdges,
      `engine ${theirs.states}/${theirs.wakeEdges}/${theirs.wakeNobodyEdges}/${theirs.wakePlaces}, `
        + `oracle ${mine.states}/${mine.wake}/${mine.wakenobody}/${mine.wakeplaces}`);
  }
  const three = oracle.nowrap && oracle.nowrap['mutex/3/4'];
  check('at three threads a two-sleeper wake makes branches outnumber places, so the page counts places',
    three && three.wake + three.wakenobody > three.wakeplaces,
    three ? `${three.wake + three.wakenobody} branches, ${three.wakeplaces} places` : 'missing');
  check('and at three threads the counter reaches the top of its range, where it stops',
    three && three.maxword === 15, three ? String(three.maxword) : 'missing');

  for (const [key, mine] of Object.entries(oracle.failed)) {
    const [id, n, bits] = key.split('/');
    const theirs = F.failedRun(id, Number(n), 1 << Number(bits));
    check(`${key}: both find a longest run of ${mine.longest} failed waits`,
      theirs.longest === mine.longest && theirs.twoInside === mine.two,
      `engine ${theirs.longest} and ${theirs.twoInside}, oracle ${mine.longest} and ${mine.two}`);
  }

  // Costs: the same set of records, call for call.
  for (const [key, mine] of Object.entries(oracle.costs)) {
    const [id, n] = key.split('/');
    const theirs = F.costs(id, Number(n));
    const a = new Set(theirs.locks.map((x) => `${x.found}|${x.segs.join('.')}|${x.syscalls}`));
    const b = new Set(mine.locks.map(([fd, segs, sy]) => `${fd}|${segs.join('.')}|${sy}`));
    const ua = new Set(theirs.unlocks.map((x) => `${x.found === null ? -1 : x.found}|${x.atomics}|${x.syscalls}|${x.woke}`));
    const ub = new Set(mine.unlocks.map((x) => x.join('|')));
    const eq = (s, t) => s.size === t.size && [...s].every((x) => t.has(x));
    check(`${key}: both find the same ${b.size} lock costs`, eq(a, b) && b.size > 0,
      `engine ${a.size}, oracle ${b.size}`);
    check(`${key}: and the same ${ub.size} unlock costs`, eq(ua, ub) && ub.size > 0,
      [...ua].join(' ') + ' / ' + [...ub].join(' '));
  }
}
// Every oracle comparison above passes a width, so none of them sees the
// default. The page's first state count does: three threads on the first
// mutex, unwrapped, at whatever width the engine assumes. The engine says a
// four-bit word, and the UI passes 16 by hand for the held run, so the default
// has to be 16: the counter climbs to 15 and the count is the width-16 one.
{
  const byDefault = F.census('mutex', 3, { noWrap: true });
  const at16 = F.census('mutex', 3, { noWrap: true, width: 16 });
  check('the default counter is a four-bit word: three threads count up to 15, as at width 16',
    byDefault.states === at16.states && Math.max(...byDefault.values) === 15,
    `${byDefault.states} states by default, ${at16.states} at 16; highest ${Math.max(...byDefault.values)}`);
}

/* ---- 3. the closed form, by arithmetic -------------------------------------- */
{
  let bad = 0;
  for (let bits = 2; bits <= 8; bits += 1) {
    const r = F.failedRun('mutex', 3, 1 << bits);
    if (r.longest !== 2 ** bits - 2 || r.twoInside === 0) bad += 1;
  }
  check('the failed run is 2^W - 2 at every width from 2 to 8 bits, the slider\'s whole range',
    bad === 0, `${bad} of 7 disagreed`);
  check('and the 32-bit figure the page prints is 4,294,967,294',
    F.runFormula(32) === 4294967294 && 2 ** 32 - 2 === 4294967294);
  check('of the 4,294,967,296 values a 32-bit counter has', 2 ** 32 === 4294967296);
  // And it takes two waiters: one is never enough, at any width the slider offers.
  let one = 0;
  for (let bits = 2; bits <= 8; bits += 1) {
    const r = F.failedRun('mutex', 2, 1 << bits);
    if (r.longest !== 0 || r.twoInside !== 0) one += 1;
  }
  check('with one waiter the run is 0 and nobody gets in, 2 to 8 bits', one === 0, `${one} disagreed`);
}

/* ---- 4. Drepper's tables, out of the archived paper ------------------------- */
//
// pdftotext reads each table as a header and then one block of lines per
// column. A stacked cell -- his upper number over his lower one -- comes out
// as its digits on separate lines. Read off the page itself at 110 dots per
// inch, mutex2's contended cell is 2 over 3, plus, 1 over 2, and the text
// layer emits the upper row's second digit first because it sits higher on
// the line: "1", "2", "3 + 2". mutex3's is 1 over 2, plus 1: "1", "2 +1".
if (RAW_DREPPER) {
  const tables = [...RAW_DREPPER.matchAll(/\nmutex2?\n\nmutex[23]\n\n([\s\S]*?)\n\n(?=[A-Z])/g)]
    .map((m) => m[1].split(/\n\n/).map((b) => b.split('\n')));
  check('the archived paper has three cost tables', tables.length === 3, String(tables.length));
  const P = F.PRINTED;
  if (tables.length === 3) {
    const [unc, con1, con2] = tables;
    const nums = (b) => b.map(Number);
    check('uncontended, mutex: lock 1 atomic 0 syscalls, unlock 0 atomic 1 syscall',
      JSON.stringify(nums(unc[0])) === JSON.stringify([P.uncontended.mutex.lock.atomic,
        P.uncontended.mutex.lock.syscall, P.uncontended.mutex.unlock.atomic,
        P.uncontended.mutex.unlock.syscall]) && unc[0].join(',') === '1,0,0,1', unc[0].join(','));
    check('uncontended, mutex2: lock 1 and 0, unlock 1 and 0',
      JSON.stringify(nums(unc[1])) === JSON.stringify([P.uncontended.mutex2.lock.atomic,
        P.uncontended.mutex2.lock.syscall, P.uncontended.mutex2.unlock.atomic,
        P.uncontended.mutex2.unlock.syscall]) && unc[1].join(',') === '1,0,1,0', unc[1].join(','));
    const plus = (x) => `${x[0]}+${x[1]}`;
    check('contended, mutex: 1+1 and 1+1, unlock 0 and 1',
      con1[0].join(',') === [plus(P.contended.mutex.lock.atomic), plus(P.contended.mutex.lock.syscall),
        P.contended.mutex.unlock.atomic, P.contended.mutex.unlock.syscall].join(','), con1[0].join(','));
    const m2 = P.contended.mutex2.lock.atomic;
    const stacked2 = [String(m2[1].upper), String(m2[0].upper), `${m2[0].lower} + ${m2[1].lower}`];
    check('contended, mutex2: the stacked cell is 2 over 3, plus 1 over 2',
      con1[1].join('|') === stacked2.join('|'), `${con1[1].join('|')} against ${stacked2.join('|')}`);
    check('and the same cell is printed again in the second table',
      con2[0].join('|') === stacked2.join('|'), con2[0].join('|'));
    const tail2 = [plus(P.contended.mutex2.lock.syscall), P.contended.mutex2.unlock.atomic,
      P.contended.mutex2.unlock.syscall].join(',');
    check('mutex2: syscalls 1+1, unlock 1 and 1, in both tables',
      con1[2].join(',') === tail2 && con2[2].join(',') === tail2, `${con1[2]} / ${con2[2]}`);
    const m3 = P.contended.mutex3.lock.atomic;
    check('contended, mutex3: the stacked cell is 1 over 2, plus 1',
      con2[1].join('|') === `${m3[0].upper}|${m3[0].lower} +${m3[1]}`, con2[1].join('|'));
    check('mutex3: syscalls 1+1, unlock 1 and 1',
      con2[3].join(',') === [plus(P.contended.mutex3.lock.syscall), P.contended.mutex3.unlock.atomic,
        P.contended.mutex3.unlock.syscall].join(','), con2[3].join(','));
  }
}

/* ---- 5. the two counts, computed a second way from the oracle's records ----- */
{
  const from = (id, found) => {
    const recs = oracle.costs[`${id}/3`].locks
      .map(([fd, segs, sy]) => ({ found: fd, segs, sy, waits: segs.length - 1,
        atomics: segs.reduce((a, b) => a + b, 0) }))
      .filter((r) => r.found === found && r.waits >= 1);
    const min = (xs) => xs.reduce((m, x) => (m === null || x < m ? x : m), null);
    return {
      before: min(recs.map((r) => r.segs[0])),
      whole: min(recs.filter((r) => r.waits === 1).map((r) => r.atomics)),
      extra: [...new Set(recs.filter((r) => r.waits === 2).map((r) => r.segs[1]))].sort((a, b) => a - b),
    };
  };
  const rd = F.readings();
  for (const r of rd) {
    const o = from(r.id, r.found);
    check(`${r.id} (found ${r.found}): before the first wait ${o.before}, whole call ${o.whole}, by the oracle too`,
      o.before === r.before && o.whole === r.whole && o.extra.join() === r.extra.join(),
      `engine ${r.before}/${r.whole}/${r.extra}, oracle ${o.before}/${o.whole}/${o.extra}`);
  }
  // The finding, computed here from the oracle and the printed table only.
  const P = F.PRINTED.contended;
  const printed = (id, found) => {
    const c = P[id].lock.atomic[0];
    return typeof c === 'number' ? c : found === 2 ? c.upper : c.lower;
  };
  const cases = [['mutex', 1], ['mutex2', 2], ['mutex2', 1], ['mutex3', 2], ['mutex3', 1]];
  const verdict = cases.map(([id, fd]) => {
    const o = from(id, fd), pr = printed(id, fd);
    return `${id}:${pr === o.before ? 'before' : ''}${pr === o.whole ? 'whole' : ''}`;
  });
  check('the second mutex\'s printed cells equal the whole call and the rest equal the count to the first wait',
    verdict.join(' ') === 'mutex:before mutex2:whole mutex2:whole mutex3:before mutex3:before',
    verdict.join(' '));
  check('so no single count reproduces every printed cell',
    !cases.every(([id, fd]) => printed(id, fd) === from(id, fd).before)
      && !cases.every(([id, fd]) => printed(id, fd) === from(id, fd).whole));
  // "2 to 3 times": the paper's ratio, and the ratio under one count.
  const m1whole = from('mutex', 1).whole;
  check('counted whole, the first mutex is 2, and the second\'s 2 or 3 is 1 to 1.5 times that, not 2 to 3',
    m1whole === 2 && printed('mutex2', 2) / m1whole === 1 && printed('mutex2', 1) / m1whole === 1.5,
    `${printed('mutex2', 2)}/${m1whole} and ${printed('mutex2', 1)}/${m1whole}`);
  check('and the paper does say 2 to 3 times',
    SRC.drepper !== null && SRC.drepper.includes('makes 2 to 3 times as many atomic operations'));
  check('counted either way, the third mutex\'s first trip equals the second\'s',
    [2, 1].every((fd) => from('mutex3', fd).before === from('mutex2', fd).before
      && from('mutex3', fd).whole === from('mutex2', fd).whole));
  check('an extra trip: the third always 1, the second 1 and 2 and more',
    from('mutex3', 2).extra.join() === '1' && from('mutex3', 1).extra.join() === '1'
      && from('mutex2', 2).extra[0] === 1 && from('mutex2', 2).extra.includes(2)
      && Math.max(...from('mutex2', 1).extra) > 2,
    `${from('mutex2', 2).extra} / ${from('mutex3', 2).extra}`);
}

/* ---- 6. what the documents say ---------------------------------------------- */
if (SRC.drepper) {
  const d = SRC.drepper;
  check('Drepper: version 1.6', d.includes('Version 1.6') && d.includes('2011-11-05 Fix a typo. Version 1.6.'));
  check('Drepper: first draft 2003-10-12', d.includes('2003-10-12 First draft.'));
  check('Drepper: the third mutex added 2004-02-22', d.includes('2004-02-22 Add mutex3 description.'));
  // "four months after the first draft", by the calendar.
  const months = (2004 - 2003) * 12 + (2 - 10);
  check('which is four months after the first draft', months === 4, String(months));
  check('Drepper: futexes "provide problems even to their inventors"',
    d.includes('they provide problems even to their inventors'));
  check('Drepper: a four processor machine, eight to ten times',
    d.includes('running on a four processor machine got sped up eight to ten times'));
  check('Drepper: the +N is the cost of going back to sleep',
    d.includes('The +N part in the fields represents the additional cost for the function call '
      + 'which has to be paid if the futex wait system call returns but the thread cannot get '
      + 'the mutex and is going back to sleep.'));
  check('Drepper: the first number is not defined anywhere near the table',
    !/\+N part[^.]*first number/.test(d) && !/number before the \+/.test(d));
  check('Drepper: the three values 0, 1 and 2',
    // The text layer reads the little table column by column.
    d.includes('following convention: 0 1 2 unlocked locked, no waiters locked, one or more waiters'));
  check('Drepper: an unlock that may call futex_wake for nobody',
    d.includes('The consequence is a possible unnecessary call to futex wake in unlock.'));
  check('Drepper: the counter runs out and the variable is free',
    d.includes('we are back to zero and magically the variable is free'));
  check('Drepper: one single thread can overflow it, through signals, which this page leaves out',
    d.includes('it is in theory possible for one single thread to overflow the counter')
      && d.includes('But there is also a way which cannot be avoided.'));
}
if (SRC.ols) {
  const o = SRC.ols;
  check('OLS 2002: integrated into 2.5.7', o.includes('integrated into the Linux kernel distribution version 2.5.7'));
  check('OLS 2002: 2.5.7 had FUTEX_UP and FUTEX_DOWN', o.includes('FUTEX_UP and FUTEX_DOWN'));
  check('OLS 2002: two new op values replaced them', o.includes('two new "op" values replaced the operations above'));
  check('OLS 2002: several independent implementations before it',
    o.includes('With several independent implementations'));
  check('OLS 2002: authors and venue',
    o.includes('Fuss, Futexes and Furwocks') && o.includes('Hubertus Franke') && o.includes('Rusty Russell')
      && o.includes('Matthew Kirkwood') && o.includes('Ottawa Linux Symposium 2002'));
}
if (SRC.listing) {
  // The directory listing's own dates, parsed rather than typed beside a filename.
  const date = (file) => {
    const m = SRC.listing.match(new RegExp(file.replace(/\./g, '\\.') + '\\s+(\\d{2}-[A-Z][a-z]{2}-\\d{4}) (\\d{2}:\\d{2})'));
    return m ? `${m[1]} ${m[2]}` : null;
  };
  check('kernel.org dates linux-2.5.7.tar.gz 18 March 2002', date('linux-2.5.7.tar.gz') === '18-Mar-2002 20:42',
    date('linux-2.5.7.tar.gz'));
  check('and ChangeLog-2.5.7 the same minute', date('ChangeLog-2.5.7') === '18-Mar-2002 20:42',
    date('ChangeLog-2.5.7'));
  check('and ChangeLog-2.5.18 25 May 2002', date('ChangeLog-2.5.18') === '25-May-2002 01:58',
    date('ChangeLog-2.5.18'));
  check('and 2.5.6, the release before, 8 March', date('linux-2.5.6.tar.gz') === '08-Mar-2002 02:22',
    date('linux-2.5.6.tar.gz'));
}
if (SRC.cl257) {
  check('ChangeLog-2.5.7 carries Futexes IV',
    SRC.cl257.includes('[PATCH] Futexes IV (Fast Lightweight Userspace Semaphores)'));
}
if (SRC.cl2518) {
  check('ChangeLog-2.5.18 changes the semantics to sleep-if-equal',
    SRC.cl2518.includes('This changes futex semantics to a simple "sleep if this address equals this value" interface'));
}
if (SRC.src257 && SRC.src2518) {
  check('futex.c at 2.5.7: two arguments, FUTEX_UP and FUTEX_DOWN, no FUTEX_WAIT',
    SRC.src257.includes('sys_futex(void *uaddr, int op)') && SRC.src257.includes('case FUTEX_UP:')
      && SRC.src257.includes('case FUTEX_DOWN:') && !SRC.src257.includes('FUTEX_WAIT'));
  check('futex.c at 2.5.18: four arguments, FUTEX_WAIT, FUTEX_WAKE and EWOULDBLOCK',
    SRC.src2518.includes('sys_futex(void *uaddr, int op, int val, struct timespec *utime)')
      && SRC.src2518.includes('case FUTEX_WAIT:') && SRC.src2518.includes('case FUTEX_WAKE:')
      && SRC.src2518.includes('-EWOULDBLOCK'));
}
if (SRC.man) {
  check('futex(2): the check and the block happen atomically',
    SRC.man.includes("The loading of the futex word's value, the comparison of that value with the "
      + 'expected value, and the actual blocking will happen atomically'));
  check('futex(2): dates the four-argument call to 2.5.40, which the 2.5.18 source contradicts',
    SRC.man.includes('A four-argument system call with the semantics described in this page was introduced in Linux 2.5.40.'));
  check('futex(2): and agrees that support was first merged in 2.5.7',
    SRC.man.includes('Initial futex support was merged in Linux 2.5.7'));
}

/* ---- 7. the real kernel ------------------------------------------------------ */
const FIX = join(HERE, 'fixtures/futex');
const kernel = JSON.parse(readFileSync(join(FIX, 'kernel.json'), 'utf8'));
check('the fixture records the kernel it was measured on', /^\d+\.\d+\.\d+/.test(kernel.uname_r), kernel.uname_r);
const run = (name) => JSON.parse(readFileSync(join(FIX, `${name}.json`), 'utf8'));

/* Every futex call strace saw on the program's own word, with its result.
 * A call that blocked is logged twice, as "<unfinished ...>" and later as
 * "<... futex resumed>" on the same thread, so the pending operation is
 * remembered per thread id. glibc's own futex calls, for pthread_join, are on
 * other addresses and are not counted. */
function strace(name, addr) {
  const text = gunzipSync(readFileSync(join(FIX, `${name}.strace.gz`))).toString('utf8');
  const out = { wait: 0, wake: 0, eagain: 0, slept: 0, wokeNone: 0, lines: 0, other: 0 };
  const pending = new Map();
  const result = (op, r) => {
    if (op === 'FUTEX_WAIT') {
      if (/= -1 EAGAIN/.test(r)) out.eagain += 1;
      else if (/= 0\b/.test(r)) out.slept += 1;
      else out.other += 1;
    } else if (/= 0\b/.test(r)) out.wokeNone += 1;
  };
  for (const line of text.split('\n')) {
    if (!line) continue;
    out.lines += 1;
    const pid = line.split(/\s+/)[0];
    const call = line.match(/futex\((0x[0-9a-f]+), (FUTEX_[A-Z_|]+)/);
    if (call && call[1] === addr) {
      const op = call[2];
      if (op === 'FUTEX_WAIT') out.wait += 1;
      else if (op === 'FUTEX_WAKE') out.wake += 1;
      else { out.other += 1; continue; }
      if (line.includes('<unfinished ...>')) pending.set(pid, op);
      else result(op, line);
      continue;
    }
    if (line.includes('<... futex resumed>') && pending.has(pid)) {
      result(pending.get(pid), line);
      pending.delete(pid);
    }
  }
  out.unresolved = pending.size;
  return out;
}

const RUNS = [];
for (const m of ['mutex', 'mutex2', 'mutex3']) for (const mode of ['uncontended', 'contended', 'held']) RUNS.push(`${m}-${mode}`);
for (const name of RUNS) {
  const r = run(name);
  const s = strace(name, r.futex_addr);
  check(`${name}: strace and the program count the same futex calls`,
    s.wait === r.futex_wait && s.wake === r.futex_wake && s.unresolved === 0 && s.other === 0,
    `strace ${s.wait} waits and ${s.wake} wakes, program ${r.futex_wait} and ${r.futex_wake}`);
  check(`${name}: and the same results: EWOULDBLOCK, slept, woke nobody`,
    s.eagain === r.ewouldblock && s.slept === r.slept && s.wokeNone === r.wakes_nobody,
    `strace ${s.eagain}/${s.slept}/${s.wokeNone}, program ${r.ewouldblock}/${r.slept}/${r.wakes_nobody}`);
  check(`${name}: every lock was released`, r.locks === r.unlocks && r.locks > 0, `${r.locks}/${r.unlocks}`);
}

// Uncontended, against the model's own uncontended row.
for (const id of F.ORDER) {
  const r = run(`${id}-uncontended`);
  const u = F.uncontended(id);
  check(`${id}: a thousand uncontended pairs cost what the model's one does, times a thousand`,
    r.iterations === 1000 && r.locks === 1000
      && r.lock_atomics === 1000 * u.lock.atomic && r.unlock_atomics === 1000 * u.unlock.atomic
      && r.futex_wait === 1000 * u.lock.syscall && r.futex_wake === 1000 * u.unlock.syscall,
    `${r.lock_atomics} ${r.unlock_atomics} ${r.futex_wait} ${r.futex_wake}`);
}
const unc1 = run('mutex-uncontended');
check('so the first mutex made 1,000 futex calls and the others none',
  unc1.futex_wake === 1000 && run('mutex2-uncontended').futex_wake === 0
    && run('mutex3-uncontended').futex_wake === 0
    && strace('mutex-uncontended', unc1.futex_addr).wake === 1000);

// Held: the second and third fail no wait while the lock is held, as the model says.
for (const id of ['mutex2', 'mutex3']) {
  const r = run(`${id}-held`);
  check(`${id}: with the lock held, no futex_wait failed`, r.ewouldblock_while_held === 0 && r.futex_wait > 0,
    `${r.ewouldblock_while_held} of ${r.futex_wait}`);
}
{
  const r = run('mutex-held');
  // The model says the first mutex CAN fail while held; whether this run did
  // is luck, and the page does not claim it did. Recorded, not asserted.
  console.log(`  --   mutex held: ${r.ewouldblock_while_held} failed waits while held, in ${r.rounds} rounds `
    + 'of 3 waiters; the model allows them and a real run need not produce any');
}

// Contended: every real lock call's cost against the model's reachable costs.
// The structural rules hold for every call, however long; the full membership
// test runs over the calls inside the model's horizon, and says how many that is.
{
  const rule = {
    mutex: (fd, a, w) => (fd === 0 ? a === 1 && w === 0 : a === w + 1),
    mutex3: (fd, a, w) => (fd === 0 ? a === 1 && w === 0 : fd === 1 ? a === w + 2 : a === w + 1),
    mutex2: (fd, a, w) => (fd === 0 ? a === 1 && w === 0 : fd === 1 ? a >= w + 2 : a >= w + 1),
  };
  const horizon = { mutex: { waits: 6, spin: 4 }, mutex2: { waits: 3, spin: 8 }, mutex3: { waits: 6, spin: 4 } };
  for (const id of F.ORDER) {
    const r = run(`${id}-contended`);
    const entries = Object.entries(r.lock_costs).map(([k, n]) => [k.split(':').map(Number), n]);
    const calls = entries.reduce((s, [, n]) => s + n, 0);
    const broke = entries.filter(([[fd, a, w]]) => !rule[id](fd, a, w));
    check(`${id}: all ${calls} real lock calls in the table obey the model's rule for their cost`,
      broke.length === 0 && calls + r.lock_costs_past_table === r.locks,
      broke.map(([k]) => k.join(':')).join(' '));
    check(`${id}: and the run really was contended`, r.contended_locks > 100, String(r.contended_locks));
    const model = F.costs(id, 3, horizon[id]);
    const reach = new Set(model.locks.map((x) => `${x.found}:${x.atomics}:${x.waits}`));
    const inside = entries.filter(([[, , w]]) => w <= horizon[id].waits);
    const missing = inside.filter(([k]) => !reach.has(k.join(':')));
    const seen = inside.reduce((s, [, n]) => s + n, 0);
    check(`${id}: every one of the ${seen} real calls with up to ${horizon[id].waits} waits costs something the model reaches`,
      missing.length === 0 && seen > 0,
      missing.length ? 'unreached: ' + missing.map(([k, n]) => `${k.join(':')} x${n}`).join(', ')
        : `${calls - seen + r.lock_costs_past_table} calls beyond the horizon, compared by rule only`);
  }
}

/* ---- 8. what the page ships -------------------------------------------------- */
const PAGE = join(SITE, 'nibbles/futex/index.html');
const spec = JSON.parse(readFileSync(join(ROOT, 'machines/futex.json'), 'utf8'));
check('the page is built', existsSync(PAGE), existsSync(PAGE) ? '' : `no ${PAGE}: build-machine.py futex has not run`);
if (existsSync(PAGE)) {
  const html = readFileSync(PAGE, 'utf8');
  const text = flat(html.replace(/<script[\s\S]*?<\/script>/g, ' ').replace(/<[^>]+>/g, ' '));
  // Every quotation on the page, written out whole, once each, because the
  // claims gate reads this file as text; held against the archived document
  // it comes from and against the page.
  const QUOTES = [
    ['drepper', 'must be atomic, too'],
    ['man', 'The loading of the futex word’s value, the comparison of that value with the expected value, and the actual blocking will happen atomically'],
    ['drepper', 'quite serious in some situations but very hard to spot'],
    ['drepper', 'This process can be continued ad infinitum.'],
    ['drepper', 'magically the variable is free'],
    ['drepper', 'One example is the first bug above.'],
    ['drepper', 'present in some form for many months'],
    ['drepper', 'got sped up eight to ten times'],
    ['drepper', 'because we do not know any better'],
    ['drepper', 'being wrong in guessing sooner or later means running into a deadlock'],
    ['drepper', 'represents the additional cost for the function call which has to be paid'],
    ['drepper', 'use the upper number, otherwise the lower number'],
    ['drepper', 'cannot be avoided'],
    ['ols', 'integrated into the Linux kernel distribution version 2.5.7'],
    ['cl257', 'Futexes IV (Fast Lightweight Userspace Semaphores)'],
    ['cl2518', 'changes futex semantics to a simple'],
    ['ols', 'several independent implementations'],
    ['drepper', 'It is used in the modern thread library implementation'],
  ];
  const onPage = [...(spec.panels.join(' ') + ' ' + spec.lede + ' '
    + spec.ledger.map((x) => x.body).join(' ')).matchAll(/&ldquo;(.*?)&rdquo;/g)].map((m) => flat(m[1]));
  check('every quotation in the spec is in this list, and only those',
    onPage.length === QUOTES.length && onPage.every((q) => QUOTES.some(([, x]) => flat(x) === q)),
    `${onPage.length} on the page, ${QUOTES.length} listed`);
  for (const [doc, q] of QUOTES) {
    check(`${doc} says, and the page quotes: ${q.slice(0, 56)}`,
      SRC[doc] !== null && SRC[doc].includes(flat(q)) && text.includes(flat(q)), q);
  }
  // The roster's stages are the page's step headings, word for word.
  const shared = JSON.parse(readFileSync(join(homedir(), 'projects/siteops/shared/logical-art/machines.json'), 'utf8'))
    .machines.find((m) => m.id === 'futex');
  const entry = shared && shared.stages ? shared
    : JSON.parse(readFileSync(join(ROOT, 'session-notes/roster-futex.json'), 'utf8'));
  const labels = [...html.matchAll(/class="fx-steplabel"><span class="fx-stepno">\d<\/span> ([^<]*)</g)]
    .map((m) => flat(m[1]));
  check('the four step headings are the roster\'s four stages, in order',
    labels.length === 4 && labels.join('|') === entry.stages.map(flat).join('|'), labels.join(' | '));
  check('the page names the kernel the measurement was made on',
    text.includes(`Linux ${kernel.uname_r.split('-')[0]}`), kernel.uname_r);
  check('and the thousand uncontended pairs and their 1,000 futex calls',
    text.includes('a thousand times made 1,000 futex calls') && unc1.iterations === 1000);
  check('the page dates the futex 18 March 2002 and 2.5.7, and the interface 2.5.18',
    text.includes('18 March 2002') && text.includes('2.5.7') && text.includes('2.5.18')
      && text.includes('2.5.40'));
  check('the page dates the paper 2003-10-12 and the third mutex 2004-02-22',
    text.includes('2003-10-12') && text.includes('2004-02-22') && text.includes('version 1.6'));
  check('the slider runs 2 to 8 bits, the range the closed form was checked over',
    /id="fx-bits"[^>]*min="2"[^>]*max="8"/.test(html) && text.includes('from 2 to 8 bits'));
  // A superlative and its refusal share words, so the pattern is proved on a
  // sentence that makes the claim before it is believed about one that does not.
  const claimsFirst = (t) => /\b(is|was) the first (user[- ]space |fast )?lock\b/i.test(t)
    || /\bfutexes? (was|were) the first\b/i.test(t) || /\binvented the (mutex|lock)\b/i.test(t);
  check('the first-claim check can see the claim when it is made',
    claimsFirst('The futex was the first fast lock in any kernel.'));
  check('and not when it is refused',
    !claimsFirst('Not the first lock that stays out of the kernel'));
  check('and the page makes no first claim', !claimsFirst(text));
  check('the page does not say Drepper\'s first mutex was the inventors\' code',
    !/inventors'? (own )?(first )?mutex/i.test(text) && !/Rusty Russell'?s? (first )?mutex/i.test(text));
  check('the ledger says the model is sequentially consistent and points at Memory Ordering',
    /sequentially consistent/.test(text) && html.includes('href="/nibbles/memory-ordering/"'));
  for (const sib of ['compare-and-swap', 'system-call', 'semaphore', 'context-switch']) {
    check(`the page points at ${sib}`, html.includes(`href="/nibbles/${sib}/"`)
      && existsSync(join(SITE, 'nibbles', sib, 'index.html')));
  }
  check('the sound verdict is written down', /Sound: no/.test(text));
}

/* ---- 8b. what the outside reviews of 2026-10-07 caught ---------------------- */
// Each check reads the evidence first and the spec second, so it fails on the
// sentence as it was before the fix. session-notes/verify-futex.md has the rest.
{
  const lede = flat(spec.lede);
  const panels = spec.panels.map(flat);
  const ledger = spec.ledger.map((x) => flat(x.body)).join(' ');
  const all = [lede, ...panels, ledger].join(' ');
  const ui = readFileSync(join(ROOT, 'site/js/futex-ui.js'), 'utf8');

  check('the 2.5.18 source has one futex system call that both waits and wakes',
    SRC.src2518 !== null && (SRC.src2518.match(/asmlinkage int sys_futex\(/g) || []).length === 1
      && SRC.src2518.includes('case FUTEX_WAIT:') && SRC.src2518.includes('case FUTEX_WAKE:'));
  check('so the lede does not call a futex two system calls', !/two system calls/.test(lede), lede.slice(0, 100));

  check('Drepper says one thread alone can overflow the first mutex\'s counter',
    SRC.drepper !== null && SRC.drepper.includes('possible for one single thread to overflow the counter'));
  check('so the page\'s one-waiter sentence names the signals the model leaves out',
    /With only one waiter/.test(all) && /With only one waiter and no signals/.test(all));

  check('Drepper\'s footnote on many months is on the first bug, the waiters keeping each other awake',
    SRC.drepper !== null && SRC.drepper.includes('quite serious in some situations but very hard to spot.2')
      && SRC.drepper.includes('2 This bug was present in some form for many months'));
  check('so the page gives it to the first bug, not the counter running out',
    /The first bug was "present in some form for many months"/.test(all));

  check('the sentence that points at the marked row names it, for a reader who cannot see the mark',
    /The marked row in the table below, an unlock with nobody waiting,/.test(panels[0])
      && ui.includes('["unlock (), nobody waiting"')
      && ui.includes('{ mark: function (r, i) { return i === 1 ? "yes" : ""; } });\n\n    var n = Number(el("fx-n1")'));

  const capped = F.costs('mutex2', 3);
  const raised = F.costs('mutex2', 3, { spin: capped.cap.spin + 2 });
  const past = Math.max(...F.contended('mutex2', 2, raised).extra);
  check('raise the census cap and the second mutex\'s extra trip goes past the old cap',
    past > capped.cap.spin, `cap ${capped.cap.spin}, reached ${past}`);
  check('so the caption does not call the capped list every value the model reaches',
    !/every value the model reaches/.test(panels[3]) && /before its cap/.test(panels[3]));
  check('and the sentence under it says the census cut the list, not the model',
    ui.includes('a list the census cuts off at'));

  const a = F.contended('mutex', 1), b = F.contended('mutex2', 2);
  check('the first mutex and the second with waiters make the same moves and are printed differently',
    a.before === b.before && a.whole === b.whole && F.printedFirst('mutex', 1) !== F.printedFirst('mutex2', 2),
    `before ${a.before}/${b.before}, whole ${a.whole}/${b.whole}, printed ${F.printedFirst('mutex', 1)}/${F.printedFirst('mutex2', 2)}`);
  check('so the two counts are a reading: the lede says the cells fit two counts, not that the table counts two ways',
    /fit only if it counts two different ways/.test(lede) && !/turns out to count/.test(lede)
      && !/a cost table that counts two ways/.test(flat(spec.description)));
  check('and the verdict under the table says it is this page\'s reading',
    ui.includes('neither reading ') && ui.includes('is more than this page\'s inference')
      && !ui.includes('But they are two counts.'));

  const unfollowed = F.ORDER.filter((id) => run(`${id}-contended`).lock_costs_past_table > 0);
  check('some real calls are too long for the measurement to record their cost',
    unfollowed.length > 0, unfollowed.join(', '));
  check('so the ledger says those are only held to a rule or counted, not matched against the model',
    /held only to a rule for their cost/.test(ledger) && /the longest of them are only counted/.test(ledger));
}

/* ---- 8c. what the outside reviews of 2026-10-08 caught ---------------------- */
// Evidence first, then the sentence. session-notes/verify2-futex.md has the rest.
{
  const lede = flat(spec.lede);
  const panels = spec.panels.map(flat);
  const ledger = spec.ledger.map((x) => flat(x.body)).join(' ');
  const summaries = spec.ledger.map((x) => flat(x.summary));
  const ui = readFileSync(join(ROOT, 'site/js/futex-ui.js'), 'utf8');

  check('2.5.7 had no wait-if-equal; 2.5.18 did',
    SRC.src257 !== null && !SRC.src257.includes('FUTEX_WAIT')
      && SRC.src2518 !== null && SRC.src2518.includes('case FUTEX_WAIT:'));
  check('so the lede, which defines a futex by that wait, also names 2.5.18',
    /2\.5\.7/.test(lede) && /2\.5\.18/.test(lede), lede.slice(0, 160));

  const s7 = F.failedRun('mutex', 3, 1 << 7).states, s8 = F.failedRun('mutex', 3, 1 << 8).states;
  const per = (s8 - s7) / (1 << 7);
  check('the first mutex\'s state space grows by about eleven states per counter value',
    per > 10 && per < 12, `${s7} at 7 bits, ${s8} at 8`);
  check('so at 32 bits it is tens of billions of states: too many for a browser, not for everybody',
    per * 2 ** 32 > 4e10);
  check('and the page says this page cannot enumerate it, not that nobody can',
    ![...panels, ledger].some((t) => /nobody can enumerate|cannot be enumerated/i.test(t))
      && !/nobody can enumerate/i.test(ui) && /this page/.test(panels[1]) && ui.includes('this page cannot enumerate it'));

  check('a real futex_wait also returns on a timeout or a signal',
    SRC.src2518 !== null && SRC.src2518.includes('-ETIMEDOUT') && SRC.src2518.includes('-EINTR'));
  check('so the ledger heading on wakeups says it is about the model',
    summaries.some((s) => /^In the model, a sleeper wakes only when futex_wake picks it$/.test(s))
      && !summaries.includes('A sleeper wakes only when futex_wake picks it'));
}

/* ---- 8d. what the red team of 2026-10-08 caught ------------------------------ */
// Evidence first, then the sentence. session-notes/redteam-futex.md and
// fix3-futex.md have the rest.
{
  const panels = spec.panels.map(flat);
  const ledger = spec.ledger.map((x) => flat(x.body)).join(' ');
  const ui = readFileSync(join(ROOT, 'site/js/futex-ui.js'), 'utf8');

  // F1. The paper names the call as the unit of the +N, so it is not silent.
  check('Drepper calls the +N the additional cost for the function call',
    SRC.drepper !== null && SRC.drepper.includes('represents the additional cost for the function call'));
  check('so no sentence says the paper is silent on what the first number counts',
    ![...panels, ledger].some((s) => /first number[^.]*(paper|he) does not say|does not say what its first number/i.test(s))
      && !/does not say what its first number/.test(ui), panels[3].slice(0, 120));
  check('and the page names the whole-call reading, under which two columns are one short',
    /points to the whole call/.test(panels[3]) && /one atomic short/.test(ledger) && ui.includes('one atomic short'));
  // Under one count, how many columns fall short is arithmetic.
  const rd = F.readings();
  const short = new Set(rd.filter((x) => x.printed !== x.whole).map((x) => x.id));
  check('and two of the three columns are short of the whole call, by one each',
    short.size === 2 && rd.filter((x) => short.has(x.id)).every((x) => x.whole - x.printed === 1),
    [...short].join(', '));

  // F2. The load-time row says what was measured, not which count the paper used.
  const row = F.verify().find((n) => /not under one count/.test(n.claim));
  check('the load-time row on the atomic cells says each column equals a count, not that it counts it',
    row && !/column counts the|two count up to/.test(row.claim) && /equals the whole call/.test(row.claim),
    row ? row.claim : 'no such row');

  // F3. Step 1's counter stops instead of wrapping, and the page says where.
  const c3 = F.census('mutex', 3, { noWrap: true });
  const top = c3.graph.width - 1;
  check('step 1 at three threads reaches the top of the counter',
    Math.max(...c3.values) === top, `${Math.max(...c3.values)} of ${top}`);
  check('and the count depends on it: a wider counter reaches more states',
    F.census('mutex', 3, { noWrap: true, width: 32 }).states > c3.states);
  check('so the ledger names the stop with the engine\'s own number',
    ledger.includes(`it reaches ${top} and stops`) && /sixteen values and does not wrap/.test(ledger)
      && c3.graph.width === 16);
  check('and the step-1 sentence names it when it is reached',
    ui.includes('" Here the counter climbs to " + top + " and stops there instead of wrapping "')
      && ui.includes('var stopped = c.values[c.values.length - 1] === top;'));
}

/* ---- 9. break it on purpose -------------------------------------------------- */
{
  const src = readFileSync(ENGINE, 'utf8');
  const cases = [
    ['a futex_wait that sleeps without checking the word',
     ['        if (s.val === want) {', '        if (true) {']],
    ['an unlock that never wakes anybody',
     ['        for (var j = 0; j < s.pc.length; j += 1) {\n          if (!s.sleep[j]) continue;',
      '        for (var j = 0; j < 0; j += 1) {\n          if (!s.sleep[j]) continue;']],
    ['the second mutex retaking with 1',
     ['        { k: "rmw", f: cmpxchg(0, 2), op: "cmpxchg (val, 0, 2)",',
      '        { k: "rmw", f: cmpxchg(0, 1), op: "cmpxchg (val, 0, 2)",']],
    ['a first mutex whose unlock checks for waiters it cannot see',
     ['        { k: "store", then: 3 },\n        { k: "wake", then: REM }',
      '        { k: "store", then: REM },\n        { k: "wake", then: REM }']],
    ['a closed form off by one', ['return Math.pow(2, width) - 2;', 'return Math.pow(2, width) - 1;']],
    ['a transcription with mutex3\'s lower number wrong',
     ['lock: { atomic: [{ upper: 1, lower: 2 }, 1]', 'lock: { atomic: [{ upper: 1, lower: 3 }, 1]']],
    ['a counter that never wraps', ['  function inc(v, c, w) { return { v: (v + 1) % w, old: v }; }',
      '  function inc(v, c, w) { return { v: Math.min(v + 1, w - 1), old: v }; }']],
  ];
  for (const [label, [from, to]] of cases) {
    if (!src.includes(from)) {
      check(`${label} is caught by the page itself`, false, 'the mutation did not match the engine, so nothing was tested');
      continue;
    }
    let bad;
    try {
      bad = engine(src.replace(from, to)).verify().filter((n) => !n.ok);
    } catch (e) {
      check(`${label} is caught by the page itself`, false, `verify() threw instead of returning a failed row: ${e.message}`);
      continue;
    }
    check(`${label} is caught by the page itself`, bad.length > 0, `${bad.length} claim(s) go red`);
  }
  check('an unmutated copy still passes every one of its own checks', engine(src).verify().every((n) => n.ok));
}

const FLOOR = 120;
check(`at least ${FLOOR} checks ran`, p + f >= FLOOR, String(p + f));
console.log(`\nfutex: ${p} passed, ${f} failed. Two model checkers in two languages agree on every `
  + 'count; the paper\'s tables are parsed from the archive; and every real lock call within the model\'s horizon '
  + 'cost something the model can reach.');
process.exit(f ? 1 : 0);