Idea: add P formal model of the sessions runtime

specs/sessions/pmodel/.gitignore

@@ -0,0 +1,3 @@
+# P compiler / checker outputs
+PGenerated/
+PCheckerOutput/

specs/sessions/pmodel/Dockerfile

@@ -0,0 +1,79 @@
+# syntax=docker/dockerfile:1
+
+# ---------------------------------------------------------------------------
+# Official P toolchain image.
+#
+# Bundles everything needed to compile and check P programs:
+#   - .NET SDK 8.0   (the P compiler / PChecker are implemented in C#)
+#   - JDK 17 + Maven (the PEx / PSym checker backends run on the JVM; the P
+#                     Java sources target Java 17 -- see Src/PEx/pom.xml)
+#   - graphviz       (used to render coverage / state-machine diagrams)
+#   - the `p` CLI    (built from this repository and installed as a global
+#                     dotnet tool)
+#
+# Build:   docker build -t p .
+# Run:     docker run --rm -it -v "$PWD":/workspace p
+# ---------------------------------------------------------------------------
+
+# --- Stage 1: build the P tool from the repository source ------------------
+FROM mcr.microsoft.com/dotnet/sdk:8.0 AS build
+
+# The P compiler build runs the ANTLR4 code generator, which shells out to
+# `java`, so a JDK is required even just to `dotnet pack` the tool.
+RUN apt-get update \
+    && apt-get install -y --no-install-recommends openjdk-17-jdk-headless \
+    && rm -rf /var/lib/apt/lists/*
+
+WORKDIR /src
+COPY . .
+
+# Pack the `p` command-line tool into a local NuGet package. This mirrors the
+# `dotnet pack` step used by the release workflow; the resulting .nupkg lands
+# under Bld/Drops/Release/Binaries/ (see Directory.Build.props).
+RUN dotnet pack Src/PCompiler/PCommandLine/PCommandLine.csproj -c Release \
+    && mkdir -p /nupkg \
+    && cp Bld/Drops/Release/Binaries/[Pp].*.nupkg /nupkg/
+
+# --- Stage 2: the toolchain image ------------------------------------------
+FROM mcr.microsoft.com/dotnet/sdk:8.0
+
+LABEL org.opencontainers.image.title="P" \
+      org.opencontainers.image.description="Toolchain image for the P formal modeling language (P compiler, PChecker, PEx). Includes .NET 8, JDK 17, Maven and graphviz." \
+      org.opencontainers.image.source="https://github.com/p-org/P" \
+      org.opencontainers.image.documentation="https://p-org.github.io/P/" \
+      org.opencontainers.image.licenses="MIT"
+
+# Install the JVM toolchain (PEx/PSym backends) and graphviz. openjdk-17 is
+# available for both amd64 and arm64 in the Debian repositories used by the
+# .NET SDK base image, so this image builds natively on both architectures.
+RUN apt-get update \
+    && apt-get install -y --no-install-recommends \
+        openjdk-17-jdk-headless \
+        maven \
+        graphviz \
+    && rm -rf /var/lib/apt/lists/*
+
+# The JDK install path is arch-specific in the Debian layout
+# (java-17-openjdk-amd64 vs -arm64), so point a stable symlink at whichever
+# one this build produced and set JAVA_HOME to that fixed location. This keeps
+# JAVA_HOME identical and correct on both amd64 and arm64.
+RUN JAVA_BIN="$(readlink -f "$(command -v java)")" \
+    && JAVA_DIR="$(dirname "$(dirname "$JAVA_BIN")")" \
+    && ln -s "$JAVA_DIR" /usr/lib/jvm/default-jdk
+ENV JAVA_HOME=/usr/lib/jvm/default-jdk
+
+# Install the `p` tool built in stage 1 from the local package source.
+COPY --from=build /nupkg /tmp/nupkg
+RUN dotnet tool install --global --add-source /tmp/nupkg P \
+    && rm -rf /tmp/nupkg
+ENV PATH="${PATH}:/root/.dotnet/tools"
+
+# Also expose the tools directory to login shells (which re-source
+# /etc/profile and would otherwise drop the ENV above).
+RUN echo 'export PATH="$PATH:/root/.dotnet/tools"' > /etc/profile.d/dotnet-tools.sh
+
+# Sanity check: fail the build if the CLI is not runnable.
+RUN p --help > /dev/null
+
+WORKDIR /workspace
+CMD ["bash"]

specs/sessions/pmodel/OpenJDSessions.pproj

@@ -0,0 +1,10 @@
+<?xml version="1.0" encoding="utf-8"?>
+<Project>
+  <ProjectName>OpenJDSessions</ProjectName>
+  <InputFiles>
+    <PFile>PSrc</PFile>
+    <PFile>PSpec</PFile>
+    <PFile>PTst</PFile>
+  </InputFiles>
+  <OutputDir>PGenerated</OutputDir>
+</Project>

specs/sessions/pmodel/PSpec/ActionLivenessSpec.p

@@ -0,0 +1,23 @@
+/*****************************************************************************
+ * ActionLivenessSpec.p — every started action eventually terminates
+ * (specs/sessions/session.md: no recovery path; subprocess always exits via
+ *  normal exit, timeout→SIGKILL, or cancel→grace→SIGKILL).
+ *
+ * Liveness: whenever an action is Running (Busy), the system must eventually
+ * reach a state where no action is Running (Idle).
+ *****************************************************************************/
+
+spec ActionLivenessSpec observes eMonActionStart, eMonActionEnd {
+    start state Idle {
+        on eMonActionStart goto Busy;
+        // A spurious end without a start is caught by SessionStateSpec.
+        ignore eMonActionEnd;
+    }
+
+    hot state Busy {
+        on eMonActionEnd goto Idle;
+        // Nested starts can't happen (SessionStateSpec enforces ≤1); ignore
+        // defensively so this spec stays focused on the liveness question.
+        ignore eMonActionStart;
+    }
+}

specs/sessions/pmodel/PSpec/CancelDeliverySpec.p

@@ -0,0 +1,48 @@
+/*****************************************************************************
+ * CancelDeliverySpec.p — a cancel that is issued must actually take effect.
+ *
+ * Invariant: if a cancel is issued for the currently-running action (via ANY
+ * delivery channel — cancel_action, a malformed directive, OR an external
+ * SessionConfig.cancel_token cascade), then that action MUST NOT complete
+ * Successfully. It must end Canceled, Failed (e.g. mark_action_failed), or
+ * Timeout. In other words, an acknowledged cancel is never silently dropped.
+ *
+ * This is exactly the guarantee the same-user path provides (its subprocess
+ * loop awaits the CancellationToken directly, so a cancel over either the
+ * watch channel or the token is observed). It is the guarantee the CROSS-USER
+ * path currently BREAKS: run_via_helper only observes cancels that arrive over
+ * the watch/pipe channel, so a token-only external cancel (viaWatch = false)
+ * is not seen and the action can run to a Success/Failed exit as if no cancel
+ * happened. Model-checking tcWorkerAgentCrossUser against this spec fails on
+ * the current (buggy) routing and passes once the cross-user path also honours
+ * a token-delivered cancel.
+ *****************************************************************************/
+
+spec CancelDeliverySpec observes eMonActionStart, eMonCancelIssued, eMonActionEnd {
+    var canceled: bool;   // a cancel was issued for the in-flight action
+
+    start state Idle {
+        on eMonActionStart goto Active;
+        ignore eMonCancelIssued, eMonActionEnd;
+    }
+
+    state Active {
+        entry { canceled = false; }
+
+        on eMonCancelIssued do (m: (actionId: tActionId, viaWatch: bool)) {
+            canceled = true;
+        }
+
+        on eMonActionEnd do (m: (actionId: tActionId, st: tActionState)) {
+            if (canceled) {
+                assert m.st != ACT_SUCCESS,
+                    format ("Action {0} was canceled but completed Successfully — the cancel was dropped (cross-user token-only cancel not observed by run_via_helper?).", m.actionId);
+            }
+            goto Idle;
+        }
+
+        // Only one action runs at a time (SessionStateSpec enforces ≤1), so a
+        // second start here would be a bug in the harness; ignore defensively.
+        ignore eMonActionStart;
+    }
+}

specs/sessions/pmodel/PSpec/EnvStackSpec.p

@@ -0,0 +1,47 @@
+/*****************************************************************************
+ * EnvStackSpec.p — environment LIFO + no-duplicate invariants
+ * (specs/sessions/session.md § Environment Management, § Why LIFO enforcement).
+ *
+ * Asserts:
+ *   - environments are popped in strict LIFO order (last pushed = first popped)
+ *   - no duplicate environment id is ever on the stack simultaneously
+ *   - cleanup() with a non-empty stack is flagged (onExit scripts skipped)
+ *****************************************************************************/
+
+spec EnvStackSpec observes eMonEnter, eMonExit, eMonCleanup {
+    var stack: seq[tEnvId];
+
+    start state Watching {
+        entry { stack = default(seq[tEnvId]); }
+
+        on eMonEnter do (id: tEnvId) {
+            assert !contains(id), format ("Duplicate environment {0} pushed onto stack", id);
+            stack += (sizeof(stack), id);
+        }
+
+        on eMonExit do (id: tEnvId) {
+            assert sizeof(stack) > 0, "Exit with empty environment stack";
+            assert stack[sizeof(stack) - 1] == id,
+                format ("Non-LIFO exit: popped {0} but top is {1}", id, stack[sizeof(stack) - 1]);
+            stack -= (sizeof(stack) - 1);
+        }
+
+        on eMonCleanup do (depth: int) {
+            assert depth == sizeof(stack), "monitor/session stack depth diverged";
+            // Documented hazard, not a correctness bug in the model, but a
+            // well-formed driver should have exited everything first.
+            assert depth == 0,
+                format ("cleanup() called with {0} environment(s) still entered", depth);
+        }
+    }
+
+    fun contains(id: tEnvId): bool {
+        var i: int;
+        i = 0;
+        while (i < sizeof(stack)) {
+            if (stack[i] == id) { return true; }
+            i = i + 1;
+        }
+        return false;
+    }
+}

specs/sessions/pmodel/PSpec/MonitorEvents.p

@@ -0,0 +1,16 @@
+/*****************************************************************************
+ * MonitorEvents.p — events announced by Session for the spec monitors.
+ * These carry no behavior; they let the monitors observe the abstract state.
+ *****************************************************************************/
+
+event eMonStateChanged : (fromState: tSessionState, toState: tSessionState);
+event eMonActionStart  : (actionId: tActionId, kind: tActionKind);
+event eMonActionEnd    : (actionId: tActionId, st: tActionState);
+event eMonEnter        : tEnvId;   // env pushed
+event eMonExit         : tEnvId;   // env popped
+event eMonCleanup      : int;      // stack depth at cleanup()
+event eMonHelperBadToken;          // helper rejected a bad/missing token
+// A cancel was issued for the current action. viaWatch = travelled the watch/
+// pipe channel (cancel_action / malformed directive); false = token-only
+// (external SessionConfig.cancel_token cascade).
+event eMonCancelIssued : (actionId: tActionId, viaWatch: bool);

specs/sessions/pmodel/PSpec/SessionStateSpec.p

@@ -0,0 +1,66 @@
+/*****************************************************************************
+ * SessionStateSpec.p — the SessionState transition + brittle-session invariants
+ * (specs/sessions/session.md § Transitions, § Brittle Sessions).
+ *
+ * Asserts:
+ *   - only documented transitions occur
+ *   - Ended is terminal (no transition out)
+ *   - at most one action Running at a time
+ *   - after any Failed/Canceled/Timeout the session is ending-only: it may only
+ *     reach Ready via S_READY_ENDING, never plain S_READY again
+ *****************************************************************************/
+
+spec SessionStateSpec observes eMonStateChanged, eMonActionStart, eMonActionEnd {
+    var actionsRunning: int;   // must never exceed 1
+    var brittle: bool;         // a terminal-failure action has occurred
+
+    start state Watching {
+        entry { actionsRunning = 0; brittle = false; }
+
+        on eMonStateChanged do (t: (fromState: tSessionState, toState: tSessionState)) {
+            assert validTransition(t.fromState, t.toState),
+                format ("Illegal SessionState transition {0} -> {1}", t.fromState, t.toState);
+
+            // Ended is terminal.
+            assert t.fromState != S_ENDED,
+                "SessionState left the terminal Ended state";
+
+            // Once brittle, the session must not return to plain Ready. The
+            // only allowed non-ending resting state after a failure is
+            // S_READY_ENDING (reached via ReadyEnding) or S_ENDED.
+            if (brittle) {
+                assert t.toState != S_READY,
+                    "Brittle session transitioned back to Ready (should be ReadyEnding)";
+            }
+        }
+
+        on eMonActionStart do (m: (actionId: tActionId, kind: tActionKind)) {
+            actionsRunning = actionsRunning + 1;
+            assert actionsRunning <= 1,
+                format ("More than one action running concurrently ({0})", actionsRunning);
+        }
+
+        on eMonActionEnd do (m: (actionId: tActionId, st: tActionState)) {
+            actionsRunning = actionsRunning - 1;
+            assert actionsRunning >= 0, "action ended without a matching start";
+            if (m.st == ACT_FAILED || m.st == ACT_CANCELED || m.st == ACT_TIMEOUT) {
+                brittle = true;
+            }
+        }
+    }
+}
+
+/* The transition relation from specs/sessions/session.md § Transitions. */
+fun validTransition(fromS: tSessionState, toS: tSessionState): bool {
+    if (fromS == toS) { return true; } // announce fires even for no-op re-sets
+    // Ready → Running | Ended
+    if (fromS == S_READY)        { return toS == S_RUNNING || toS == S_ENDED; }
+    // Running → Ready | ReadyEnding | Canceling
+    if (fromS == S_RUNNING)      { return toS == S_READY || toS == S_READY_ENDING || toS == S_CANCELING; }
+    // Canceling → Ready | ReadyEnding
+    if (fromS == S_CANCELING)    { return toS == S_READY || toS == S_READY_ENDING; }
+    // ReadyEnding → Running | Ended
+    if (fromS == S_READY_ENDING) { return toS == S_RUNNING || toS == S_ENDED; }
+    // Ended → (none)
+    return false;
+}