Spaces:
Running
Running
| <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 <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 " + | |
| "“no deadlock” 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, "&").replace(/</g, "<")}</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> | |