Idea: add P formal model of the sessions runtime - #289
Conversation
Add a P (p-org/P) model of crates/openjd-sessions under specs/sessions/pmodel: the SessionState machine, an abstract Subprocess, the persistent cross-user Helper + token protocol, and spec monitors for the state machine, environment LIFO stack, action liveness, and cancel delivery. Includes drivers, six test cases, a Dockerfile (from p-org/P PR #983) for the toolchain, and a README documenting scope. The model checks clean with P CLI 3.1.0. It models cancellation as a two-channel delivery (watch channel + CancellationToken) and asserts, via CancelDeliverySpec, that an issued cancel is never dropped whichever channel carries it. A CROSS_USER_HONORS_TOKEN_CANCEL knob provides fault injection to demonstrate that spec has teeth.
crowecawcaw
changed the title
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
| // (session.rs), which delivers the action's CONFIGURED cancel | ||
| // method — NOT an unconditional Terminate. | ||
| requestCancel(curCancelMethod); | ||
| goto Canceling; |
There was a problem hiding this comment.
The eCancelMarkFailed handler goes to Canceling without first calling setState(S_CANCELING), unlike the two sibling cancel handlers (eCancelAction at line 192 and eSessionCancelToken at line 201, which both do setState(S_CANCELING); goto Canceling;).
The comment here states a malformed directive routes through cancel_action(None, true) — the same cancel_action path that, in the real code, transitions the session to Canceling. So on the malformed-directive path the model leaves sstate == S_RUNNING while it is conceptually canceling, and never announces the S_RUNNING -> S_CANCELING transition to SessionStateSpec.
This does not trip an assertion (the eventual finalizeAction does S_RUNNING -> S_READY_ENDING, which validTransition permits), so it silently reduces SessionStateSpecs coverage of the Canceling state on this path rather than surfacing an error. Adding setState(S_CANCELING); before the goto here would make the three cancel paths consistent and let the spec verify the transition uniformly.
crowecawcaw
changed the title
1 participant
What
Adds a P formal model of the
openjd-sessionsruntime underspecs/sessions/pmodel/. Documentation/tooling only — no changes to any crate.The model captures the sessions runtime as a set of communicating state machines:
SessionStatemachine (Ready / Running / Canceling / ReadyEnding / Ended), the environment LIFO stack, the cumulative env-var change set, and the brittle-session (ending-only) contract.Spec monitors assert the invariants: legal state transitions and ≤1 running action, LIFO environment exits with no duplicates, action liveness, and cancel delivery (an issued cancel is never silently dropped). A
Dockerfile(from p-org/P PR #983) provides the toolchain; aREADME.mddocuments scope, what's abstracted away, and how to run it.Status
Compiles and model-checks clean with P CLI 3.1.0 — all test cases report 0 bugs. Two fault-injection knobs demonstrate the monitors are not vacuous (removing the exit-time stack pop breaks
EnvStackSpec;CROSS_USER_HONORS_TOKEN_CANCELbreaksCancelDeliverySpecon the cross-user token-only path).Why draft
Opened as a draft for discussion: this is the first formal-methods artifact in the repo, so the questions worth settling before merge are whether the team wants P models living in-tree at all, where they should sit, and whether CI should run the checker.
Related
Building this model surfaced two behavioral bugs in
openjd-sessions, filed separately:ending_onlynever set on action failureSessionConfig.cancel_tokencancelsCancelDeliverySpecin this model corresponds to the invariant #288 violates.