Recover held slots on restart — an empty memory is not an empty pool #40

New issue

Closed

opened 2026-09-03 22:34:45 +00:00 by larandar · 0 comments

larandar commented

2026-09-03 22:34:45 +00:00

Owner

Proposal

Reconstruct which slots are held when the cycle starts, so a restart does not hand out identities that are still in use.

Delivery class

agent-unit — durable occupancy state and its recovery, with capture doubles.

Design

Cycle::new currently starts every slot Available. That is correct for a pool that has never run and wrong for every restart after the first: a process that restarts while drones hold slots comes back believing the pool is empty, and hands the same identities to a second set of occupants.

This is the failure #37 exists to prevent, arriving through a door #37 does not watch. #37 guarantees that nothing infers a slot is free — no timeout, no staleness rule, no unreachable runtime. It says nothing about a process that never knew the slot was held, and an empty in-memory map is not an inference. The safety property is stated per-transition and the gap is in the initial state.

Occupancy becomes durable. Checkout writes the holder — session, assignment, grant, generation — before the slot is handed out; completion and release clear it after the slot is safely back. Startup reads it and reconstructs SlotStatus from what is recorded rather than from the absence of a record.

Unreadable state denies, it does not default. A recovery that cannot read its own record must refuse to allocate rather than start empty: "I do not know what is held" and "nothing is held" are different answers, and only one of them is safe. This is the same discipline operations.rs applies to its journal, and the same one #37 applies to a failed liveness check.

Ordering mirrors the cycle's. The occupancy record is written before the stamp and the hand-out, and cleared after revoke and rotate — so a crash at any point leaves the slot held, which is the recoverable side of every window.

Tasks

Persist occupancy — session, assignment, grant, generation — before a slot is handed out.
Clear it only after revoke and rotate have succeeded.
Reconstruct SlotStatus at startup from the durable record.
Refuse allocation when the record cannot be read; never start empty on error.
Prove a restart mid-occupancy comes back with the slot still held, at the same generation.
Prove a crash between write and hand-out leaves the slot held and releasable.

Specification Delta

Requirement: a restart does not free a held slot

Scenario: the process restarts while a drone holds a slot

GIVEN a slot bound to a live session
WHEN the cycle restarts
THEN the slot is still held, by the same session, assignment and generation
AND it is not offered to a new session

Requirement: unknown occupancy is not empty occupancy

Scenario: the durable record cannot be read

GIVEN occupancy state that is missing, unreadable, or damaged
WHEN the cycle starts
THEN allocation is refused and the failure is reported
AND the pool does not start with every slot available

Provenance

Found while building #35–#37 and flagged in PR #39 and in Cycle::new's own doc comment. Filed rather than left in a merged PR body: it is a safety gap, and src/checkout.rs must not run against a real pool until this lands.

OpenSpec 30 does not currently specify restart recovery at all — that is a package gap rather than a Session that missed its scope, so the package wants an amendment alongside this record.

OpenSpec

OpenSpec 30

Structural parent

Ting/Ting#2 — Epic: agent identity pool lifecycle.

## Proposal Reconstruct which slots are held when the cycle starts, so a restart does not hand out identities that are still in use. ## Delivery class `agent-unit` — durable occupancy state and its recovery, with capture doubles. ## Design `Cycle::new` currently starts every slot `Available`. That is correct for a pool that has never run and **wrong for every restart after the first**: a process that restarts while drones hold slots comes back believing the pool is empty, and hands the same identities to a second set of occupants. This is the failure [#37](https://jo.et0.pw/Ting/Vedanta/issues/37) exists to prevent, arriving through a door #37 does not watch. #37 guarantees that nothing *infers* a slot is free — no timeout, no staleness rule, no unreachable runtime. It says nothing about a process that never knew the slot was held, and an empty in-memory map is not an inference. The safety property is stated per-transition and the gap is in the initial state. **Occupancy becomes durable.** Checkout writes the holder — session, assignment, grant, generation — before the slot is handed out; completion and release clear it after the slot is safely back. Startup reads it and reconstructs `SlotStatus` from what is recorded rather than from the absence of a record. **Unreadable state denies, it does not default.** A recovery that cannot read its own record must refuse to allocate rather than start empty: "I do not know what is held" and "nothing is held" are different answers, and only one of them is safe. This is the same discipline `operations.rs` applies to its journal, and the same one #37 applies to a failed liveness check. **Ordering mirrors the cycle's.** The occupancy record is written before the stamp and the hand-out, and cleared after revoke and rotate — so a crash at any point leaves the slot held, which is the recoverable side of every window. ## Tasks - [ ] Persist occupancy — session, assignment, grant, generation — before a slot is handed out. - [ ] Clear it only after revoke and rotate have succeeded. - [ ] Reconstruct `SlotStatus` at startup from the durable record. - [ ] Refuse allocation when the record cannot be read; never start empty on error. - [ ] Prove a restart mid-occupancy comes back with the slot still held, at the same generation. - [ ] Prove a crash between write and hand-out leaves the slot held and releasable. ## Specification Delta ### Requirement: a restart does not free a held slot #### Scenario: the process restarts while a drone holds a slot - **GIVEN** a slot bound to a live session - **WHEN** the cycle restarts - **THEN** the slot is still held, by the same session, assignment and generation - **AND** it is not offered to a new session ### Requirement: unknown occupancy is not empty occupancy #### Scenario: the durable record cannot be read - **GIVEN** occupancy state that is missing, unreadable, or damaged - **WHEN** the cycle starts - **THEN** allocation is refused and the failure is reported - **AND** the pool does not start with every slot available ## Provenance Found while building [#35](https://jo.et0.pw/Ting/Vedanta/issues/35)–[#37](https://jo.et0.pw/Ting/Vedanta/issues/37) and flagged in [PR #39](https://jo.et0.pw/Ting/Vedanta/pulls/39) and in `Cycle::new`'s own doc comment. Filed rather than left in a merged PR body: it is a safety gap, and **`src/checkout.rs` must not run against a real pool until this lands.** [OpenSpec 30](https://jo.et0.pw/Ting/Vedanta/wiki/OpenSpec-30-agent-identity-pool-lifecycle) does not currently specify restart recovery at all — that is a package gap rather than a Session that missed its scope, so the package wants an amendment alongside this record. ## OpenSpec [OpenSpec 30](https://jo.et0.pw/Ting/Vedanta/wiki/OpenSpec-30-agent-identity-pool-lifecycle) ## Structural parent [Ting/Ting#2](https://jo.et0.pw/Ting/Ting/issues/2) — Epic: agent identity pool lifecycle.

larandar added the

Kind/Feature

Kind/Security

labels

2026-09-03 22:34:48 +00:00

larandar referenced this issue

2026-09-03 22:34:56 +00:00

Session: pool checkout and return — the steady-state slot cycle #31

larandar referenced this issue from a commit

2026-09-03 22:40:57 +00:00

pool: recover held slots on restart — an empty memory is not an empty pool (#40)

larandar referenced this issue from a pull request that will close it,