Example: a lease pool object with an alarm
A pool of build runners shared by many projects lives in one SQLite-backed Durable Object. acquire leases the first free runner for five minutes and records the grant for billing; the object's alarm wakes at the next expiry, takes expired leases back and closes their grants. The Worker in front of it asks for a lease and retries a call to the object that failed, with the same token, since a call can fail before it ever reaches the object.
Run the check
From examples/lease-pool in the repository:
pnpm install
pnpm checkThe scenario in leases.sim.ts seeds the object's tables with three free runners, sends two lease requests, and lets the alarm fire in virtual time, so the five-minute expiry takes no time to reach. Every call to the object can fail before it arrives, fail after it committed with the answer lost, or crash the caller after it. The check reports:
VIOLATED leases (seed leases)
Invariant one-runner-per-request is violated: 2 rows of pool/grants in DO:POOL share token = "..."
Schedule (run seed ...), events kept: req-1, req-2
ambiguous at req-2#1 effect #0 (DO:POOL acquire)The object granted the lease and committed it, but its answer was lost. The Worker's retry is right for a call that never arrived and wrong for this one: acquire took the next free runner, and one request now holds two. Ordinary tests never see it, because a call to a Durable Object either succeeds or fails before it starts in every one of them. The trace shows the alarm firing three times afterwards and closing every grant, which the second invariant, every-lease-ends, checks.
The fix
worker.fixed.ts looks up the project's lease before taking a free runner: a call with the same token is a retry and gets its lease back, and a call with another token waits its turn. pnpm check:fixed reports BOUNDED over the same scenario, faults on the alarm included.
Using it in your own project
durableObject clears the namespace before each run; its sql option creates a SQLite-backed object's tables and rows, and durableObjectTable reads one table at the end of the run for state invariants. An alarm fires in virtual time at the time the object set, and a failed alarm is retried on Cloudflare's schedule.
The code
The complete project is examples/lease-pool in the repository.
/**
* A pool of build runners shared by many projects. A Durable Object hands
* out a runner for five minutes, records each grant for billing, and its
* alarm takes expired leases back. The Worker asks the pool for a lease and
* retries a call that failed, with the same token. Run `eutaxy check
* ./leases.sim.ts` to see what the retry does when only the answer was lost.
*/
import { DurableObject } from "cloudflare:workers";
export interface Env {
readonly POOL: DurableObjectNamespace<LeasePool>;
}
export interface Lease {
readonly slot: string;
readonly token: string;
readonly expiresAt: number;
}
export const leaseMs = 5 * 60 * 1000;
export class LeasePool extends DurableObject<Env> {
/** The first free runner, leased to `project` until five minutes from now; null when none is free. */
async acquire(project: string, token: string): Promise<Lease | null> {
const sql = this.ctx.storage.sql;
const free = sql
.exec<{ id: string }>("SELECT id FROM slots WHERE project IS NULL ORDER BY id LIMIT 1")
.toArray()[0];
if (!free) return null;
return this.grant(free.id, project, token);
}
protected async grant(slot: string, project: string, token: string): Promise<Lease> {
const sql = this.ctx.storage.sql;
const now = Date.now();
const expiresAt = now + leaseMs;
sql.exec(
"UPDATE slots SET project = ?, token = ?, expires_at = ? WHERE id = ?",
project,
token,
expiresAt,
slot,
);
sql.exec(
"INSERT INTO grants (token, project, slot, granted_at) VALUES (?, ?, ?, ?)",
token,
project,
slot,
now,
);
const alarm = await this.ctx.storage.getAlarm();
if (alarm === null || expiresAt < alarm) await this.ctx.storage.setAlarm(expiresAt);
return { slot, token, expiresAt };
}
/** Takes back every expired lease, closes its grant, and wakes again for the next expiry. */
override async alarm(): Promise<void> {
const sql = this.ctx.storage.sql;
const now = Date.now();
const expired = sql
.exec<{ id: string; token: string }>(
"SELECT id, token FROM slots WHERE project IS NOT NULL AND expires_at <= ?",
now,
)
.toArray();
for (const { id, token } of expired) {
sql.exec("UPDATE grants SET ended_at = ? WHERE token = ? AND slot = ?", now, token, id);
sql.exec("UPDATE slots SET project = NULL, token = NULL, expires_at = NULL WHERE id = ?", id);
}
const next = sql
.exec<{ at: number | null }>(
"SELECT MIN(expires_at) AS at FROM slots WHERE project IS NOT NULL",
)
.one().at;
if (next !== null) await this.ctx.storage.setAlarm(next);
}
}
export default {
async fetch(request: Request, env: Env): Promise<Response> {
const match = /^\/projects\/([\w-]+)\/lease$/.exec(new URL(request.url).pathname);
if (request.method !== "POST" || !match?.[1]) return new Response("not found", { status: 404 });
const pool = env.POOL.getByName("pool");
const token = crypto.randomUUID();
// One retry: a call can fail before it reaches the pool.
for (let attempt = 1; ; attempt++) {
try {
const lease = await pool.acquire(match[1], token);
return lease ? Response.json(lease) : new Response("no free runner", { status: 409 });
} catch {
if (attempt === 2) return new Response("pool unavailable", { status: 503 });
}
}
},
} satisfies ExportedHandler<Env>;import {
defineScenario,
durableObject,
durableObjectTable,
everyRow,
http,
unique,
} from "eutaxy/cloudflare";
// The pool's tables, as a deployment would create them in a migration, with three free runners.
const pool = {
schema: `
CREATE TABLE slots (id TEXT PRIMARY KEY, project TEXT, token TEXT, expires_at INTEGER);
CREATE TABLE grants (token TEXT NOT NULL, project TEXT NOT NULL, slot TEXT NOT NULL,
granted_at INTEGER NOT NULL, ended_at INTEGER);`,
rows: { slots: [{ id: "r-1" }, { id: "r-2" }, { id: "r-3" }] },
};
const grants = durableObjectTable("POOL", "pool", "grants");
export default defineScenario({
name: "leases",
worker: { entry: "./worker.ts", config: "./wrangler.jsonc" },
// The alarm wakes once per expiry; three requests at most (two, and a retry) need three wake-ups,
// and the cap leaves room for more (a capped alarm would leave a grant open by the bound, not a bug).
setup: [durableObject("POOL", {}, { sql: { pool }, alarmsPerObject: 6 })],
// Two projects ask for a runner; the caller does not resend (the Worker retries the pool itself).
drive: http(
[
{ path: "/projects/p-1/lease", method: "POST" },
{ path: "/projects/p-2/lease", method: "POST" },
],
{ retries: 0 },
),
invariants: [
// One request, one runner: no token is granted twice.
unique("one-runner-per-request", grants, "token"),
// The alarm takes every lease back once it expires, so every grant is closed by the end.
everyRow("every-lease-ends", grants, [{ column: "ended_at", op: "notNull" }]),
],
bounds: { maxFaultsPerRun: 1, maxRedeliveries: 2, maxConcurrentInvocations: 1, budgetMs: 2000 },
});/**
* The same pool, made safe to retry: `acquire` looks for the project's
* lease first and hands it back when the token matches, so a retry after a
* lost answer gets the runner it already holds. `eutaxy check
* ./leases.fixed.sim.ts` reports BOUNDED.
*/
import { type Lease, LeasePool as PlantedPool } from "./worker.ts";
export { default } from "./worker.ts";
export class LeasePool extends PlantedPool {
override async acquire(project: string, token: string): Promise<Lease | null> {
const held = this.ctx.storage.sql
.exec<{ id: string; token: string; expires_at: number }>(
"SELECT id, token, expires_at FROM slots WHERE project = ?",
project,
)
.toArray()[0];
// A retry gets its own lease back; another caller for the same project waits its turn.
if (held)
return held.token === token ? { slot: held.id, token, expiresAt: held.expires_at } : null;
return super.acquire(project, token);
}
}