Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 9 additions & 4 deletions docs/architecture/task-lifecycle-model.md
Original file line number Diff line number Diff line change
Expand Up @@ -52,12 +52,16 @@ TLA+/PlusCal or Quint with TLC becomes a better fit when the lifecycle needs tem
| Atomic event step | `atomicReadAndUpdate`, `atomicUpdatePair`, and per-parent delegation transition lock |
| Event interleaving | Competing completion, cancellation, abandonment, and new delegation calls |

The model has three fixed task slots, enough to cover competing siblings and a nested parent-child-grandchild chain. It explores every reachable interleaving through depth 12, deduplicating canonical states. Representative checks also exercise rejected operations that do not create a new state: a second concurrent delegation while the first child is active, stale completion after re-delegation, late completion after abandonment, completion after interruption, and nested completion. Named semantic landmarks require the graph to retain interrupted-child re-delegation and nested delegation even when the raw state total changes.
The model has three fixed task slots, enough to cover competing siblings and a nested parent-child-grandchild chain. It explores every reachable interleaving through depth 12, deduplicating canonical states. Runtime ownership is modeled separately from persisted status: an `owner-loss` fault can remove the live owner of an active or delegated child without changing its history record, matching process termination or session skip. Recovery is enabled only when the awaited delegation chain has no live owner and ends in an interrupted/completed task, a delegated task with no `awaitingChildId`, or a missing awaited record whose task ID also has no live owner. Representative checks also exercise rejected operations that do not create a new state: a second concurrent delegation while the first child is active, stale completion after re-delegation, late completion after abandonment, completion after interruption, and nested completion. Named semantic landmarks require the graph to retain interrupted-child re-delegation, nested delegation, and owner-loss recovery even when the raw state total changes.

Each task slot can also hold one of two pending `create_subtask` actions. A `stage` action mirrors `setPendingTaskAction` overwrite semantics, delegation clears the action its request carried, completion clears the child's action only when its event carries the matching action ID, and a `settle-rejected` action models the settlement that follows an authoritative delegation rejection (#1714). Production settles through the typed `LifecycleTransitionError` from the shared guards: the provider calls the disk-authoritative `TaskHistoryStore.clearPendingActionIfMatching` compare-and-clear under the per-file lock, then propagates the original rejection. Six named witnesses must remain reachable: settlement from an interrupted record after rejection, settlement through a successful active delegation, unrelated-action preservation during completion, stale-action protection where a settlement targeting one action ID leaves a replacement action intact, matching-ID completion clearing, and replacement-ID completion preservation. A mismatched pending-action request keeps its production behavior: the atomic update throws before any transition, and no settlement runs.

Production completion also accepts a recovery-compatible `active` parent that still awaits the returning child, then clears the stale pointers. Normal model transitions never create that intermediate state, so it is covered by a focused reducer test rather than admitted as a generally valid reachable state.

The `recover-active` action models startup repair after an active child loses its owner. `recoverDelegationParent` clears the parent's child pointers but interrupts it when an ancestor still awaits it; a top-level parent becomes active. The repair journal accepts both target statuses so a crash between the child and parent writes cannot break that ancestor link. Filesystem tests cover journal replay and subsequent re-delegation. Provider tests separately cover registration delayed by the recovery reservation, including disposal or cancellation before registration and preventing later scheduling.

For [#1624](https://github.com/Zoo-Code-Org/Zoo-Code/issues/1624), `recoverDeadDelegatedChild` repairs a nested delegated child whose descendant chain ends dead. Startup reconciliation preserves chains ending in an interrupted descendant, allowing its resumed completion to reopen its immediate parent; only explicit runtime re-delegation may retire such a chain. The model checks this startup preservation policy and requires an interrupted grandchild's completion after owner loss to remain reachable. Both recovery paths check provider-wide ownership while reserving registration through persistence; persisted delegated status alone is not evidence of a live session. Runtime re-delegation refreshes the chain with `TaskHistoryStore.refreshStrict`, so an unreadable or invalid descendant record aborts recovery instead of looking missing. Delegation checks cancellation, current-task identity, and pending-action identity before recovery and again after its asynchronous write. If disposal cancels a delegation after the parent commit, rollback releases the parent through `recoverDelegationParent` and restores its pending action, without recreating a task on the disposed provider.

## Shared-store concurrency model

The same `pnpm lifecycle:model-check` command also runs a second bounded explorer over two `TaskHistoryStore` hosts. It imports the production `computeHistoryDelta` and `mergeHistoryDelta` functions, so its semantics match the store rather than assuming coherent caches or transactional pair writes:
Expand Down Expand Up @@ -139,9 +143,10 @@ The task delegation checker currently enforces:
4. Every active or delegated linked child is the child its parent currently awaits. An interrupted prior child may retain lineage after re-delegation but cannot complete back into that parent.
5. Parent-child lineage is acyclic.
6. Completed task records cannot be changed by later lifecycle events.
7. Active-child re-delegation, stale completion after ownership moves to another child, duplicate/late completion, and abandonment of a live child are rejected by the shared production guards.
8. A rejected delegation settles only the exact matching pending `create_subtask` action. Settlement preserves status, lineage, and accounting, never clears a replacement or different-kind action, and never mutates a completed record. The settlement compare-and-clear reads the persisted record under the per-file lock, so it never clears from a stale host cache.
9. A completion clears the completing child's pending action only when the completion event carries the exact matching action ID. A completion with no action ID or a different ID preserves the pending action.
7. Active-child re-delegation, stale completion after ownership moves to another child, duplicate/late completion, and abandonment of a live child are rejected by the shared production guards. A delegated child may transition to `interrupted` only through dead-chain recovery after runtime liveness checks establish that neither it nor its descendants has a live owner.
8. Runtime owner loss does not mutate persisted status. A delegated chain with no remaining live owner has a reachable recovery transition within the bounded graph, after which its parent can re-delegate.
9. A rejected delegation settles only the exact matching pending `create_subtask` action. Settlement preserves status, lineage, and accounting, never clears a replacement or different-kind action, and never mutates a completed record. The settlement compare-and-clear reads the persisted record under the per-file lock, so it never clears from a stale host cache.
10. A completion clears the completing child's pending action only when the completion event carries the exact matching action ID. A completion with no action ID or a different ID preserves the pending action.

The completion persistence checker additionally enforces:

Expand Down
139 changes: 130 additions & 9 deletions scripts/check-task-lifecycle.ts
Original file line number Diff line number Diff line change
Expand Up @@ -7,12 +7,15 @@ import {
completeDelegatedChild,
delegateTaskToChild,
interruptDelegatedChild,
isDeadDelegationChain,
recoverDeadDelegatedChild,
recoverDelegationParent,
settleRejectedCreateSubtaskAction,
} from "../src/core/task-persistence/taskLifecycle"

const taskIds = ["parent", "child-a", "child-b"] as const
type TaskId = (typeof taskIds)[number]
type ModelState = Record<TaskId, HistoryItem | undefined>
type ModelState = Record<TaskId, HistoryItem | undefined> & { liveTaskIds: TaskId[] }

interface Transition {
name: string
Expand All @@ -36,7 +39,17 @@ interface WitnessContext {
const MAX_DEPTH = 12
const MAX_STATES = 10_000
const actionIds = ["action-1", "action-2"] as const
const expectedActions = ["delegate", "interrupt", "complete", "abandon", "stage", "settle-rejected"] as const
const expectedActions = [
"delegate",
"owner-loss",
"interrupt",
"recover-active",
"recover",
"complete",
"abandon",
"stage",
"settle-rejected",
] as const
const semanticLandmarks = {
"interrupted-child-redelegation": (state: ModelState) =>
state.parent?.status === "delegated" &&
Expand All @@ -47,8 +60,26 @@ const semanticLandmarks = {
state.parent.awaitingChildId === "child-a" &&
state["child-a"]?.status === "delegated" &&
state["child-a"].awaitingChildId === "child-b",
"delegated-owner-loss": (state: ModelState) =>
state["child-a"]?.status === "delegated" && !state.liveTaskIds.includes("child-a"),
"dead-nested-chain-recovered": (state: ModelState) =>
state.parent?.status === "delegated" &&
state.parent.awaitingChildId === "child-a" &&
state["child-a"]?.status === "interrupted" &&
state["child-a"].awaitingChildId === undefined &&
state["child-b"]?.status === "interrupted",
} satisfies Record<string, (state: ModelState) => boolean>
const semanticWitnesses = {
"interrupted-grandchild-completes-after-owner-loss": ({ prev, next, transition }: WitnessContext) =>
transition.completion?.childId === "child-b" &&
prev.liveTaskIds.length === 0 &&
prev.parent?.awaitingChildId === "child-a" &&
prev["child-a"]?.status === "delegated" &&
prev["child-a"].awaitingChildId === "child-b" &&
prev["child-b"]?.status === "interrupted" &&
next["child-a"]?.status === "active" &&
next["child-a"].completedByChildId === "child-b" &&
next.parent?.awaitingChildId === "child-a",
"interrupted-pending-delegation-settled": ({ prev, next, transition }: WitnessContext) =>
transition.settlement !== undefined &&
prev[transition.settlement.taskId]?.status === "interrupted" &&
Expand Down Expand Up @@ -129,7 +160,7 @@ function createSubtaskAction(actionId: (typeof actionIds)[number]): PendingTaskA
}

function initialState(): ModelState {
return { parent: task("parent"), "child-a": undefined, "child-b": undefined }
return { parent: task("parent"), "child-a": undefined, "child-b": undefined, liveTaskIds: ["parent"] }
}

function replace(state: ModelState, ...updates: HistoryItem[]): ModelState {
Expand All @@ -138,6 +169,10 @@ function replace(state: ModelState, ...updates: HistoryItem[]): ModelState {
return next
}

function withLiveTasks(state: ModelState, ...liveTaskIds: TaskId[]): ModelState {
return { ...state, liveTaskIds: Array.from(new Set(liveTaskIds)).sort() }
}

function transitions(state: ModelState): Transition[] {
const result: Transition[] = []
for (const parentId of taskIds) {
Expand All @@ -152,9 +187,10 @@ function transitions(state: ModelState): Transition[] {
if (childId === parentId || state[childId]) continue
if (!delegationValid) continue
const delegated = { ...delegateTaskToChild(parent, childId, awaitedStatus), pendingAction: undefined }
const next = replace(state, delegated, task(childId, parentId))
result.push({
name: `delegate(${parentId}, ${childId})`,
next: replace(state, delegated, task(childId, parentId)),
next: withLiveTasks(next, ...state.liveTaskIds.filter((id) => id !== parentId), childId),
delegation: { parentId },
})
}
Expand All @@ -178,6 +214,16 @@ function transitions(state: ModelState): Transition[] {
}
}

for (const taskId of state.liveTaskIds) {
const current = state[taskId]
if (current && current.parentTaskId && (current.status === "active" || current.status === "delegated")) {
result.push({
name: `owner-loss(${taskId})`,
next: withLiveTasks(state, ...state.liveTaskIds.filter((id) => id !== taskId)),
})
}
}

for (const childId of taskIds) {
const child = state[childId]
if (!child?.parentTaskId) continue
Expand All @@ -186,7 +232,30 @@ function transitions(state: ModelState): Transition[] {

if (parent.status === "delegated" && parent.awaitingChildId === child.id && child.status === "active") {
const interrupted = interruptDelegatedChild(parent, child)
result.push({ name: `interrupt(${childId})`, next: replace(state, interrupted) })
result.push({
name: `interrupt(${childId})`,
next: withLiveTasks(replace(state, interrupted), ...state.liveTaskIds.filter((id) => id !== childId)),
})
if (!state.liveTaskIds.includes(childId) && !state.liveTaskIds.includes(parent.id as TaskId)) {
const ancestor = parent.parentTaskId ? state[parent.parentTaskId as TaskId] : undefined
result.push({
name: `recover-active(${childId})`,
next: replace(state, interrupted, recoverDelegationParent(parent, ancestor)),
})
}
}

if (
parent.status === "delegated" &&
parent.awaitingChildId === child.id &&
isDeadDelegationChain(
child,
(id) => state[id as TaskId],
(id) => state.liveTaskIds.includes(id as TaskId),
)
) {
const recovered = recoverDeadDelegatedChild(parent, child)
result.push({ name: `recover(${childId})`, next: replace(state, recovered) })
}

if (
Expand All @@ -197,7 +266,11 @@ function transitions(state: ModelState): Transition[] {
const completed = completeDelegatedChild(parent, child, `${childId} result`)
result.push({
name: `complete(${childId})`,
next: replace(state, completed.parent, completed.child),
next: withLiveTasks(
replace(state, completed.parent, completed.child),
...state.liveTaskIds.filter((id) => id !== childId),
child.parentTaskId as TaskId,
),
completion: { childId },
})
for (const actionId of actionIds) {
Expand All @@ -207,7 +280,11 @@ function transitions(state: ModelState): Transition[] {
: completed.child
result.push({
name: `complete(${childId}, ${actionId})`,
next: replace(state, completed.parent, completedChild),
next: withLiveTasks(
replace(state, completed.parent, completedChild),
...state.liveTaskIds.filter((id) => id !== childId),
child.parentTaskId as TaskId,
),
completion: { childId, pendingActionId: actionId },
})
}
Expand All @@ -217,12 +294,33 @@ function transitions(state: ModelState): Transition[] {
const abandoned = abandonDelegatedChild(parent, child)
result.push({
name: `abandon(${childId})`,
next: replace(state, abandoned.parent, abandoned.child),
next: withLiveTasks(
replace(state, abandoned.parent, abandoned.child),
...state.liveTaskIds.filter((id) => id !== childId),
child.parentTaskId as TaskId,
),
})
}
}

return result
}
function deadDelegatedChildren(state: ModelState): TaskId[] {
return taskIds.filter((childId) => {
const child = state[childId]
if (!child?.parentTaskId) return false
const parent = state[child.parentTaskId as TaskId]
return (
parent?.status === "delegated" &&
parent.awaitingChildId === child.id &&
isDeadDelegationChain(
child,
(id) => state[id as TaskId],
(id) => state.liveTaskIds.includes(id as TaskId),
)
)
})
}

function invariantViolations(state: ModelState): string[] {
const violations: string[] = []
Expand All @@ -242,6 +340,17 @@ function invariantViolations(state: ModelState): string[] {
if (!current.childIds?.includes(current.awaitingChildId)) {
violations.push(`${id}: awaited child must be retained in childIds`)
}
if (
child?.status === "interrupted" &&
isDeadDelegationChain(
current,
(taskId) => state[taskId as TaskId],
(taskId) => state.liveTaskIds.includes(taskId as TaskId),
{ preserveInterrupted: true },
)
) {
violations.push(`${id}: startup recovery must preserve the interrupted child's completion route`)
}
} else if (current.awaitingChildId || current.delegatedToId) {
violations.push(`${id}: only delegated tasks may retain an awaited-child pointer`)
}
Expand All @@ -264,11 +373,16 @@ function invariantViolations(state: ModelState): string[] {
cursor = state[cursor as TaskId]?.parentTaskId
}
}
for (const childId of deadDelegatedChildren(state)) {
if (!transitions(state).some((transition) => transition.name === `recover(${childId})`)) {
violations.push(`${childId}: dead delegated chain must be recoverable in the next transition`)
}
}
return violations
}

function canonical(state: ModelState): string {
return JSON.stringify(taskIds.map((id) => state[id] ?? null))
return JSON.stringify({ tasks: taskIds.map((id) => state[id] ?? null), liveTaskIds: state.liveTaskIds })
}

function formatCounterexample(message: string, trace: TraceStep[]): string {
Expand Down Expand Up @@ -427,6 +541,13 @@ function runRepresentativeScenarios(): void {
const nestedCompletion = completeDelegatedChild(nestedParent, childB, "nested result")
assert.equal(nestedCompletion.parent.status, "active")
assert.equal(nestedCompletion.parent.completedByChildId, childB.id)
const interruptedNestedChild = interruptDelegatedChild(nestedParent, childB)
const recoveredNestedParent = recoverDeadDelegatedChild(delegated, {
...nestedParent,
awaitingChildId: interruptedNestedChild.id,
})
assert.equal(recoveredNestedParent.status, "interrupted")
assert.equal(recoveredNestedParent.awaitingChildId, undefined)

const interruptedCompletion = completeDelegatedChild(delegated, interruptedA, "resumed result")
assert.equal(interruptedCompletion.child.status, "completed")
Expand Down
Loading
Loading