Park and resume

A contract instance can outlive its process. Parking writes the instance’s durable state into one store row; resuming reads the row back in another process and stands the instance up as a live signature. This is what makes a session survive a network partition, a server death, and a supervisor restart, and it is the same mechanism from C, from Python, from inside the language, and over the gRPC bridge.

What parks

geas_instance_park(c, dsn, key) puts everything durable about an instance into one row in the runtime’s own geas_park table in the database behind dsn, created on first use, one INSERT OR REPLACE per key:

• the contract’s name, version, and shape hash
• the lifecycle state and the signing time
• every vow value
• every pledge latch, with the Err payload it carries
• the fate of every transactional episode

Parking is a write, not an ending. The caller still holds a live signature it may keep driving or break. A park is a state between walks, never a snapshot of one mid flight: an instance with an unwaited future or an open transactional episode refuses with GEAS_ERR_STATE. So does an instance an explicit break already ended, since the break reclaimed the heap the vows and payloads live on; an automatically broken instance keeps that heap and parks with its errors readable, because keeping them readable is what the automatic break is for.

What resumes

geas_instance_resume(rt, dsn, key, expected_hash, out) reads the row back and stands the instance up against the current runtime: the contract is found by the recorded name, the vows decode onto the new instance, the latches and their Err payloads replay, a store backed contract reopens its dsn vow and reconciles its schemas exactly as sign does, and the recorded state and signing time land unchanged, so the partial surface reads what the parked instance read.

The new signature is as live as any: pledges still pending fulfill on latches set before the park, and a broken or fulfilled record resumes readable with further fulfillment refused the way it always is. The recorded version and shape hash must match the registered module’s, and a nonzero expected_hash must match as well, else GEAS_ERR_VERSION, the same skew rule sign enforces. A key with no row is GEAS_ERR_NAME. A resumed committed transaction stays committed, so a transactional episode can never run twice, no matter how many times the instance crosses the table.

From every surface

From C the calls are geas_instance_park and geas_instance_resume. From Python the ctypes wrapper carries them as one method each:

run.contract.park(self.dsn, name)

contract = self.runtime.resume(self.dsn, name)

From inside the language, park and resume are builtin contract methods beside sign, status, and partial: instance.park(dsn, key) writes the instance’s durable state and returns Unit with the instance staying live, and Contract.resume(dsn, key) stands a parked instance back up, the signed instance the answer the way sign’s is. The refusals are the same ones the C surface answers.

The one shot token

Over the bridge, a server started with a park store issues every session a park token beside its signature. When a stream ends without an explicit Break, the server parks the instance under that token before dropping the row that backed the stream. Resume takes the token, stands the instance back up under a fresh id on a new stream, and consumes the row, one shot: a spent or unknown token is NOT_FOUND, a lying hash is ABORTED before the row is touched, and a resumed session that later drops parks again under the same token. An explicit Break stays the one true ending, and the token dies with the instance.

Who may resume a token, how often, and for how long is server policy, deliberately outside the runtime: the runtime writes and reads park rows, and the bridge decides what a token is worth.

The delete is the claim

Two replicas may hold one park store, and then the delete is the claim. A Resume stands the instance up and then deletes the row; the delete says how many rows it removed, and only the replica whose delete removed one keeps the instance. When two replicas race the same token they both stand a copy up, but exactly one delete removes the row, so exactly one replica wins. The loser removed nothing, breaks the copy it just built, and answers NOT_FOUND, the same answer a spent token gets, because a token another replica already claimed is spent from where the loser stands.

A lying hash still fails before any of this: the resume that reads the row is refused for a hash that disagrees, and the store is never touched, so a wrong hash stays ABORTED and a lost race stays NOT_FOUND with no way to confuse the two.

The gates prove both claims. One kills the server between the park and the resume and finishes the contract on a fresh server holding the same store; the other stands two replicas over one store, kills the one holding an instance, resumes it on the other, then races both for a single token and demands exactly one win and one NOT_FOUND:

# park, kill the server, resume on a fresh one, finish the contract
make test-grpc-resume

# two replicas, one park store: kill one mid session, resume on the other,
# then race both for a single token and demand exactly one winner
make test-grpc-failover

The worked story: the supervisor

examples/supervisor is a small process supervisor whose service state machine is a contract instance, one instance per run: Signed is starting, Partial is running, Fulfilled is a clean exit, Broken is a crash. The host binds the spawn and the health pass over abstract pledges, and the run record and the crash count live on the store. Park and resume is what lets the supervisor restart without losing the services it watches.

On SIGTERM it parks every running instance into a park store keyed by the service name, one park call per instance, and exits:

def park_all(self):
    with self._runs_lock:
        runs = list(self.running.items())
    for name, run in runs:
        run.contract.park(self.dsn, name)
        print(f"[supervisor] parked {name}", flush=True)
    with self._runs_lock:
        self.running.clear()

The processes themselves survive because each is spawned in its own session with setsid, so it is not in the supervisor’s process group and does not take the signal. Started again with --resume, the supervisor stands each parked instance back up from its key, reads the recorded pid back from the pidfile, and reattaches:

def resume_or_start(self, name, command, resume):
    if not resume:
        return self.sign_fresh(name, command)
    try:
        contract = self.runtime.resume(self.dsn, name)
    except GeasError:
        return self.sign_fresh(name, command)

    self.consume_park(name)
    saved = self.read_pidfile(name)
    if saved is not None and self.alive(saved[0]):
        run = Run(name, command, contract, saved[1])
        run.pid = saved[0]
        with self._runs_lock:
            self.running[name] = run
        print(f"[supervisor] resumed {name} pid {run.pid}", flush=True)
        return run

The supervisor applies the same claim rule the bridge does, at host level: resume reads the row, and the delete makes the successful claim one shot.

def consume_park(self, name):
    """resume reads the row; DELETE makes the successful claim one-shot."""
    with sqlite3.connect(self.dsn) as db:
        db.execute("DELETE FROM geas_park WHERE pkey = ?", (name.encode(),))

A parked instance is still Partial, still running, and the row in the park store is the state between two supervisor lifetimes. A running service never notices its supervisor cycled. The crash count survives the restart too, because it lives in the database, not in the host.

# two services up, one crashes into its budget, one survives a supervisor
# restart through the park store and stops clean into Fulfilled
make test-supervisor

What the example shows is the seam: a host drives a store backed, parkable contract with the five calls it always had, and the service lifecycle falls out of the contract lifecycle for free.