Spaces:

nickh007
/

wait-for-visualiser

Running

File size: 13,907 Bytes

<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>Will it wedge? — wait-for graph visualiser</title>
<style>
  :root {
    --bg: #0f1117; --panel: #171a23; --line: #262b38; --ink: #e6e9f0; --dim: #98a0b3;
    --safe: #35c07f; --wedge: #ff6b6b; --abstain: #f5b544; --accent: #7aa2f7;
    --mono: ui-monospace, SFMono-Regular, "SF Mono", Menlo, Consolas, monospace;
  }
  @media (prefers-color-scheme: light) {
    :root { --bg:#f7f8fa; --panel:#fff; --line:#e2e5ec; --ink:#161922; --dim:#5c6479; }
  }
  * { box-sizing: border-box; }
  body {
    margin: 0; background: var(--bg); color: var(--ink); line-height: 1.55;
    font: 15px/1.55 -apple-system, BlinkMacSystemFont, "Segoe UI", Inter, Roboto, sans-serif;
  }
  .wrap { max-width: 1080px; margin: 0 auto; padding: 32px 20px 64px; }
  h1 { font-size: 26px; margin: 0 0 6px; letter-spacing: -0.01em; }
  .sub { color: var(--dim); margin: 0 0 28px; }
  .grid { display: grid; grid-template-columns: 1fr 1fr; gap: 20px; }
  @media (max-width: 860px) { .grid { grid-template-columns: 1fr; } }
  .panel { background: var(--panel); border: 1px solid var(--line); border-radius: 12px; padding: 18px; }
  label { display: block; font-size: 12px; text-transform: uppercase; letter-spacing: .08em;
          color: var(--dim); margin-bottom: 8px; }
  textarea {
    width: 100%; min-height: 210px; resize: vertical; background: var(--bg); color: var(--ink);
    border: 1px solid var(--line); border-radius: 8px; padding: 12px; font-family: var(--mono);
    font-size: 13px;
  }
  textarea:focus { outline: 2px solid var(--accent); outline-offset: -1px; }
  .examples { display: flex; flex-wrap: wrap; gap: 8px; margin-top: 12px; }
  button {
    background: var(--bg); color: var(--ink); border: 1px solid var(--line); border-radius: 999px;
    padding: 6px 13px; font-size: 13px; cursor: pointer; font-family: inherit;
  }
  button:hover { border-color: var(--accent); color: var(--accent); }
  .verdict { display: flex; align-items: baseline; gap: 12px; margin-bottom: 4px; }
  .badge { font-family: var(--mono); font-size: 22px; font-weight: 700; letter-spacing: .02em; }
  .safe { color: var(--safe); } .wedge { color: var(--wedge); } .abstain { color: var(--abstain); }
  .exit { font-family: var(--mono); font-size: 12px; color: var(--dim); }
  .why { color: var(--dim); font-size: 14px; margin: 6px 0 16px; }
  table { width: 100%; border-collapse: collapse; font-family: var(--mono); font-size: 13px; }
  td { padding: 3px 0; vertical-align: top; }
  td:first-child { color: var(--dim); width: 45%; }
  svg { width: 100%; height: 300px; display: block; margin-top: 14px;
        background: var(--bg); border: 1px solid var(--line); border-radius: 8px; }
  .node text { font-family: var(--mono); font-size: 11px; fill: var(--ink); }
  .note { font-size: 13px; color: var(--dim); border-top: 1px solid var(--line);
          margin-top: 22px; padding-top: 16px; }
  code { font-family: var(--mono); background: rgba(122,162,247,.12); padding: 1px 5px;
         border-radius: 4px; font-size: .92em; }
  a { color: var(--accent); }
  .err { color: var(--wedge); font-family: var(--mono); font-size: 13px; white-space: pre-wrap; }
</style>
</head>
<body>
<div class="wrap">
  <h1>Will it wedge?</h1>
  <p class="sub">
    Paste a wait-for relation — who is waiting on whom — and this exhibits the cycle if one
    exists. Everything runs in your browser; nothing is uploaded.
  </p>

  <div class="grid">
    <div class="panel">
      <label for="in">wait-for graph &nbsp;<span style="text-transform:none;letter-spacing:0">{ waiter: [waited-on] }</span></label>
      <textarea id="in" spellcheck="false"></textarea>
      <div class="examples">
        <button data-ex="safe">acyclic</button>
        <button data-ex="wedge">two-cycle</button>
        <button data-ex="long">long cycle</button>
        <button data-ex="k8s">namespace deadlock</button>
        <button data-ex="empty">empty</button>
        <button data-ex="nowait">nobody waits</button>
      </div>
    </div>

    <div class="panel">
      <div class="verdict">
        <span class="badge" id="badge">—</span>
        <span class="exit" id="exit"></span>
      </div>
      <div class="why" id="why">Paste a graph to begin.</div>
      <table id="stats"></table>
      <div class="err" id="err"></div>
      <svg id="viz" viewBox="0 0 520 300" preserveAspectRatio="xMidYMid meet" aria-label="graph"></svg>
    </div>
  </div>

  <p class="note">
    <strong>Why the empty graph abstains.</strong> A graph with no nodes contains no cycle, so
    “no deadlock” is true — and says nothing whatever about your system. The overwhelmingly likely
    cause of an empty graph is a config that failed to load or a query that returned no rows, and
    answering “your system cannot wedge” to that question is a confident answer nobody earned.
    <code>all(…)</code> over an empty set is <code>True</code>; that is a fact about logic, not
    evidence about software.
    <br><br>
    <strong>“Nobody waits” is different, and it really is safe.</strong> Nodes that exist and wait
    on nothing genuinely cannot deadlock. Collapsing that case into “empty” would throw away a
    correct answer, so it is kept separate.
    <br><br>
    Same check locally, with importers that build the graph from Kubernetes manifests or Python
    source: <code>pip install gridlock</code> then
    <code>gridlock import k8s ./manifests | gridlock check -</code> —
    <a href="https://github.com/nickharris808/gridlock">github.com/nickharris808/gridlock</a>.
    Part of a <a href="https://github.com/nickharris808?tab=repositories">portfolio of verifiers
    that abstain</a> rather than guess.
  </p>
</div>

<script>
const EXAMPLES = {
  safe:  {"web": ["api"], "api": ["db"], "db": []},
  wedge: {"a": ["b"], "b": ["a"]},
  long:  {"a": ["b"], "b": ["c"], "c": ["d"], "d": ["a"], "e": ["a"]},
  k8s:   {"prod/api": ["prod/db"], "prod/db": ["prod/cache"], "prod/cache": ["prod/api"]},
  empty: {},
  nowait: {"alice": [], "bob": [], "carol": []}
};

const $ = id => document.getElementById(id);

/* Exact cycle detection: iterative DFS with colour marking, the same procedure gridlock uses.
   Iterative rather than recursive so a deep graph cannot blow the stack — a checker that
   crashes on large input is a checker that silently stops covering large input. */
function findCycle(edges) {
  const WHITE = 0, GREY = 1, BLACK = 2;
  const colour = {}, parent = {};
  const nodes = Object.keys(edges).sort();
  for (const n of nodes) colour[n] = WHITE;

  for (const root of nodes) {
    if (colour[root] !== WHITE) continue;
    colour[root] = GREY; parent[root] = null;
    const stack = [[root, (edges[root] || []).slice().sort().reverse()]];
    while (stack.length) {
      const top = stack[stack.length - 1];
      if (!top[1].length) { colour[top[0]] = BLACK; stack.pop(); continue; }
      const next = top[1].pop();
      const c = colour[next] === undefined ? WHITE : colour[next];
      if (c === GREY) {
        const cyc = [next];
        let cur = top[0];
        while (cur !== null && cur !== next) { cyc.push(cur); cur = parent[cur]; }
        cyc.push(next); cyc.reverse();
        return cyc;
      }
      if (c === WHITE) {
        colour[next] = GREY; parent[next] = top[0];
        stack.push([next, (edges[next] || []).slice().sort().reverse()]);
      }
    }
  }
  return null;
}

function normalise(raw) {
  const g = {};
  for (const [k, v] of Object.entries(raw)) {
    g[k] = g[k] || [];
    for (const w of v) { g[k].push(String(w)); g[String(w)] = g[String(w)] || []; }
  }
  for (const k of Object.keys(g)) g[k] = [...new Set(g[k])].sort();
  return g;
}

function draw(g, cycle) {
  const svg = $("viz");
  svg.innerHTML = "";
  const nodes = Object.keys(g).sort();
  if (!nodes.length) return;
  const NS = "http://www.w3.org/2000/svg";
  const cx = 260, cy = 150, r = Math.min(110, 40 + nodes.length * 8);
  const pos = {};
  nodes.forEach((n, i) => {
    const a = (2 * Math.PI * i) / nodes.length - Math.PI / 2;
    pos[n] = [cx + r * Math.cos(a), cy + r * Math.sin(a)];
  });

  const inCycle = new Set();
  const cycleEdges = new Set();
  if (cycle) {
    cycle.forEach(n => inCycle.add(n));
    for (let i = 0; i + 1 < cycle.length; i++) cycleEdges.add(cycle[i] + "" + cycle[i + 1]);
  }

  const defs = document.createElementNS(NS, "defs");
  defs.innerHTML =
    '<marker id="ah" viewBox="0 0 10 10" refX="9" refY="5" markerWidth="6" markerHeight="6" orient="auto-start-reverse">' +
    '<path d="M 0 0 L 10 5 L 0 10 z" fill="#98a0b3"/></marker>' +
    '<marker id="ahc" viewBox="0 0 10 10" refX="9" refY="5" markerWidth="6" markerHeight="6" orient="auto-start-reverse">' +
    '<path d="M 0 0 L 10 5 L 0 10 z" fill="#ff6b6b"/></marker>';
  svg.appendChild(defs);

  for (const a of nodes) {
    for (const b of g[a]) {
      if (!pos[b]) continue;
      const hot = cycleEdges.has(a + "" + b);
      const [x1, y1] = pos[a], [x2, y2] = pos[b];
      const dx = x2 - x1, dy = y2 - y1, len = Math.hypot(dx, dy) || 1;
      const line = document.createElementNS(NS, "line");
      line.setAttribute("x1", x1 + (dx / len) * 22); line.setAttribute("y1", y1 + (dy / len) * 22);
      line.setAttribute("x2", x2 - (dx / len) * 26); line.setAttribute("y2", y2 - (dy / len) * 26);
      line.setAttribute("stroke", hot ? "#ff6b6b" : "#98a0b3");
      line.setAttribute("stroke-width", hot ? "2.2" : "1.2");
      line.setAttribute("opacity", hot ? "1" : ".55");
      line.setAttribute("marker-end", hot ? "url(#ahc)" : "url(#ah)");
      svg.appendChild(line);
    }
  }
  for (const n of nodes) {
    const [x, y] = pos[n];
    const gEl = document.createElementNS(NS, "g");
    gEl.setAttribute("class", "node");
    const c = document.createElementNS(NS, "circle");
    c.setAttribute("cx", x); c.setAttribute("cy", y); c.setAttribute("r", 19);
    c.setAttribute("fill", inCycle.has(n) ? "rgba(255,107,107,.18)" : "rgba(122,162,247,.13)");
    c.setAttribute("stroke", inCycle.has(n) ? "#ff6b6b" : "#7aa2f7");
    c.setAttribute("stroke-width", "1.4");
    const t = document.createElementNS(NS, "text");
    t.setAttribute("x", x); t.setAttribute("y", y + 4);
    t.setAttribute("text-anchor", "middle");
    t.textContent = n.length > 9 ? n.slice(0, 8) + "…" : n;
    const title = document.createElementNS(NS, "title");
    title.textContent = n;
    gEl.appendChild(c); gEl.appendChild(t); gEl.appendChild(title);
    svg.appendChild(gEl);
  }
}

function run() {
  const txt = $("in").value.trim();
  const badge = $("badge"), why = $("why"), stats = $("stats"), err = $("err");
  err.textContent = ""; stats.innerHTML = ""; $("viz").innerHTML = "";
  $("exit").textContent = "";

  if (!txt) { badge.textContent = "—"; badge.className = "badge";
              why.textContent = "Paste a graph to begin."; return; }

  let raw;
  try { raw = JSON.parse(txt); }
  catch (e) {
    badge.textContent = "ABSTAIN"; badge.className = "badge abstain";
    $("exit").textContent = "exit 2";
    why.textContent = "That is not valid JSON, so there is no graph to reason about.";
    err.textContent = e.message;
    return;
  }
  if (raw === null || typeof raw !== "object" || Array.isArray(raw)) {
    badge.textContent = "ABSTAIN"; badge.className = "badge abstain";
    $("exit").textContent = "exit 2";
    why.textContent = 'Expected an object mapping each waiter to what it waits on, e.g. {"alice": ["bob"], "bob": []}.';
    return;
  }
  for (const [k, v] of Object.entries(raw)) {
    if (!Array.isArray(v)) {
      badge.textContent = "ABSTAIN"; badge.className = "badge abstain";
      $("exit").textContent = "exit 2";
      why.textContent = `Key ${JSON.stringify(k)} maps to a ${typeof v}; each value is the list that node is WAITING ON.`;
      return;
    }
  }

  const g = normalise(raw);
  const nodes = Object.keys(g);
  const nEdges = nodes.reduce((s, n) => s + g[n].length, 0);

  if (!nodes.length) {
    badge.textContent = "ABSTAIN"; badge.className = "badge abstain";
    $("exit").textContent = "exit 2";
    why.innerHTML = "There is nothing here to certify. A graph with no nodes has no cycle, so " +
      "&ldquo;no deadlock&rdquo; is <em>true</em> and tells you nothing about your system — " +
      "and an empty graph is far more often a config that failed to load than a system with " +
      "nothing in it.";
    return;
  }

  const cycle = findCycle(g);
  const drains = nodes.filter(n => !g[n].length);
  const rows = [["nodes", nodes.length], ["wait-for edges", nEdges],
                ["drains (can proceed)", drains.length ? drains.join(", ") : "none"]];

  if (cycle) {
    badge.textContent = "WEDGES"; badge.className = "badge wedge";
    $("exit").textContent = "exit 1";
    why.textContent = "Every holder in this cycle waits on the next; none can ever proceed.";
    rows.push(["cycle", cycle.join(" → ")]);
  } else {
    badge.textContent = "SAFE"; badge.className = "badge safe";
    $("exit").textContent = "exit 0";
    why.textContent = nEdges === 0
      ? "Nodes exist and none waits on another. That is a real result: a system where nobody waits cannot wedge."
      : "Acyclic, and a rank strictly decreases along every edge — so no set of these holders can be stuck waiting on each other.";
  }
  stats.innerHTML = rows.map(([a, b]) =>
    `<tr><td>${a}</td><td>${String(b).replace(/&/g, "&amp;").replace(/</g, "&lt;")}</td></tr>`).join("");
  draw(g, cycle);
}

document.querySelectorAll("button[data-ex]").forEach(b =>
  b.addEventListener("click", () => {
    $("in").value = JSON.stringify(EXAMPLES[b.dataset.ex], null, 2);
    run();
  }));
$("in").addEventListener("input", run);
$("in").value = JSON.stringify(EXAMPLES.k8s, null, 2);
run();
</script>
</body>
</html>