Skip to content

Commit 6d5d0fb

Browse files
edelaunaedelauna
committed
test(delegation): add TLA+ formal model + drift-monitor spec
1 parent fa561b1 commit 6d5d0fb

4 files changed

Lines changed: 666 additions & 0 deletions

File tree

‎docs/formal/task-delegation/README.md‎

Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,84 @@
1+
# Task Delegation Formal Model
2+
3+
This directory contains a small TLA+ model for the task-delegation state machine.
4+
5+
The model is intentionally abstract. It does not model VS Code, webviews, prompt contents, provider implementations, or task message history. It only models the state that must remain consistent while a parent task delegates work to a child task:
6+
7+
- parent task liveness while a child is created
8+
- child focus after creation
9+
- semaphore reservation and release
10+
- rollback after child creation or history persistence failures
11+
- parent and child API profile isolation
12+
- parent history status after delegation
13+
14+
## Local Checks
15+
16+
The executable CI check lives in `src/core/task/__tests__/delegation-state-machine.spec.ts`. It exhaustively explores the same small state machine with Vitest and includes explicit negative controls for the highest-risk invariant violations:
17+
18+
- broadcasting a child provider-profile change to the live parent
19+
- leaking a reserved permit after failed child creation
20+
- failing to restore a suspended parent after serial child creation fails
21+
22+
Run it with:
23+
24+
```bash
25+
pnpm --dir src exec vitest run core/task/__tests__/delegation-state-machine.spec.ts
26+
```
27+
28+
## TLA+ Checks
29+
30+
The TLA+ spec can be checked with TLC from the TLA+ Toolbox, the VS Code TLA+ extension, or a CLI TLC installation:
31+
32+
```bash
33+
java -cp /path/to/tla2tools.jar tlc2.TLC TaskDelegation.tla -config TaskDelegation.cfg
34+
```
35+
36+
The main invariants are:
37+
38+
- `PermitBound`: held plus reserved permits never exceed the configured concurrency.
39+
- `ParentProfileIsolation`: a live parent keeps its original API profile.
40+
- `ChildProfileIsolation`: a live child uses the child API profile.
41+
- `RollbackRestoresParent`: failed delegation releases reservations and returns focus to the parent.
42+
- `RunningChildHasDelegatedParent`: a running child implies the parent history item is delegated.
43+
44+
## Drift Control
45+
46+
The Vitest model is the primary drift monitor because it runs with the normal test suite. If production delegation behavior changes, update the Vitest model and this TLA+ model in the same change.
47+
48+
Reviewers should check this mapping when touching delegation code:
49+
50+
- `TaskScheduler.tryReserve()` / `runWithReservation()` map to the `reservedPermit` and `permitsHeld` transitions.
51+
- `delegateParentAndOpenChild()` maps to the parent liveness, child creation, focus, rollback, and history transitions.
52+
- provider-profile switching maps to `globalProfile`, `parentLocalProfile`, and `childLocalProfile`.
53+
- task-history updates map to `parentHistoryStatus` and `childHistoryStatus`.
54+
55+
Run TLC locally for changes that alter delegation ordering, rollback, profile switching, or scheduler permits. For smaller implementation-only changes, the Vitest model plus targeted unit/e2e coverage is usually sufficient.
56+
57+
## State-Machine Review Checklist
58+
59+
Use this checklist for changes that touch delegation, task focus, scheduler permits, provider profile or mode switching, task-local API configuration, or rollback behavior.
60+
61+
Before coding, state the invariant the change is preserving. Example: "provider/profile mutations are serialized; a timed-out caller must not allow a later mutation to overtake an earlier one."
62+
63+
For every async or mutating fix, answer:
64+
65+
- Does a timeout cancel the work, or only stop waiting for it?
66+
- If timed-out work can still complete later, can it mutate state after a newer operation?
67+
- Can a later mode/profile mutation overtake an earlier one?
68+
- Does rejection poison the queue, skip queued work, or create an unhandled rejection?
69+
- If a required setup step fails, does delegation abort or continue?
70+
- If rollback fails, what live task, focused task, history status, and reserved permits remain?
71+
- Does rollback route through the same queue or lock that may already be blocked?
72+
- Does any code read shared provider state where task-local state is required?
73+
- Does any webview push re-derive the focused task when the operation is about a different task?
74+
75+
Required tests for these changes:
76+
77+
- A positive test for the intended path.
78+
- A negative test that would fail with the original bug.
79+
- A fix-interaction test that would fail if the fix introduces a stale completion, queue overtake, leaked permit, or rollback-of-rollback failure.
80+
81+
Any timeout around a mutating async operation must prove one of these two properties:
82+
83+
- the underlying operation is actually cancelled before later conflicting mutations can run; or
84+
- later conflicting mutations remain queued until the timed-out operation truly settles.

‎docs/formal/task-delegation/TaskDelegation.cfg‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
SPECIFICATION Spec
2+
3+
CONSTANTS
4+
ParentProfile = parent_profile
5+
ChildProfile = child_profile
6+
7+
INVARIANT PermitBound
8+
INVARIANT NonNegativePermits
9+
INVARIANT ParentProfileIsolation
10+
INVARIANT ChildProfileIsolation
11+
INVARIANT RollbackRestoresParent
12+
INVARIANT RunningChildHasDelegatedParent
13+
INVARIANT FocusReferencesLiveTask
14+
15+
CHECK_DEADLOCK FALSE

‎docs/formal/task-delegation/TaskDelegation.tla‎

Lines changed: 208 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,208 @@
1+
---- MODULE TaskDelegation ----
2+
EXTENDS Naturals, TLC
3+
4+
CONSTANTS ParentProfile, ChildProfile
5+
6+
Profiles == { ParentProfile, ChildProfile }
7+
FocusValues == { "parent", "child", "none" }
8+
Phases == {
9+
"parent-running",
10+
"parent-suspended",
11+
"permit-reserved",
12+
"child-profile-selected",
13+
"child-created",
14+
"delegation-persisted",
15+
"child-running",
16+
"child-completed",
17+
"failed"
18+
}
19+
HistoryStatuses == { "active", "delegated", "completed" }
20+
21+
VARIABLES
22+
phase,
23+
maxConcurrency,
24+
permitsHeld,
25+
reservedPermit,
26+
focus,
27+
globalProfile,
28+
parentLive,
29+
parentLocalProfile,
30+
parentHistoryStatus,
31+
childLive,
32+
childLocalProfile,
33+
childHistoryStatus
34+
35+
vars == <<
36+
phase,
37+
maxConcurrency,
38+
permitsHeld,
39+
reservedPermit,
40+
focus,
41+
globalProfile,
42+
parentLive,
43+
parentLocalProfile,
44+
parentHistoryStatus,
45+
childLive,
46+
childLocalProfile,
47+
childHistoryStatus
48+
>>
49+
50+
Init ==
51+
/\ phase = "parent-running"
52+
/\ maxConcurrency \in { 1, 2 }
53+
/\ permitsHeld = IF maxConcurrency = 2 THEN 1 ELSE 0
54+
/\ reservedPermit = FALSE
55+
/\ focus = "parent"
56+
/\ globalProfile = ParentProfile
57+
/\ parentLive = TRUE
58+
/\ parentLocalProfile = ParentProfile
59+
/\ parentHistoryStatus = "active"
60+
/\ childLive = FALSE
61+
/\ childLocalProfile = ChildProfile
62+
/\ childHistoryStatus = "active"
63+
64+
ActivePermits == permitsHeld + IF reservedPermit THEN 1 ELSE 0
65+
66+
ReserveFanOutPermit ==
67+
/\ phase = "parent-running"
68+
/\ maxConcurrency > 1
69+
/\ ActivePermits < maxConcurrency
70+
/\ phase' = "permit-reserved"
71+
/\ reservedPermit' = TRUE
72+
/\ UNCHANGED << maxConcurrency, permitsHeld, focus, globalProfile, parentLive, parentLocalProfile, parentHistoryStatus,
73+
childLive, childLocalProfile, childHistoryStatus >>
74+
75+
SuspendParentForSerialDelegation ==
76+
/\ phase = "parent-running"
77+
/\ maxConcurrency = 1
78+
/\ phase' = "parent-suspended"
79+
/\ parentLive' = FALSE
80+
/\ focus' = "none"
81+
/\ UNCHANGED << maxConcurrency, permitsHeld, reservedPermit, globalProfile, parentLocalProfile, parentHistoryStatus,
82+
childLive, childLocalProfile, childHistoryStatus >>
83+
84+
CreateChildAfterSuspendSucceeds ==
85+
/\ phase = "parent-suspended"
86+
/\ phase' = "child-created"
87+
/\ focus' = "child"
88+
/\ globalProfile' = ChildProfile
89+
/\ childLive' = TRUE
90+
/\ childLocalProfile' = ChildProfile
91+
/\ childHistoryStatus' = "active"
92+
/\ UNCHANGED << maxConcurrency, permitsHeld, reservedPermit, parentLive, parentLocalProfile, parentHistoryStatus >>
93+
94+
CreateChildAfterSuspendFails ==
95+
/\ phase = "parent-suspended"
96+
/\ phase' = "failed"
97+
/\ parentLive' = TRUE
98+
/\ focus' = "parent"
99+
/\ UNCHANGED << maxConcurrency, permitsHeld, reservedPermit, globalProfile, parentLocalProfile, parentHistoryStatus,
100+
childLive, childLocalProfile, childHistoryStatus >>
101+
102+
SelectChildProfile ==
103+
/\ phase = "permit-reserved"
104+
/\ phase' = "child-profile-selected"
105+
/\ globalProfile' = ChildProfile
106+
/\ UNCHANGED << maxConcurrency, permitsHeld, reservedPermit, focus, parentLive, parentLocalProfile, parentHistoryStatus,
107+
childLive, childLocalProfile, childHistoryStatus >>
108+
109+
CreateChildSucceeds ==
110+
/\ phase = "child-profile-selected"
111+
/\ phase' = "child-created"
112+
/\ focus' = "child"
113+
/\ childLive' = TRUE
114+
/\ childLocalProfile' = globalProfile
115+
/\ childHistoryStatus' = "active"
116+
/\ UNCHANGED << maxConcurrency, permitsHeld, reservedPermit, globalProfile, parentLive, parentLocalProfile, parentHistoryStatus >>
117+
118+
CreateChildFails ==
119+
/\ phase = "child-profile-selected"
120+
/\ phase' = "failed"
121+
/\ reservedPermit' = FALSE
122+
/\ focus' = "parent"
123+
/\ globalProfile' = ParentProfile
124+
/\ childLive' = FALSE
125+
/\ childLocalProfile' = ChildProfile
126+
/\ childHistoryStatus' = "active"
127+
/\ UNCHANGED << maxConcurrency, permitsHeld, parentLive, parentLocalProfile, parentHistoryStatus >>
128+
129+
PersistDelegationSucceeds ==
130+
/\ phase = "child-created"
131+
/\ phase' = "delegation-persisted"
132+
/\ parentHistoryStatus' = "delegated"
133+
/\ UNCHANGED << maxConcurrency, permitsHeld, reservedPermit, focus, globalProfile, parentLive, parentLocalProfile,
134+
childLive, childLocalProfile, childHistoryStatus >>
135+
136+
PersistDelegationFails ==
137+
/\ phase = "child-created"
138+
/\ phase' = "failed"
139+
/\ reservedPermit' = FALSE
140+
/\ focus' = "parent"
141+
/\ globalProfile' = ParentProfile
142+
/\ parentLive' = TRUE
143+
/\ childLive' = FALSE
144+
/\ childLocalProfile' = ChildProfile
145+
/\ childHistoryStatus' = "active"
146+
/\ UNCHANGED << maxConcurrency, permitsHeld, parentLocalProfile, parentHistoryStatus >>
147+
148+
StartChildWithReservation ==
149+
/\ phase = "delegation-persisted"
150+
/\ reservedPermit = TRUE
151+
/\ phase' = "child-running"
152+
/\ reservedPermit' = FALSE
153+
/\ permitsHeld' = permitsHeld + 1
154+
/\ UNCHANGED << maxConcurrency, focus, globalProfile, parentLive, parentLocalProfile, parentHistoryStatus,
155+
childLive, childLocalProfile, childHistoryStatus >>
156+
157+
ParentContinues ==
158+
/\ phase = "child-running"
159+
/\ UNCHANGED vars
160+
161+
ChildUsesScopedProfile ==
162+
/\ phase = "child-running"
163+
/\ UNCHANGED vars
164+
165+
ChildCompletes ==
166+
/\ phase = "child-running"
167+
/\ phase' = "child-completed"
168+
/\ permitsHeld' = permitsHeld - 1
169+
/\ focus' = "parent"
170+
/\ childLive' = FALSE
171+
/\ childHistoryStatus' = "completed"
172+
/\ UNCHANGED << maxConcurrency, reservedPermit, globalProfile, parentLive, parentLocalProfile, parentHistoryStatus,
173+
childLocalProfile >>
174+
175+
Next ==
176+
\/ ReserveFanOutPermit
177+
\/ SuspendParentForSerialDelegation
178+
\/ CreateChildAfterSuspendSucceeds
179+
\/ CreateChildAfterSuspendFails
180+
\/ SelectChildProfile
181+
\/ CreateChildSucceeds
182+
\/ CreateChildFails
183+
\/ PersistDelegationSucceeds
184+
\/ PersistDelegationFails
185+
\/ StartChildWithReservation
186+
\/ ParentContinues
187+
\/ ChildUsesScopedProfile
188+
\/ ChildCompletes
189+
190+
Spec == Init /\ [][Next]_vars
191+
192+
PermitBound == ActivePermits <= maxConcurrency
193+
NonNegativePermits == permitsHeld >= 0
194+
ParentProfileIsolation == parentLive => parentLocalProfile = ParentProfile
195+
ChildProfileIsolation == childLive => childLocalProfile = ChildProfile
196+
RollbackRestoresParent ==
197+
phase = "failed" => /\ reservedPermit = FALSE
198+
/\ parentLive = TRUE
199+
/\ focus = "parent"
200+
RunningChildHasDelegatedParent ==
201+
phase = "child-running" => /\ childLive = TRUE
202+
/\ parentHistoryStatus = "delegated"
203+
FocusReferencesLiveTask ==
204+
/\ focus \in FocusValues
205+
/\ (focus = "parent" => parentLive)
206+
/\ (focus = "child" => childLive)
207+
208+
====

0 commit comments

Comments
 (0)