gizmoduck: row 271 design: session.cancel and the cancelled stage built in 271 (sage-2828 re-rules Q3 per D7:263-264), pre- and post-retire paths, cancel tests and the fence-release mutant; N2 refuses session-name-too-long at accept
This commit is contained in:
1 parent
4cca8e785a
commit
78e14352f6
1 file changed
+67
-11
@@ -37,6 +37,8 @@ Answer, the operation envelope:
|
||||
resumes when proof arrives.
|
||||
- `retired`: the old session is retired and the successor exists, in one bus transaction.
|
||||
- `failed`: no retirement happened, and `refusal` names why. The old session stays as it was.
|
||||
- `cancelled`: a human cancelled the clear (session.cancel below, sage-2828). `retired` is
|
||||
null if it was cancelled before retirement and true if after. `start` stays as it was.
|
||||
- `start` is null until `state` is `retired`. After that it is `held` (waiting for capacity),
|
||||
`started`, or `refused` with `refusal` set.
|
||||
- `at`: the time of the latest state change.
|
||||
@@ -50,6 +52,33 @@ Repeats and conflicts:
|
||||
- Other refusals: `session-not-found`, `session-retired`, `processing-halted` (D8: a halt refuses
|
||||
and changes nothing), and the owner refusals `session.create` already gives.
|
||||
|
||||
### session.cancel (sage-2828)
|
||||
|
||||
Input, every key required, with no other key:
|
||||
|
||||
```json
|
||||
{ "thread": "<thread id>", "op": "<the clear's op>", "confirm": true }
|
||||
```
|
||||
|
||||
This is a human write with the same owner or write-grant check as session.clear, rechecked under
|
||||
the session fence. An agent caller refuses as session.clear does. `confirm` must be the literal
|
||||
`true`, or it refuses `confirm-required`. The answer is the operation envelope with `state`
|
||||
`cancelled`.
|
||||
|
||||
- Before retirement, cancel stops the replacement:
|
||||
- The successor id is never created or started.
|
||||
- Messages already cancelled stay cancelled and are never replayed.
|
||||
- The old session is `active` again.
|
||||
- After retirement, cancel stops the startup only:
|
||||
- No further start attempts are made.
|
||||
- Both sessions stay as they are. Nothing un-retires.
|
||||
- Repeats and refusals:
|
||||
- A repeat with the same payload returns the original cancelled envelope.
|
||||
- The payload digest covers `{thread, op}` and the calling principal. A cancel from a
|
||||
different principal, or a payload that otherwise differs, refuses `session-op-conflict`.
|
||||
- An op that isn't a clear refuses `operation-not-found`.
|
||||
- A cancel of a clear whose successor has started refuses `session-clear-complete`.
|
||||
|
||||
### session.operation
|
||||
|
||||
Input `{ "thread": "...", "op": "..." }`. Answer: the same envelope. Unknown op refuses
|
||||
@@ -60,7 +89,8 @@ queries the op here and never resends the clear.
|
||||
|
||||
Each row gains:
|
||||
|
||||
- `state`: `active`, `clearing`, `uncertain` or `retired`.
|
||||
- `state`: `active`, `clearing`, `uncertain` or `retired`. A cancelled clear leaves the session
|
||||
`active` if cancelled before retirement, and `retired` if after.
|
||||
- `revision`: an integer. 0 at creation, plus 1 for each lifecycle event on that session.
|
||||
- `successor`: the successor's id once retired, otherwise null.
|
||||
|
||||
@@ -68,7 +98,8 @@ A successor row has `predecessor` set (264a's column). When the cleared session
|
||||
default, `default` moves to the successor at retirement. Clearing any other session leaves the
|
||||
default where it is.
|
||||
|
||||
On a base without 264d, `session.clear` refuses `unknown-verb`, and the rows have no `state`,
|
||||
On a base without 264d, `session.clear`, `session.cancel` and `session.operation` refuse
|
||||
`unknown-verb`, and the rows have no `state`,
|
||||
`revision` or `successor`.
|
||||
|
||||
## Design (draft 2: Sage's sage-2826 rulings and Mos's mos-1315 folded in)
|
||||
@@ -165,12 +196,23 @@ alone can't show that no child is running.
|
||||
code. Nothing is retired, and the old session goes back to `active` with its messages still
|
||||
cancelled.
|
||||
|
||||
Human cancel of an open clear is out of 271 (sage-2826 Q3). This is a **departure from D7**
|
||||
(duckworth-0170 N1). D7's last paragraph (t1-sessions.md:263-264) does define cancel: before
|
||||
retirement it stops the replacement, and after retirement it cancels startup and leaves both
|
||||
identities intact. sage-2826 said D7 defines none, and that premise is wrong. I've asked Sage to
|
||||
re-rule (gizmoduck-0271). Until then, 271 builds no cancel and the DEFERRED entry carries the D7
|
||||
text.
|
||||
**Cancel** (sage-2828, re-ruling sage-2826 Q3, D7:263-264). `session.cancel` checks the owner or
|
||||
write grant under the fence and appends `cancelled`, attempt 0, in one transaction:
|
||||
- Before `retired` it releases the fence:
|
||||
- If no `drained` was recorded, the drain is still waiting. Nothing is signalled, the clear
|
||||
ends, and the run's next receive delivers again.
|
||||
- If `drained` was recorded with the claim still held and no SIGTERM sent, the launcher skips
|
||||
the stop because the op is no longer open. The run keeps its claim, and its next receive
|
||||
delivers again.
|
||||
- If the SIGTERM was already sent or the run has exited, the old session is `active` with no
|
||||
runner. The next send launches it through D8 like any idle session.
|
||||
- The successor row is never inserted, and the cancelled messages stay cancelled.
|
||||
- The launcher reads the op state right before its SIGTERM, in the same tick as its start-time
|
||||
check. A cancel after that point still finds a stopping runner, which takes the "active with
|
||||
no runner" path above. This is a residual: a cancel can't take back a SIGTERM already sent.
|
||||
- After `retired` and before `start-started`, no further start attempts are made. threadPass
|
||||
skips a successor whose clear is cancelled. Both identities stay historical.
|
||||
- After `start-started` it refuses `session-clear-complete`.
|
||||
|
||||
### Early look d2 folds (duckworth-0170, 98dc69f0c)
|
||||
|
||||
@@ -198,9 +240,10 @@ text.
|
||||
- `session.create` (broker.mjs:5859-5872) refuses an op already in `session_ops`, instead of
|
||||
answering the successor row.
|
||||
- **B4** is in the schema step below (the `attempt` key).
|
||||
- **N2, name cap.** `name()` caps names at 200 characters (broker.mjs:323). The successor base is
|
||||
the old name cut to `200 - len("-N")` characters, then `-N`, computed and bound at accept. Test:
|
||||
a 200-character name clears to a 200-character successor name.
|
||||
- **N2, name cap.** `name()` caps names at 200 characters (broker.mjs:323). When `<old>-N` would
|
||||
be longer than that, session.clear refuses `session-name-too-long` at accept and writes nothing
|
||||
(sage-2828). Test: a 199-character name clears to a 201-character `<old>-1` and is refused, and
|
||||
a 198-character name clears.
|
||||
- **N3, batch.** Drain waits for the runner's whole receive batch. Messages already delivered
|
||||
are a turn in progress, and the runner runs each of them before its next receive (:543-590).
|
||||
Only undelivered messages are cancelled. This is a residual: a batch of k delivered messages
|
||||
@@ -219,6 +262,17 @@ text.
|
||||
- **N8**: row 206 is approved at 3l→3m, so if it lands first, 271 is 3m→3n (as mos-1315 item 4
|
||||
says).
|
||||
|
||||
Cancel tests (sage-2828):
|
||||
- before retirement (no drained yet; and drained with the claim held)
|
||||
- after retirement, with no further start
|
||||
- an idempotent repeat
|
||||
- a changed payload refused
|
||||
- after completion: `session-clear-complete`
|
||||
- an agent caller refused
|
||||
|
||||
Mutant: drop the fence release in cancel's pre-retire path. The kill is the pre-retire test's next
|
||||
send/receive.
|
||||
|
||||
Tests gained: B1 a cancel at arrival (reply chain and spec notice) for clearing and retired; B2
|
||||
a claim refused while clearing, and retire refusing a live claim; B3 both op directions; B4 a
|
||||
second `start-held` appended; N2; N5.
|
||||
@@ -228,6 +282,8 @@ second `start-held` appended; N2; N5.
|
||||
- `session_ops(seq, at, business, thread, session, op, stage, attempt, successor, successor_name,
|
||||
run, generation, digest, refusal)`:
|
||||
- append-only, with `UNIQUE(thread, op, stage, attempt)` and a CHECK on `stage`
|
||||
- the stages are `requested`, `drained`, `uncertain`, `exited`, `retired`, `failed`,
|
||||
`cancelled`, `start-held`, `start-started` and `start-refused`
|
||||
- `attempt` is 0 for every stage up to `retired`, and the launcher's start attempt (1, 2, ...)
|
||||
for `start-held`, `start-started` and `start-refused`, so D7's retryable start can append
|
||||
again (duckworth-0170 B4)
|
||||
|
||||
Reference in new issue
Block a user