gridlock

The four-way-junction deadlock and the Kubernetes namespace deadlock are the same theorem.

Certify that a wait-for relation cannot wedge — and get the concrete cycle when it can.

pip install gridlock

Why this exists

Every domain that has holders waiting on resources rediscovers deadlock, and rediscovers the same fix, under a different name. Dimension-ordered routing. Lock ordering. Yield-to-the-right. Customer-provider preference hierarchies. Egress policy tiers. They are all one argument:

Absence of a wedged state follows from acyclicity of the wait-for relation together with a rank that strictly decreases on every drain step.

gridlock states that argument once and instantiates it in seven unrelated domains, each with a foil that actually wedges. The foils are the point — a certifier that returned SAFE for everything would satisfy the safe cases too.

Install

pip install gridlock        # zero runtime dependencies

30-second quickstart

gridlock domains                    # what's built in
gridlock demo kubernetes            # one domain: safe case + foil
gridlock demo                       # all seven
echo '{"a":["b"],"b":["a"]}' > g.json && gridlock check g.json

Worked example — your own graph

$ echo '{"a": ["b"], "b": ["c"], "c": []}' > safe.json
$ gridlock check safe.json
SAFE — no reachable wedged state
  nodes ............... 3
  wait-for edges ...... 2
  drains (can proceed)  c
  rank strictly decreases on every edge: yes
  max rank ............ 2

$ echo '{"a": ["b"], "b": ["a"]}' > wedged.json
$ gridlock check wedged.json
WEDGES — a cycle exists
  nodes ............... 2
  wait-for edges ...... 2
  cycle ............... a -> b -> a
  every holder in that cycle waits on the next; none can ever proceed

Exit 0 when safe, 1 when wedged — so it drops into a pipeline, though gridlock itself decides nothing (see below).

Worked example — the same theorem in seven domains

$ gridlock demo
=== kubernetes — Container-orchestrated workloads across namespaces
    waiting means: a workload waits on a service in another namespace
    SAFE arrangement -> SAFE   (5 nodes, 4 edges)
    FOIL             -> WEDGES as intended: ns-api/svc -> ns-data/db -> ns-api/svc
       (an open egress policy lets the data tier call back into the API tier)

=== noc — On-chip interconnect routing
    waiting means: a channel waits on the next channel in the route
    SAFE arrangement -> SAFE   (4 nodes, 3 edges)
    FOIL             -> WEDGES as intended: ch(0,0)->(1,0) -> ch(1,0)->(1,1) -> ch(1,1)->(0,1) -> ch(0,1)->(0,0) -> ch(0,0)->(1,0)
       (adaptive routing permits a Y hop before an X hop, closing the ring)

=== vehicles — Coordinated autonomous vehicles
    waiting means: a vehicle yields to another vehicle
    SAFE arrangement -> SAFE   (4 nodes, 3 edges)
    FOIL             -> WEDGES as intended: east -> south -> west -> north -> east
       (a four-way junction where everyone yields to the right)

...

RESULT: every domain certifies safe and every foil fires

The seven: kubernetes, noc, pipeline, vehicles, warehouse, routing-policy, agent-tools.

Library use

from gridlock import WaitForGraph, certify

g = WaitForGraph.from_mapping({
    "ns-web/pod": ["ns-api/svc"],
    "ns-api/svc": ["ns-data/db"],
    "ns-data/db": [],
})

cert = certify(g, domain="kubernetes")
cert.safe            # True
cert.rank            # {'ns-data/db': 0, 'ns-api/svc': 1, 'ns-web/pod': 2}
cert.drains          # ['ns-data/db']
cert.to_dict()       # JSON-serialisable certificate

g.add("ns-data/db", "ns-api/svc")     # the foil
certify(g).cycle     # ['ns-api/svc', 'ns-data/db', 'ns-api/svc']

What it actually guarantees

• Cycle detection is exact, not sampled or heuristic — iterative depth-first search with explicit colour marking. Iterative rather than recursive, so a 5,000-node chain does not blow the interpreter stack. A certifier that crashes on large inputs silently stops covering them.
• The rank is verified, not asserted. certify computes the longest-outgoing-path rank and then checks rank[a] > rank[b] on every edge before reporting rank_is_strictly_decreasing.
• Every foil fires. The test suite asserts, per domain, that the foil is refused. A foil that stopped firing would make its domain's safe case vacuous, and the suite fails.

Honest limits — read before you rely on a SAFE verdict

• You supply the graph. gridlock is a decision procedure over a finite, explicit wait-for relation. It does not infer that relation from your source code, and it cannot — extracting a sound wait-for graph from a real program is the hard part, and it is out of scope.
• Therefore a SAFE verdict is a statement about the graph you gave it. If your graph is wrong or incomplete, the verdict is worthless. Garbage in, certified garbage out.
• The seven domains are illustrations of the argument, not models of any particular production system. kubernetes is a five-node sketch, not a cluster analyser.
• Acyclicity rules out circular wait. It does not address livelock, starvation, priority inversion, or timeouts.

An empty graph ABSTAINS — it does not pass

$ echo '{}' | tee empty.json && gridlock check empty.json
ABSTAIN — nothing to certify
  The graph has ZERO nodes, so there is no wait-for relation to reason about.
  REFUSING to report SAFE: 'no reachable wedged state' is vacuously true over
  an empty system and tells you nothing about yours.
  Most likely your input did not load. Expected a JSON object mapping each
  waiter to the list it waits on, e.g. {"a": ["b"], "b": []}
$ echo $?
2

This is worth stating because the bug was ours. all(...) over an empty edge set is vacuously True in Python, so an earlier version certified a zero-node graph as SAFE — printing "rank strictly decreases on every edge: yes" when there were no edges and no nodes. Nothing had been checked, because there was nothing to check.

Worse, test_empty_graph_is_safe asserted that behaviour as correct, so the test suite could never have caught it. Both are fixed; the test is now inverted rather than deleted, as a marker.

The overwhelmingly likely cause of an empty graph is a config that failed to load or a query that returned no rows — exactly the moment a green tick does the most damage.

code	verdict	meaning
0	SAFE	acyclic, and the rank strictly decreases across every edge
1	WEDGES	a cycle exists; the certificate names it
2	ABSTAIN	there was no graph to certify, or the input could not be read

A graph with nodes but no edges is genuinely SAFE — if nobody waits, nobody is stuck — and it says so, while marking the rank check vacuously true — there are no edges.

What this does not do

gridlock measures. It never admits, refuses, provisions, or actuates — certify returns a certificate and the caller decides. That boundary is deliberate and enforced in CI (see CLAIMS-MAP.md).

If you need the enforcing side — an admission gate that refuses to grant a resource when the grant would close a cycle, instantiated for your domain and carrying a machine-checked proof — that is a separate, commercially licensed product. See CLAIMS-MAP.md.

Development

pip install -e ".[dev]"
python -m pytest -q          # 43 tests
gridlock demo                # all seven domains and their foils

License

Apache-2.0. See LICENSE and CONTRIBUTING.md.

Honest scope — what a passing run proves, and what it does not

The two halves are inseparable. A tool that states only the first half is marketing.

It proves:

• that the wait-for graph YOU SUPPLIED is acyclic, with a rank verified edge by edge
• if it is not: the actual cycle, as a path

It does NOT prove:

• that your SYSTEM cannot deadlock — only that the graph you handed it cannot. Extracting a sound wait-for graph from a real program is the hard part and is out of scope
• anything about livelock, starvation, priority inversion or timeouts — acyclicity rules out circular wait and nothing else
• anything at all about an empty graph; that case ABSTAINS

Troubleshooting

you see	what it means and how to fix it
gridlock check empty.json prints ABSTAIN	Your graph has zero nodes — almost always a config that failed to load. Expected {"waiter": ["waited-on"]}.

These strings are checked against the live code by python oss/tools/gen_docs.py --verify, so a changed message cannot leave stale advice behind.

Full CLI reference, generated from --help: docs/CLI.md

---

The rest of the portfolio

Seventeen artifacts, one idea: a measurement you cannot check is a press release. Every tool here reports; none of them gates.

Tools

signoff-cert	certificates that carry their own false-pass bound
honestbench	measure your CI's escape rate
kvprobe	model-substitution detector with a measured FPR
kvleak	cross-tenant leak scanner
gridlock	certify a wait-for relation cannot wedge ← you are here
tokencount	a token count both parties can recompute
formal-proof-mcp	a proof kernel for your coding agent
proof-to-code-drift	fail the build when the proof stops matching
sf-verify	re-derive admission decisions offline

Benchmarks — each recomputes one of our own published numbers from its certificate

illusion-bench	how many broken kernels does your oracle admit?
kv-reuse-econ-bench	recompute our economics headline
llm-tenant-isolation-bench	recompute our isolation figures

Datasets

llm-precision-fingerprints	precision-labelled logprobs with a negative control
kv-tenant-isolation-bench	isolation observations, uninterpretable rows included
kv-reuse-econ-traces	per-workload reuse accounting + the closed form

Try it in a browser — no install, no GPU

tenant-leak-demo	the residency calculator
negative-results-atlas	ten claims we took back

The commercial edition

Everything above is measure-only and Apache-2.0: it tells you what is true and never acts on it. The enforcement side — binding a partition key at the admission decision, the compiled gate corpus, and the certificate-issuing faucet — is covered by filed patents and licensed separately.

Reading is free. Enforcing is licensed.