ms2k/lazaret
SHA256
Watch
0
Code Releases 3 Activity

Separate lease-loss release and finalize session terminals

Browse source
This commit is contained in:
ms2k 2026-07-12 01:27:19 +09:00
commit eded0faa7a
4 changed files with 316 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

1
docs/protocol/Lazaret.cfg
View file

@ -102,3 +102,4 @@ PROPERTIES
PromptEventuallyRestoresTerminal
EmptyDomainEventuallyStops
FailedDomainEventuallyRecovers
LeaseLossUnmountRetainsPreparedLowerLease

64
docs/protocol/Lazaret.tla
View file

@ -919,7 +919,6 @@ UnmountStateAnchor(d) ==
/\ sidecarState[d] = "Stopped"
/\ stateAnchorState[d] = "Mounted"
/\ stateAnchorState' = [stateAnchorState EXCEPT ![d] = "Unmounted"]
/\ preparedLowerLeased' = [preparedLowerLeased EXCEPT ![d] = FALSE]
/\ UNCHANGED <<
domainPhase, sidecarState, sandboxState, trustReady,
lockOwner, published, registered, connected, sessionPhase,
@ -929,6 +928,24 @@ UnmountStateAnchor(d) ==
runtimeCausalEdge, supervisorLease, runtimeFaultsRemaining,
domainGeneration,
durableDecision, durableIntent, pathMismatch, genCoordinatorId,
genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
>>
ReleasePreparedLowerLease(d) ==
/\ domainPhase[d] = "Stopping"
/\ HostCoordinatorAlive(d)
/\ stateAnchorState[d] = "Unmounted"
/\ preparedLowerLeased[d]
/\ preparedLowerLeased' = [preparedLowerLeased EXCEPT ![d] = FALSE]
/\ UNCHANGED <<
domainPhase, stateAnchorState, sidecarState, sandboxState, trustReady,
lockOwner, published, registered, connected, sessionPhase,
terminalRoute, connectionState, activeRequest, requestPhase,
approvalSource, approvedCommand, hostRunning, domainLockHeld,
hostCoordinatorProc, runtimeSupervisorProc, attachedRunscProc,
runtimeCausalEdge, supervisorLease, runtimeFaultsRemaining,
domainGeneration,
durableDecision, durableIntent, pathMismatch, genCoordinatorId,
genSidecarId, genSandboxId, networkReady, helperProc
>>
@ -940,6 +957,7 @@ GracefulSupervisorExit(d) ==
/\ sandboxState[d] = "Stopped"
/\ sidecarState[d] = "Stopped"
/\ stateAnchorState[d] = "Unmounted"
/\ ~preparedLowerLeased[d]
/\ attachedRunscProc[d] = "Absent"
/\ runtimeCausalEdge[d] = "Unarmed"
/\ runtimeSupervisorProc' = [runtimeSupervisorProc EXCEPT ![d] = "Dead"]
@ -963,6 +981,7 @@ FinishTeardown(d) ==
/\ domainPhase[d] = "Stopping"
/\ HostCoordinatorAlive(d)
/\ stateAnchorState[d] = "Unmounted"
/\ ~preparedLowerLeased[d]
/\ sidecarState[d] = "Stopped"
/\ sandboxState[d] = "Stopped"
/\ supervisorLease[d] = "Unarmed"
@ -1266,8 +1285,9 @@ Failure, Host Coordinator lease loss, and recovery
Hard Host Coordinator loss withdraws publication and marks the generation
Failed without itself stopping the sandbox. The surviving Runtime Supervisor
observes supervisorLease = Lost and performs ordered teardown, then exits.
External recovery begins only after the supervisor is no longer present.
observes supervisorLease = Lost, stops runtime use, unmounts the State Anchor,
and exits while retaining the prepared-lower lease. External recovery begins
only after the supervisor is no longer present and releases that lease.
***************************************************************************)
FailDomain(d) ==
@ -1526,7 +1546,6 @@ LeaseTeardownUnmountStateAnchor(d) ==
/\ sidecarState[d] = "Stopped"
/\ stateAnchorState[d] = "Mounted"
/\ stateAnchorState' = [stateAnchorState EXCEPT ![d] = "Unmounted"]
/\ preparedLowerLeased' = [preparedLowerLeased EXCEPT ![d] = FALSE]
/\ UNCHANGED <<
domainPhase, sidecarState, sandboxState, trustReady,
lockOwner, published, registered, connected, sessionPhase,
@ -1535,7 +1554,8 @@ LeaseTeardownUnmountStateAnchor(d) ==
hostCoordinatorProc, runtimeSupervisorProc, attachedRunscProc,
runtimeCausalEdge, supervisorLease, runtimeFaultsRemaining,
domainGeneration,
durableDecision, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, helperProc
durableDecision, durableIntent, pathMismatch, genCoordinatorId,
genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
>>
LeaseTeardownSupervisorExit(d) ==
@ -1693,7 +1713,6 @@ RecoverStateAnchor(d) ==
/\ sidecarState[d] = "Stopped"
/\ stateAnchorState[d] = "Mounted"
/\ stateAnchorState' = [stateAnchorState EXCEPT ![d] = "Unmounted"]
/\ preparedLowerLeased' = [preparedLowerLeased EXCEPT ![d] = FALSE]
/\ UNCHANGED <<
domainPhase, sidecarState, sandboxState, trustReady,
lockOwner, published, registered, connected, sessionPhase,
@ -1703,6 +1722,29 @@ RecoverStateAnchor(d) ==
runtimeCausalEdge, supervisorLease, runtimeFaultsRemaining,
domainGeneration,
durableDecision, durableIntent, pathMismatch, genCoordinatorId,
genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
>>
RecoverPreparedLowerLease(d) ==
/\ domainPhase[d] = "Recovering"
/\ HostCoordinatorAlive(d)
/\ sandboxState[d] = "Stopped"
/\ attachedRunscProc[d] \in {"Absent", "Dead"}
/\ runtimeCausalEdge[d] = "Unarmed"
/\ ~ProcessPresent(runtimeSupervisorProc[d])
/\ sidecarState[d] = "Stopped"
/\ stateAnchorState[d] = "Unmounted"
/\ preparedLowerLeased[d]
/\ preparedLowerLeased' = [preparedLowerLeased EXCEPT ![d] = FALSE]
/\ UNCHANGED <<
domainPhase, stateAnchorState, sidecarState, sandboxState, trustReady,
lockOwner, published, registered, connected, sessionPhase,
terminalRoute, connectionState, activeRequest, requestPhase,
approvalSource, approvedCommand, hostRunning, domainLockHeld,
hostCoordinatorProc, runtimeSupervisorProc, attachedRunscProc,
runtimeCausalEdge, supervisorLease, runtimeFaultsRemaining,
domainGeneration,
durableDecision, durableIntent, pathMismatch, genCoordinatorId,
genSidecarId, genSandboxId, networkReady, helperProc
>>
@ -1710,6 +1752,7 @@ FinishRecovery(d) ==
/\ domainPhase[d] = "Recovering"
/\ HostCoordinatorAlive(d)
/\ stateAnchorState[d] = "Unmounted"
/\ ~preparedLowerLeased[d]
/\ sidecarState[d] = "Stopped"
/\ sandboxState[d] = "Stopped"
/\ attachedRunscProc[d] \in {"Absent", "Dead"}
@ -1871,6 +1914,7 @@ DomainServiceProgress(d) ==
\/ StopSandbox(d)
\/ StopSidecar(d)
\/ UnmountStateAnchor(d)
\/ ReleasePreparedLowerLease(d)
\/ GracefulSupervisorExit(d)
\/ FinishTeardown(d)
\/ HostCoordinatorTerminateUnresponsiveRuntime(d)
@ -1884,6 +1928,7 @@ DomainServiceProgress(d) ==
\/ RecoverSandbox(d)
\/ RecoverSidecar(d)
\/ RecoverStateAnchor(d)
\/ RecoverPreparedLowerLease(d)
\/ FinishRecovery(d)
RuntimePhysicalInterleaving(d) ==
@ -2255,6 +2300,13 @@ PreparedLowerLeaseBeforeMount ==
/\ preparedLowerLeased[d]
/\ durableIntent[d]["prepared_lower"]
LeaseLossUnmountRetainsPreparedLowerLeaseAction ==
\A d \in Domains :
LeaseTeardownUnmountStateAnchor(d) => preparedLowerLeased'[d]
LeaseLossUnmountRetainsPreparedLowerLease ==
[][LeaseLossUnmountRetainsPreparedLowerLeaseAction]_vars
HelperUnderSupervisor ==
\A d \in Domains :
helperProc[d] = "Alive" =>

140
docs/schema.md
View file

@ -1,6 +1,7 @@
# Lazaret schemas
This document is the normative design schema for Lazaret records. The
This document is the normative design schema for Lazaret records and protocol
data shapes. The
[specification](specification.md) defines their physical use, while the TLA+
models define lifecycle and ordering above the implementation abstraction. The
diagrams define logical fields, variants, and relationships; they do not select a
@ -69,6 +70,21 @@ classDiagram
session_phase
}
class SessionTerminal {
generation_id
session_id
state
container_id
}
class SessionTerminalState {
<<enumeration>>
Intent
Running
ReleaseIntent
Clean
}
class Mailbox {
generation_id
identity_path
@ -84,6 +100,8 @@ classDiagram
Participant --> ParticipantState
Participant --> ParticipantOwnership
Generation "1" --> "0..*" Session
Session "1" --> "0..1" SessionTerminal
SessionTerminal --> SessionTerminalState
Generation "1" --> "0..1" Mailbox
Mailbox --> ParticipantState
```
@ -92,6 +110,122 @@ classDiagram
protocol model. This schema records them without redefining either state machine.
Each store carries its own schema identity and version.
### Session terminal ownership
```mermaid
classDiagram
class SessionTerminal {
generation_id
session_id
state
container_id
}
class PtyIdentity {
master_fd
device
inode
}
class ProcessIdentity {
pid
start_time
}
class GuestProcessIdentity {
leader_pid
leader_start_time
process_group_id
}
SessionTerminal --> ProcessIdentity : host_coordinator
SessionTerminal --> PtyIdentity : pty_master
SessionTerminal --> ProcessIdentity : exec_client
SessionTerminal --> GuestProcessIdentity : guest_process
```
Host process identities use host pid and start time. Guest process identity uses
the leader PID and start time observed inside the exact generation-bound runsc
container; its process-group ID is relative to that container's root PID
namespace.
The PTY identity is exact only in combination with its Host Coordinator process
identity. `SessionTerminalState` is a physical recovery state below the
application protocol model; it does not redefine `session_phase`.
## Session terminal protocol
```mermaid
classDiagram
class SessionTerminalEvent {
<<union>>
}
class TerminalInput {
session_id
bytes
}
class TerminalResize {
session_id
rows
columns
pixel_width
pixel_height
}
class TerminalSignal {
session_id
signal
}
class TerminalSignalKind {
<<enumeration>>
Interrupt
Quit
Suspend
}
class SessionClose {
session_id
}
class SessionTerminalMessage {
<<union>>
}
class TerminalOutput {
session_id
bytes
}
class SessionExit {
session_id
outcome
exit_code
}
class SessionExitOutcome {
<<enumeration>>
Exited
Terminated
RuntimeLost
}
SessionTerminalEvent --> TerminalInput
SessionTerminalEvent --> TerminalResize
SessionTerminalEvent --> TerminalSignal
SessionTerminalEvent --> SessionClose
TerminalSignal --> TerminalSignalKind
SessionTerminalMessage --> TerminalOutput
SessionTerminalMessage --> SessionExit
SessionExit --> SessionExitOutcome
```
`exit_code` is present only for `Exited` and is the status collected from the
non-detached runsc exec client. Interactive PTY output is one merged byte stream;
it does not preserve stdout and stderr as separate channels. Protocol
cryptographic envelopes and wire encoding are outside this schema.
### Participant ownership
```mermaid
@ -251,7 +385,9 @@ do not form one transactional database.
`ReleaseIntent` is a physical recovery state. It does not redefine the modeled
lease lifecycle: the specification defines how Domain Store release intent,
physical unmount, and Storage Catalog lease removal refine model unmount and
release actions.
release actions. After Host Coordinator loss, the exact Runtime Supervisor may
unmount under the retained Prepared ownership record, but the Artifact Lease
remains until bootstrap Host Coordinator recovery records release intent.
## Derived network policy

133
docs/specification.md
View file

@ -9,7 +9,7 @@ This document is the normative product specification for Lazaret.
| This specification | Product north star, trust model, stable vocabulary and identifiers, below-abstraction architecture, and product requirements |
| [TLA+ application protocol model](protocol/Lazaret.tla) and [TLC config](protocol/Lazaret.cfg) | Protocol lifecycle, communication semantics, publication, registration, escalation, recovery, and checked invariants |
| [Prepared-lower TLA+ model](protocol/PreparedLower.tla) and [TLC config](protocol/PreparedLower.cfg) | Prepared-artifact publication, generation leases, mounts, reclamation, stage recovery, and checked invariants |
| [Design schemas](schema.md) | Logical durable records, network-policy documents, readiness evidence, and their relationships |
| [Design schemas](schema.md) | Logical records, protocol data shapes, network-policy documents, readiness evidence, and their relationships |
This specification does **not** restate modeled actions or invariants. The TLA+
models are authoritative above their abstraction boundaries. This specification
@ -207,20 +207,105 @@ session identity needed for routing and cleanup, including Session ID, PTY maste
Interactive terminal control requires:
- Window resize applied to the host PTY master and guest `SIGWINCH` delivered to
the exact session process or process group through runsc.
- Client control events (for example interrupt) translated into runsc signal
operations for that exact session process or process group; raw host PTY
control characters alone are not a sufficient contract.
- Per-session exit status collected from the non-detached `runsc exec` client as
the primary source.
- On session close, PTY master loss, or exec-client loss: apply the modeled
session-close transition, stop the exact guest session process or process
group through runsc, reap the exec client, and close the PTY.
- Each interactive command starts as the leader of a generation-bound guest
process group. The Host Coordinator records both the leader PID and process
start time and the process group ID relative to the exact runsc container
before admitting terminal events.
- Window resize applies `TIOCSWINSZ` to the host PTY master and then delivers
guest `SIGWINCH` to that process group through runsc. Rows and columns are
nonzero unsigned 16-bit values; pixel dimensions may be zero when unknown.
- Client `Interrupt`, `Quit`, and `Suspend` events translate respectively to
`SIGINT`, `SIGQUIT`, and `SIGTSTP` for that process group. Raw control bytes do
not substitute for these events. Host CLI suspension is local: the CLI
restores its terminal before stopping itself and sends the current window size
after resuming; it does not synthesize a guest signal.
- Per-session exit status comes from the non-detached `runsc exec` client. An
interactive PTY produces one merged output byte stream, so the protocol does
not label its bytes as separate stdout and stderr streams.
Disconnected Client Sessions close rather than reattach to an unbounded scrollback
owned by the coordinator.
The session connection carries the terminal events and messages defined by the
normative design schema. One Host Coordinator event loop serializes input,
resize, signal, close, prompt-routing, PTY output, and exec-client completion for
each Session ID. It uses bounded queues and PTY backpressure; terminal data for
one session cannot consume another session's control capacity. Input, resize,
and signal events are accepted only while the modeled terminal route is the
sandbox route. An invalid Session ID, inactive route, stale generation, or
terminal in release refuses the event.
PTY output is forwarded only while the modeled terminal route is the sandbox
route. During `Prompt` or `HostProcess` routing the Host Coordinator stops reading
the PTY master and relies on bounded kernel PTY buffering and backpressure; it
does not accumulate an unbounded user-space queue. Forwarding resumes only after
the model restores the sandbox route.
Normal guest completion begins the modeled session close and physical release,
so no new terminal or escalation event is admitted. The Host Coordinator
first cancels any active prompt or exact host process and serializes that
cancellation before terminal output. It then collects and reaps the exec client,
drains and forwards PTY bytes in order until EOF or a bounded drain deadline,
and emits at most one `SessionExit` after the last forwarded byte on the closing
connection. This close handshake does not restore session routing. If the
connection is already lost, the outcome is not retained for reattachment.
Physical Session Terminal acquisition is ordered as follows:
1. The Host Coordinator records `SessionTerminal=Intent` in the Domain Store.
2. It allocates the PTY and forks a wrapper with the expected HC pid/start
identity. The wrapper arms its HC parent-death edge, re-reads its parent pid
and start identity, and aborts before invoking runsc if either differs. It may
create the guest process only after that recheck succeeds.
3. It establishes the guest process group and obtains the guest leader PID,
start time, and group ID.
4. One Domain Store transaction records the exact Host Coordinator, PTY, exec
client, container, guest leader, and guest process-group identities and sets
`SessionTerminal=Running`.
5. Only then may the Host Coordinator accept terminal events for the session.
Failure before `Running` never admits the terminal. A live Host Coordinator uses
its in-memory exact handles to terminate any partial exec and guest group and
records release intent. If HC itself is lost, the armed exec edge stops the host
client and the generation lease-loss path stops the guest sandbox; bootstrap
recovery cleans the retained Intent only after runtime absence.
Session close, Client connection loss, PTY loss, or exec-client loss starts the
same physical release:
1. Apply the modeled session close, remove terminal and escalation routing, and
record `SessionTerminal=ReleaseIntent` while retaining all exact identities.
2. If the exact generation is still serviceable and the guest leader identity
and group still match, send `SIGHUP`, wait for a bounded grace period, then
send `SIGTERM`, wait again, and send `SIGKILL` if the group remains. A leader
mismatch refuses the numeric process-group signal. If the leader is absent,
an empty recorded group needs no signal; a nonempty group is left in release
intent for Domain teardown.
3. Terminate and reap the exact exec client when it is still a Host Coordinator
child and close the exact PTY master. Record `SessionTerminal=Clean` only
after the guest group, exec client, and PTY are absent; otherwise retain
release intent.
The process-group boundary is the per-session cleanup contract, not a security
boundary. A sandbox process may daemonize or move into another process group;
the final Client Session leaving the Domain triggers Domain teardown, which is
the containment boundary for such processes.
Hard Host Coordinator loss closes its PTY descriptors and fails modeled open
sessions; the exec-client lifetime edge prevents an unrecorded or recorded exec
client from surviving that loss. The surviving Runtime Supervisor follows the
generation lease-loss teardown: it stops the complete Agent Sandbox, unmounts
the exact State Anchor while retaining the prepared-lower lease, and exits.
Bootstrap recovery waits until the Runtime Supervisor and attached runsc are
absent, never recreates a PTY or reattaches a Client Session, releases the
retained prepared lower under the durable generation refinement, verifies that
the exact generation container and guest processes are gone, terminates any
still-live exact exec-client host process, and then records each retained Session
Terminal `Clean`. An `Intent` without physical identities becomes `Clean` only
after that runtime-absence check. A process, container, PTY, or generation
mismatch fails closed and retains the record; it is never adopted or signaled as
the recorded session.
### 3.4 Filesystem and Git Model
The Agent Workspace is mounted read-write. Tracked paths and untracked paths that
@ -338,6 +423,23 @@ The physical unmount and lease-release refinement is:
catalog transaction.
5. Commit `prepared_lower = Clean` in the Domain Store.
Host Coordinator hard loss uses the model's split lease-loss refinement. The
surviving exact Runtime Supervisor stops the sandbox and sidecar, verifies and
unmounts its exact State Anchor, and exits without opening the Domain Store or
Storage Catalog. The original durable anchor intent and exact Prepared ownership
authorize rollback of the resource the supervisor created; they do not authorize
catalog lease removal. The catalog lease remains held after unmount.
Bootstrap recovery begins only after the Runtime Supervisor and attached runsc
are absent. If the exact mount remains, the bootstrap Host Coordinator records
`state_anchor = ReleaseIntent` and completes normal exact unmount. If the
surviving Runtime Supervisor already unmounted it, bootstrap independently
verifies exact mount absence. It then atomically commits `state_anchor = Clean`
and `prepared_lower = ReleaseIntent`, removes the exact catalog lease under the
catalog lock, and commits `prepared_lower = Clean`. Thus lease-loss unmount and
lease release are distinct: only a lock-holding Host Coordinator releases the
prepared-lower lease.
Recovery resumes only from matching durable identity. `state_anchor =
ReleaseIntent` retains the catalog lease while recovery verifies and completes
the unmount. `prepared_lower = ReleaseIntent` permits removal of a still-present
@ -346,8 +448,11 @@ permits the Domain participant to become `Clean`. A catalog lease with missing,
unreadable, non-release, or mismatched Domain evidence is retained and reported.
A Domain `LeaseHeld` record whose exact catalog lease is absent is inconsistent
and fails closed; recovery neither recreates the lease nor mounts the State
Anchor. These rules make every interrupted release conservative and prevent a
mounted State Anchor from becoming unleased.
Anchor. A failed generation with a Prepared anchor, an absent exact mount, and a
still-present exact catalog lease is the conservative HC-loss state above; only
bootstrap recovery may advance it to release intent. These rules make every
interrupted release conservative and prevent a mounted State Anchor from
becoming unleased.
Store version acceptance occurs before physical resource inspection. The first
product version has no product predecessor. Future migration steps create and
@ -487,7 +592,7 @@ not duplicated here.
| **FR-9** | Trusted host configuration shall allow the developer to disable Git-ignored path isolation for an Agent Profile. |
| **FR-11** | The host CLI shall list, inspect, structurally verify, and reset all or selected State Anchors without requiring direct manipulation of Lazaret's storage layout. |
| **FR-14** | The Host Coordinator shall own one host PTY master per interactive Client Session; the PTY slave shall attach through non-detached `runsc exec` standard streams. The root attached `runsc run` client shall remain terminal-neutral. Production Session PTYs shall not depend on `runsc exec -console-socket`. |
| **FR-15** | For each interactive Client Session, Lazaret shall apply window resize to the host PTY master and deliver guest `SIGWINCH` to the exact session process or process group through runsc; translate Client control events into runsc signal operations; collect exit status primarily from the non-detached `runsc exec` client; and after the modeled session-end transition stop the exact guest process or process group, reap the exec client, and close the PTY. |
| **FR-15** | For each interactive Client Session, Lazaret shall preserve the Session Terminal record and protocol in the normative design schema; serialize bounded terminal events and merged output by Session ID; map resize and the `Interrupt`, `Quit`, and `Suspend` events to the specified exact process-group operations; collect exit status from the non-detached `runsc exec` client; and follow the specified release and hard-loss recovery ordering without reattachment or mismatched cleanup. |
| **FR-16** | Domain network connectivity shall use `slirp4netns` as the production connectivity helper. The Domain Store shall record independent `helper` intent before launch and exact helper and supervising Runtime Supervisor pid/start identities before network readiness. |
| **FR-17** | The Domain Store shall be opened only by the Host Coordinator process holding the Domain `flock`; mutations shall use whole redb transactions. Storage Catalog opens shall be bounded by `storage-catalog.lock` and one transaction. Cross-store lease release shall follow the durable release-intent, exact-unmount, catalog-delete, Domain-clean ordering defined by the durable generation refinement. |
| **FR-18** | Product network-readiness evidence shall conform to the normative design schema and include the readiness fingerprint plus the generation-bound deny/permit/DNS probe result. |