From 7bd7a826608f5a3c60713274980b02dc646ae52f Mon Sep 17 00:00:00 2001 From: calvin-archastro Date: Fri, 30 Oct 2026 14:40:05 -0700 Subject: [PATCH 1/4] Model pail Actions (designed, not yet built): orchestrator, runners, leases, fencing verify/actions.qnt: replicas that read, decide and write one guarded Tier 1 commit from a stale read; runners that claim, refresh, report and crash; results, sweep, cancel, rerun, environment gate, checks. actions_sim.qnt: random interleavings with a ghost for the history properties; mutate_actions.sh flips each of 13 design switches. actions_scenarios.qnt: 16 runs for UC1-4, 6-8. Co-Authored-By: Claude Opus 5.5 --- verify/README.md | 98 ++++- verify/actions.qnt | 713 +++++++++++++++++++++++++++++++++++ verify/actions_scenarios.qnt | 600 +++++++++++++++++++++++++++++ verify/actions_sim.qnt | 100 +++++ verify/mutate_actions.sh | 18 + verify/package.json | 9 +- 6 files changed, 1533 insertions(+), 5 deletions(-) create mode 100644 verify/actions.qnt create mode 100644 verify/actions_scenarios.qnt create mode 100644 verify/actions_sim.qnt create mode 100644 verify/mutate_actions.sh diff --git a/verify/README.md b/verify/README.md index f8637ca..2a4e0a4 100644 --- a/verify/README.md +++ b/verify/README.md @@ -6,7 +6,8 @@ collects it, the properties they must keep, and scenarios the real code is check against request by request with [quint-refinements](https://github.com/ArchAstro/quint-refinements). Beside it: the store contract every backend follows, the branch policy every enforcement point decides, and the -pull request protocol of `pail pr` (`pr.qnt`, below). +pull request protocol of `pail pr` (`pr.qnt`, below) and, designed but not yet built, the +workflow system pail Actions (`actions.qnt`, below). Layers, each importing those below. A feature is a set of pure steps (`xCan(s, ...)`: may it happen; `xNext(s, ...)`: the state after) over one shared state, so a new protocol @@ -46,6 +47,10 @@ pr.qnt ─── pr_sim.qnt ──quint run──▶ safety + history properties pr_scenarios.qnt ──compile──▶ pr-refinements.json + tests/pr_refinement/generated.rs │ tests/pr_refinement.rs ── the real extensions/pail-pr, its put and land held by a shim ──▶ same records after every step + +actions.qnt ─── actions_sim.qnt ──quint run──▶ safety + history properties hold in every simulated interleaving + │ +actions_scenarios.qnt ──quint test──▶ the runs a refinement harness will follow (no code to refine yet) ``` ## Files @@ -72,6 +77,10 @@ tests/pr_refinement.rs ── the real extensions/pail-pr, its put and land held | `pr_scenarios.qnt` | `@conformance` runs: the interleavings the plugin must follow | | `pr_sim.qnt` | `pr.qnt` under random interleavings, with a ghost for the history properties | | `mutate_pr.sh` | Flips each design switch in a scratch copy and expects `pr_sim.qnt` to find a violation | +| `actions.qnt` | pail Actions (not built yet): orchestrator replicas, runners, leases, results, the properties (`safety`) and the design switches | +| `actions_scenarios.qnt` | `@conformance` runs: the interleavings the orchestrator and runner must follow (run by `quint test`; not yet compiled into a harness) | +| `actions_sim.qnt` | `actions.qnt` under random interleavings, with a ghost for the history properties | +| `mutate_actions.sh` | Flips each design switch in a scratch copy and expects `actions_sim.qnt` to find a violation | | `quint-refinements.json`, `store-refinements.json`, `policy/policy-refinements.json`, `pr-refinements.json` | Generated scenario artifacts (do not edit) | | `../tests/*/generated.rs`, `policy/pailpolicy_refinement_gen_test.go` | Generated Rust traits and Go interface (do not edit) | | `../tests/refinement.rs` | `Repo::commit`, `Repo::rewrite_ref`, `Repo::land_stack`, `Repo::successor` and `gc` against `pail.qnt`: real actors over a shared in-memory bucket | @@ -84,8 +93,9 @@ tests/pr_refinement.rs ── the real extensions/pail-pr, its put and land held ```sh cd verify && npm ci npm test # scenarios pass in Quint -npm run simulate # random interleavings against `safety` (`step`, then writers only: `contendStep`; then `pr_sim.qnt`) +npm run simulate # random interleavings against `safety` (`step`, then writers only: `contendStep`; then `pr_sim.qnt`, `actions_sim.qnt`) npm run mutate:pr # each design switch of pr.qnt off: the simulation must find a violation +npm run witness:actions && npm run mutate:actions # the cases actions.qnt reaches; each of its switches off is caught npm run compile # after editing any .qnt file cd .. && cargo test --release --test refinement --test store_refinement --test policy_refinement --test pr_refinement # GCS runs in `cargo test` against the in-process emulator (src/gcs_emulator.rs); as a process: @@ -826,6 +836,90 @@ crashes between a claim and its land; reviews or checks withdrawn while a merge judging and claiming; policy files; pail-web (its server follows the same rules and is tested in `web/test`, not refined). +## Actions (designed, not yet built) (`actions.qnt`) + +pail Actions is a workflow system over a bucket: orchestrator replicas own run and job state +on the `_actions` and `_checks` branches (Tier 1: commits, `put --expect`, `--if-absent`), and +runners touch only plain objects under `.actions/` (Tier 2: queue, leases, progress, +results, cancel markers). The orchestrator is the one bridge from the second to the first. +There is no implementation yet: the model comes first, and the orchestrator and runner are +built and refined against it. `actions.qnt` models one workflow (jobs `build`, `test`, +`deploy`; the last two need `build`, `deploy` waits for an environment approval), runs from +three event keys (two pushes in one concurrency group with cancel-in-progress, one cron +slot), two orchestrator replicas, three runners, two attempts and a small clock (`TTL`). + +A replica's tick is `read`, then `write`: it observes both tiers, decides one intent and holds +the commit at its write, which lands or finds a conflict; so every write is from a stale +read. Runners claim a lease (`claimRead`, then `claimWrite`: create, or take over an expired +one by generation match), refresh it, report a step started, write a create-only result, see a +cancel marker, or crash. Approvers create approval files. + +| Intent | Commit | +|---|---| +| `ITrigger` | a run from an event key, cron slot: `runs/` (`--if-absent`), `claims/` (`--if-absent`), its jobs, `concurrency/` (CAS), cancelling the group's previous run | +| `IPromote` | a pending job whose `needs` succeeded is queued, or waits for its environment's approval; one whose need failed is skipped | +| `IStart` | a queued job whose lease a runner holds is in_progress under (holder, seq) | +| `IAccept` | a runner's result becomes the job's conclusion, if fenced | +| `ISweep` | a lease expired with no result: the job is requeued if no step started, else fails "runner lost" (a cancelled run's job is cancelled) | +| `IFinish`, `IRerun` | the run concludes; a new attempt copies the successes, restarts the rest and takes its group back | +| `ICheck` | the `_checks` projection of a completed job | + +Properties (`safety` in `actions.qnt`; `simSafety` adds the history ones of `actions_sim.qnt`): + +1. `atMostOneAccepted` (sim): at most one runner's result is ever accepted per (run, attempt, + job); `acceptedWasHolder`: the result a job concluded by is the holder's and seq's it + started under. +2. `noStranded`: a job is never in_progress with a lapsed lease unless the orchestrator can + accept its result or sweep it (the state form of "no job stays in_progress forever"). +3. `finality` and `attemptsAreFrozen` (sim): `completed`, its conclusion and who concluded it + never change; a rerun is a new attempt and the old one keeps its conclusion. +4. `ordering`: a job is queued, waiting, started or concluded by a runner only when every + need succeeded, and is skipped only when one did not. +5. `checksEarned`: a `_checks` success names a job that an accepted result (or a copy of one) + concluded success, of a run at that sha. +6. `oneActivePerGroup`: at most one run of a group is active and not cancelled; with + `cancelledIsIdle`: a cancelled run has nothing left to start. +7. `gatesHold`: an environment job is queued only with an approval from someone other than + the run's actor. +8. `oneRunPerKey`, `oneCreationPerKey` (sim): an event key or cron slot has one run, and one + commit ever created it, across replicas. + +and `leaseExclusive`: no two runners hold one job under one seq. + +Design switches (`actions.qnt`), each `true` the fix; `npm run mutate:actions` turns each off in +a scratch copy and the simulation finds a violation: + +| Switch off | What breaks | +|---|---| +| `CAS` | a stale replica overwrites a record with its read: a finished job restarted or concluded twice (`finality`, `atMostOneAccepted`) | +| `IF_ABSENT` | two replicas claim one run id, or one key, and overwrite each other (`oneRunPerKey`, `oneCreationPerKey`) | +| `GUARD_READS` | a commit expects only the records it writes: a sweep requeues a job of a run cancelled since it read, a rerun keeping its group does not see the group taken (`cancelledIsIdle`, `oneActivePerGroup`) | +| `LEASE_CREATE_ONLY` | a blind lease put: two runners hold one job under one seq (`leaseExclusive`) | +| `FENCE` | any result of an in_progress job is accepted: a stalled runner's late result concludes the job its successor holds (`acceptedWasHolder`) | +| `FENCE_ON_JOB` | intake also compares the live lease's seq (the plan's "lease seq matches"): a lease taken over after the job started strands the job (`noStranded`) | +| `RESULT_PER_LEASE` | one create-only result path per job: a late result of a lost runner blocks the next holder's, and the sweep sees a result (`noStranded`) | +| `SWEEP` | a runner that dies leaves its job in_progress for good (`noStranded`) | +| `NEEDS_CHECK` | a job is queued before its need concluded (`ordering`) | +| `APPROVAL_EXCLUDES_ACTOR` | the actor approves their own deploy (`gatesHold`) | +| `CANCEL_IN_PROGRESS` | a push does not cancel the run it supersedes (`oneActivePerGroup`) | +| `RERUN_NEW_ATTEMPT` | a rerun resets the attempt's jobs in place (`finality`, `attemptsAreFrozen`) | +| `CHECK_FROM_JOB` | `_checks` is written from the runners' raw results: a late success becomes a check on a failed job (`checksEarned`) | + +Witnesses (`npm run witness:actions`): a lost runner's job is requeued and runs again, a run is +cancelled, a run is rerun, an environment job is queued on an approval, a job is skipped. +`actions_scenarios.qnt` has 16 runs, for the plan's UC1, UC2, UC3, UC4, UC6, UC7 and UC8 +(and UC9's projection), written as single actions so that they compile with +`quint-refinements` (checked by hand: the artifact is large, so none is committed). The +refinement harness comes with the orchestrator (T1.7) and the runner (T2.5); until then the +scenarios run in Quint only (`npm test`). + +Not modelled: matrices and expressions, logs, progress beyond "a step started", artifacts and +caches, secrets, retention, `workflow_dispatch` requests (a second kind of create-only +trigger), several workflows, the orchestrator's leader lease (every write is guarded, so +correctness does not depend on it), batching of several intents in one commit (a commit here +is one intent), clock skew between replicas and runners, and runner restarts (a crash is +for good). + ## Not modelled yet Nothing on the list. What is still abstracted is named in each section's simplifications: diff --git a/verify/actions.qnt b/verify/actions.qnt new file mode 100644 index 0000000..489e102 --- /dev/null +++ b/verify/actions.qnt @@ -0,0 +1,713 @@ +// -*- mode: Bluespec; -*- +/// pail Actions (designed, not yet built): a workflow system over a bucket. Orchestrator +/// replicas own all run and job state on the `_actions` and `_checks` branches (Tier 1); +/// runners only touch plain objects under `.actions/` (Tier 2: queue, leases, progress, +/// results, cancel markers). The orchestrator is the one bridge: it reads what runners +/// reported, checks it against the job file, and commits the transition. `actions_sim.qnt` +/// simulates random interleavings; `actions_scenarios.qnt` has the runs the orchestrator and +/// runner will be refined against. +/// +/// A replica's tick is `read`, then `write`: `read` observes Tier 1 and Tier 2 and decides +/// one intent, which becomes a commit held at its write (`Pend`); `write` lets it land, or +/// finds a conflict (the replica reads again). Between the two, anything may have happened, +/// so a replica always writes from a stale read. The intents (one per commit; the real +/// orchestrator batches several in one commit, which only means more of them land together): +/// +/// ITrigger a run from an event key (push, PR synchronize, a cron slot): `runs/`, +/// `claims/` (the key), its jobs and `concurrency/`, one commit +/// IPromote a pending job whose `needs` all succeeded is queued, or waits for its +/// environment's approval; one whose need failed is skipped +/// IStart a queued job whose lease a runner holds is in_progress (names holder, seq) +/// IAccept a runner's result becomes the job's conclusion, if fenced +/// ISweep a job whose lease expired, with no result: requeue, or "runner lost" +/// IFinish all jobs of the attempt are completed: the run is +/// IRerun a new attempt: successes copied, the rest fresh; the old attempt is frozen +/// ICheck the `_checks` projection of a completed job +/// +/// Tier 1 guards: a write of a record the replica read is `put --expect` (CAS: the record +/// is as read); a write of a record it did not find is `--if-absent`. Each guard can be off +/// below. A runner claims a job by creating its lease (generation 0 matches one writer), or +/// takes over an expired one by generation match; it refreshes, reports a step started, +/// writes a create-only result, sees a cancel marker, or crashes. Time is `now` and `TTL`. +/// +/// Small on purpose: one workflow, jobs `build`, `test` and `deploy` (both need `build`; +/// `deploy` is gated by environment `prod`), runs from three event keys (two pushes in one +/// concurrency group with cancel-in-progress, one cron slot), at most two attempts. +/// Matrices, expressions, artifacts, logs, retention and the leader lease (correctness +/// never depends on it: every write is guarded) are left out. +module actions { + // ---------- the world ---------- + + pure val RUNNERS: Set[str] = Set("r1", "r2", "r3") + pure val REPLICAS: Set[str] = Set("o1", "o2") + pure val APPROVERS: Set[str] = Set("alice", "bob") + pure val EVENTS: Set[str] = Set("push1", "push2", "cron1") + pure val JOBS: Set[str] = Set("build", "test", "deploy") + pure val MAX_RUNS = 3 + pure val MAX_ATT = 2 + /// A lease lives `TTL` ticks past its last refresh. + pure val TTL = 2 + pure val MAX_T = 6 + + // The protocol's design choices. Each `true` is the fix; `false` is the bug it prevents, + // and what `npm run mutate:actions` shows `safety` (and `simSafety`) catching. + /// Writes of records the replica read are compare-and-swap (else blind overwrite). + pure val CAS = true + /// Writes of records it did not find are `--if-absent` (else blind overwrite): run ids, + /// event and slot claims, the concurrency file. + pure val IF_ABSENT = true + /// A commit expects every record it read, not only those it writes (the concurrency file + /// on a rerun that keeps the holder; the run on a sweep). + pure val GUARD_READS = true + /// A runner claims a lease by create or generation match (else a blind put). + pure val LEASE_CREATE_ONLY = true + /// Intake accepts a result only if the job file names its runner and seq (else any + /// result of an in_progress job). + pure val FENCE = true + /// ... and that is all it checks: the job file's holder and seq, not also the live lease's + /// (the plan's "lease seq matches": a lease taken over after the job started would + /// strand the job). + pure val FENCE_ON_JOB = true + /// A result is created at a path with the lease seq (else one per job: a late result of + /// a lost runner blocks the next holder's). + pure val RESULT_PER_LEASE = true + /// The sweep exists: an expired lease with no result requeues or concludes the job. + pure val SWEEP = true + /// A job is queued only when its `needs` succeeded; one whose need failed is skipped. + pure val NEEDS_CHECK = true + /// An approval counts only from someone other than the run's actor. + pure val APPROVAL_EXCLUDES_ACTOR = true + /// A new run cancels the group's previous holder (cancel-in-progress). + pure val CANCEL_IN_PROGRESS = true + /// A rerun is a new attempt (else it resets the attempt's jobs in place). + pure val RERUN_NEW_ATTEMPT = true + /// `_checks` is projected from the accepted job (else from the runners' raw results). + pure val CHECK_FROM_JOB = true + + pure def needsOf(j: str): Set[str] = if (j == "build") Set() else Set("build") + /// The job has `environment: prod`. + pure def gated(j: str): bool = j == "deploy" + /// The concurrency group of a run ("": none). + pure def groupOf(k: str): str = if (k == "cron1") "" else "main" + pure def shaOf(k: str): int = if (k == "push1") 1 else 2 + pure def actorOf(k: str): str = if (k == "push1") "alice" else if (k == "push2") "bob" else "cron" + + // ---------- Tier 1: `_actions` and `_checks` ---------- + + type JobKey = { rid: int, att: int, job: str } + type Status = Pending | Queued | Waiting | InProgress | Completed + type Concl = NoConcl | Success | Failure | Cancelled | Skipped + + /// `holder`, `seq`: the lease it is (or was last) in progress under. `by`, `byseq`: the + /// runner and seq whose result concluded it ("": none, as for skipped, lost, copied). + type Job = { + status: Status, concl: Concl, holder: str, seq: int, lost: int, + by: str, byseq: int, copied: bool, + } + /// `runs/.json`; `key` is the event key or cron slot it was created for. + type Run = { key: str, att: int, done: bool, concl: Concl, cancel: bool } + /// `_checks:/ci..json` + type CheckKey = { sha: int, job: str } + type Check = { rid: int, att: int, state: Concl } + /// `runs///approvals/prod/.json` (create-only) + type Approval = { rid: int, att: int, who: str } + + type T1 = { + runs: int -> Run, + // `claims/`: the run created for an event key or cron slot + claims: str -> int, + jobs: JobKey -> Job, + // `concurrency/`: the newest run + groups: str -> int, + checks: CheckKey -> Check, + approvals: Set[Approval], + } + + // ---------- Tier 2: `.actions/` ---------- + + /// `holder` "" and `seq` 0: no lease. `seq` grows with every claim. + type Lease = { holder: str, seq: int, exp: int } + /// A result's path: the job and (with `RESULT_PER_LEASE`) the lease seq. + type ResKey = { jk: JobKey, seq: int } + type Result = { runner: str, seq: int, concl: Concl } + + type T2 = { + queue: Set[JobKey], + leases: JobKey -> Lease, + results: ResKey -> Result, + cancels: Set[JobKey], + // progress: a step started under this lease seq + started: Set[ResKey], + } + + // ---------- orchestrator replicas, runners ---------- + + type Intent = + | ITrigger(str) + | IPromote(JobKey) + | IStart(JobKey) + | IAccept(ResKey) + | ISweep(JobKey) + | IFinish(int) + | IRerun(int) + | ICheck(JobKey) + + /// What a decision writes, and the records it read without writing them. + type Delta = { w: T1, rdRuns: Set[int], rdGroups: Set[str] } + type Dec = Refuse | Do(Delta) + /// A commit held at its write: what Tier 1 was when it read, and what it writes. + type Commit = { intent: Intent, snap: T1, d: Delta } + type PendO = NoPend | Pend(Commit) + + type RPhase = + | RIdle + // read the queue entry and the lease (`seen`); held at the lease write + | RReading({ jk: JobKey, seen: Lease }) + | RHolding({ jk: JobKey, seq: int, started: bool }) + type Runner = { alive: bool, ph: RPhase } + + type State = { + now: int, + // the events that happened (a push, a PR synchronize, a cron slot came due) + occurred: Set[str], + t1: T1, + t2: T2, + runners: str -> Runner, + pend: str -> PendO, + } + + pure val EMPTY1: T1 = { runs: Map(), claims: Map(), jobs: Map(), groups: Map(), checks: Map(), approvals: Set() } + + pure val INITIAL: State = { + now: 0, + occurred: Set(), + t1: EMPTY1, + t2: { queue: Set(), leases: Map(), results: Map(), cancels: Set(), started: Set() }, + runners: RUNNERS.mapBy(r => { alive: true, ph: RIdle }), + pend: REPLICAS.mapBy(o => NoPend), + } + + // ---------- reading ---------- + + pure val NOJOB: Job = { status: Pending, concl: NoConcl, holder: "", seq: 0, lost: 0, by: "", byseq: 0, copied: false } + pure val NORUN: Run = { key: "", att: 0, done: false, concl: NoConcl, cancel: false } + pure val NOLEASE: Lease = { holder: "", seq: 0, exp: 0 } + + pure def jobOf(v: T1, jk: JobKey): Job = if (v.jobs.keys().contains(jk)) v.jobs.get(jk) else NOJOB + pure def runOf(v: T1, id: int): Run = if (v.runs.keys().contains(id)) v.runs.get(id) else NORUN + pure def leaseOf(t: T2, jk: JobKey): Lease = if (t.leases.keys().contains(jk)) t.leases.get(jk) else NOLEASE + pure def groupHolder(v: T1, g: str): int = if (v.groups.keys().contains(g)) v.groups.get(g) else 0 + + pure def needOf(jk: JobKey, n: str): JobKey = { rid: jk.rid, att: jk.att, job: n } + pure def concluded(v: T1, jk: JobKey): bool = v.jobs.keys().contains(jk) and v.jobs.get(jk).status == Completed + pure def succeeded(v: T1, jk: JobKey): bool = concluded(v, jk) and v.jobs.get(jk).concl == Success + pure def needsMet(v: T1, jk: JobKey): bool = needsOf(jk.job).forall(n => succeeded(v, needOf(jk, n))) + pure def needFailed(v: T1, jk: JobKey): bool = + needsOf(jk.job).exists(n => concluded(v, needOf(jk, n)) and v.jobs.get(needOf(jk, n)).concl != Success) + + pure def isActive(st: Status): bool = match st { + | Pending => true + | Queued => true + | Waiting => true + | _ => false + } + + /// An approval for the job's run and attempt; `strict`: by someone other than the actor. + pure def approved(v: T1, jk: JobKey, strict: bool): bool = + v.approvals.exists(a => a.rid == jk.rid and a.att == jk.att and (not(strict) or a.who != actorOf(runOf(v, jk.rid).key))) + + /// A result's path: its seq is the lease's, or 0. + pure def resSeq(seq: int): int = if (RESULT_PER_LEASE) seq else 0 + + pure def liveFor(s: State, jk: JobKey, j: Job): bool = { + val l = leaseOf(s.t2, jk) + l.holder == j.holder and l.seq == j.seq and l.exp > s.now + } + + // ---------- what the orchestrator decides ---------- + + pure def overlay(a: k -> v, b: k -> v): k -> v = b.keys().fold(a, (m, x) => m.put(x, b.get(x))) + + pure def merge(a: T1, b: T1): T1 = { + runs: overlay(a.runs, b.runs), + claims: overlay(a.claims, b.claims), + jobs: overlay(a.jobs, b.jobs), + groups: overlay(a.groups, b.groups), + checks: overlay(a.checks, b.checks), + approvals: Set(), + } + + pure def jobDelta(jk: JobKey, j: Job): T1 = { ...EMPTY1, jobs: Map(jk -> j) } + pure def runDelta(id: int, r: Run): T1 = { ...EMPTY1, runs: Map(id -> r) } + pure def doing(w: T1): Dec = Do({ w: w, rdRuns: Set(), rdGroups: Set() }) + + /// A job's first state: queued at once if nothing holds it back, else pending. + pure def freshJob(j: str): Job = { + ...NOJOB, + status: if (needsOf(j).size() == 0 and not(gated(j))) Queued else Pending, + } + + pure def freshJobs(id: int, att: int): JobKey -> Job = + JOBS.map(j => { rid: id, att: att, job: j }).mapBy(jk => freshJob(jk.job)) + + /// Making run `id` the newest of its group: the previous holder, if it is still going, is + /// cancelled (its jobs not yet started are completed cancelled; the markers for the running + /// ones are made by `sync`). Writes `concurrency/` when the holder changes. + pure def claimGroup(v: T1, id: int, key: str): Delta = { + val g = groupOf(key) + val prev = groupHolder(v, g) + val pr = runOf(v, prev) + val cancelling = CANCEL_IN_PROGRESS and prev != 0 and prev != id and v.runs.keys().contains(prev) and not(pr.done) + val doomed = v.jobs.keys().filter(jk => cancelling and jk.rid == prev and jk.att == pr.att and isActive(v.jobs.get(jk).status)) + val w: T1 = { + ...EMPTY1, + runs: if (cancelling) Map(prev -> { ...pr, cancel: true }) else Map(), + jobs: doomed.mapBy(jk => { ...v.jobs.get(jk), status: Completed, concl: Cancelled }), + groups: if (prev == id) Map() else Map(g -> id), + } + { w: w, rdRuns: Set(), rdGroups: Set(g) } + } + + pure def withBase(d: Delta, base: T1): Delta = { ...d, w: merge(d.w, base) } + + pure def maxId(v: T1): int = v.runs.keys().fold(0, (m, k) => if (k > m) k else m) + + pure def decideTrigger(s: State, k: str): Dec = { + val v = s.t1 + val id = maxId(v) + 1 + if (not(s.occurred.contains(k)) or v.claims.keys().contains(k) or id > MAX_RUNS) Refuse + else { + val base: T1 = { + ...EMPTY1, + runs: Map(id -> { key: k, att: 1, done: false, concl: NoConcl, cancel: false }), + claims: Map(k -> id), + jobs: freshJobs(id, 1), + } + if (groupOf(k) == "") doing(base) else Do(withBase(claimGroup(v, id, k), base)) + } + } + + pure def decidePromote(s: State, jk: JobKey): Dec = { + val v = s.t1 + val j = jobOf(v, jk) + val r = runOf(v, jk.rid) + val target = if (gated(jk.job) and not(approved(v, jk, APPROVAL_EXCLUDES_ACTOR))) Waiting else Queued + if (not(v.jobs.keys().contains(jk)) or r.att != jk.att or not(j.status == Pending or j.status == Waiting)) Refuse + else if (NEEDS_CHECK and j.status == Pending and needFailed(v, jk)) + doing(jobDelta(jk, { ...j, status: Completed, concl: Skipped })) + else if (NEEDS_CHECK and not(needsMet(v, jk))) Refuse + else if (j.status == Waiting and target == Waiting) Refuse + else doing(jobDelta(jk, { ...j, status: target })) + } + + pure def decideStart(s: State, jk: JobKey): Dec = { + val j = jobOf(s.t1, jk) + val l = leaseOf(s.t2, jk) + if (j.status == Queued and l.seq > 0 and l.exp > s.now) + doing(jobDelta(jk, { ...j, status: InProgress, holder: l.holder, seq: l.seq })) + else Refuse + } + + pure def decideAccept(s: State, rk: ResKey): Dec = { + val j = jobOf(s.t1, rk.jk) + if (not(s.t2.results.keys().contains(rk)) or j.status != InProgress) Refuse + else { + val res = s.t2.results.get(rk) + val fenced = res.runner == j.holder and res.seq == j.seq and (FENCE_ON_JOB or leaseOf(s.t2, rk.jk).seq == res.seq) + if (FENCE and not(fenced)) Refuse + else doing(jobDelta(rk.jk, { ...j, status: Completed, concl: res.concl, by: res.runner, byseq: res.seq })) + } + } + + pure def decideSweep(s: State, jk: JobKey): Dec = { + val j = jobOf(s.t1, jk) + val r = runOf(s.t1, jk.rid) + val seen: ResKey = { jk: jk, seq: resSeq(j.seq) } + if (not(SWEEP) or j.status != InProgress or liveFor(s, jk, j) or s.t2.results.keys().contains(seen)) Refuse + else { + val nj = + if (r.cancel) { ...j, status: Completed, concl: Cancelled } + else if (s.t2.started.contains({ jk: jk, seq: j.seq })) { ...j, status: Completed, concl: Failure, lost: j.lost + 1 } + else { ...j, status: Queued, holder: "", lost: j.lost + 1 } + Do({ w: jobDelta(jk, nj), rdRuns: Set(jk.rid), rdGroups: Set() }) + } + } + + pure def decideFinish(s: State, id: int): Dec = { + val v = s.t1 + val r = runOf(v, id) + val jks = JOBS.map(j => { rid: id, att: r.att, job: j }) + if (not(v.runs.keys().contains(id)) or r.done or not(jks.forall(jk => concluded(v, jk)))) Refuse + else { + val concl = + if (r.cancel) Cancelled + else if (jks.exists(jk => v.jobs.get(jk).concl == Failure)) Failure + else Success + doing(runDelta(id, { ...r, done: true, concl: concl })) + } + } + + pure def decideRerun(s: State, id: int): Dec = { + val v = s.t1 + val r = runOf(v, id) + val att = if (RERUN_NEW_ATTEMPT) r.att + 1 else r.att + if (not(v.runs.keys().contains(id)) or not(r.done) or r.concl == Success or att > MAX_ATT) Refuse + else { + // successes are copied (frozen), the rest start over + val jobs = JOBS.map(j => { rid: id, att: att, job: j }).mapBy(jk => { + val old = jobOf(v, { rid: id, att: r.att, job: jk.job }) + if (old.status == Completed and old.concl == Success) { ...old, copied: true } else freshJob(jk.job) + }) + val base = { ...runDelta(id, { ...r, att: att, done: false, concl: NoConcl, cancel: false }), jobs: jobs } + Do(withBase(claimGroup(v, id, r.key), base)) + } + } + + pure def decideCheck(s: State, jk: JobKey): Dec = { + val v = s.t1 + val j = jobOf(v, jk) + val r = runOf(v, jk.rid) + if (not(v.jobs.keys().contains(jk)) or j.status != Completed or jk.att != r.att) Refuse + else { + val raw = s.t2.results.keys().exists(rk => rk.jk == jk and s.t2.results.get(rk).concl == Success) + val state = if (CHECK_FROM_JOB or not(raw)) j.concl else Success + val ck: CheckKey = { sha: shaOf(r.key), job: jk.job } + val ch: Check = { rid: jk.rid, att: jk.att, state: state } + if (v.checks.keys().contains(ck) and v.checks.get(ck) == ch) Refuse + else Do({ w: { ...EMPTY1, checks: Map(ck -> ch) }, rdRuns: Set(jk.rid), rdGroups: Set() }) + } + } + + pure def decide(s: State, i: Intent): Dec = match i { + | ITrigger(k) => decideTrigger(s, k) + | IPromote(jk) => decidePromote(s, jk) + | IStart(jk) => decideStart(s, jk) + | IAccept(rk) => decideAccept(s, rk) + | ISweep(jk) => decideSweep(s, jk) + | IFinish(id) => decideFinish(s, id) + | IRerun(id) => decideRerun(s, id) + | ICheck(jk) => decideCheck(s, jk) + } + + pure def deciding(s: State, i: Intent): bool = match decide(s, i) { + | Refuse => false + | Do(_) => true + } + + // ---------- committing ---------- + + /// The guard of a write: a record read (`snap`) must still be as read (`CAS`); one that was + /// absent must still be (`IF_ABSENT`). `rd`: records read but not written. + pure def guardOk(cur: k -> v, snap: k -> v, wr: Set[k], rd: Set[k]): bool = + wr.union(if (GUARD_READS) rd else Set()).forall(x => + if (snap.keys().contains(x)) (not(CAS) or (cur.keys().contains(x) and cur.get(x) == snap.get(x))) + else (not(IF_ABSENT) or not(cur.keys().contains(x)))) + + pure def landable(cur: T1, c: Commit): bool = all { + guardOk(cur.runs, c.snap.runs, c.d.w.runs.keys(), c.d.rdRuns), + guardOk(cur.claims, c.snap.claims, c.d.w.claims.keys(), Set()), + guardOk(cur.jobs, c.snap.jobs, c.d.w.jobs.keys(), Set()), + guardOk(cur.groups, c.snap.groups, c.d.w.groups.keys(), c.d.rdGroups), + guardOk(cur.checks, c.snap.checks, c.d.w.checks.keys(), Set()), + } + + pure def landed(cur: T1, c: Commit): T1 = { ...merge(cur, c.d.w), approvals: cur.approvals } + + // ---------- steps ---------- + + pure def isPend(p: PendO): bool = match p { + | Pend(_) => true + | NoPend => false + } + + pure def readCan(s: State, o: str, i: Intent): bool = not(isPend(s.pend.get(o))) and deciding(s, i) + + pure def readNext(s: State, o: str, i: Intent): State = match decide(s, i) { + | Refuse => s + | Do(d) => s.with("pend", s.pend.set(o, Pend({ intent: i, snap: s.t1, d: d }))) + } + + pure def writeCan(s: State, o: str): bool = isPend(s.pend.get(o)) + + /// The commit lands, or finds a conflict; either way the replica is done with it. + pure def writeNext(s: State, o: str): State = match s.pend.get(o) { + | NoPend => s + | Pend(c) => + val s2 = s.with("pend", s.pend.set(o, NoPend)) + if (landable(s.t1, c)) s2.with("t1", landed(s.t1, c)) else s2 + } + + /// The orchestrator keeps the queue to the queued jobs, and marks the running jobs of + /// cancelled runs. (Both are idempotent Tier 2 writes, and may lag.) + pure def syncNext(s: State): State = { + val v = s.t1 + s.with("t2", { + ...s.t2, + queue: v.jobs.keys().filter(jk => v.jobs.get(jk).status == Queued), + cancels: s.t2.cancels.union(v.jobs.keys().filter(jk => v.jobs.get(jk).status == InProgress and runOf(v, jk.rid).cancel)), + }) + } + + pure def tickCan(s: State): bool = s.now < MAX_T + pure def tickNext(s: State): State = s.with("now", s.now + 1) + + pure def setRunner(s: State, r: str, ph: RPhase): State = + s.with("runners", s.runners.set(r, { alive: s.runners.get(r).alive, ph: ph })) + + pure def setLease(s: State, jk: JobKey, l: Lease): State = + s.with("t2", { ...s.t2, leases: s.t2.leases.put(jk, l) }) + + /// A runner reads a queue entry and the lease, free or expired. + pure def claimReadCan(s: State, r: str, jk: JobKey): bool = all { + s.runners.get(r).alive, + s.runners.get(r).ph == RIdle, + s.t2.queue.contains(jk), + leaseOf(s.t2, jk).exp <= s.now, + } + + pure def claimReadNext(s: State, r: str, jk: JobKey): State = + setRunner(s, r, RReading({ jk: jk, seen: leaseOf(s.t2, jk) })) + + pure def readingOf(s: State, r: str): bool = match s.runners.get(r).ph { + | RReading(_) => s.runners.get(r).alive + | _ => false + } + + /// The lease write: create (generation 0) or take over (the generation read), one winner. + pure def claimWriteNext(s: State, r: str): State = match s.runners.get(r).ph { + | RReading(x) => + if (not(LEASE_CREATE_ONLY) or leaseOf(s.t2, x.jk) == x.seen) + setRunner(setLease(s, x.jk, { holder: r, seq: x.seen.seq + 1, exp: s.now + TTL }), r, + RHolding({ jk: x.jk, seq: x.seen.seq + 1, started: false })) + else setRunner(s, r, RIdle) + | _ => s + } + + pure def holdingOf(s: State, r: str): bool = match s.runners.get(r).ph { + | RHolding(_) => s.runners.get(r).alive + | _ => false + } + + /// The refresh is a generation match: it fails once another holds the lease, and the runner + /// stops. One whose lease merely expired still succeeds, if nobody took it over. + pure def refreshNext(s: State, r: str): State = match s.runners.get(r).ph { + | RHolding(x) => + val l = leaseOf(s.t2, x.jk) + if (l.holder == r and l.seq == x.seq) setLease(s, x.jk, { ...l, exp: s.now + TTL }) + else setRunner(s, r, RIdle) + | _ => s + } + + pure def startedCan(s: State, r: str): bool = match s.runners.get(r).ph { + | RHolding(x) => s.runners.get(r).alive and not(x.started) + | _ => false + } + + pure def startedNext(s: State, r: str): State = match s.runners.get(r).ph { + | RHolding(x) => + setRunner(s, r, RHolding({ ...x, started: true })) + .with("t2", { ...s.t2, started: s.t2.started.union(Set({ jk: x.jk, seq: x.seq })) }) + | _ => s + } + + /// Finished its steps, or (`Cancelled`) saw the cancel marker: the create-only result. + pure def resultCan(s: State, r: str, c: Concl): bool = match s.runners.get(r).ph { + | RHolding(x) => s.runners.get(r).alive and ( + if (c == Cancelled) s.t2.cancels.contains(x.jk) else x.started and (c == Success or c == Failure)) + | _ => false + } + + pure def resultNext(s: State, r: str, c: Concl): State = match s.runners.get(r).ph { + | RHolding(x) => + val rk: ResKey = { jk: x.jk, seq: resSeq(x.seq) } + if (s.t2.results.keys().contains(rk)) setRunner(s, r, RIdle) + else setRunner(s, r, RIdle).with("t2", { ...s.t2, results: s.t2.results.put(rk, { runner: r, seq: x.seq, concl: c }) }) + | _ => s + } + + pure def crashNext(s: State, r: str): State = + s.with("runners", s.runners.set(r, { alive: false, ph: RIdle })) + + pure def approveCan(s: State, a: Approval): bool = + s.t1.runs.keys().contains(a.rid) and a.att <= s.t1.runs.get(a.rid).att and not(s.t1.approvals.contains(a)) + + pure def approveNext(s: State, a: Approval): State = + s.with("t1", { ...s.t1, approvals: s.t1.approvals.union(Set(a)) }) + + // ---------- every step, as data (so that the simulation can wrap each) ---------- + + type Act = + | ATick + | AFire(str) + | AApprove(Approval) + | ARead({ o: str, i: Intent }) + | AWrite(str) + | ASync + | AClaimRead({ r: str, jk: JobKey }) + | AClaimWrite(str) + | ARefresh(str) + | AStarted(str) + | AResult({ r: str, c: Concl }) + | ACrash(str) + + pure def intentsOf(s: State): Set[Intent] = { + val js = s.t1.jobs.keys() + EVENTS.map(k => ITrigger(k)) + .union(js.map(jk => IPromote(jk))) + .union(js.map(jk => IStart(jk))) + .union(js.map(jk => ISweep(jk))) + .union(js.map(jk => ICheck(jk))) + .union(s.t2.results.keys().map(rk => IAccept(rk))) + .union(s.t1.runs.keys().map(id => IFinish(id))) + .union(s.t1.runs.keys().map(id => IRerun(id))) + .filter(i => deciding(s, i)) + } + + pure def unions(xs: Set[Set[a]]): Set[a] = xs.fold(Set(), (acc, x) => acc.union(x)) + + /// Every step that may happen in `s`. + pure def acts(s: State): Set[Act] = { + val live = RUNNERS.filter(r => s.runners.get(r).alive) + val approvals = unions(s.t1.runs.keys().map(id => unions(1.to(MAX_ATT).map(a => APPROVERS.map(w => { rid: id, att: a, who: w }))))) + .filter(a => approveCan(s, a)) + val intents = intentsOf(s) + Set(ATick).filter(a => tickCan(s)) + .union(EVENTS.filter(k => not(s.occurred.contains(k))).map(k => AFire(k))) + .union(approvals.map(a => AApprove(a))) + .union(unions(REPLICAS.filter(o => not(isPend(s.pend.get(o)))).map(o => intents.map(i => ARead({ o: o, i: i }))))) + .union(REPLICAS.filter(o => writeCan(s, o)).map(o => AWrite(o))) + .union(Set(ASync)) + .union(unions(live.map(r => s.t2.queue.filter(jk => claimReadCan(s, r, jk)).map(jk => AClaimRead({ r: r, jk: jk }))))) + .union(live.filter(r => readingOf(s, r)).map(r => AClaimWrite(r))) + .union(live.filter(r => holdingOf(s, r)).map(r => ARefresh(r))) + .union(live.filter(r => startedCan(s, r)).map(r => AStarted(r))) + .union(unions(live.map(r => Set(Success, Failure, Cancelled).filter(c => resultCan(s, r, c)).map(c => AResult({ r: r, c: c }))))) + .union(live.map(r => ACrash(r))) + } + + pure def apply(s: State, a: Act): State = match a { + | ATick => tickNext(s) + | AFire(k) => s.with("occurred", s.occurred.union(Set(k))) + | AApprove(x) => approveNext(s, x) + | ARead(x) => readNext(s, x.o, x.i) + | AWrite(o) => writeNext(s, o) + | ASync => syncNext(s) + | AClaimRead(x) => claimReadNext(s, x.r, x.jk) + | AClaimWrite(r) => claimWriteNext(s, r) + | ARefresh(r) => refreshNext(s, r) + | AStarted(r) => startedNext(s, r) + | AResult(x) => resultNext(s, x.r, x.c) + | ACrash(r) => crashNext(s, r) + } + + // ---------- actions ---------- + + var state: State + + action init = state' = INITIAL + + action tick: bool = all { tickCan(state), state' = tickNext(state) } + action fire(k: str): bool = all { not(state.occurred.contains(k)), state' = apply(state, AFire(k)) } + action approve(who: str, id: int, att: int): bool = all { + approveCan(state, { rid: id, att: att, who: who }), + state' = approveNext(state, { rid: id, att: att, who: who }), + } + action read(o: str, i: Intent): bool = all { readCan(state, o, i), state' = readNext(state, o, i) } + action write(o: str): bool = all { writeCan(state, o), state' = writeNext(state, o) } + action sync: bool = state' = syncNext(state) + action claimRead(r: str, jk: JobKey): bool = all { + claimReadCan(state, r, jk), + state' = claimReadNext(state, r, jk), + } + action claimWrite(r: str): bool = all { readingOf(state, r), state' = claimWriteNext(state, r) } + action refresh(r: str): bool = all { holdingOf(state, r), state' = refreshNext(state, r) } + action started(r: str): bool = all { startedCan(state, r), state' = startedNext(state, r) } + action result(r: str, c: Concl): bool = all { resultCan(state, r, c), state' = resultNext(state, r, c) } + action crash(r: str): bool = all { state.runners.get(r).alive, state' = crashNext(state, r) } + + /// Any interleaving: one enabled step, uniformly. + action step = { + nondet a = acts(state).oneOf() + state' = apply(state, a) + } + + // ---------- properties ---------- + + /// 2. No job stays in_progress once its lease has expired: it is live (its holder's lease + /// has not), or the orchestrator can accept its result or sweep it. + val noStranded: bool = state.t1.jobs.keys().forall(jk => { + val j = state.t1.jobs.get(jk) + j.status != InProgress or liveFor(state, jk, j) or + state.t2.results.keys().exists(rk => rk.jk == jk and deciding(state, IAccept(rk))) or deciding(state, ISweep(jk)) + }) + + /// 4. A job queued, waiting, started or concluded by a runner has all its needs succeeded; + /// a skipped one has a need that did not. + val ordering: bool = state.t1.jobs.keys().forall(jk => { + val j = state.t1.jobs.get(jk) + val ran = j.status != Pending and (j.status != Completed or j.concl == Success or j.concl == Failure) + (not(ran) or needsMet(state.t1, jk)) and (j.concl != Skipped or needFailed(state.t1, jk)) + }) + + /// 5. A `_checks` success names a job completed success by an accepted result (or copied + /// from an attempt that had one), of a run at that sha. + val checksEarned: bool = state.t1.checks.keys().forall(ck => { + val c = state.t1.checks.get(ck) + val jk: JobKey = { rid: c.rid, att: c.att, job: ck.job } + c.state != Success or ( + state.t1.jobs.keys().contains(jk) and succeeded(state.t1, jk) and + (state.t1.jobs.get(jk).by != "" or state.t1.jobs.get(jk).copied) and + shaOf(runOf(state.t1, c.rid).key) == ck.sha) + }) + + /// 6. At most one run per concurrency group is active and not cancelled. + val oneActivePerGroup: bool = Set("main").forall(g => + state.t1.runs.keys().filter(id => groupOf(state.t1.runs.get(id).key) == g and not(state.t1.runs.get(id).done) and not(state.t1.runs.get(id).cancel)).size() <= 1) + + /// A cancelled run has nothing left to start. + val cancelledIsIdle: bool = state.t1.runs.keys().forall(id => { + val r = state.t1.runs.get(id) + not(r.cancel) or not(state.t1.jobs.keys().exists(jk => jk.rid == id and jk.att == r.att and isActive(state.t1.jobs.get(jk).status))) + }) + + /// 7. A job with an environment reaches queued (and on) only with an approval from + /// someone other than the actor, whatever `APPROVAL_EXCLUDES_ACTOR` says. + val gatesHold: bool = state.t1.jobs.keys().forall(jk => { + val j = state.t1.jobs.get(jk) + val ran = j.status == Queued or j.status == InProgress or (j.status == Completed and (j.concl == Success or j.concl == Failure) and not(j.copied)) + not(gated(jk.job)) or not(ran) or approved(state.t1, jk, true) + }) + + /// 8. One run per event key or cron slot: its claim names a run of that key, and every run + /// is the one its key claims. + val oneRunPerKey: bool = + state.t1.claims.keys().forall(k => state.t1.runs.keys().contains(state.t1.claims.get(k)) and state.t1.runs.get(state.t1.claims.get(k)).key == k) and + state.t1.runs.keys().forall(id => state.t1.claims.keys().contains(state.t1.runs.get(id).key) and state.t1.claims.get(state.t1.runs.get(id).key) == id) + + /// 1, in state terms: a conclusion by a runner is by the holder and seq the job started under. + val acceptedWasHolder: bool = state.t1.jobs.keys().forall(jk => { + val j = state.t1.jobs.get(jk) + j.by == "" or (j.by == j.holder and j.byseq == j.seq) + }) + + /// A runner holds a lease alone: no two runners hold one job under one seq. + val leaseExclusive: bool = RUNNERS.forall(a => RUNNERS.forall(b => a == b or match state.runners.get(a).ph { + | RHolding(x) => match state.runners.get(b).ph { + | RHolding(y) => x.jk != y.jk or x.seq != y.seq + | _ => true + } + | _ => true + })) + + val safety: bool = all { + noStranded, + ordering, + checksEarned, + oneActivePerGroup, + cancelledIsIdle, + gatesHold, + oneRunPerKey, + acceptedWasHolder, + leaseExclusive, + } +} diff --git a/verify/actions_scenarios.qnt b/verify/actions_scenarios.qnt new file mode 100644 index 0000000..5a6ccc5 --- /dev/null +++ b/verify/actions_scenarios.qnt @@ -0,0 +1,600 @@ +// -*- mode: Bluespec; -*- +/// Interleavings the orchestrator and the runner must follow (`actions.qnt`), step by step: +/// a refinement harness (with the orchestrator, T1.7, and the runner, T2.5) will run each +/// against the real code with Tier 1 writes and Tier 2 requests held until the scenario +/// releases them. The use cases of the plan's section 5 that touch state: UC1 a push runs +/// jobs, UC2 cancel-in-progress, UC3 needs, UC4 a runner dies, UC6 rerun, UC7 an +/// environment gate, UC8 a cron slot; UC9 checks are the projection. (UC5 logs, UC10 +/// artifacts and caches, UC11 listing and retention, UC12 secrets are not state of this +/// model.) `o1`, `o2` are orchestrator replicas, `r1`..`r3` runners; push1 is by alice and +/// push2 by bob, both in one concurrency group. +module actionsScenarios { + import actions.* from "./actions" + + pure def jb(id: int, att: int, j: str): JobKey = { rid: id, att: att, job: j } + pure val BLD: JobKey = jb(1, 1, "build") + pure val TST: JobKey = jb(1, 1, "test") + pure val DEP: JobKey = jb(1, 1, "deploy") + pure val CK_BUILD_1: CheckKey = { sha: 1, job: "build" } + + // Each step below is one action, so that a refinement harness can drive it: a replica's + // tick is `read(o, i)` then `write(o)`; a runner's claim `claimRead(r, jk)` then + // `claimWrite(r)`; a lease lapses after `TTL` (2) `tick`s. Several runs start with push1 + // triggered, r1 holding run 1's build (in progress), and then r1 running its steps and the + // orchestrator accepting the result. + + /// UC1. A push runs a job: the run is created with its claim, jobs and concurrency file in + /// one commit; the runner's lease and result; the orchestrator's acceptance and the check. + /// @conformance + run pushRun = init + .then(fire("push1")) + .then(read("o1", ITrigger("push1"))) + .then(write("o1")) + .then(all { + assert(all { + state.t1.runs.keys() == Set(1), + state.t1.runs.get(1) == { key: "push1", att: 1, done: false, concl: NoConcl, cancel: false }, + state.t1.claims == Map("push1" -> 1), + state.t1.groups == Map("main" -> 1), + state.t1.jobs.get(BLD).status == Queued, + state.t1.jobs.get(TST).status == Pending, + state.t1.jobs.get(DEP).status == Pending, + state.t2.queue == Set(), + }), + state' = state, + }) + .then(sync) + .then(claimRead("r1", BLD)) + .then(claimWrite("r1")) + .then(all { + assert(all { + state.t2.queue == Set(BLD), + state.t2.leases.get(BLD) == { holder: "r1", seq: 1, exp: 2 }, + // the job file does not know yet + state.t1.jobs.get(BLD).status == Queued, + }), + state' = state, + }) + .then(read("o1", IStart(BLD))) + .then(write("o1")) + .then(started("r1")) + .then(refresh("r1")) + .then(result("r1", Success)) + .then(read("o1", IAccept({ jk: BLD, seq: 1 }))) + .then(write("o1")) + .then(read("o1", ICheck(BLD))) + .then(write("o1")) + .then(all { + assert(all { + state.t1.jobs.get(BLD).status == InProgress or state.t1.jobs.get(BLD).status == Completed, + state.t1.jobs.get(BLD).concl == Success, + state.t1.jobs.get(BLD).by == "r1", + state.t1.jobs.get(BLD).byseq == 1, + state.t1.checks.get(CK_BUILD_1) == { rid: 1, att: 1, state: Success }, + state.runners.get("r1").ph == RIdle, + }), + state' = state, + }) + + /// UC2. A second push supersedes the first: one commit creates run 2, takes the group over + /// and cancels run 1 (jobs not started are completed cancelled; the running build gets a + /// marker, its runner stops and reports cancelled, and the run concludes cancelled). + /// @conformance + run supersedeRun = init + .then(fire("push1")) + .then(read("o1", ITrigger("push1"))) + .then(write("o1")) + .then(sync) + .then(claimRead("r1", BLD)) + .then(claimWrite("r1")) + .then(read("o1", IStart(BLD))) + .then(write("o1")) + .then(started("r1")) + .then(fire("push2")) + .then(read("o2", ITrigger("push2"))) + .then(write("o2")) + .then(all { + assert(all { + state.t1.runs.get(1).cancel, + not(state.t1.runs.get(1).done), + state.t1.runs.get(2).key == "push2", + state.t1.groups == Map("main" -> 2), + state.t1.jobs.get(BLD).status == InProgress, + state.t1.jobs.get(TST).concl == Cancelled, + state.t1.jobs.get(DEP).concl == Cancelled, + state.t1.jobs.get(jb(2, 1, "build")).status == Queued, + }), + state' = state, + }) + .then(sync) + .then(all { assert(state.t2.cancels == Set(BLD)), state' = state }) + .then(result("r1", Cancelled)) + .then(read("o1", IAccept({ jk: BLD, seq: 1 }))) + .then(write("o1")) + .then(read("o1", IFinish(1))) + .then(write("o1")) + .then(all { + assert(all { + state.t1.runs.get(1).done, + state.t1.runs.get(1).concl == Cancelled, + state.t1.jobs.get(BLD).concl == Cancelled, + // the cancelled run's deploy was never queued, so never needed its approval + state.t1.approvals == Set(), + not(state.t1.runs.get(2).cancel), + }), + state' = state, + }) + + /// UC2, two replicas. Both read the empty branch for two different pushes: the first + /// commit wins the run id and the group, the second finds them taken, reads again and + /// cancels the first run: never two active runs in the group. + /// @conformance + run concurrentPushesRun = init + .then(fire("push1")) + .then(fire("push2")) + .then(read("o1", ITrigger("push1"))) + .then(read("o2", ITrigger("push2"))) + .then(write("o1")) + .then(write("o2")) + .then(all { + assert(all { + state.t1.runs.keys() == Set(1), + state.t1.claims == Map("push1" -> 1), + state.pend.get("o2") == NoPend, + }), + state' = state, + }) + .then(read("o2", ITrigger("push2"))) + .then(write("o2")) + .then(all { + assert(all { + state.t1.runs.keys() == Set(1, 2), + state.t1.runs.get(1).cancel, + not(state.t1.runs.get(2).cancel), + state.t1.groups == Map("main" -> 2), + oneActivePerGroup, + }), + state' = state, + }) + + /// UC3. A need failed: the dependents are skipped (never queued), and the run fails. + /// @conformance + run needFailedRun = init + .then(fire("push1")) + .then(read("o1", ITrigger("push1"))) + .then(write("o1")) + .then(sync) + .then(claimRead("r1", BLD)) + .then(claimWrite("r1")) + .then(read("o1", IStart(BLD))) + .then(write("o1")) + .then(started("r1")) + .then(result("r1", Failure)) + .then(read("o1", IAccept({ jk: BLD, seq: 1 }))) + .then(write("o1")) + .then(read("o2", IPromote(TST))) + .then(write("o2")) + .then(read("o2", IPromote(DEP))) + .then(write("o2")) + .then(all { + assert(all { + state.t1.jobs.get(TST).status == Completed, + state.t1.jobs.get(TST).concl == Skipped, + state.t1.jobs.get(DEP).concl == Skipped, + not(deciding(state, IFinish(2))), + deciding(state, IFinish(1)), + }), + state' = state, + }) + .then(read("o1", IFinish(1))) + .then(write("o1")) + .then(all { assert(state.t1.runs.get(1).concl == Failure), state' = state }) + + /// UC3. A need succeeded: its dependent is queued, the gated one waits for approval. + /// @conformance + run needMetRun = init + .then(fire("push1")) + .then(read("o1", ITrigger("push1"))) + .then(write("o1")) + .then(sync) + .then(claimRead("r1", BLD)) + .then(claimWrite("r1")) + .then(read("o1", IStart(BLD))) + .then(write("o1")) + .then(started("r1")) + .then(result("r1", Success)) + .then(read("o1", IAccept({ jk: BLD, seq: 1 }))) + .then(write("o1")) + .then(all { assert(deciding(state, IPromote(TST)) and deciding(state, IPromote(DEP))), state' = state }) + .then(read("o1", IPromote(TST))) + .then(write("o1")) + .then(read("o1", IPromote(DEP))) + .then(write("o1")) + .then(all { + assert(all { + state.t1.jobs.get(TST).status == Queued, + state.t1.jobs.get(DEP).status == Waiting, + }), + state' = state, + }) + + /// UC4. The runner dies before reporting a step: the lease lapses, the sweep requeues the + /// job, another runner takes the expired lease over (seq 2) and the job runs there. + /// @conformance + run lostBeforeStartRun = init + .then(fire("push1")) + .then(read("o1", ITrigger("push1"))) + .then(write("o1")) + .then(sync) + .then(claimRead("r1", BLD)) + .then(claimWrite("r1")) + .then(read("o1", IStart(BLD))) + .then(write("o1")) + .then(crash("r1")) + .then(all { assert(not(deciding(state, ISweep(BLD)))), state' = state }) + .then(tick) + .then(tick) + .then(read("o2", ISweep(BLD))) + .then(write("o2")) + .then(sync) + .then(all { + assert(all { + state.t1.jobs.get(BLD).status == Queued, + state.t1.jobs.get(BLD).holder == "", + state.t1.jobs.get(BLD).lost == 1, + state.t2.queue == Set(BLD), + }), + state' = state, + }) + .then(claimRead("r2", BLD)) + .then(claimWrite("r2")) + .then(read("o1", IStart(BLD))) + .then(write("o1")) + .then(all { + assert(all { + state.t1.jobs.get(BLD).status == InProgress, + state.t1.jobs.get(BLD).holder == "r2", + state.t1.jobs.get(BLD).seq == 2, + }), + state' = state, + }) + + /// UC4. The runner dies after a step started: the job concludes failure, "runner lost", + /// and its dependents are skipped. + /// @conformance + run lostAfterStartRun = init + .then(fire("push1")) + .then(read("o1", ITrigger("push1"))) + .then(write("o1")) + .then(sync) + .then(claimRead("r1", BLD)) + .then(claimWrite("r1")) + .then(read("o1", IStart(BLD))) + .then(write("o1")) + .then(started("r1")) + .then(crash("r1")) + .then(tick) + .then(tick) + .then(read("o1", ISweep(BLD))) + .then(write("o1")) + .then(all { + assert(all { + state.t1.jobs.get(BLD).status == Completed, + state.t1.jobs.get(BLD).concl == Failure, + state.t1.jobs.get(BLD).by == "", + state.t1.jobs.get(BLD).lost == 1, + }), + state' = state, + }) + .then(read("o1", IPromote(TST))) + .then(write("o1")) + .then(all { assert(state.t1.jobs.get(TST).concl == Skipped), state' = state }) + + /// UC4. A runner that only stalled reports late: its lease was taken over and the job runs + /// under seq 2, so its result (seq 1) is not accepted, and the new holder's is. + /// @conformance + run lateResultRun = init + .then(fire("push1")) + .then(read("o1", ITrigger("push1"))) + .then(write("o1")) + .then(sync) + .then(claimRead("r1", BLD)) + .then(claimWrite("r1")) + .then(read("o1", IStart(BLD))) + .then(write("o1")) + .then(tick) + .then(tick) + .then(read("o2", ISweep(BLD))) + .then(write("o2")) + .then(sync) + .then(claimRead("r2", BLD)) + .then(claimWrite("r2")) + .then(read("o1", IStart(BLD))) + .then(write("o1")) + .then(started("r1")) + .then(result("r1", Success)) + .then(all { + assert(all { + not(deciding(state, IAccept({ jk: BLD, seq: 1 }))), + state.t2.results.get({ jk: BLD, seq: 1 }).runner == "r1", + // the job is the new holder's + state.t1.jobs.get(BLD).holder == "r2", + }), + state' = state, + }) + .then(started("r2")) + .then(result("r2", Success)) + .then(read("o1", IAccept({ jk: BLD, seq: 2 }))) + .then(write("o1")) + .then(all { + assert(all { + state.t1.jobs.get(BLD).concl == Success, + state.t1.jobs.get(BLD).by == "r2", + state.t1.jobs.get(BLD).byseq == 2, + }), + state' = state, + }) + + /// UC4 and UC9. A runner reports success after the sweep concluded its job "runner lost": + /// the job stays failed and so does its check. + /// @conformance + run lateSuccessIsNotACheckRun = init + .then(fire("push1")) + .then(read("o1", ITrigger("push1"))) + .then(write("o1")) + .then(sync) + .then(claimRead("r1", BLD)) + .then(claimWrite("r1")) + .then(read("o1", IStart(BLD))) + .then(write("o1")) + .then(started("r1")) + .then(tick) + .then(tick) + .then(read("o1", ISweep(BLD))) + .then(write("o1")) + .then(result("r1", Success)) + .then(read("o2", ICheck(BLD))) + .then(write("o2")) + .then(all { + assert(all { + state.t1.jobs.get(BLD).concl == Failure, + state.t1.checks.get(CK_BUILD_1).state == Failure, + not(deciding(state, IAccept({ jk: BLD, seq: 1 }))), + }), + state' = state, + }) + + /// Two runners read the queue entry at once: the lease write has one winner, and the other + /// finds the lease changed and leaves the job. + /// @conformance + run leaseRaceRun = init + .then(fire("push1")) + .then(read("o1", ITrigger("push1"))) + .then(write("o1")) + .then(sync) + .then(claimRead("r1", BLD)) + .then(claimRead("r2", BLD)) + .then(claimWrite("r1")) + .then(claimWrite("r2")) + .then(all { + assert(all { + state.t2.leases.get(BLD).holder == "r1", + state.runners.get("r2").ph == RIdle, + leaseExclusive, + }), + state' = state, + }) + + /// Two replicas accept the same result: the second finds the job changed and leaves it. + /// @conformance + run twoReplicasAcceptRun = init + .then(fire("push1")) + .then(read("o1", ITrigger("push1"))) + .then(write("o1")) + .then(sync) + .then(claimRead("r1", BLD)) + .then(claimWrite("r1")) + .then(read("o1", IStart(BLD))) + .then(write("o1")) + .then(started("r1")) + .then(result("r1", Success)) + .then(read("o1", IAccept({ jk: BLD, seq: 1 }))) + .then(read("o2", IAccept({ jk: BLD, seq: 1 }))) + .then(write("o1")) + .then(write("o2")) + .then(all { + assert(all { + state.t1.jobs.get(BLD).concl == Success, + state.pend.get("o2") == NoPend, + }), + state' = state, + }) + + /// A replica read a queued job a runner held, then a newer push cancelled its run: its + /// write finds the job changed, and the cancelled job is not started. + /// @conformance + run staleStartRun = init + .then(fire("push1")) + .then(read("o1", ITrigger("push1"))) + .then(write("o1")) + .then(sync) + .then(claimRead("r1", BLD)) + .then(claimWrite("r1")) + .then(read("o1", IStart(BLD))) + .then(fire("push2")) + .then(read("o2", ITrigger("push2"))) + .then(write("o2")) + .then(write("o1")) + .then(all { + assert(all { + state.t1.jobs.get(BLD).status == Completed, + state.t1.jobs.get(BLD).concl == Cancelled, + state.t1.runs.get(1).cancel, + }), + state' = state, + }) + + /// UC7. The deploy waits for an approval; the run's own actor (alice) does not count; bob's + /// does, and the job is queued. + /// @conformance + run gateRun = init + .then(fire("push1")) + .then(read("o1", ITrigger("push1"))) + .then(write("o1")) + .then(sync) + .then(claimRead("r1", BLD)) + .then(claimWrite("r1")) + .then(read("o1", IStart(BLD))) + .then(write("o1")) + .then(started("r1")) + .then(result("r1", Success)) + .then(read("o1", IAccept({ jk: BLD, seq: 1 }))) + .then(write("o1")) + .then(read("o1", IPromote(DEP))) + .then(write("o1")) + .then(all { assert(state.t1.jobs.get(DEP).status == Waiting), state' = state }) + .then(approve("alice", 1, 1)) + .then(all { assert(not(deciding(state, IPromote(DEP)))), state' = state }) + .then(approve("bob", 1, 1)) + .then(read("o2", IPromote(DEP))) + .then(write("o2")) + .then(sync) + .then(all { + assert(all { + state.t1.jobs.get(DEP).status == Queued, + state.t2.queue.contains(DEP), + gatesHold, + }), + state' = state, + }) + + /// UC8. A cron slot comes due and two replicas fire it: one run (the slot's claim is + /// create-only), and a replica that reads again finds the slot claimed. + /// @conformance + run cronSlotRun = init + .then(fire("cron1")) + .then(read("o1", ITrigger("cron1"))) + .then(read("o2", ITrigger("cron1"))) + .then(write("o1")) + .then(write("o2")) + .then(all { + assert(all { + state.t1.runs.keys() == Set(1), + state.t1.claims == Map("cron1" -> 1), + // a cron run is in no concurrency group + state.t1.groups == Map(), + not(deciding(state, ITrigger("cron1"))), + }), + state' = state, + }) + + /// UC6. A cancelled run is rerun: attempt 2 starts, attempt 1 is untouched (frozen), and + /// the rerun takes its group back, cancelling the newer run. + /// @conformance + run rerunRun = init + .then(fire("push1")) + .then(read("o1", ITrigger("push1"))) + .then(write("o1")) + .then(fire("push2")) + .then(read("o1", ITrigger("push2"))) + .then(write("o1")) + .then(read("o1", IFinish(1))) + .then(write("o1")) + .then(all { + assert(all { + state.t1.runs.get(1).concl == Cancelled, + not(deciding(state, IRerun(2))), + }), + state' = state, + }) + .then(read("o2", IRerun(1))) + .then(write("o2")) + .then(all { + assert(all { + state.t1.runs.get(1).att == 2, + not(state.t1.runs.get(1).done), + state.t1.jobs.get(BLD).concl == Cancelled, + state.t1.jobs.get(jb(1, 2, "build")).status == Queued, + state.t1.groups == Map("main" -> 1), + state.t1.runs.get(2).cancel, + oneActivePerGroup, + }), + state' = state, + }) + + /// UC1, UC3, UC6, UC7 together. build succeeds, test fails, deploy waits for bob and + /// succeeds; the run fails. Rerunning the failed jobs copies build and deploy into attempt 2 + /// (no new approval) and queues test again; attempt 1 stays as it was. + /// @conformance + run rerunFailedRun = init + .then(fire("push1")) + .then(read("o1", ITrigger("push1"))) + .then(write("o1")) + .then(sync) + .then(claimRead("r1", BLD)) + .then(claimWrite("r1")) + .then(read("o1", IStart(BLD))) + .then(write("o1")) + .then(started("r1")) + .then(result("r1", Success)) + .then(read("o1", IAccept({ jk: BLD, seq: 1 }))) + .then(write("o1")) + .then(read("o1", IPromote(TST))) + .then(write("o1")) + .then(read("o1", IPromote(DEP))) + .then(write("o1")) + .then(sync) + .then(claimRead("r2", TST)) + .then(claimWrite("r2")) + .then(read("o1", IStart(TST))) + .then(write("o1")) + .then(started("r2")) + .then(result("r2", Failure)) + .then(read("o1", IAccept({ jk: TST, seq: 1 }))) + .then(write("o1")) + .then(approve("bob", 1, 1)) + .then(read("o2", IPromote(DEP))) + .then(write("o2")) + .then(sync) + .then(claimRead("r3", DEP)) + .then(claimWrite("r3")) + .then(read("o1", IStart(DEP))) + .then(write("o1")) + .then(started("r3")) + .then(result("r3", Success)) + .then(read("o1", IAccept({ jk: DEP, seq: 1 }))) + .then(write("o1")) + .then(read("o1", IFinish(1))) + .then(write("o1")) + .then(read("o1", ICheck(TST))) + .then(write("o1")) + .then(all { + assert(all { + state.t1.runs.get(1).concl == Failure, + state.t1.checks.get({ sha: 1, job: "test" }).state == Failure, + }), + state' = state, + }) + .then(read("o2", IRerun(1))) + .then(write("o2")) + .then(read("o2", IPromote(jb(1, 2, "test")))) + .then(write("o2")) + .then(read("o2", ICheck(jb(1, 2, "build")))) + .then(write("o2")) + .then(all { + assert(all { + state.t1.runs.get(1).att == 2, + state.t1.jobs.get(jb(1, 2, "build")).copied, + state.t1.jobs.get(jb(1, 2, "build")).concl == Success, + state.t1.jobs.get(jb(1, 2, "deploy")).copied, + state.t1.jobs.get(jb(1, 2, "test")).status == Queued, + // attempt 1 is as it was + state.t1.jobs.get(TST).concl == Failure, + state.t1.jobs.get(TST).by == "r2", + state.t1.jobs.get(DEP).by == "r3", + state.t1.checks.get(CK_BUILD_1) == { rid: 1, att: 2, state: Success }, + state.t1.checks.get({ sha: 1, job: "test" }).att == 1, + }), + state' = state, + }) +} diff --git a/verify/actions_sim.qnt b/verify/actions_sim.qnt new file mode 100644 index 0000000..dc322ae --- /dev/null +++ b/verify/actions_sim.qnt @@ -0,0 +1,100 @@ +// -*- mode: Bluespec; -*- +/// `actions.qnt`'s protocol under random interleavings, with a ghost remembering what was +/// concluded and accepted, for the properties that need history: at most one result is ever +/// accepted per job, a conclusion never changes, an attempt is frozen, one run is ever +/// created per event key. (The refinement cannot see ghosts, so they stay out of +/// `actions.qnt`'s state.) `npm run simulate:actions` checks `simSafety` here; `npm run +/// mutate:actions` flips each design switch of `actions.qnt` and expects a violation. +module actionsSim { + import actions.* from "./actions" + + type Conclusion = { concl: Concl, by: str, byseq: int } + type RunAtt = { rid: int, att: int } + + type Ghost = { + // every runner result ever accepted for a job + accepted: JobKey -> Set[{ by: str, byseq: int }], + // the first conclusion of each job + done: JobKey -> Conclusion, + // the first conclusion of each attempt of each run + ran: RunAtt -> Concl, + // how many commits created the run of each event key + creates: str -> int, + } + + var ghost: Ghost + + pure val GHOST0: Ghost = { accepted: Map(), done: Map(), ran: Map(), creates: EVENTS.mapBy(k => 0) } + + /// What the step `a`, taking `s` to `t`, did to the ghost. + pure def ghostAfter(g: Ghost, s: State, a: Act, t: State): Ghost = { + val jobs = t.t1.jobs + val byRunner = jobs.keys().filter(jk => jobs.get(jk).by != "") + val fresh = jobs.keys().filter(jk => jobs.get(jk).status == Completed and not(g.done.keys().contains(jk))) + val runs = t.t1.runs + val freshRuns = runs.keys().filter(id => runs.get(id).done and not(g.ran.keys().contains({ rid: id, att: runs.get(id).att }))) + val created = match a { + | AWrite(o) => match s.pend.get(o) { + | Pend(c) => match c.intent { + | ITrigger(k) => if (landable(s.t1, c)) Set(k) else Set() + | _ => Set() + } + | NoPend => Set() + } + | _ => Set() + } + { + accepted: byRunner.fold(g.accepted, (m, jk) => + m.put(jk, (if (m.keys().contains(jk)) m.get(jk) else Set()).union(Set({ by: jobs.get(jk).by, byseq: jobs.get(jk).byseq })))), + done: fresh.fold(g.done, (m, jk) => m.put(jk, { concl: jobs.get(jk).concl, by: jobs.get(jk).by, byseq: jobs.get(jk).byseq })), + ran: freshRuns.fold(g.ran, (m, id) => m.put({ rid: id, att: runs.get(id).att }, runs.get(id).concl)), + creates: g.creates.keys().mapBy(k => g.creates.get(k) + (if (created.contains(k)) 1 else 0)), + } + } + + action simInit = all { state' = INITIAL, ghost' = GHOST0 } + + action simStep = { + nondet a = acts(state).oneOf() + all { + state' = apply(state, a), + ghost' = ghostAfter(ghost, state, a, apply(state, a)), + } + } + + // ---------- properties that need the ghost ---------- + + /// 1. At most one runner's result is ever accepted for a job (run, attempt, job). + val atMostOneAccepted: bool = ghost.accepted.keys().forall(jk => ghost.accepted.get(jk).size() <= 1) + + /// 3. completed and its conclusion never change, nor who concluded it; a rerun is a new + /// attempt, and its run's earlier attempts keep their conclusion. + val finality: bool = ghost.done.keys().forall(jk => { + val j = jobOf(state.t1, jk) + val d = ghost.done.get(jk) + j.status == Completed and j.concl == d.concl and j.by == d.by and j.byseq == d.byseq + }) + + val attemptsAreFrozen: bool = ghost.ran.keys().forall(x => { + val r = runOf(state.t1, x.rid) + r.att > x.att or (r.att == x.att and r.done and r.concl == ghost.ran.get(x)) + }) + + /// 8. Exactly one commit ever created the run of an event key or cron slot. + val oneCreationPerKey: bool = ghost.creates.keys().forall(k => ghost.creates.get(k) <= 1) + + val simSafety: bool = all { safety, atMostOneAccepted, finality, attemptsAreFrozen, oneCreationPerKey } + + // ---------- witnesses: each is violated by a run that reaches the case ---------- + + /// A lost runner's job goes back to the queue and runs again. + val neverRequeued: bool = not(state.t1.jobs.keys().exists(jk => state.t1.jobs.get(jk).lost > 0 and state.t1.jobs.get(jk).status == InProgress)) + /// A run is cancelled (superseded in its group). + val neverCancelled: bool = not(state.t1.runs.keys().exists(id => state.t1.runs.get(id).done and state.t1.runs.get(id).concl == Cancelled)) + /// A run has a second attempt. + val neverRerun: bool = not(state.t1.runs.keys().exists(id => state.t1.runs.get(id).att > 1)) + /// A job behind an environment gate is queued, on an approval. + val neverApproved: bool = not(state.t1.jobs.keys().exists(jk => gated(jk.job) and (state.t1.jobs.get(jk).status == InProgress or state.t1.jobs.get(jk).status == Queued))) + /// A job is skipped because a need failed. + val neverSkipped: bool = not(state.t1.jobs.keys().exists(jk => state.t1.jobs.get(jk).concl == Skipped)) +} diff --git a/verify/mutate_actions.sh b/verify/mutate_actions.sh new file mode 100644 index 0000000..4f19933 --- /dev/null +++ b/verify/mutate_actions.sh @@ -0,0 +1,18 @@ +#!/bin/sh +# Flip each design switch of actions.qnt (the protocol without that fix) in a scratch copy and +# check that the simulation finds a violation of `simSafety`. +set -e +tmp=$(mktemp -d) +trap 'rm -rf "$tmp"' EXIT +for sw in CAS IF_ABSENT GUARD_READS LEASE_CREATE_ONLY FENCE FENCE_ON_JOB RESULT_PER_LEASE SWEEP \ + NEEDS_CHECK APPROVAL_EXCLUDES_ACTOR CANCEL_IN_PROGRESS RERUN_NEW_ATTEMPT CHECK_FROM_JOB; do + cp actions.qnt actions_sim.qnt "$tmp"/ + sed "s/pure val $sw = true/pure val $sw = false/" actions.qnt > "$tmp/actions.qnt" + if cmp -s actions.qnt "$tmp/actions.qnt"; then echo "no such switch: $sw"; exit 1; fi + if (cd "$tmp" && quint run actions_sim.qnt --main=actionsSim --init=simInit --step=simStep --invariant=simSafety --max-steps=60 --max-samples=300000 | grep -q '^\[violation\]'); then + echo "caught: $sw = false" + else + echo "not caught: $sw = false" + exit 1 + fi +done diff --git a/verify/package.json b/verify/package.json index f811b21..1ed08d6 100644 --- a/verify/package.json +++ b/verify/package.json @@ -9,12 +9,15 @@ "compile:policy": "quint-refinements compile policy_scenarios.qnt --module policyScenarios --compact --artifact policy/policy-refinements.json --rust ../tests/policy_refinement/generated.rs --go policy/pailpolicy_refinement_gen_test.go --go-package gateway", "compile:pr": "quint-refinements compile pr_scenarios.qnt --module prScenarios --compact --artifact pr-refinements.json --rust ../tests/pr_refinement/generated.rs", "check": "npm run compile:publish -- --check && npm run compile:store -- --check && npm run compile:policy -- --check && npm run compile:pr -- --check", - "test": "quint test store_scenarios.qnt --main=storeScenarios --match='Run$' && quint test scenarios.qnt --main=scenarios --match='Run$' && quint test policy_scenarios.qnt --main=policyScenarios --match='Run$' && quint test pr_scenarios.qnt --main=prScenarios --match='Run$'", - "simulate": "quint run pail.qnt --main=pail --invariant=safety --max-steps=100 --max-samples=20000 && quint run pail.qnt --main=pail --step=contendStep --invariant=safety --max-steps=60 --max-samples=20000 && npm run simulate:pr", + "test": "quint test store_scenarios.qnt --main=storeScenarios --match='Run$' && quint test scenarios.qnt --main=scenarios --match='Run$' && quint test policy_scenarios.qnt --main=policyScenarios --match='Run$' && quint test pr_scenarios.qnt --main=prScenarios --match='Run$' && quint test actions_scenarios.qnt --main=actionsScenarios --match='Run$'", + "simulate": "quint run pail.qnt --main=pail --invariant=safety --max-steps=100 --max-samples=20000 && quint run pail.qnt --main=pail --step=contendStep --invariant=safety --max-steps=60 --max-samples=20000 && npm run simulate:pr && npm run simulate:actions", "simulate:pr": "quint run pr_sim.qnt --main=prSim --init=simInit --step=simStep --invariant=simSafety --max-steps=60 --max-samples=50000", "witness": "for inv in gcNeverDeletesAPack gcNeverDeletesAChunk branchHasNoHugeFile; do quint run pail.qnt --main=pail --invariant=$inv --max-steps=100 --max-samples=200000 | grep -q '^\\[violation\\]' || { echo \"never reached: $inv\"; exit 1; }; done", "witness:pr": "for inv in neverMerged neverOutdated neverStale; do quint run pr_sim.qnt --main=prSim --init=simInit --step=simStep --invariant=$inv --max-steps=60 --max-samples=50000 | grep -q '^\\[violation\\]' || { echo \"never reached: $inv\"; exit 1; }; done", - "mutate:pr": "sh mutate_pr.sh" + "mutate:pr": "sh mutate_pr.sh", + "simulate:actions": "quint run actions_sim.qnt --main=actionsSim --init=simInit --step=simStep --invariant=simSafety --max-steps=60 --max-samples=60000", + "witness:actions": "for inv in neverRequeued neverCancelled neverRerun neverApproved neverSkipped; do quint run actions_sim.qnt --main=actionsSim --init=simInit --step=simStep --invariant=$inv --max-steps=60 --max-samples=50000 | grep -q '^\\[violation\\]' || { echo \"never reached: $inv\"; exit 1; }; done", + "mutate:actions": "sh mutate_actions.sh" }, "devDependencies": { "@informalsystems/quint": "0.33.0", From 8a929c33fe15fef023f070667a3128dc2838735b Mon Sep 17 00:00:00 2001 From: calvin-archastro Date: Fri, 30 Oct 2026 15:51:14 -0700 Subject: [PATCH 2/4] Actions model: guard the records a commit read (previous holder, its jobs); two race scenarios Co-Authored-By: Claude Opus 5.5 --- verify/README.md | 44 +++++++++-- verify/{ => actions}/actions.qnt | 20 +++-- verify/{ => actions}/actions_scenarios.qnt | 92 ++++++++++++++++++++++ verify/{ => actions}/actions_sim.qnt | 22 +++++- verify/mutate_actions.sh | 18 ++++- verify/package.json | 6 +- 6 files changed, 180 insertions(+), 22 deletions(-) rename verify/{ => actions}/actions.qnt (96%) rename verify/{ => actions}/actions_scenarios.qnt (87%) rename verify/{ => actions}/actions_sim.qnt (87%) diff --git a/verify/README.md b/verify/README.md index 2a4e0a4..a3bfd60 100644 --- a/verify/README.md +++ b/verify/README.md @@ -48,7 +48,7 @@ pr_scenarios.qnt ──compile──▶ pr-refinements.json + tests/pr_refinemen │ tests/pr_refinement.rs ── the real extensions/pail-pr, its put and land held by a shim ──▶ same records after every step -actions.qnt ─── actions_sim.qnt ──quint run──▶ safety + history properties hold in every simulated interleaving +actions/actions.qnt ─── actions_sim.qnt ──quint run──▶ safety + history properties hold in every simulated interleaving │ actions_scenarios.qnt ──quint test──▶ the runs a refinement harness will follow (no code to refine yet) ``` @@ -77,9 +77,9 @@ actions_scenarios.qnt ──quint test──▶ the runs a refinement harness wi | `pr_scenarios.qnt` | `@conformance` runs: the interleavings the plugin must follow | | `pr_sim.qnt` | `pr.qnt` under random interleavings, with a ghost for the history properties | | `mutate_pr.sh` | Flips each design switch in a scratch copy and expects `pr_sim.qnt` to find a violation | -| `actions.qnt` | pail Actions (not built yet): orchestrator replicas, runners, leases, results, the properties (`safety`) and the design switches | -| `actions_scenarios.qnt` | `@conformance` runs: the interleavings the orchestrator and runner must follow (run by `quint test`; not yet compiled into a harness) | -| `actions_sim.qnt` | `actions.qnt` under random interleavings, with a ghost for the history properties | +| `actions/actions.qnt` | pail Actions (not built yet): orchestrator replicas, runners, leases, results, the properties (`safety`) and the design switches | +| `actions/actions_scenarios.qnt` | `@conformance` runs: the interleavings the orchestrator and runner must follow (run by `quint test`; not yet compiled into a harness) | +| `actions/actions_sim.qnt` | `actions.qnt` under random interleavings, with a ghost for the history properties | | `mutate_actions.sh` | Flips each design switch in a scratch copy and expects `actions_sim.qnt` to find a violation | | `quint-refinements.json`, `store-refinements.json`, `policy/policy-refinements.json`, `pr-refinements.json` | Generated scenario artifacts (do not edit) | | `../tests/*/generated.rs`, `policy/pailpolicy_refinement_gen_test.go` | Generated Rust traits and Go interface (do not edit) | @@ -836,7 +836,11 @@ crashes between a claim and its land; reviews or checks withdrawn while a merge judging and claiming; policy files; pail-web (its server follows the same rules and is tested in `web/test`, not refined). -## Actions (designed, not yet built) (`actions.qnt`) +## Actions (designed, not yet built) (`actions/`) + +(The files live in `actions/`, not beside the others: `quint-refinements` digests every `.qnt` +in the directory of the scenarios it compiles, so one more here would make all four generated +artifacts drift.) pail Actions is a workflow system over a bucket: orchestrator replicas own run and job state on the `_actions` and `_checks` branches (Tier 1: commits, `put --expect`, `--if-absent`), and @@ -893,7 +897,7 @@ a scratch copy and the simulation finds a violation: |---|---| | `CAS` | a stale replica overwrites a record with its read: a finished job restarted or concluded twice (`finality`, `atMostOneAccepted`) | | `IF_ABSENT` | two replicas claim one run id, or one key, and overwrite each other (`oneRunPerKey`, `oneCreationPerKey`) | -| `GUARD_READS` | a commit expects only the records it writes: a sweep requeues a job of a run cancelled since it read, a rerun keeping its group does not see the group taken (`cancelledIsIdle`, `oneActivePerGroup`) | +| `GUARD_READS` | a commit expects only the records it writes: a sweep requeues a job of a run cancelled since it read, a push does not see the run it found done restarted by a rerun (`cancelledIsIdle`, `oneActivePerGroup`) | | `LEASE_CREATE_ONLY` | a blind lease put: two runners hold one job under one seq (`leaseExclusive`) | | `FENCE` | any result of an in_progress job is accepted: a stalled runner's late result concludes the job its successor holds (`acceptedWasHolder`) | | `FENCE_ON_JOB` | intake also compares the live lease's seq (the plan's "lease seq matches"): a lease taken over after the job started strands the job (`noStranded`) | @@ -905,9 +909,35 @@ a scratch copy and the simulation finds a violation: | `RERUN_NEW_ATTEMPT` | a rerun resets the attempt's jobs in place (`finality`, `attemptsAreFrozen`) | | `CHECK_FROM_JOB` | `_checks` is written from the runners' raw results: a late success becomes a check on a failed job (`checksEarned`) | +No single switch breaks `atMostOneAccepted`: a result is accepted once by the fence (a job takes +only the result under its holder and seq) and once by the guard on the job file (a second +accept of a finished job conflicts). `mutate:actions` turns both off to show it can fail. + +What modelling found in the design (before any code), each now a rule of the model: + +1. A result path needs the lease seq (`results////`): with one create-only + path per job, a late result of a lost runner blocks the next holder's, and the sweep (which + sees "a result") leaves the job in_progress for good. +2. Intake compares the result with the job file's holder and seq, not also with the live lease: + a lease can be taken over (the queue entry outlives the start) after the job file named the + first holder, and "the lease seq matches" would then strand the job. +3. A lease's `seq` counts claims, not refreshes, and an expired lease is taken over by + generation match (not deleted and created again, which would reuse seq 1). +4. A commit expects every record it read, not only those it writes. Simulation found two + races with only the written records guarded: a push that cancels run 1 did not expect the + job a sweep requeued meanwhile (a cancelled run kept a queued job: `cancelRacesSweepRun`), + and a push that found the previous run done did not expect the run a rerun then restarted + (two active runs in one group: `rerunRacesPushRun`). So a trigger or rerun expects the + group file, the group's previous holder and, when it cancels it, every job of it; a sweep + the run. +5. A sweep of a cancelled run's job concludes it cancelled, not requeued. +6. A rerun is a new commit into the concurrency group: it cancels a newer active run. +7. `_checks` is projected from the accepted job in `_actions`, never from `results/`, and is + repaired by reconcile (it is a second branch, written after the first). + Witnesses (`npm run witness:actions`): a lost runner's job is requeued and runs again, a run is cancelled, a run is rerun, an environment job is queued on an approval, a job is skipped. -`actions_scenarios.qnt` has 16 runs, for the plan's UC1, UC2, UC3, UC4, UC6, UC7 and UC8 +`actions_scenarios.qnt` has 18 runs, for the plan's UC1, UC2, UC3, UC4, UC6, UC7 and UC8 (and UC9's projection), written as single actions so that they compile with `quint-refinements` (checked by hand: the artifact is large, so none is committed). The refinement harness comes with the orchestrator (T1.7) and the runner (T2.5); until then the diff --git a/verify/actions.qnt b/verify/actions/actions.qnt similarity index 96% rename from verify/actions.qnt rename to verify/actions/actions.qnt index 489e102..701edff 100644 --- a/verify/actions.qnt +++ b/verify/actions/actions.qnt @@ -57,7 +57,8 @@ module actions { /// event and slot claims, the concurrency file. pure val IF_ABSENT = true /// A commit expects every record it read, not only those it writes (the concurrency file - /// on a rerun that keeps the holder; the run on a sweep). + /// on a rerun that keeps the holder; the run on a sweep; the group's previous holder; the + /// running jobs of a run it cancels). pure val GUARD_READS = true /// A runner claims a lease by create or generation match (else a blind put). pure val LEASE_CREATE_ONLY = true @@ -153,7 +154,7 @@ module actions { | ICheck(JobKey) /// What a decision writes, and the records it read without writing them. - type Delta = { w: T1, rdRuns: Set[int], rdGroups: Set[str] } + type Delta = { w: T1, rdRuns: Set[int], rdJobs: Set[JobKey], rdGroups: Set[str] } type Dec = Refuse | Do(Delta) /// A commit held at its write: what Tier 1 was when it read, and what it writes. type Commit = { intent: Intent, snap: T1, d: Delta } @@ -239,7 +240,7 @@ module actions { pure def jobDelta(jk: JobKey, j: Job): T1 = { ...EMPTY1, jobs: Map(jk -> j) } pure def runDelta(id: int, r: Run): T1 = { ...EMPTY1, runs: Map(id -> r) } - pure def doing(w: T1): Dec = Do({ w: w, rdRuns: Set(), rdGroups: Set() }) + pure def doing(w: T1): Dec = Do({ w: w, rdRuns: Set(), rdJobs: Set(), rdGroups: Set() }) /// A job's first state: queued at once if nothing holds it back, else pending. pure def freshJob(j: str): Job = { @@ -265,7 +266,12 @@ module actions { jobs: doomed.mapBy(jk => { ...v.jobs.get(jk), status: Completed, concl: Cancelled }), groups: if (prev == id) Map() else Map(g -> id), } - { w: w, rdRuns: Set(), rdGroups: Set(g) } + // it read the previous holder (done, or not: a rerun of it that lands in between must be + // seen), and every job of the run it cancels (a running one decides the marker, and a + // sweep or a start of one that lands between must not be overwritten by a cancelled run's + // job going back to the queue) + val read = v.jobs.keys().filter(jk => cancelling and jk.rid == prev and jk.att == pr.att) + { w: w, rdRuns: if (prev != 0 and prev != id) Set(prev) else Set(), rdJobs: read, rdGroups: Set(g) } } pure def withBase(d: Delta, base: T1): Delta = { ...d, w: merge(d.w, base) } @@ -329,7 +335,7 @@ module actions { if (r.cancel) { ...j, status: Completed, concl: Cancelled } else if (s.t2.started.contains({ jk: jk, seq: j.seq })) { ...j, status: Completed, concl: Failure, lost: j.lost + 1 } else { ...j, status: Queued, holder: "", lost: j.lost + 1 } - Do({ w: jobDelta(jk, nj), rdRuns: Set(jk.rid), rdGroups: Set() }) + Do({ w: jobDelta(jk, nj), rdRuns: Set(jk.rid), rdJobs: Set(), rdGroups: Set() }) } } @@ -374,7 +380,7 @@ module actions { val ck: CheckKey = { sha: shaOf(r.key), job: jk.job } val ch: Check = { rid: jk.rid, att: jk.att, state: state } if (v.checks.keys().contains(ck) and v.checks.get(ck) == ch) Refuse - else Do({ w: { ...EMPTY1, checks: Map(ck -> ch) }, rdRuns: Set(jk.rid), rdGroups: Set() }) + else Do({ w: { ...EMPTY1, checks: Map(ck -> ch) }, rdRuns: Set(jk.rid), rdJobs: Set(), rdGroups: Set() }) } } @@ -406,7 +412,7 @@ module actions { pure def landable(cur: T1, c: Commit): bool = all { guardOk(cur.runs, c.snap.runs, c.d.w.runs.keys(), c.d.rdRuns), guardOk(cur.claims, c.snap.claims, c.d.w.claims.keys(), Set()), - guardOk(cur.jobs, c.snap.jobs, c.d.w.jobs.keys(), Set()), + guardOk(cur.jobs, c.snap.jobs, c.d.w.jobs.keys(), c.d.rdJobs), guardOk(cur.groups, c.snap.groups, c.d.w.groups.keys(), c.d.rdGroups), guardOk(cur.checks, c.snap.checks, c.d.w.checks.keys(), Set()), } diff --git a/verify/actions_scenarios.qnt b/verify/actions/actions_scenarios.qnt similarity index 87% rename from verify/actions_scenarios.qnt rename to verify/actions/actions_scenarios.qnt index 5a6ccc5..f30fb9b 100644 --- a/verify/actions_scenarios.qnt +++ b/verify/actions/actions_scenarios.qnt @@ -364,6 +364,98 @@ module actionsScenarios { state' = state, }) + /// A newer push cancels run 1 while a sweep requeues its running job (the runner's lease + /// lapsed). The sweep lands first: the cancel commit, which read that job, finds it changed + /// and conflicts; read again, it cancels the requeued job too. (Without the guard on the + /// jobs it read, the cancelled run would keep a queued job: found by simulation.) + /// @conformance + run cancelRacesSweepRun = init + .then(fire("push1")) + .then(read("o1", ITrigger("push1"))) + .then(write("o1")) + .then(sync) + .then(claimRead("r1", BLD)) + .then(claimWrite("r1")) + .then(read("o1", IStart(BLD))) + .then(write("o1")) + .then(tick) + .then(tick) + .then(read("o2", ISweep(BLD))) + .then(fire("push2")) + .then(read("o1", ITrigger("push2"))) + .then(write("o2")) + .then(write("o1")) + .then(all { + assert(all { + state.t1.jobs.get(BLD).status == Queued, + not(state.t1.runs.get(1).cancel), + state.t1.runs.keys() == Set(1), + }), + state' = state, + }) + .then(read("o1", ITrigger("push2"))) + .then(write("o1")) + .then(all { + assert(all { + state.t1.runs.get(1).cancel, + state.t1.jobs.get(BLD).concl == Cancelled, + cancelledIsIdle, + oneActivePerGroup, + }), + state' = state, + }) + + /// A failed run is rerun while a newer push takes the group over. Both read the run done + /// (so the push has nothing to cancel); the rerun lands first, the push finds the run + /// changed and conflicts, and read again it cancels the rerun. (Without the guard on the + /// previous holder, two runs would be active in the group: found by simulation.) + /// @conformance + run rerunRacesPushRun = init + .then(fire("push1")) + .then(read("o1", ITrigger("push1"))) + .then(write("o1")) + .then(sync) + .then(claimRead("r1", BLD)) + .then(claimWrite("r1")) + .then(read("o1", IStart(BLD))) + .then(write("o1")) + .then(started("r1")) + .then(result("r1", Failure)) + .then(read("o1", IAccept({ jk: BLD, seq: 1 }))) + .then(write("o1")) + .then(read("o1", IPromote(TST))) + .then(write("o1")) + .then(read("o1", IPromote(DEP))) + .then(write("o1")) + .then(read("o1", IFinish(1))) + .then(write("o1")) + .then(fire("push2")) + .then(read("o1", IRerun(1))) + .then(read("o2", ITrigger("push2"))) + .then(write("o1")) + .then(write("o2")) + .then(all { + assert(all { + state.t1.runs.keys() == Set(1), + state.t1.runs.get(1).att == 2, + not(state.t1.runs.get(1).done), + state.pend.get("o2") == NoPend, + }), + state' = state, + }) + .then(read("o2", ITrigger("push2"))) + .then(write("o2")) + .then(all { + assert(all { + state.t1.runs.get(1).cancel, + not(state.t1.runs.get(2).cancel), + state.t1.groups == Map("main" -> 2), + oneActivePerGroup, + cancelledIsIdle, + }), + state' = state, + }) + /// Two runners read the queue entry at once: the lease write has one winner, and the other /// finds the lease changed and leaves the job. /// @conformance diff --git a/verify/actions_sim.qnt b/verify/actions/actions_sim.qnt similarity index 87% rename from verify/actions_sim.qnt rename to verify/actions/actions_sim.qnt index dc322ae..f6da210 100644 --- a/verify/actions_sim.qnt +++ b/verify/actions/actions_sim.qnt @@ -54,8 +54,28 @@ module actionsSim { action simInit = all { state' = INITIAL, ghost' = GHOST0 } + /// A step's kind: a trace picks among the kinds that can happen, then a step of that kind, + /// so that the rare (a replica's write between a runner's steps) are not drowned by the many + /// (every intent a replica might read). + pure def kindOf(a: Act): int = match a { + | ATick => 0 + | AFire(_) => 1 + | AApprove(_) => 2 + | ARead(_) => 3 + | AWrite(_) => 4 + | ASync => 5 + | AClaimRead(_) => 6 + | AClaimWrite(_) => 7 + | ARefresh(_) => 8 + | AStarted(_) => 9 + | AResult(_) => 10 + | ACrash(_) => 11 + } + action simStep = { - nondet a = acts(state).oneOf() + val all_ = acts(state) + nondet kind = all_.map(kindOf).oneOf() + nondet a = all_.filter(x => kindOf(x) == kind).oneOf() all { state' = apply(state, a), ghost' = ghostAfter(ghost, state, a, apply(state, a)), diff --git a/verify/mutate_actions.sh b/verify/mutate_actions.sh index 4f19933..7accc2b 100644 --- a/verify/mutate_actions.sh +++ b/verify/mutate_actions.sh @@ -1,14 +1,15 @@ #!/bin/sh # Flip each design switch of actions.qnt (the protocol without that fix) in a scratch copy and -# check that the simulation finds a violation of `simSafety`. +# check that the simulation finds a violation of `simSafety`. (The models live in `actions/`: a +# `.qnt` file beside `scenarios.qnt` would change the digest of every generated artifact.) set -e tmp=$(mktemp -d) trap 'rm -rf "$tmp"' EXIT for sw in CAS IF_ABSENT GUARD_READS LEASE_CREATE_ONLY FENCE FENCE_ON_JOB RESULT_PER_LEASE SWEEP \ NEEDS_CHECK APPROVAL_EXCLUDES_ACTOR CANCEL_IN_PROGRESS RERUN_NEW_ATTEMPT CHECK_FROM_JOB; do - cp actions.qnt actions_sim.qnt "$tmp"/ - sed "s/pure val $sw = true/pure val $sw = false/" actions.qnt > "$tmp/actions.qnt" - if cmp -s actions.qnt "$tmp/actions.qnt"; then echo "no such switch: $sw"; exit 1; fi + cp actions/actions.qnt actions/actions_sim.qnt "$tmp"/ + sed "s/pure val $sw = true/pure val $sw = false/" actions/actions.qnt > "$tmp/actions.qnt" + if cmp -s actions/actions.qnt "$tmp/actions.qnt"; then echo "no such switch: $sw"; exit 1; fi if (cd "$tmp" && quint run actions_sim.qnt --main=actionsSim --init=simInit --step=simStep --invariant=simSafety --max-steps=60 --max-samples=300000 | grep -q '^\[violation\]'); then echo "caught: $sw = false" else @@ -16,3 +17,12 @@ for sw in CAS IF_ABSENT GUARD_READS LEASE_CREATE_ONLY FENCE FENCE_ON_JOB RESULT_ exit 1 fi done +# At most one accepted result per job is held twice over (the fence, and the guard on the job +# file): it takes both off to break it. +sed "s/pure val CAS = true/pure val CAS = false/; s/pure val FENCE = true/pure val FENCE = false/" actions/actions.qnt > "$tmp/actions.qnt" +if (cd "$tmp" && quint run actions_sim.qnt --main=actionsSim --init=simInit --step=simStep --invariant=atMostOneAccepted --max-steps=60 --max-samples=300000 | grep -q '^\[violation\]'); then + echo "caught: CAS = false and FENCE = false" +else + echo "not caught: CAS = false and FENCE = false" + exit 1 +fi diff --git a/verify/package.json b/verify/package.json index 1ed08d6..a74066e 100644 --- a/verify/package.json +++ b/verify/package.json @@ -9,14 +9,14 @@ "compile:policy": "quint-refinements compile policy_scenarios.qnt --module policyScenarios --compact --artifact policy/policy-refinements.json --rust ../tests/policy_refinement/generated.rs --go policy/pailpolicy_refinement_gen_test.go --go-package gateway", "compile:pr": "quint-refinements compile pr_scenarios.qnt --module prScenarios --compact --artifact pr-refinements.json --rust ../tests/pr_refinement/generated.rs", "check": "npm run compile:publish -- --check && npm run compile:store -- --check && npm run compile:policy -- --check && npm run compile:pr -- --check", - "test": "quint test store_scenarios.qnt --main=storeScenarios --match='Run$' && quint test scenarios.qnt --main=scenarios --match='Run$' && quint test policy_scenarios.qnt --main=policyScenarios --match='Run$' && quint test pr_scenarios.qnt --main=prScenarios --match='Run$' && quint test actions_scenarios.qnt --main=actionsScenarios --match='Run$'", + "test": "quint test store_scenarios.qnt --main=storeScenarios --match='Run$' && quint test scenarios.qnt --main=scenarios --match='Run$' && quint test policy_scenarios.qnt --main=policyScenarios --match='Run$' && quint test pr_scenarios.qnt --main=prScenarios --match='Run$' && quint test actions/actions_scenarios.qnt --main=actionsScenarios --match='Run$'", "simulate": "quint run pail.qnt --main=pail --invariant=safety --max-steps=100 --max-samples=20000 && quint run pail.qnt --main=pail --step=contendStep --invariant=safety --max-steps=60 --max-samples=20000 && npm run simulate:pr && npm run simulate:actions", "simulate:pr": "quint run pr_sim.qnt --main=prSim --init=simInit --step=simStep --invariant=simSafety --max-steps=60 --max-samples=50000", "witness": "for inv in gcNeverDeletesAPack gcNeverDeletesAChunk branchHasNoHugeFile; do quint run pail.qnt --main=pail --invariant=$inv --max-steps=100 --max-samples=200000 | grep -q '^\\[violation\\]' || { echo \"never reached: $inv\"; exit 1; }; done", "witness:pr": "for inv in neverMerged neverOutdated neverStale; do quint run pr_sim.qnt --main=prSim --init=simInit --step=simStep --invariant=$inv --max-steps=60 --max-samples=50000 | grep -q '^\\[violation\\]' || { echo \"never reached: $inv\"; exit 1; }; done", "mutate:pr": "sh mutate_pr.sh", - "simulate:actions": "quint run actions_sim.qnt --main=actionsSim --init=simInit --step=simStep --invariant=simSafety --max-steps=60 --max-samples=60000", - "witness:actions": "for inv in neverRequeued neverCancelled neverRerun neverApproved neverSkipped; do quint run actions_sim.qnt --main=actionsSim --init=simInit --step=simStep --invariant=$inv --max-steps=60 --max-samples=50000 | grep -q '^\\[violation\\]' || { echo \"never reached: $inv\"; exit 1; }; done", + "simulate:actions": "quint run actions/actions_sim.qnt --main=actionsSim --init=simInit --step=simStep --invariant=simSafety --max-steps=60 --max-samples=60000", + "witness:actions": "for inv in neverRequeued neverCancelled neverRerun neverApproved neverSkipped; do quint run actions/actions_sim.qnt --main=actionsSim --init=simInit --step=simStep --invariant=$inv --max-steps=60 --max-samples=50000 | grep -q '^\\[violation\\]' || { echo \"never reached: $inv\"; exit 1; }; done", "mutate:actions": "sh mutate_actions.sh" }, "devDependencies": { From 7d780740881bc8668ac6429c3b4dffc5ae614df9 Mon Sep 17 00:00:00 2001 From: calvin-archastro Date: Sat, 31 Oct 2026 08:54:49 -0700 Subject: [PATCH 3/4] Run the actions witnesses and mutants in the manual model workflow Co-Authored-By: Claude Opus 5.5 --- .github/workflows/model.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/model.yml b/.github/workflows/model.yml index 2ecd624..66757f1 100644 --- a/.github/workflows/model.yml +++ b/.github/workflows/model.yml @@ -22,3 +22,5 @@ jobs: - run: npm run witness - run: npm run witness:pr - run: npm run mutate:pr + - run: npm run witness:actions + - run: npm run mutate:actions From 169352e537a388257a8aef16fde5cc8330e6ad08 Mon Sep 17 00:00:00 2001 From: calvin-archastro Date: Sat, 31 Oct 2026 09:48:36 -0700 Subject: [PATCH 4/4] Actions model: wake-ups come from the events model's contract; mutant: events only An orchestrator replica ticks (`read`) only when woken. Every write to a branch or an object of the area is announced to all replicas; an announcement may be lost, repeated or reordered (a wake is a flag), and the safety poll and the start-up diff against the cursor (verify/events/events.qnt) wake a replica whatever it was told. Time passing announces nothing, so a lease that lapses is found only by the poll. - State `woken`; actions `wake` (safety poll / resume) and `lose` (announcement lost). - `noStranded` now also needs some replica to tick (`willTick`). - New switch SAFETY_POLL: off is "the orchestrator relies on events only"; the sim finds a stranded job (noStranded). mutate_actions.sh runs it with the other switches. - Scenario safetyPollSweepsRun; witnesses neverLostWake, neverPolled. - All earlier properties, witnesses, mutants and the 18 scenarios still pass. Co-Authored-By: Claude Opus 5.5 --- verify/README.md | 18 +++++-- verify/actions/actions.qnt | 76 ++++++++++++++++++++++------ verify/actions/actions_scenarios.qnt | 40 +++++++++++++++ verify/actions/actions_sim.qnt | 13 ++++- verify/mutate_actions.sh | 2 +- verify/package.json | 2 +- 6 files changed, 130 insertions(+), 21 deletions(-) diff --git a/verify/README.md b/verify/README.md index a3bfd60..9626e42 100644 --- a/verify/README.md +++ b/verify/README.md @@ -858,6 +858,14 @@ read. Runners claim a lease (`claimRead`, then `claimWrite`: create, or take ove one by generation match), refresh it, report a step started, write a create-only result, see a cancel marker, or crash. Approvers create approval files. +A replica ticks only when woken (`woken`), by the contract of `pail events --branch '*' +--prefix actions/ --cursor ...` (`events/events.qnt`, in the events model's section): every +write to `_actions`, `_checks` or an object of the area is announced (`announced`) to every +replica; an announcement may be lost (`lose`), and repeating or reordering one changes +nothing (a wake is a flag); the safety poll (`wake`) and the start-up diff against the +cursor wake a replica whatever it was told; time passing announces nothing, so a lease that +lapses is found only by the poll. A write that conflicts sends its replica back to read. + | Intent | Commit | |---|---| | `ITrigger` | a run from an event key, cron slot: `runs/` (`--if-absent`), `claims/` (`--if-absent`), its jobs, `concurrency/` (CAS), cancelling the group's previous run | @@ -874,7 +882,9 @@ Properties (`safety` in `actions.qnt`; `simSafety` adds the history ones of `act job); `acceptedWasHolder`: the result a job concluded by is the holder's and seq's it started under. 2. `noStranded`: a job is never in_progress with a lapsed lease unless the orchestrator can - accept its result or sweep it (the state form of "no job stays in_progress forever"). + accept its result or sweep it, and some replica will tick to do it (`willTick`: woken, + mid-commit, or the safety poll will come); the state form of "no job stays in_progress + forever", given that events may be lost. 3. `finality` and `attemptsAreFrozen` (sim): `completed`, its conclusion and who concluded it never change; a rerun is a new attempt and the old one keeps its conclusion. 4. `ordering`: a job is queued, waiting, started or concluded by a runner only when every @@ -903,6 +913,7 @@ a scratch copy and the simulation finds a violation: | `FENCE_ON_JOB` | intake also compares the live lease's seq (the plan's "lease seq matches"): a lease taken over after the job started strands the job (`noStranded`) | | `RESULT_PER_LEASE` | one create-only result path per job: a late result of a lost runner blocks the next holder's, and the sweep sees a result (`noStranded`) | | `SWEEP` | a runner that dies leaves its job in_progress for good (`noStranded`) | +| `SAFETY_POLL` | the orchestrator relies on events only: a lease that lapses, a lost announcement, writes nothing to wake anyone, and the job is stranded (`noStranded`) | | `NEEDS_CHECK` | a job is queued before its need concluded (`ordering`) | | `APPROVAL_EXCLUDES_ACTOR` | the actor approves their own deploy (`gatesHold`) | | `CANCEL_IN_PROGRESS` | a push does not cancel the run it supersedes (`oneActivePerGroup`) | @@ -936,8 +947,9 @@ What modelling found in the design (before any code), each now a rule of the mod repaired by reconcile (it is a second branch, written after the first). Witnesses (`npm run witness:actions`): a lost runner's job is requeued and runs again, a run is -cancelled, a run is rerun, an environment job is queued on an approval, a job is skipped. -`actions_scenarios.qnt` has 18 runs, for the plan's UC1, UC2, UC3, UC4, UC6, UC7 and UC8 +cancelled, a run is rerun, an environment job is queued on an approval, a job is skipped, a +wake-up is lost, the safety poll wakes a replica. +`actions_scenarios.qnt` has 19 runs, for the plan's UC1, UC2, UC3, UC4, UC6, UC7 and UC8 (and UC9's projection), written as single actions so that they compile with `quint-refinements` (checked by hand: the artifact is large, so none is committed). The refinement harness comes with the orchestrator (T1.7) and the runner (T2.5); until then the diff --git a/verify/actions/actions.qnt b/verify/actions/actions.qnt index 701edff..f6161f5 100644 --- a/verify/actions/actions.qnt +++ b/verify/actions/actions.qnt @@ -85,6 +85,12 @@ module actions { /// `_checks` is projected from the accepted job (else from the runners' raw results). pure val CHECK_FROM_JOB = true + /// The orchestrator also ticks every so often, whatever it was told (the events model's + /// safety poll, `verify/events/events.qnt`), and when it starts (the cursor resume). Else + /// it ticks only on events, and a lease that expires, which writes nothing and so announces + /// nothing, strands its job. + pure val SAFETY_POLL = true + pure def needsOf(j: str): Set[str] = if (j == "build") Set() else Set("build") /// The job has `environment: prod`. pure def gated(j: str): bool = j == "deploy" @@ -175,6 +181,9 @@ module actions { t2: T2, runners: str -> Runner, pend: str -> PendO, + // the replicas with a wake-up pending: an event announced a write, the safety poll came + // due, or the replica started. A replica ticks (`read`) only when woken. + woken: Set[str], } pure val EMPTY1: T1 = { runs: Map(), claims: Map(), jobs: Map(), groups: Map(), checks: Map(), approvals: Set() } @@ -186,6 +195,7 @@ module actions { t2: { queue: Set(), leases: Map(), results: Map(), cancels: Set(), started: Set() }, runners: RUNNERS.mapBy(r => { alive: true, ph: RIdle }), pend: REPLICAS.mapBy(o => NoPend), + woken: REPLICAS, } // ---------- reading ---------- @@ -426,11 +436,36 @@ module actions { | NoPend => false } - pure def readCan(s: State, o: str, i: Intent): bool = not(isPend(s.pend.get(o))) and deciding(s, i) + // ---------- wake-ups: the events model's contract ---------- + // + // `pail events --branch '*' --prefix actions/ --cursor ...` runs beside each replica and + // wakes it. Its contract (`events.qnt`): a notification is only a hint; one may be lost, + // repeated or reordered (a wake is a flag, so repeating and reordering change nothing, and + // `lose` drops it); the safety poll re-lists everything every so often and the start-up + // diff against the cursor emits what changed while the process was down, so a wake lost + // only delays a tick (`wake`). What announces nothing, the passing of time, wakes no one. + + /// A write to a branch or an object of the area was announced to every replica. + pure def announced(s: State): State = s.with("woken", REPLICAS) + + pure def wakeCan(s: State, o: str): bool = SAFETY_POLL and not(s.woken.contains(o)) + pure def wakeNext(s: State, o: str): State = s.with("woken", s.woken.union(Set(o))) + + pure def loseCan(s: State, o: str): bool = s.woken.contains(o) + pure def loseNext(s: State, o: str): State = s.with("woken", s.woken.exclude(Set(o))) + + /// Some replica will tick: it is woken, mid-commit (its write is a ref event and a retry), + /// or the safety poll will come. + pure def willTick(s: State): bool = SAFETY_POLL or s.woken.size() > 0 or REPLICAS.exists(o => isPend(s.pend.get(o))) + + pure def readCan(s: State, o: str, i: Intent): bool = + not(isPend(s.pend.get(o))) and s.woken.contains(o) and deciding(s, i) + /// A tick takes the wake-up it answers. pure def readNext(s: State, o: str, i: Intent): State = match decide(s, i) { | Refuse => s | Do(d) => s.with("pend", s.pend.set(o, Pend({ intent: i, snap: s.t1, d: d }))) + .with("woken", s.woken.exclude(Set(o))) } pure def writeCan(s: State, o: str): bool = isPend(s.pend.get(o)) @@ -439,19 +474,21 @@ module actions { pure def writeNext(s: State, o: str): State = match s.pend.get(o) { | NoPend => s | Pend(c) => - val s2 = s.with("pend", s.pend.set(o, NoPend)) - if (landable(s.t1, c)) s2.with("t1", landed(s.t1, c)) else s2 + // a conflict sends the replica back to read again; a landed commit is announced to all + val s2 = s.with("pend", s.pend.set(o, NoPend)).with("woken", s.woken.union(Set(o))) + if (landable(s.t1, c)) announced(s2.with("t1", landed(s.t1, c))) else s2 } /// The orchestrator keeps the queue to the queued jobs, and marks the running jobs of /// cancelled runs. (Both are idempotent Tier 2 writes, and may lag.) pure def syncNext(s: State): State = { val v = s.t1 - s.with("t2", { + val t = s.with("t2", { ...s.t2, queue: v.jobs.keys().filter(jk => v.jobs.get(jk).status == Queued), cancels: s.t2.cancels.union(v.jobs.keys().filter(jk => v.jobs.get(jk).status == InProgress and runOf(v, jk.rid).cancel)), }) + if (t.t2 == s.t2) s else announced(t) } pure def tickCan(s: State): bool = s.now < MAX_T @@ -483,8 +520,8 @@ module actions { pure def claimWriteNext(s: State, r: str): State = match s.runners.get(r).ph { | RReading(x) => if (not(LEASE_CREATE_ONLY) or leaseOf(s.t2, x.jk) == x.seen) - setRunner(setLease(s, x.jk, { holder: r, seq: x.seen.seq + 1, exp: s.now + TTL }), r, - RHolding({ jk: x.jk, seq: x.seen.seq + 1, started: false })) + announced(setRunner(setLease(s, x.jk, { holder: r, seq: x.seen.seq + 1, exp: s.now + TTL }), r, + RHolding({ jk: x.jk, seq: x.seen.seq + 1, started: false }))) else setRunner(s, r, RIdle) | _ => s } @@ -499,7 +536,7 @@ module actions { pure def refreshNext(s: State, r: str): State = match s.runners.get(r).ph { | RHolding(x) => val l = leaseOf(s.t2, x.jk) - if (l.holder == r and l.seq == x.seq) setLease(s, x.jk, { ...l, exp: s.now + TTL }) + if (l.holder == r and l.seq == x.seq) announced(setLease(s, x.jk, { ...l, exp: s.now + TTL })) else setRunner(s, r, RIdle) | _ => s } @@ -511,8 +548,8 @@ module actions { pure def startedNext(s: State, r: str): State = match s.runners.get(r).ph { | RHolding(x) => - setRunner(s, r, RHolding({ ...x, started: true })) - .with("t2", { ...s.t2, started: s.t2.started.union(Set({ jk: x.jk, seq: x.seq })) }) + announced(setRunner(s, r, RHolding({ ...x, started: true })) + .with("t2", { ...s.t2, started: s.t2.started.union(Set({ jk: x.jk, seq: x.seq })) })) | _ => s } @@ -527,7 +564,7 @@ module actions { | RHolding(x) => val rk: ResKey = { jk: x.jk, seq: resSeq(x.seq) } if (s.t2.results.keys().contains(rk)) setRunner(s, r, RIdle) - else setRunner(s, r, RIdle).with("t2", { ...s.t2, results: s.t2.results.put(rk, { runner: r, seq: x.seq, concl: c }) }) + else announced(setRunner(s, r, RIdle).with("t2", { ...s.t2, results: s.t2.results.put(rk, { runner: r, seq: x.seq, concl: c }) })) | _ => s } @@ -538,7 +575,7 @@ module actions { s.t1.runs.keys().contains(a.rid) and a.att <= s.t1.runs.get(a.rid).att and not(s.t1.approvals.contains(a)) pure def approveNext(s: State, a: Approval): State = - s.with("t1", { ...s.t1, approvals: s.t1.approvals.union(Set(a)) }) + announced(s.with("t1", { ...s.t1, approvals: s.t1.approvals.union(Set(a)) })) // ---------- every step, as data (so that the simulation can wrap each) ---------- @@ -555,6 +592,8 @@ module actions { | AStarted(str) | AResult({ r: str, c: Concl }) | ACrash(str) + | AWake(str) + | ALose(str) pure def intentsOf(s: State): Set[Intent] = { val js = s.t1.jobs.keys() @@ -589,11 +628,13 @@ module actions { .union(live.filter(r => startedCan(s, r)).map(r => AStarted(r))) .union(unions(live.map(r => Set(Success, Failure, Cancelled).filter(c => resultCan(s, r, c)).map(c => AResult({ r: r, c: c }))))) .union(live.map(r => ACrash(r))) + .union(REPLICAS.filter(o => wakeCan(s, o)).map(o => AWake(o))) + .union(REPLICAS.filter(o => loseCan(s, o)).map(o => ALose(o))) } pure def apply(s: State, a: Act): State = match a { | ATick => tickNext(s) - | AFire(k) => s.with("occurred", s.occurred.union(Set(k))) + | AFire(k) => announced(s.with("occurred", s.occurred.union(Set(k)))) | AApprove(x) => approveNext(s, x) | ARead(x) => readNext(s, x.o, x.i) | AWrite(o) => writeNext(s, o) @@ -604,6 +645,8 @@ module actions { | AStarted(r) => startedNext(s, r) | AResult(x) => resultNext(s, x.r, x.c) | ACrash(r) => crashNext(s, r) + | AWake(o) => wakeNext(s, o) + | ALose(o) => loseNext(s, o) } // ---------- actions ---------- @@ -630,6 +673,8 @@ module actions { action started(r: str): bool = all { startedCan(state, r), state' = startedNext(state, r) } action result(r: str, c: Concl): bool = all { resultCan(state, r, c), state' = resultNext(state, r, c) } action crash(r: str): bool = all { state.runners.get(r).alive, state' = crashNext(state, r) } + action wake(o: str): bool = all { wakeCan(state, o), state' = wakeNext(state, o) } + action lose(o: str): bool = all { loseCan(state, o), state' = loseNext(state, o) } /// Any interleaving: one enabled step, uniformly. action step = { @@ -640,11 +685,12 @@ module actions { // ---------- properties ---------- /// 2. No job stays in_progress once its lease has expired: it is live (its holder's lease - /// has not), or the orchestrator can accept its result or sweep it. + /// has not), or the orchestrator can accept its result or sweep it, and some replica will + /// tick to do it (`willTick`: woken, mid-commit, or the safety poll will come). val noStranded: bool = state.t1.jobs.keys().forall(jk => { val j = state.t1.jobs.get(jk) - j.status != InProgress or liveFor(state, jk, j) or - state.t2.results.keys().exists(rk => rk.jk == jk and deciding(state, IAccept(rk))) or deciding(state, ISweep(jk)) + j.status != InProgress or liveFor(state, jk, j) or (willTick(state) and ( + state.t2.results.keys().exists(rk => rk.jk == jk and deciding(state, IAccept(rk))) or deciding(state, ISweep(jk)))) }) /// 4. A job queued, waiting, started or concluded by a runner has all its needs succeeded; diff --git a/verify/actions/actions_scenarios.qnt b/verify/actions/actions_scenarios.qnt index f30fb9b..3c9efbb 100644 --- a/verify/actions/actions_scenarios.qnt +++ b/verify/actions/actions_scenarios.qnt @@ -259,6 +259,46 @@ module actionsScenarios { state' = state, }) + /// UC4, and the events contract (`events.qnt`). The runner dies; the lease lapsing writes + /// nothing, so no event announces it, and the events that did arrive were lost. Only the + /// safety poll wakes a replica, which sweeps the job. (A replica cannot tick unwoken.) + /// @conformance + run safetyPollSweepsRun = init + .then(fire("push1")) + .then(read("o1", ITrigger("push1"))) + .then(write("o1")) + .then(sync) + .then(claimRead("r1", BLD)) + .then(claimWrite("r1")) + .then(read("o1", IStart(BLD))) + .then(write("o1")) + .then(crash("r1")) + // the announcements of those writes are lost, and the lease lapses in silence + .then(lose("o1")) + .then(lose("o2")) + .then(tick) + .then(tick) + .then(all { + assert(all { + deciding(state, ISweep(BLD)), + state.woken == Set(), + not(readCan(state, "o1", ISweep(BLD))), + }), + state' = state, + }) + .then(wake("o2")) + .then(read("o2", ISweep(BLD))) + .then(write("o2")) + .then(all { + assert(all { + state.t1.jobs.get(BLD).status == Queued, + state.t1.jobs.get(BLD).lost == 1, + // the commit was announced: both replicas are woken again + state.woken == Set("o1", "o2"), + }), + state' = state, + }) + /// UC4. The runner dies after a step started: the job concludes failure, "runner lost", /// and its dependents are skipped. /// @conformance diff --git a/verify/actions/actions_sim.qnt b/verify/actions/actions_sim.qnt index f6da210..00468de 100644 --- a/verify/actions/actions_sim.qnt +++ b/verify/actions/actions_sim.qnt @@ -20,11 +20,14 @@ module actionsSim { ran: RunAtt -> Concl, // how many commits created the run of each event key creates: str -> int, + // for the witnesses: a wake-up was lost, a safety poll ticked a replica + lost: bool, + polled: bool, } var ghost: Ghost - pure val GHOST0: Ghost = { accepted: Map(), done: Map(), ran: Map(), creates: EVENTS.mapBy(k => 0) } + pure val GHOST0: Ghost = { accepted: Map(), done: Map(), ran: Map(), creates: EVENTS.mapBy(k => 0), lost: false, polled: false } /// What the step `a`, taking `s` to `t`, did to the ghost. pure def ghostAfter(g: Ghost, s: State, a: Act, t: State): Ghost = { @@ -49,6 +52,8 @@ module actionsSim { done: fresh.fold(g.done, (m, jk) => m.put(jk, { concl: jobs.get(jk).concl, by: jobs.get(jk).by, byseq: jobs.get(jk).byseq })), ran: freshRuns.fold(g.ran, (m, id) => m.put({ rid: id, att: runs.get(id).att }, runs.get(id).concl)), creates: g.creates.keys().mapBy(k => g.creates.get(k) + (if (created.contains(k)) 1 else 0)), + lost: g.lost or (match a { | ALose(_) => true | _ => false }), + polled: g.polled or (match a { | AWake(_) => true | _ => false }), } } @@ -70,6 +75,8 @@ module actionsSim { | AStarted(_) => 9 | AResult(_) => 10 | ACrash(_) => 11 + | AWake(_) => 12 + | ALose(_) => 13 } action simStep = { @@ -115,6 +122,10 @@ module actionsSim { val neverRerun: bool = not(state.t1.runs.keys().exists(id => state.t1.runs.get(id).att > 1)) /// A job behind an environment gate is queued, on an approval. val neverApproved: bool = not(state.t1.jobs.keys().exists(jk => gated(jk.job) and (state.t1.jobs.get(jk).status == InProgress or state.t1.jobs.get(jk).status == Queued))) + /// An event's wake-up is lost. + val neverLostWake: bool = not(ghost.lost) + /// The safety poll wakes a replica. + val neverPolled: bool = not(ghost.polled) /// A job is skipped because a need failed. val neverSkipped: bool = not(state.t1.jobs.keys().exists(jk => state.t1.jobs.get(jk).concl == Skipped)) } diff --git a/verify/mutate_actions.sh b/verify/mutate_actions.sh index 7accc2b..c0ccf02 100644 --- a/verify/mutate_actions.sh +++ b/verify/mutate_actions.sh @@ -6,7 +6,7 @@ set -e tmp=$(mktemp -d) trap 'rm -rf "$tmp"' EXIT for sw in CAS IF_ABSENT GUARD_READS LEASE_CREATE_ONLY FENCE FENCE_ON_JOB RESULT_PER_LEASE SWEEP \ - NEEDS_CHECK APPROVAL_EXCLUDES_ACTOR CANCEL_IN_PROGRESS RERUN_NEW_ATTEMPT CHECK_FROM_JOB; do + NEEDS_CHECK APPROVAL_EXCLUDES_ACTOR CANCEL_IN_PROGRESS RERUN_NEW_ATTEMPT CHECK_FROM_JOB SAFETY_POLL; do cp actions/actions.qnt actions/actions_sim.qnt "$tmp"/ sed "s/pure val $sw = true/pure val $sw = false/" actions/actions.qnt > "$tmp/actions.qnt" if cmp -s actions/actions.qnt "$tmp/actions.qnt"; then echo "no such switch: $sw"; exit 1; fi diff --git a/verify/package.json b/verify/package.json index a74066e..8e164ab 100644 --- a/verify/package.json +++ b/verify/package.json @@ -16,7 +16,7 @@ "witness:pr": "for inv in neverMerged neverOutdated neverStale; do quint run pr_sim.qnt --main=prSim --init=simInit --step=simStep --invariant=$inv --max-steps=60 --max-samples=50000 | grep -q '^\\[violation\\]' || { echo \"never reached: $inv\"; exit 1; }; done", "mutate:pr": "sh mutate_pr.sh", "simulate:actions": "quint run actions/actions_sim.qnt --main=actionsSim --init=simInit --step=simStep --invariant=simSafety --max-steps=60 --max-samples=60000", - "witness:actions": "for inv in neverRequeued neverCancelled neverRerun neverApproved neverSkipped; do quint run actions/actions_sim.qnt --main=actionsSim --init=simInit --step=simStep --invariant=$inv --max-steps=60 --max-samples=50000 | grep -q '^\\[violation\\]' || { echo \"never reached: $inv\"; exit 1; }; done", + "witness:actions": "for inv in neverRequeued neverCancelled neverRerun neverApproved neverSkipped neverLostWake neverPolled; do quint run actions/actions_sim.qnt --main=actionsSim --init=simInit --step=simStep --invariant=$inv --max-steps=60 --max-samples=50000 | grep -q '^\\[violation\\]' || { echo \"never reached: $inv\"; exit 1; }; done", "mutate:actions": "sh mutate_actions.sh" }, "devDependencies": {