NEO.K / MSSP FIELD LAB012-two-writers
編號012-two-writers
語言javascript
版本v1.0
日期2026-08-12
行數577
執行node src/main.mjs

012 — Two writers, and the schedule the test could not produce

candidate. This is the limitation example 011 named for itself, gone after the next day.

What this program does

Two writers increment the same counter. A schedule decides who moves next — and it is written down rather than raced for, so what happens is a fact about the code and not about this machine this morning.

node src/main.mjs             # what SCL runs, plus the combination it refuses
node src/main.mjs --all       # every medium x operation x schedule
node src/main.mjs --strict    # exit 1 when a requirement is unmet
node src/island_test.mjs      # 28 checks across 7 sections
$ node src/main.mjs --all

  medium        operation           schedule                ends at   lost   was anybody told?
  atomic-file   compare-and-set     interleaved             1         1      yes, refused
  atomic-file   compare-and-set     one-at-a-time           2         -      -
  atomic-file   compare-and-set     interleaved + retry     2         -      -
  atomic-file   read-modify-write   interleaved             1         1      NO, silently
  atomic-file   read-modify-write   one-at-a-time           2         -      -
  atomic-file   read-modify-write   interleaved + retry     1         1      NO, silently
  torn-file     compare-and-set     interleaved             1         1      yes, refused
  torn-file     read-modify-write   interleaved             1         1      NO, silently

The structural decision

An operation declares what it REQUIRES; a medium declares what it GUARANTEES; the store compares them and fails closed.

  !! read-modify-write requires serialised-transaction; atomic-file guarantees atomic-replace - fail closed

The consequence is the point: no medium here provides serialised-transaction, and none can. A read-modify-write needs nothing to happen between its read and its write, and that is not a property of a medium — it is a property of a transaction. So the repair is the shape of the operation, not a better medium.

Three things the table says that the numbers alone do not

1. The medium column changes nothing. atomic-file and torn-file agree on every row. Atomicity of a write is a real guarantee and it is not the one a read-modify-write needs — measured, not argued:

  PASS  atomic-file and torn-file give identical outcomes under the same schedule

The archaeology filed the same day found exactly this upstream: dbm.dumb and dbm.sqlite3 both lose the update; only dbm.dumb corrupts.

2. The two interleaved rows end at the same number. read-modify-write and compare-and-set both leave the counter at 1. What differs is that one of them said so:

  PASS  read-modify-write and compare-and-set end at the same value - both 1
  PASS  and only one of them reported anything
  PASS  retrying fixes the one that reported - ends at 2
  PASS  and does nothing for the one that did not - there was nothing to retry, because nobody was told

Compare-and-set does not make the second increment happen. It refuses, and a refusal is worth exactly as much as somebody's willingness to retry.

3. Every one-at-a-time row is clean. That is the control, and it is the methodological finding.

The island test — section 4 is a control, not an assertion

  PASS  all 4 one-at-a-time runs end at 2 with nothing lost - 2, 2, 2, 2
  PASS  all 4 interleaved runs lose one - 1, 1, 1, 1
  PASS  so the schedule, not the assertion, is what decides whether this is visible

A single-writer test cannot see a lost update, however many assertions it makes. This is a different axis from the ones mssp-d-003 has collected. Those ask what an observation can distinguish and which event it is about. This one asks what the test is able to produce at all — and no assertion can rescue a schedule that never happens.

Section 6 checks the atomicity claim by running it rather than reading it: a medium claiming atomic-replace must complete a write in one step, and the island test interleaves inside a write to find there is no inside. torn-file is the control, and it is observably torn:

  PASS  and torn-file is observably torn halfway through a write - halfway: "{\"n\":1"

What this example does not solve

Measurable, not measured. What retries cost under real contention, and how often a real application's writes actually overlap.

Not measurable here. Whether these two schedules cover what a real scheduler produces. Two are written down; a system with more steps has more of them, and nothing here enumerates that space. This is the honest limit of the whole approach in this entry — a written-down schedule proves a failure exists, and proves nothing about the ones nobody wrote down.

And whether compare-and-set is the right repair. It converts a lost update into a retry, which is a different problem rather than no problem.

Source

FMS

FMS/contract.json
{
  "name": "012-two-writers",
  "what_it_is": "The store from example 011 with a second writer, and the vocabulary that lets a mismatch be refused before an interleaving finds it.",
  "the_structural_decision": "An operation declares what it REQUIRES of the medium; a medium declares what it GUARANTEES; the store compares them and fails closed. The consequence that matters: read-modify-write requires a serialised transaction, which is not a property any medium has — so the repair is the shape of the operation, not a better medium.",
  "why_now": "Example 011 named this itself: one process, one writer, and two writers would break it while nothing noticed. That sentence was the limitation section of an entry published yesterday, and the switch to real market applications is eight days away.",
  "status": "candidate",

  "guarantees": {
    "atomic-replace": "a write completes in one step; nothing can be scheduled inside it",
    "serialised-transaction": "nothing else writes between a read and its write. NO MEDIUM HERE PROVIDES THIS, and that is the finding rather than an omission"
  },

  "media": {
    "atomic-file": {"guarantees": ["atomic-replace"], "how": "write to a staging name, rename over the target"},
    "torn-file": {"guarantees": [], "how": "write the record in two halves", "why_it_exists": "the control. Without a medium whose atomicity claim is false, the section checking atomicity cannot come out badly."}
  },

  "operations": {
    "read-modify-write": {"requires": ["serialised-transaction"], "note": "the shape everyone writes"},
    "compare-and-set": {"requires": ["atomic-replace"], "note": "the same intent with a requirement a medium can actually meet"}
  },

  "the_finding": "Locking and lost updates are two different guarantees, and both get called safe for concurrent use. Measured in archaeology 012 the same day: dbm.dumb and dbm.sqlite3 BOTH lose an update under the same written-down schedule; only dbm.dumb corrupts. Real locking buys integrity and buys nothing at all on lost updates.",

  "the_methodological_finding": "A single-writer test cannot observe a lost update no matter how many assertions it makes. This is not about how many values a check can read or which event they are about — it is about which SCHEDULES the test is able to produce. Section 4 is that control.",

  "sets": {
    "FMS": "this file: the guarantee vocabulary, what each medium and operation declares, and the compatibility rule",
    "SCL": "which medium and operation this deployment runs, and whether an unmet requirement is fatal",
    "SMS": "resolution by id, the requirement comparison, and the schedule harness",
    "TMS": "one file per medium and per operation - each declares what it guarantees or requires, and reaches no sibling set",
    "DMS": "the traces, the final values, and what none of it can see"
  },

  "non_goals": [
    "Being a database or a lock manager. Two media, two operation shapes, and a written-down schedule.",
    "Racing. There are no threads here; a schedule is chosen so the result is a fact about the code rather than about this machine's timing. Archaeology 012 runs the same schedule against real CPython backends, which is what stops the model from agreeing with itself.",
    "Claiming compare-and-set is the answer. It converts a lost update into a retry, and this example does not measure what retries cost under contention."
  ]
}

SCL

SCL/policy.json
{
  "medium": "atomic-file",
  "operation": "compare-and-set",
  "unmet_requirement_is_fatal": true,
  "_note": "island_test.mjs runs every medium and operation regardless of what this says, including the combinations this policy refuses. A policy able to silence the comparison would make the comparison worthless."
}
SCL/policy.mjs
// Which medium and operation this deployment runs, and what it refuses to ship.
import fs from "node:fs";
import path from "node:path";
import { fileURLToPath } from "node:url";

const here = path.dirname(fileURLToPath(import.meta.url));
const config = JSON.parse(fs.readFileSync(path.join(here, "policy.json"), "utf8"));

export const medium = () => config.medium;
export const operation = () => config.operation;
export const unmetIsFatal = () => Boolean(config.unmet_requirement_is_fatal);

SMS

SMS/schedule.mjs
// The interleaving is written down, not raced for.
//
// No threads and no timing. A schedule is a list of which writer moves next, so
// a lost update here is a fact about the code rather than about this machine on
// this morning. Archaeology 012 runs the same schedule against real CPython dbm
// backends, which is what stops this from being a model agreeing with itself.

export function run(writers, order) {
  const cursors = writers.map(() => 0);
  const trace = [];
  for (const who of order) {
    const step = writers[who]?.[cursors[who]];
    if (!step) continue;
    cursors[who] += 1;
    trace.push({ who, ...step() });
  }
  // Anything the schedule did not reach still has to finish, in writer order.
  for (const [who, steps] of writers.entries()) {
    while (cursors[who] < steps.length) {
      trace.push({ who, ...steps[cursors[who]++]() });
    }
  }
  return trace;
}

// Re-run whoever was refused, one at a time, until nobody is.
//
// The first version of this looped on the WHOLE accumulated trace, so the
// original refusals never stopped satisfying the condition and it retried until
// the budget ran out - two increments ended at five. Only the newest round can
// answer "is anyone still being refused".
export function runWithRetries(makeWriters, order, budget = 5) {
  let round = run(makeWriters(), order);
  const trace = [...round];
  let rounds = 1;
  while (round.some((step) => step.retry) && rounds < budget) {
    const refused = [...new Set(round.filter((step) => step.retry).map((step) => step.who))];
    const writers = makeWriters();
    // An empty order means the drain runs each of them to completion in turn,
    // which is what a retry after a conflict actually is.
    round = run(refused.map((who) => writers[who]), []);
    trace.push(...round);
    rounds += 1;
  }
  return { trace, rounds };
}

// Two named schedules. The second is the control: it is what a test with a
// single writer produces, and it is why such a test cannot see any of this.
export const INTERLEAVED = [0, 1, 0, 1, 0, 1];
export const ONE_AT_A_TIME = [0, 0, 0, 1, 1, 1];
SMS/store.mjs
// The store: resolve a medium and an operation by id, and refuse a mismatch.
//
// The one rule this example adds: an operation declares what it REQUIRES, a
// medium declares what it GUARANTEES, and the store compares them before
// anything runs. A requirement nothing provides is refused rather than
// discovered by an interleaving in production.
import * as atomicFile from "../TMS/media/atomic_file.mjs";
import * as tornFile from "../TMS/media/torn_file.mjs";
import * as compareAndSet from "../TMS/operations/compare_and_set.mjs";
import * as readModifyWrite from "../TMS/operations/read_modify_write.mjs";

const MEDIA = Object.fromEntries(
  [atomicFile, tornFile].map((module) => [module.MEDIUM, module]));
const OPERATIONS = Object.fromEntries(
  [readModifyWrite, compareAndSet].map((module) => [module.OPERATION, module]));

export const mediaNames = () => Object.keys(MEDIA).sort();
export const operationNames = () => Object.keys(OPERATIONS).sort();

export function resolveMedium(name) {
  const module = MEDIA[name];
  if (!module) return { problem: `medium "${name}" has no implementation - fail closed (known: ${mediaNames().join(", ")})` };
  return { module };
}

export function resolveOperation(name) {
  const module = OPERATIONS[name];
  if (!module) return { problem: `operation "${name}" has no implementation - fail closed (known: ${operationNames().join(", ")})` };
  return { module };
}

// The comparison. Two declarations, and the one thing that makes it more than
// two labels agreeing is that section 5 of the island test proves each of them
// against behaviour before this is consulted.
export function unmetRequirements(operation, medium) {
  return operation.REQUIRES.filter((need) => !medium.GUARANTEES.includes(need));
}

export function open({ mediumName, operationName, dir, allowUnmet = false }) {
  const medium = resolveMedium(mediumName);
  if (medium.problem) return { problem: medium.problem };
  const operation = resolveOperation(operationName);
  if (operation.problem) return { problem: operation.problem };

  const unmet = unmetRequirements(operation.module, medium.module);
  if (unmet.length && !allowUnmet) {
    return {
      problem: `${operationName} requires ${unmet.join(", ")}; ${mediumName} guarantees `
        + `${medium.module.GUARANTEES.join(", ") || "nothing"} - fail closed`,
      unmet,
    };
  }

  const handle = medium.module.make({ dir });
  return {
    unmet,
    store: {
      medium: mediumName,
      operation: operationName,
      seed(key, record) { for (const write of handle.writeSteps(key, JSON.stringify(record))) write(); },
      read(key) { const raw = handle.read(key); return raw === null ? null : JSON.parse(raw); },
      raw: (key) => handle.read(key),
      // A writer is not run here. It is a list of steps, so a schedule decides
      // when each one happens.
      writer: (key, change) => operation.module.steps(handle, key, change),
    },
  };
}

TMS

TMS/media/atomic_file.mjs
// A medium whose write is one step, because it writes elsewhere and renames.
//
// "Atomic" here is not a label: a write() returns the steps it takes, and this
// one returns exactly one. The island test interleaves INSIDE a write and finds
// there is no inside. A medium that claimed this and returned two steps would
// be caught by that, not by anyone reading this comment.
import fs from "node:fs";
import path from "node:path";

export const MEDIUM = "atomic-file";
export const GUARANTEES = ["atomic-replace"];

export function make({ dir }) {
  fs.mkdirSync(dir, { recursive: true });
  const file = (key) => path.join(dir, `${encodeURIComponent(key)}.json`);
  return {
    read: (key) => (fs.existsSync(file(key)) ? fs.readFileSync(file(key), "utf8") : null),
    // One step. The temporary file and the rename happen together or not at all.
    writeSteps: (key, value) => [() => {
      const staging = `${file(key)}.${process.pid}.tmp`;
      fs.writeFileSync(staging, value, "utf8");
      fs.renameSync(staging, file(key));
    }],
  };
}
TMS/media/torn_file.mjs
// A medium that writes in two steps, and says so.
//
// It is here as the control. Without a medium whose atomicity claim is FALSE,
// the section that checks atomicity cannot come out badly - the same reason
// example 011 keeps a medium whose persistence claim is false.
import fs from "node:fs";
import path from "node:path";

export const MEDIUM = "torn-file";
export const GUARANTEES = [];

export function make({ dir }) {
  fs.mkdirSync(dir, { recursive: true });
  const file = (key) => path.join(dir, `${encodeURIComponent(key)}.json`);
  return {
    read: (key) => (fs.existsSync(file(key)) ? fs.readFileSync(file(key), "utf8") : null),
    // Two steps. Anything scheduled between them sees half a record.
    writeSteps: (key, value) => {
      const half = Math.ceil(value.length / 2);
      return [
        () => fs.writeFileSync(file(key), value.slice(0, half), "utf8"),
        () => fs.appendFileSync(file(key), value.slice(half), "utf8"),
      ];
    },
  };
}
TMS/operations/compare_and_set.mjs
// Read, change, and write back only if nothing moved underneath.
//
// It needs one thing from the medium - that a replace is a single step - and
// nothing from a transaction. That is the whole difference: the requirement
// shrank to something a medium can actually provide.
//
// What it does NOT do is make the second writer's increment happen. It refuses,
// and a refusal is only worth something if somebody retries. The final value
// under one interleaving is the same as read-modify-write's; what differs is
// that here someone was told.
export const OPERATION = "compare-and-set";
export const REQUIRES = ["atomic-replace"];

export function steps(medium, key, change) {
  let seen = null;
  let next = null;
  return [
    () => { seen = medium.read(key); return { step: "read" }; },
    () => { next = JSON.stringify(change(JSON.parse(seen))); return { step: "modify" }; },
    () => {
      // The comparison and the write are one step, which is what atomic-replace
      // buys. If the medium moved, this attempt is abandoned and reported.
      if (medium.read(key) !== seen) return { step: "compare+write", retry: true };
      for (const write of medium.writeSteps(key, next)) write();
      return { step: "compare+write", retry: false };
    },
  ];
}
TMS/operations/read_modify_write.mjs
// Read the record, change it, write it back.
//
// The shape everyone writes. It requires that nothing else writes between the
// read and the write, which is not a property any medium has - it is a property
// of a transaction. Declaring the requirement is what makes the mismatch
// visible before an interleaving does.
export const OPERATION = "read-modify-write";
export const REQUIRES = ["serialised-transaction"];

export function steps(medium, key, change) {
  let held = null;
  return [
    () => { held = JSON.parse(medium.read(key)); return { step: "read" }; },
    () => { held = change(held); return { step: "modify" }; },
    () => {
      for (const write of medium.writeSteps(key, JSON.stringify(held))) write();
      return { step: "write", retry: false };
    },
  ];
}

DMS

DMS/report.mjs
// The traces, the final values, and what nothing here is watching.

export function outcome(rows, out) {
  out(`\n  ${"medium".padEnd(13)} ${"operation".padEnd(19)} ${"schedule".padEnd(23)} `
    + `${"ends at".padEnd(9)} ${"lost".padEnd(6)} was anybody told?`);
  for (const row of rows) {
    const lost = row.expected - row.final;
    out(`  ${row.medium.padEnd(13)} ${row.operation.padEnd(19)} ${row.schedule.padEnd(23)} `
      + `${String(row.final).padEnd(9)} ${(lost === 0 ? "-" : String(lost)).padEnd(6)} `
      + `${lost === 0 ? "-" : (row.reported ? "yes, refused" : "NO, silently")}`);
  }
}

export function trace(steps, out) {
  out("\n  what actually happened, step by step:");
  for (const step of steps) out(`    writer ${step.who}  ${step.step}${step.retry ? "  -> refused, retry" : ""}`);
}

export function gaps(out) {
  out("\n  measurable, not measured here:");
  out("    - what retries cost under real contention");
  out("    - how often a real application's writes actually overlap");
  out("\n  not measurable by this program at all:");
  out("    - whether any schedule a real scheduler produces is covered. The two");
  out("      here are written down; a system with more steps has more of them,");
  out("      and nothing in this example enumerates that space.");
  out("    - whether compare-and-set is the right repair. It converts a lost");
  out("      update into a retry, which is a different problem, not no problem.");
}

root

island_test.mjs
// The island test.
//
//   node src/island_test.mjs
//
// Section 4 is the one this example exists for, and it is a control rather than
// an assertion: the same operations under a single-writer schedule are clean
// everywhere in the table. A test that can only produce one schedule cannot see
// a lost update, however many assertions it makes.
import fs from "node:fs";
import os from "node:os";
import path from "node:path";
import { fileURLToPath } from "node:url";

import * as schedule from "./SMS/schedule.mjs";
import * as store from "./SMS/store.mjs";
import { runOnce } from "./main.mjs";

const here = path.dirname(fileURLToPath(import.meta.url));
const CONTRACT = JSON.parse(fs.readFileSync(path.join(here, "FMS", "contract.json"), "utf8"));
const failures = [];

const check = (label, ok, detail = "") => {
  process.stdout.write(`  ${ok ? "PASS" : "FAIL"}  ${label}${detail ? ` - ${detail}` : ""}\n`);
  if (!ok) failures.push(label);
};
const say = (line = "") => process.stdout.write(`${line}\n`);
const tempDir = () => fs.mkdtempSync(path.join(os.tmpdir(), "mssp-012-"));

say("\n== 1. every TMS unit is an island and declares its side of the contract");
for (const kind of ["media", "operations"]) {
  const dir = path.join(here, "TMS", kind);
  const files = fs.readdirSync(dir).filter((n) => n.endsWith(".mjs")).sort();
  check(`there are two ${kind} files`, files.length === 2, files.join(", "));
  for (const file of files) {
    const source = fs.readFileSync(path.join(dir, file), "utf8");
    const reaches = [...source.matchAll(/^\s*import[^"']*["']([^"']+)["']/gm)].map((m) => m[1]);
    const siblings = reaches.filter((spec) => /\.\.\/|FMS|SCL|SMS|DMS/.test(spec));
    check(`${file} reaches no sibling set`, siblings.length === 0,
      reaches.join(", ") || "no imports at all");
  }
}
for (const name of store.mediaNames()) {
  const { module } = store.resolveMedium(name);
  check(`${name} declares what it guarantees`, Array.isArray(module.GUARANTEES),
    JSON.stringify(module.GUARANTEES));
}
for (const name of store.operationNames()) {
  const { module } = store.resolveOperation(name);
  check(`${name} declares what it requires`, module.REQUIRES.length > 0,
    JSON.stringify(module.REQUIRES));
}

say("\n== 2. a requirement nothing provides is refused before anything runs");
const refused = store.open({
  mediumName: "atomic-file", operationName: "read-modify-write", dir: tempDir() });
check("read-modify-write on any medium is refused", Boolean(refused.problem), refused.problem);
check("and no store is handed back", refused.store === undefined);
const allowed = store.open({
  mediumName: "atomic-file", operationName: "compare-and-set", dir: tempDir() });
check("compare-and-set on atomic-file is allowed", Boolean(allowed.store),
  `unmet: ${JSON.stringify(allowed.unmet)}`);
const mismatched = store.open({
  mediumName: "torn-file", operationName: "compare-and-set", dir: tempDir() });
check("compare-and-set on torn-file is refused - it needs atomic-replace",
  Boolean(mismatched.problem), mismatched.problem);
for (const [label, args] of [
  ["an unknown medium", { mediumName: "redis", operationName: "compare-and-set", dir: tempDir() }],
  ["an unknown operation", { mediumName: "atomic-file", operationName: "upsert", dir: tempDir() }],
]) {
  check(`${label} stops the run`, Boolean(store.open(args).problem), store.open(args).problem);
}

say("\n== 3. the medium column changes nothing, which is the point");
const byMedium = {};
for (const mediumName of store.mediaNames()) {
  byMedium[mediumName] = store.operationNames().map((operationName) => {
    const row = runOnce(mediumName, operationName, "interleaved");
    return `${operationName}:${row.final}:${row.reported}`;
  }).join(" | ");
}
check("atomic-file and torn-file give identical outcomes under the same schedule",
  new Set(Object.values(byMedium)).size === 1, Object.values(byMedium)[0]);
say("        Atomicity of a write is a real guarantee. It is not the guarantee a");
say("        read-modify-write needs, and no amount of it will be.");

say("\n== 4. THE CONTROL: a single-writer schedule sees none of this");
const oneAtATime = [];
const interleaved = [];
for (const mediumName of store.mediaNames()) {
  for (const operationName of store.operationNames()) {
    oneAtATime.push(runOnce(mediumName, operationName, "one-at-a-time"));
    interleaved.push(runOnce(mediumName, operationName, "interleaved"));
  }
}
check(`all ${oneAtATime.length} one-at-a-time runs end at 2 with nothing lost`,
  oneAtATime.every((row) => row.final === 2),
  oneAtATime.map((row) => row.final).join(", "));
check(`all ${interleaved.length} interleaved runs lose one`,
  interleaved.every((row) => row.final === 1),
  interleaved.map((row) => row.final).join(", "));
check("so the schedule, not the assertion, is what decides whether this is visible",
  oneAtATime.every((row) => row.final === 2) && interleaved.every((row) => row.final === 1));

say("\n== 5. two outcomes that end at the same number");
const silent = runOnce("atomic-file", "read-modify-write", "interleaved");
const told = runOnce("atomic-file", "compare-and-set", "interleaved");
check("read-modify-write and compare-and-set end at the same value",
  silent.final === told.final, `both ${silent.final}`);
check("and only one of them reported anything",
  silent.reported !== told.reported,
  `read-modify-write reported=${silent.reported}, compare-and-set reported=${told.reported}`);
const retried = runOnce("atomic-file", "compare-and-set", "interleaved", { retry: true });
const retriedSilently = runOnce("atomic-file", "read-modify-write", "interleaved", { retry: true });
check("retrying fixes the one that reported", retried.final === 2, `ends at ${retried.final}`);
check("and does nothing for the one that did not", retriedSilently.final === 1,
  `ends at ${retriedSilently.final} - there was nothing to retry, because nobody was told`);

say("\n== 6. the atomicity claim is checked by running it, not by reading it");
for (const name of store.mediaNames()) {
  const { module } = store.resolveMedium(name);
  const handle = module.make({ dir: tempDir() });
  const steps = handle.writeSteps("k", '{"n":1}');
  const claimsAtomic = module.GUARANTEES.includes("atomic-replace");
  check(`${name}: declared atomic-replace=${claimsAtomic}, write takes ${steps.length} step(s)`,
    claimsAtomic === (steps.length === 1),
    claimsAtomic ? "one step means nothing can be scheduled inside it" : "two steps, and it says so");
}
// The drill: a medium that claimed atomicity and wrote in two steps must be
// caught by the line above, or that line is a label agreeing with a label.
const liar = { GUARANTEES: ["atomic-replace"], writeSteps: () => [() => {}, () => {}] };
check("a medium claiming atomic-replace with a two-step write would be caught",
  liar.GUARANTEES.includes("atomic-replace") !== (liar.writeSteps().length === 1),
  "declared true, measured two steps");
// And the torn medium is observably torn: schedule something between its steps.
const torn = store.resolveMedium("torn-file").module.make({ dir: tempDir() });
const tornSteps = torn.writeSteps("k", '{"n":123456}');
tornSteps[0]();
const halfway = torn.read("k");
tornSteps[1]();
check("and torn-file is observably torn halfway through a write",
  halfway !== torn.read("k") && halfway.length < torn.read("k").length,
  `halfway: ${JSON.stringify(halfway)}`);

say("\n== 7. what this example does not solve");
say("        MEASURABLE, NOT MEASURED");
say("          - what retries cost under real contention");
say("          - how often a real application's writes actually overlap");
say("        NOT MEASURABLE HERE");
say("          - whether the schedules here cover what a real scheduler produces.");
say("            Two are written down. A system with more steps has more of them,");
say("            and nothing in this example enumerates that space.");
say("          - whether compare-and-set is the right repair. It converts a lost");
say("            update into a retry, which is a different problem, not none.");

say(failures.length ? `\n${failures.length} failure(s)` : "\nall checks passed");
for (const f of failures) say(`  - ${f}`);
process.exit(failures.length ? 1 : 0);
main.mjs
// Two writers, a written-down schedule, and a requirement that is refused.
//
//   node src/main.mjs            what SCL runs, plus the combination it refuses
//   node src/main.mjs --strict   exit 1 when a requirement is unmet
//   node src/main.mjs --all      every medium x operation x schedule
import fs from "node:fs";
import os from "node:os";
import path from "node:path";
import { fileURLToPath } from "node:url";

import * as report from "./DMS/report.mjs";
import * as policy from "./SCL/policy.mjs";
import * as schedule from "./SMS/schedule.mjs";
import * as store from "./SMS/store.mjs";

const here = path.dirname(fileURLToPath(import.meta.url));
const CONTRACT = JSON.parse(fs.readFileSync(path.join(here, "FMS", "contract.json"), "utf8"));
const tempDir = () => fs.mkdtempSync(path.join(os.tmpdir(), "mssp-012-"));

const SCHEDULES = { interleaved: schedule.INTERLEAVED, "one-at-a-time": schedule.ONE_AT_A_TIME };
const increment = (record) => ({ ...record, n: record.n + 1 });

export function runOnce(mediumName, operationName, scheduleName, { retry = false } = {}) {
  const opened = store.open({ mediumName, operationName, dir: tempDir(), allowUnmet: true });
  if (opened.problem) return { problem: opened.problem };
  const { store: orders } = opened;
  orders.seed("counter", { n: 0 });

  const makeWriters = () => [orders.writer("counter", increment), orders.writer("counter", increment)];
  const { trace } = retry
    ? schedule.runWithRetries(makeWriters, SCHEDULES[scheduleName])
    : { trace: schedule.run(makeWriters(), SCHEDULES[scheduleName]) };
  return {
    medium: mediumName,
    operation: operationName,
    schedule: scheduleName + (retry ? " + retry" : ""),
    expected: 2,
    final: orders.read("counter")?.n ?? null,
    // The measure that separates a refusal from a silent loss. They can end at
    // the same number; only one of them told anybody.
    reported: trace.some((step) => step.retry),
    unmet: opened.unmet,
    trace,
  };
}

function main(argv) {
  const out = (line = "") => process.stdout.write(`${line}\n`);

  if (argv.includes("--all")) {
    const rows = [];
    for (const mediumName of store.mediaNames()) {
      for (const operationName of store.operationNames()) {
        for (const scheduleName of Object.keys(SCHEDULES)) {
          rows.push(runOnce(mediumName, operationName, scheduleName));
        }
        rows.push(runOnce(mediumName, operationName, "interleaved", { retry: true }));
      }
    }
    out("\n== every combination, both schedules");
    report.outcome(rows, out);
    out("\n  Three things this table says that the numbers alone do not:");
    out("    - the medium column changes nothing. atomic-file and torn-file agree");
    out("      on every row, because atomicity of a write is not the guarantee a");
    out("      read-modify-write needs.");
    out("    - the two interleaved rows for one medium END AT THE SAME NUMBER.");
    out("      What differs is whether anybody was told, and a retry is only");
    out("      worth anything to the one that reported.");
    out("    - every one-at-a-time row is clean. A test with a single writer sees");
    out("      nothing here at all, however many assertions it makes.");
    return 0;
  }

  const configured = store.open({
    mediumName: policy.medium(), operationName: policy.operation(), dir: tempDir(),
  });
  out(`\n== what this deployment runs: ${policy.medium()} + ${policy.operation()}`);
  if (configured.problem) {
    out(`  !! ${configured.problem}`);
    return 1;
  }
  const rows = [
    ...Object.keys(SCHEDULES).map((name) => runOnce(policy.medium(), policy.operation(), name)),
    runOnce(policy.medium(), policy.operation(), "interleaved", { retry: true }),
  ];
  report.outcome(rows, out);
  report.trace(rows[0].trace, out);

  out("\n== the combination this deployment refuses, and why");
  const refused = store.open({
    mediumName: policy.medium(), operationName: "read-modify-write", dir: tempDir(),
  });
  out(`  !! ${refused.problem}`);
  const anyway = runOnce(policy.medium(), "read-modify-write", "interleaved");
  out(`     run anyway, interleaved: two increments from 0 end at ${anyway.final}`);
  out(`     ${CONTRACT.guarantees["serialised-transaction"].split(". ")[1]}`);

  report.gaps(out);

  if (argv.includes("--strict") && refused.unmet?.length && policy.unmetIsFatal()) return 1;
  return 0;
}

process.exitCode = main(process.argv.slice(2));