From faa4af857da309ce6de293250e59f11134097d6e Mon Sep 17 00:00:00 2001 From: Bernard Ladenthin Date: Sun, 13 Sep 2026 01:33:45 +0200 Subject: [PATCH 1/2] feat: formal verification suite (OpenJML ESC/RAC + JPF) in a separate CI pipeline Add machine-checked formal verification for StreamBuffer, run in a new pipeline (.github/workflows/formal-verification.yml) kept fully separate from the synchronous Publish pipeline and never a required check. Four layers: - OpenJML ESC (deductive proof, Z3): the 14 static sequential-core methods (2 offset/length validators incl. the (off+len)<0 overflow idiom, + 12 trim-decision/arithmetic helpers) are proven against full functional contracts. A proof-count guard fails the job if the verified scope silently shrinks. - OpenJML RAC: the existing JUnit suite runs against RAC-instrumented classes (contracts checked at runtime, violations throw), forking OpenJML's own JVM so the bundled-spec bigint runtime resolves. - jcstress Mode.Termination: four new tests extend deadlock-freedom coverage to every blocking entry point (read(byte[],off,len) phase-2 and the public waitForAtLeast API), each paired with a write and a close wakeup. - JPF (scheduled/dispatch job): exhaustively model-checks the concurrent read/write/close protocol over all enumerated interleavings; local Docker+JDK11 recipe in src/test/jpf/README.md. Specifications live only in src/main/jml/.../StreamBuffer.jml (the .java stays JML-free, spotless-compatible). Behaviour-preserving production changes were needed for the tooling: 12 pure helpers made static (instance-method ESC is undecidable here), read/write logic lifted into private outer methods (OpenJML RAC miscompiles outer-field access from non-static inner classes), and the write validator's null check inlined (nullable_by_default + Objects.requireNonNull leaves an unprovable ESC goal). SpotBugs suppressions added for the false positives this relocation surfaces (safe volatile increments under bufferLock; single-package OPM on public API; a clear constant NPE message). Default pipeline unchanged and green: 288 tests, SpotBugs 0, PIT 100%. ESC 14/14, RAC 277/277, jcstress 7/7, JPF "no errors detected" (~14k states, negative-control-validated oracle). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01TU5B8DDtDwKSS6ohSfoz2Y --- .github/actions/setup-openjml/action.yml | 82 ++++ .github/workflows/formal-verification.yml | 305 ++++++++++++ .gitignore | 10 + CLAUDE.md | 79 +++ README.md | 35 ++ TODO.md | 54 +++ pom.xml | 93 ++++ spotbugs-exclude.xml | 56 +++ .../ladenthin/streambuffer/StreamBuffer.java | 454 +++++++++++------- .../ladenthin/streambuffer/StreamBuffer.jml | 382 +++++++++++++++ .../StreamBufferLincheckTest.java | 12 +- .../streambuffer/StreamBufferTest.java | 111 ++--- .../jcstress/CloseUnblocksArrayReadRace.java | 59 +++ .../CloseUnblocksWaitForAtLeastRace.java | 46 ++ .../jcstress/WriteUnblocksArrayReadRace.java | 63 +++ .../WriteUnblocksWaitForAtLeastRace.java | 50 ++ src/test/jpf/README.md | 83 ++++ src/test/jpf/StreamBuffer.jpf | 22 + .../util/concurrent/atomic/AtomicLong.java | 132 +++++ .../jpf/JpfStreamBufferHarness.java | 78 +++ 20 files changed, 1976 insertions(+), 230 deletions(-) create mode 100644 .github/actions/setup-openjml/action.yml create mode 100644 .github/workflows/formal-verification.yml create mode 100644 src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml create mode 100644 src/test/java/net/ladenthin/streambuffer/jcstress/CloseUnblocksArrayReadRace.java create mode 100644 src/test/java/net/ladenthin/streambuffer/jcstress/CloseUnblocksWaitForAtLeastRace.java create mode 100644 src/test/java/net/ladenthin/streambuffer/jcstress/WriteUnblocksArrayReadRace.java create mode 100644 src/test/java/net/ladenthin/streambuffer/jcstress/WriteUnblocksWaitForAtLeastRace.java create mode 100644 src/test/jpf/README.md create mode 100644 src/test/jpf/StreamBuffer.jpf create mode 100644 src/test/jpf/jpf-model/java/util/concurrent/atomic/AtomicLong.java create mode 100644 src/test/jpf/net/ladenthin/streambuffer/jpf/JpfStreamBufferHarness.java diff --git a/.github/actions/setup-openjml/action.yml b/.github/actions/setup-openjml/action.yml new file mode 100644 index 0000000..7cf2f31 --- /dev/null +++ b/.github/actions/setup-openjml/action.yml @@ -0,0 +1,82 @@ +# SPDX-FileCopyrightText: 2014-2026 Bernard Ladenthin +# +# SPDX-License-Identifier: Apache-2.0 + +name: Set up OpenJML +description: > + Installs a pinned, checksum-verified OpenJML release (Ubuntu x64 build) into + $RUNNER_TEMP/openjml and exposes the location as the OPENJML_HOME environment + variable. The unzipped distribution (~1 GB, zip 392 MB) is cached keyed on + version + checksum + fixup revision. Known-broken bundled JDK specification + files are deleted on install (see the fixup step below); because the deletion + happens before the cache is saved, cache hits already contain the fixed tree. + +inputs: + version: + description: OpenJML release version (GitHub release tag) + required: true + sha256: + description: Expected SHA-256 of the openjml-ubuntu-24.04-.zip release asset + required: true + +runs: + using: composite + steps: + - name: Restore OpenJML from cache + id: cache + uses: actions/cache@v6 + with: + path: ${{ runner.temp }}/openjml + # spec-fixups-v1: bump this suffix whenever the fixup step below changes, + # otherwise cached installs keep the previous fixup state. + key: openjml-ubuntu-x64-${{ inputs.version }}-${{ inputs.sha256 }}-spec-fixups-v1 + + - name: Download pinned OpenJML (checksum-verified) + if: steps.cache.outputs.cache-hit != 'true' + shell: bash + run: | + set -euo pipefail + curl --fail --location --retry 3 -o "$RUNNER_TEMP/openjml.zip" \ + "https://github.com/OpenJML/OpenJML/releases/download/${{ inputs.version }}/openjml-ubuntu-24.04-${{ inputs.version }}.zip" + echo "${{ inputs.sha256 }} $RUNNER_TEMP/openjml.zip" | sha256sum --check --strict + mkdir -p "$RUNNER_TEMP/openjml" + unzip -q "$RUNNER_TEMP/openjml.zip" -d "$RUNNER_TEMP/openjml" + rm "$RUNNER_TEMP/openjml.zip" + chmod +x "$RUNNER_TEMP/openjml/openjml" "$RUNNER_TEMP/openjml/openjml-java" + + - name: Delete known-broken bundled JDK specs (fixups v1) + if: steps.cache.outputs.cache-hit != 'true' + shell: bash + # Both files ship broken in OpenJML 21.0.27 and break the RAC layer; deleting a + # bundled spec degrades the affected JDK class to default (empty) contracts, which + # is exactly what this repo needs — StreamBuffer's own contracts are the ones being + # checked. `rm` without -f: if an upgrade removes/fixes these files upstream, this + # step fails loudly and the fixup (plus the cache-key suffix) must be revisited. + # - ArrayDeque.jml: references the undeclared model variable `containsNull`; + # `openjml --rac` fails with "cannot find symbol: containsNull". + # - concurrent/atomic/AtomicLong.jml: RAC-generated checks read the private field + # AtomicLong.value across the module boundary; every test touching the + # statistics counters then dies with java.lang.IllegalAccessError. + run: | + set -euo pipefail + rm "$RUNNER_TEMP/openjml/specs/java/util/ArrayDeque.jml" + rm "$RUNNER_TEMP/openjml/specs/java/util/concurrent/atomic/AtomicLong.jml" + + - name: Repair the bundled JDK release file (fixups v1) + if: steps.cache.outputs.cache-hit != 'true' + shell: bash + # OpenJML 21.0.27's bundled jdk/release omits the JAVA_VERSION key. maven-surefire-plugin + # reads that key to fingerprint a forked (SystemUtils.toJdkVersionFromReleaseFile); + # without it the RAC job — which forks this exact JVM so the org.jmlspecs bigint runtime + # class resolves — dies before any test with an NPE. Add the key if it is missing. + run: | + set -euo pipefail + rel="$RUNNER_TEMP/openjml/jdk/release" + grep -q '^JAVA_VERSION=' "$rel" || printf 'JAVA_VERSION="21"\n' >> "$rel" + + - name: Export OPENJML_HOME and print version + shell: bash + run: | + set -euo pipefail + echo "OPENJML_HOME=$RUNNER_TEMP/openjml" >> "$GITHUB_ENV" + "$RUNNER_TEMP/openjml/openjml" --version diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml new file mode 100644 index 0000000..2b1e832 --- /dev/null +++ b/.github/workflows/formal-verification.yml @@ -0,0 +1,305 @@ +# SPDX-FileCopyrightText: 2014-2026 Bernard Ladenthin +# +# SPDX-License-Identifier: Apache-2.0 + +# --------------------------------------------------------------------------------------------- +# Formal verification — a SEPARATE pipeline, on purpose. +# +# The synchronous Publish pipeline (publish.yml) stays untouched: these jobs are additional +# evidence, not release gates, and none of them is (or should be made) a required check. +# Failure surfacing is a red check on the PR/commit that does not block a merge. +# +# Three layers (see CLAUDE.md "Formal verification" for the full story and the local recipes; +# the scope rationale with citations lives in the header of +# src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml): +# +# openjml-esc Deductive proof (OpenJML/Z3, extended static checking) of the sequential +# static core: both offset/length validators — including the intentional +# "(off + len) < 0" int-overflow idiom, proven equivalent to the clean bounds +# condition under Java wrap semantics — and the twelve static trim-decision/ +# arithmetic helpers with full functional contracts. +# +# openjml-rac Runtime assertion checking: the EXISTING JUnit suite runs against +# RAC-instrumented classes, so every JML contract is exercised dynamically +# (violations throw instead of the default print-and-continue). +# +# jpf-interleavings (scheduled/dispatch only) Java PathFinder EXHAUSTIVELY model-checks the +# concurrent read/write/close protocol over all enumerated thread interleavings — +# deadlock-freedom + byte fidelity, stronger than the jcstress stress tests. +# Heavy (builds jpf-core from source), so it is off the per-PR path. +# +# What is deliberately NOT here (evaluated 2026-09, see TODO.md "Formal verification"): +# the @GuardedBy("bufferLock") lock discipline is already gated in the DEFAULT pipeline by +# Error Prone's GuardedBy check; the Checker Framework Lock Checker would add soundness but +# cascades into unwinnable receiver-typing on the Closeable/InputStream/OutputStream JDK stubs +# (their stub receivers disagree), so it is deferred. Also not here: KeY (proof maintenance +# dwarfs the gain over OpenJML for this scope), VerCors (would require re-modeling the class in +# a Java subset; no volatile/JMM semantics), JBMC (no ArrayDeque/java.util.concurrent models), +# Infer/RacerD (explicitly does not reason about volatile). Concurrency is additionally covered +# empirically by Lincheck/jcstress/vmlens in the main pipeline. +# --------------------------------------------------------------------------------------------- + +name: Formal Verification + +on: + push: + branches: [main] + pull_request: + schedule: + # Weekly replay on main: catches drift that no PR touches — an OpenJML release pulled from + # GitHub, a broken download URL, or bit-rot in the pinned tool itself. + - cron: '17 4 * * 1' + workflow_dispatch: + +# Same expression as publish.yml (see the long rationale there): PR runs share a group per ref +# and supersede each other; every non-PR run gets a unique group via run_id so a scheduled or +# dispatched run is never queued behind (and thus never cancelled by) a sibling. +concurrency: + group: ${{ github.workflow }}-${{ github.ref }}-${{ github.event_name == 'pull_request' && 'pr' || github.run_id }} + cancel-in-progress: ${{ github.event_name == 'pull_request' }} + +permissions: + contents: read + +env: + OPENJML_VERSION: "21.0.27" + # SHA-256 of openjml-ubuntu-24.04-21.0.27.zip, taken from the GitHub release asset digest + # (https://github.com/OpenJML/OpenJML/releases/tag/21.0.27). ubuntu-latest is ubuntu-24.04, + # matching the asset. When bumping the version: update both values, re-test the RAC spec + # fixups in .github/actions/setup-openjml/action.yml, and re-try the class invariants noted + # in src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml. + OPENJML_SHA256: "325b93e0133736053cadb536d4dc6c9c6523e104691724135e4e03457188b06d" + # The ESC scope: the complete static, sequential core of StreamBuffer. Every method listed + # here MUST prove — and the count guard below additionally fails the job if the number of + # completed proofs is not exactly ESC_EXPECTED_PROOFS, so a typo here (or a rename in the + # class) cannot silently shrink the verified scope to zero. Methods NOT listed are covered + # by RAC + the ordinary test pyramid; the exception-message builder + # newInvalidOffsetOrLengthToWriteException carries a documented ASSUMED contract (string + # concatenation is beyond the SMT encoding) and is exercised by RAC and the unit tests. + ESC_METHODS: "validateOffsetAndLengthToRead;validateOffsetAndLengthToWrite;decideTrimExecution;clampToMaxInt;decrementAvailableBytesBudget;calculateResultingChunks;shouldSkipTrimDueToEdgeCase;shouldSkipTrimDueToInvalidMaxBufferElements;shouldSkipTrimDueToSmallBuffer;shouldSkipTrimDueToSufficientBuffer;isAvailableBytesPositive;isMaxAllocSizeLessThanAvailable;shouldCheckEdgeCase;shouldUpdateMaxObservedBytes" + ESC_EXPECTED_PROOFS: "14" + +jobs: + openjml-esc: + name: OpenJML ESC (deductive proof, static core) + runs-on: ubuntu-latest + # ESC can in principle hang on a hard proof obligation (per-attempt --timeout + # notwithstanding); the job-level timeout is the hard stop. + timeout-minutes: 30 + steps: + - uses: actions/checkout@v7 + - uses: actions/setup-java@v6 + with: + java-version: '21' + distribution: temurin + cache: maven + - name: Set up OpenJML (pinned + checksum-verified) + uses: ./.github/actions/setup-openjml + with: + version: ${{ env.OPENJML_VERSION }} + sha256: ${{ env.OPENJML_SHA256 }} + - name: Resolve compile classpath (error_prone_annotations, jspecify, checker-qual) + run: | + set -euo pipefail + mkdir -p target + mvn -B --no-transfer-progress -q dependency:build-classpath \ + -Dmdep.outputFile=target/compile-classpath.txt -DincludeScope=compile + - name: ESC — prove the static sequential core + # Exit codes: 0 = all proved, 6 = verification failure, 1-5 = tool/spec error. + # No pipes around the openjml call except tee under `set -o pipefail` — a bare + # `| tee` would swallow the exit code and turn every failure green. + run: | + set -euo pipefail + "$OPENJML_HOME/openjml" --esc --progress \ + --timeout 300 --esc-max-warnings 100 \ + --spec-math=bigint \ + --class-path "$(cat target/compile-classpath.txt)" \ + --specs-path src/main/jml \ + --method "$ESC_METHODS" \ + src/main/java/net/ladenthin/streambuffer/StreamBuffer.java \ + | tee esc-output.log + - name: Guard — exactly the expected number of proofs completed cleanly + # `openjml --method ` exits 0 even when the list matches NOTHING, so a green + # ESC step alone does not prove the scope ran. This counts the per-method + # "Completed proof of ... - no warnings" progress lines. + run: | + set -euo pipefail + completed="$(grep -c '^Completed proof of .* - no warnings' esc-output.log || true)" + echo "Completed clean proofs: $completed (expected: $ESC_EXPECTED_PROOFS)" + if [ "$completed" != "$ESC_EXPECTED_PROOFS" ]; then + echo "::error::ESC proof count mismatch: $completed != $ESC_EXPECTED_PROOFS — the --method selection drifted (rename? typo?) or a proof completed with warnings." + exit 1 + fi + { + echo "### OpenJML ESC" + echo "$completed/$ESC_EXPECTED_PROOFS methods of the static sequential core proved (OpenJML $OPENJML_VERSION, Z3)." + } >> "$GITHUB_STEP_SUMMARY" + + openjml-rac: + name: OpenJML RAC (contracts under the full test suite) + runs-on: ubuntu-latest + timeout-minutes: 30 + steps: + - uses: actions/checkout@v7 + - uses: actions/setup-java@v6 + with: + java-version: '21' + distribution: temurin + cache: maven + - name: Set up OpenJML (pinned + checksum-verified) + uses: ./.github/actions/setup-openjml + with: + version: ${{ env.OPENJML_VERSION }} + sha256: ${{ env.OPENJML_SHA256 }} + - name: Resolve compile classpath + run: | + set -euo pipefail + mkdir -p target + mvn -B --no-transfer-progress -q dependency:build-classpath \ + -Dmdep.outputFile=target/compile-classpath.txt -DincludeScope=compile + - name: Compile RAC-instrumented classes + # RAC checks CONTRACTS at runtime; it must not re-derive the overflow-freedom that ESC + # already proves, so both math modes are set to Java (runtime) semantics: + # --code-math=java — narrowing casts (e.g. the (byte) cast of an int 128..255 in + # write(int)) and any arithmetic wrap match the JVM instead of + # raising a spurious "cast out of range" RAC assertion. + # --spec-math=java — spec expressions evaluate as Java longs. (bigint would need a + # runtime class from OpenJML's patched JDK; the suite forks that + # exact JVM anyway — see the jml-rac profile — but Java math is + # sufficient for every contract here and keeps the bytecode simple.) + run: | + set -euo pipefail + mkdir -p target/rac-classes + "$OPENJML_HOME/openjml" --rac --rac-show-source=line \ + --code-math=java --spec-math=java \ + --class-path "$(cat target/compile-classpath.txt)" \ + --specs-path src/main/jml \ + -d target/rac-classes \ + src/main/java/net/ladenthin/streambuffer/StreamBuffer.java + - name: Guard — RAC instrumentation is actually present + # The whole job is meaningless if the instrumented classes silently contain no JML + # checks (e.g. specs path drift). RAC-generated code references org.jmlspecs.runtime; + # a plain javac class file does not. + run: | + set -euo pipefail + if ! grep -q "org/jmlspecs" target/rac-classes/net/ladenthin/streambuffer/StreamBuffer.class; then + echo "::error::target/rac-classes/.../StreamBuffer.class contains no org.jmlspecs references — RAC instrumentation did not happen." + exit 1 + fi + - name: Run the test suite against the RAC classes (violations throw) + # The jml-rac profile (pom.xml) points surefire's classesDirectory at + # target/rac-classes, forks OpenJML's own JVM (so the bigint runtime class resolves), + # puts jmlruntime.jar on the test classpath and sets -Dorg.jmlspecs.openjml.rac=exception + # so a violated contract fails the suite. + run: | + set -euo pipefail + mvn -B --no-transfer-progress -P jml-rac \ + "-Dopenjml.home=$OPENJML_HOME" \ + "-Dopenjml.jdk.java=$OPENJML_HOME/jdk/bin/java" \ + test + { + echo "### OpenJML RAC" + echo "Full JUnit suite passed against RAC-instrumented classes (every JML contract checked at runtime, violations thrown)." + } >> "$GITHUB_STEP_SUMMARY" + + # --------------------------------------------------------------------------------------------- + # JPF — exhaustive thread-interleaving model check of the concurrent read/write/close protocol. + # Scheduled/dispatch only (NOT per-PR): building jpf-core from source is minutes-long. This is + # the erschöpfende counterpart to the jcstress termination tests — see src/test/jpf/README.md. + # Java PathFinder requires JDK 11 to build and run; the harness is compiled at --release 8 and + # nothing here reaches the shipped jar. The jpf-core build is cached, keyed on the pinned commit + # plus the AtomicLong model patch (a completed jpf-core model — see the README). + # --------------------------------------------------------------------------------------------- + jpf-interleavings: + name: JPF exhaustive interleavings (blocking read/write/close) + runs-on: ubuntu-latest + if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch' + timeout-minutes: 30 + env: + # Pinned jpf-core commit (no upstream releases exist). Bump deliberately; re-validate the + # AtomicLong model patch on any bump (jpf-core has no release cadence to track). + JPF_SHA: "e61e396087983cde00b1e4a5f4b3dde39c0f9f7f" + steps: + - uses: actions/checkout@v7 + - uses: actions/setup-java@v6 + with: + # 21 builds the repo's Java-8 production classes (matching the shipped bytecode); + # 11 builds and runs jpf-core. + java-version: | + 11 + 21 + distribution: temurin + cache: maven + - name: Build Java-8 production classes + collect annotation jars (JDK 21) + run: | + set -euo pipefail + export JAVA_HOME="$JAVA_HOME_21_X64" + mvn -B --no-transfer-progress -DskipTests -Denforcer.skip=true compile + # Resolve the compile classpath (includes the optional checker-qual/jspecify/error-prone + # annotation jars the production bytecode references) and stage them under stable names. + mvn -B --no-transfer-progress -q dependency:build-classpath \ + -Dmdep.outputFile=target/compile-cp.txt -DincludeScope=compile + mkdir -p src/test/jpf/lib + tr ':;' '\n\n' < target/compile-cp.txt | while read -r jar; do + case "$jar" in + *checker-qual*) cp "$jar" src/test/jpf/lib/checker-qual.jar ;; + *jspecify*) cp "$jar" src/test/jpf/lib/jspecify.jar ;; + *error_prone_annotations*) cp "$jar" src/test/jpf/lib/error-prone-annotations.jar ;; + esac + done + test -f src/test/jpf/lib/checker-qual.jar + test -f src/test/jpf/lib/jspecify.jar + test -f src/test/jpf/lib/error-prone-annotations.jar + - name: Cache jpf-core build + id: jpf-cache + uses: actions/cache@v6 + with: + path: jpf-core/build + key: jpf-core-${{ env.JPF_SHA }}-atomiclong-${{ hashFiles('src/test/jpf/jpf-model/java/util/concurrent/atomic/AtomicLong.java') }} + - name: Build jpf-core with the AtomicLong model patch (JDK 11) + if: steps.jpf-cache.outputs.cache-hit != 'true' + run: | + set -euo pipefail + export JAVA_HOME="$JAVA_HOME_11_X64" + git clone https://github.com/javapathfinder/jpf-core.git jpf-core + git -C jpf-core checkout "$JPF_SHA" + # Patch jpf-core's incomplete AtomicLong model (see src/test/jpf/README.md). + cp src/test/jpf/jpf-model/java/util/concurrent/atomic/AtomicLong.java \ + jpf-core/src/classes/modules/java.base/java/util/concurrent/atomic/AtomicLong.java + (cd jpf-core && ./gradlew --no-daemon buildJars -x test) + - name: Model-check the harness (JDK 11) + # RunJPF exits 0 even when it reports "error #N", so the result is gated on the log below, + # never on the exit code. + run: | + set -euo pipefail + export JAVA_HOME="$JAVA_HOME_11_X64" + cd src/test/jpf + rm -rf out streambuffer-classes && mkdir -p out streambuffer-classes + cp -r "$GITHUB_WORKSPACE/target/classes/net" streambuffer-classes/ + "$JAVA_HOME/bin/javac" --release 8 -cp streambuffer-classes -d out \ + net/ladenthin/streambuffer/jpf/JpfStreamBufferHarness.java + "$JAVA_HOME/bin/java" -jar "$GITHUB_WORKSPACE/jpf-core/build/RunJPF.jar" StreamBuffer.jpf \ + | tee jpf-output.log + - name: Gate on the JPF result + run: | + set -euo pipefail + log=src/test/jpf/jpf-output.log + if grep -qE '^error #' "$log"; then + echo "::error::JPF reported an interleaving defect (see log)." + exit 1 + fi + if ! grep -q 'no errors detected' "$log"; then + echo "::error::JPF did not finish cleanly ('no errors detected' absent) — treat as failure." + exit 1 + fi + states="$(grep -oE 'new=[0-9]+' "$log" | head -1 || echo 'new=?')" + { + echo "### JPF exhaustive interleavings" + echo "No errors detected over all enumerated schedules ($states states) — no deadlock, no uncaught exception, byte fidelity held." + } >> "$GITHUB_STEP_SUMMARY" + - uses: actions/upload-artifact@v7 + if: always() + with: + name: jpf-output + path: src/test/jpf/jpf-output.log + if-no-files-found: ignore diff --git a/.gitignore b/.gitignore index 8915662..b4f1f36 100644 --- a/.gitignore +++ b/.gitignore @@ -25,6 +25,16 @@ # virtual machine crash logs, see http://www.java.com/en/download/help/error_hotspot.xml hs_err_pid* +# heap dumps (HeapDumpOnOutOfMemoryError, surefire -Xmx cap, ad-hoc RAC/test forks) +*.hprof + +# JPF interleaving check — build outputs assembled next to src/test/jpf/StreamBuffer.jpf at run +# time, plus a locally cloned jpf-core. None of it is checked in. +/jpf-core/ +src/test/jpf/out/ +src/test/jpf/streambuffer-classes/ +src/test/jpf/lib/ +src/test/jpf/jpf-output.log /target/ /bin/ diff --git a/CLAUDE.md b/CLAUDE.md index 4b6361d..60d1828 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -59,6 +59,85 @@ mvn -Pvmlens test ``` The `vmlens` profile pulls in `com.vmlens:api` and runs the `vmlens-maven-plugin` during the `test` phase. Tests using `com.vmlens.api.AllInterleavings` are then driven through every possible thread interleaving. The profile is off by default — vmlens overhead is too high for every build. +## Formal Verification + +Two layers, run in a **separate** CI pipeline (`.github/workflows/formal-verification.yml` — +deliberately not part of the synchronous Publish pipeline and never a required check): + +1. **OpenJML ESC** (deductive proof, Z3): the 14 static sequential-core methods (2 validators + + 12 pure helpers) are proven against full functional contracts. +2. **OpenJML RAC**: the existing JUnit suite runs against RAC-instrumented classes + (violations throw), checking the static contracts plus the instance/stream-adapter contracts. +3. **JPF interleavings** (`src/test/jpf/`, scheduled/dispatch CI job `jpf-interleavings`): Java + PathFinder exhaustively model-checks the concurrent read/write/close protocol. Requires JDK 11; + builds jpf-core from a pinned commit with a one-file `AtomicLong` model patch; the harness is + compiled at `--release 8` and run under JPF. Local recipe (Docker+JDK 11) in + `src/test/jpf/README.md`. Never touches the shipped jar. + +The `@GuardedBy("bufferLock")` lock discipline is gated separately by Error Prone in the default +build. The Checker Framework Lock Checker was evaluated as a further layer and deferred — see +TODO.md "Formal verification". + +**Local commands** (OpenJML 21.0.27 — a native Windows build exists since this release; +`` = unzipped release dir, `` = output of +`mvn dependency:build-classpath -Dmdep.outputFile=... -DincludeScope=compile`): + +```bash +# ESC — the --method list is the verified scope; it is mirrored in ESC_METHODS in the workflow +/openjml --esc --progress --timeout 300 --spec-math=bigint \ + --class-path "" --specs-path src/main/jml \ + --method "" \ + src/main/java/net/ladenthin/streambuffer/StreamBuffer.java + +# RAC — compile instrumented classes (Java math both sides), then run the suite against them. +# The suite MUST fork OpenJML's own JVM (it carries the org.jmlspecs bigint runtime class that +# the bundled JDK specs reference); the profile does this via -Dopenjml.jdk.java. +/openjml --rac --code-math=java --spec-math=java --class-path "" \ + --specs-path src/main/jml -d target/rac-classes \ + src/main/java/net/ladenthin/streambuffer/StreamBuffer.java +mvn -P jml-rac -Dopenjml.home= -Dopenjml.jdk.java=/jdk/bin/java test +``` + +**Rules that keep this sound — read before touching `StreamBuffer.java` or the specs:** + +- Specs live ONLY in `src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml`. A `.jml` file + **replaces** all class-level JML in the `.java` (which therefore stays JML-free), and OpenJML + errors on any signature mismatch — so every signature change in `StreamBuffer.java` must be + mirrored there, and the verification workflow catches drift. +- The 12 pure helpers are `static` **because instance-method proof obligations are undecidable + for Z3 in this class** (the non-static inner stream classes poison the receiver context — + measured, not theorized). New pure helpers must be static or they cannot join the ESC scope. +- The ESC scope is guarded by an exact proof COUNT in the workflow (`ESC_EXPECTED_PROOFS`); + adding/removing a method from the scope means updating `ESC_METHODS` + the count together. +- `validateOffsetAndLengthToWrite` and `calculateResultingChunks` are marked `code_java_math` + in the spec file: both deliberately rely on wrap semantics (overflow-guard idiom; wrap-back + at the ceiling-division boundary). Everything else is proven overflow-free under safe math. +- The exception-message builder `newInvalidOffsetOrLengthToWriteException` carries an ASSUMED + (unproven) contract — string concatenation defeats the SMT encoding. Do not inline it back. +- NO class invariants in the `.jml`: OpenJML 21.0.27's RAC crashes on invariants combined with + non-static inner classes ("no enclosing instance" AssertionError). Re-test on upgrades. +- `//@ nullable_by_default` at the class head is load-bearing for RAC: without it JML's + non-null-by-default inserts an implicit non-null precondition on every reference parameter, so + the null-argument tests hit `JmlAssertionError.Precondition` instead of the specified NPE. + Non-null intent is still enforced where it matters via explicit `requires ... != null`. +- `validateOffsetAndLengthToWrite` uses a manual `if (b == null) throw new NPE(...)` rather than + `Objects.requireNonNull`: under `nullable_by_default` the bundled `Objects.requireNonNull` + contract leaves ESC an unprovable ExceptionList goal. Behaviour is identical. +- The stream logic lives in `private` OUTER methods (`availableClamped`, `readSingleByte`, + `readIntoArray`, `writeSingleByte`, `writeFromArray`); the inner `SBInputStream`/ + `SBOutputStream` are pure delegating shells. Required: OpenJML RAC miscompiles outer-field + access from inside non-static inner classes (`NoSuchFieldError` at runtime). Do not move field + access back into the inner classes. +- RAC forks OpenJML's OWN JVM (`-Dopenjml.jdk.java`), because the bundled JDK library specs pull + in `org.jmlspecs.lang.internal.bigint`, a class present only in OpenJML's patched JDK image. + The setup action also patches `jdk/release` to add the `JAVA_VERSION` key surefire needs to + fork that JVM. +- Two bundled OpenJML JDK specs are known-broken and deleted at install time by + `.github/actions/setup-openjml` (`ArrayDeque.jml`: undeclared `containsNull`; + `atomic/AtomicLong.jml`: RAC reads the private field `value` → `IllegalAccessError`). +- RAC classes are class-file 65 and live only under `target/rac-classes` — they never enter the + shipped jar, so the Java 8 bytecode floor is unaffected. + ## Architecture `StreamBuffer` is a single-class Java library (`net.ladenthin.streambuffer`) that connects an `OutputStream` and `InputStream` through a dynamic FIFO queue — solving the fixed-buffer and cross-thread-deadlock limitations of Java's `PipedInputStream`/`PipedOutputStream`. diff --git a/README.md b/README.md index 6cb577e..3820327 100644 --- a/README.md +++ b/README.md @@ -411,6 +411,13 @@ Test coverage includes: - Thread interruption during blocked reads (wraps `InterruptedException` in `IOException`) - Concurrent read/write stress tests - Parallel close without deadlock +- Deadlock-freedom of every blocking entry point, stress-checked with jcstress `Mode.Termination` + (`-Pjcstress`): a thread parked in `read()`, in the second wait phase of `read(byte[], off, len)`, + or in `waitForAtLeast(...)` is always released by both a concurrent `write` and a concurrent + `close` +- Exhaustive thread-interleaving model check of the read/write/close protocol with Java PathFinder + (`src/test/jpf/`, scheduled CI job + local Docker recipe) — the erschöpfende counterpart to the + jcstress stress tests - Signal/slot notification via external semaphores on write and all close paths - `removeSignal(null)` returning `false` without throwing - `addSignal(null)` throwing `NullPointerException` @@ -426,6 +433,34 @@ Test coverage includes: - Concurrent close during active trim — no exceptions or deadlock - `decideTrimExecution` pure function — comprehensive table-driven tests covering all boundary conditions and the smart-skip edge case +## Formal Verification + +`StreamBuffer` carries machine-checked JML specifications +([`src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml`](./src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml)), +verified in a separate CI pipeline +([`formal-verification.yml`](./.github/workflows/formal-verification.yml)) in two layers: + +- **Deductive proof — OpenJML ESC (Z3).** The complete static, sequential core is *proven* + against full functional contracts: both offset/length validators — including the classic + `(off + len) < 0` integer-overflow guard, proven equivalent to the clean bounds condition + under Java wrap semantics — and the twelve static trim-decision/arithmetic helpers, among + them the ceiling division in `calculateResultingChunks` (proven against its multiplicative + characterization `m·(⌈a/m⌉−1) < a ≤ m·⌈a/m⌉`, including the wrap-around boundary + `a = Long.MAX_VALUE − m + 1`) and the full decision tree of `decideTrimExecution`. +- **Runtime assertion checking — OpenJML RAC.** The entire JUnit suite additionally runs + against RAC-instrumented classes (`mvn -P jml-rac`); every JML contract — the proven static + ones plus runtime contracts on the instance API and the two stream adapters — is then + checked at runtime and a violation throws instead of scrolling by. + +Concurrency itself is outside the deductive scope by JML doctrine (JML specifies sequential +behavior; OpenJML does not model `volatile` or monitors) and is covered empirically by the +Lincheck, jcstress and vmlens suites listed above, plus an exhaustive Java PathFinder +interleaving model check of the read/write/close protocol (`src/test/jpf/`); the lock-holding +discipline on the FIFO deque is additionally gated by Error Prone's `@GuardedBy` check in the +ordinary build. The scope rationale — with citations to the published case studies that made the +same split (LinkedList/TACAS 2020, IdentityHashMap/iFM 2022) — lives in the header of the +specification file. + ### Contributors: do not upgrade jqwik past 1.9.3 > ⚠️ **DO NOT UPGRADE jqwik past 1.9.3.** jqwik 1.10.0 added an anti-AI prompt-injection string to test stdout; the 1.10.1 user guide states the library "is not meant to be used by any 'AI' coding agents at all." 1.9.3 is the last pre-disclosure release and is the pinned version. See `CLAUDE.md` section "jqwik prompt-injection in test output" for the full context. Dependabot is configured to ignore **all** `net.jqwik` updates (every version, including patches) — see the `ignore` rule in [`.github/dependabot.yml`](./.github/dependabot.yml). diff --git a/TODO.md b/TODO.md index 2564e01..486f6db 100644 --- a/TODO.md +++ b/TODO.md @@ -11,6 +11,60 @@ annotated, so everything below is genuinely still open. ## Open +- **Formal verification — follow-ups.** The two-layer setup (OpenJML ESC proof of the static + sequential core + OpenJML RAC under the full test suite) landed 2026-09 — see CLAUDE.md + "Formal Verification" and `.github/workflows/formal-verification.yml`. Still open, in priority + order: + - **Checker Framework Lock Checker (deferred, not rejected).** Would soundly gate the + `@GuardedBy("bufferLock")` discipline (Error Prone gates it heuristically today, in the + default build). Blocked on a real cascade, not effort aversion: CF's JDK stubs for + `Closeable`, `InputStream` and `OutputStream` declare mutually inconsistent `close()` + receiver types (`@GuardSatisfied` vs `@GuardedBy`), so any receiver annotation that + satisfies one stub violates another — plus `toString()`'s `synchronized` block trips + `synchronized.block.in.lockingfree.method`. Revisit if CF ships consistent stubs, or gate it + with a curated `-AskipDefs`/stub override. + - ~~JPF interleaving harness~~ **DONE (2026-09).** Java PathFinder now exhaustively model-checks + the concurrent read/write/close protocol over all enumerated interleavings — the erschöpfende + counterpart to the jcstress stress tests. Lives in `src/test/jpf/` (harness, `.jpf` config, and + a completed jpf-core `AtomicLong` model patch); wired as the scheduled/dispatch + `jpf-interleavings` job in `formal-verification.yml`; locally reproducible via the Docker+JDK 11 + recipe in `src/test/jpf/README.md`. Confirmed: `no errors detected`, ~14k states, with a + negative-control proving the byte-fidelity oracle is non-vacuous. jpf-core is pinned to commit + `e61e396`. Open sub-item: the AtomicLong model completion is a genuine jpf-core deficiency worth + reporting upstream (its native peer already implements the methods the stub model never + declared). Possible extension: a second harness for the array-read / `waitForAtLeast` blocking + paths (jcstress already covers those; JPF would make them exhaustive too). + - **Report the three OpenJML defects upstream** (all reproduced on 21.0.27, all documented in + the spec-file header / setup-openjml action): bundled `ArrayDeque.jml` references undeclared + `containsNull`; bundled `atomic/AtomicLong.jml` makes RAC emit an access to the private field + `AtomicLong.value` (`IllegalAccessError` at test runtime); RAC crashes with a javac `Lower` + AssertionError ("no enclosing instance") when a class with non-static inner classes declares + any instance invariant. + - **Deeper ESC — instance-method / trim() functional correctness (parked, revisit).** Today + ESC proves the 14 static helpers; the instance methods and trim() are RAC-only. A full + functional proof (e.g. a ghost model sequence for the deque with the invariant + `availableBytes == sum of buffered byte[] lengths`, preserved across read/write/trim) is the + "TimSort-level" target. Currently blocked two ways: OpenJML ESC returns solver "unknown" on + instance methods of this class (the non-static inner stream classes poison the receiver + context), and modelling the deque as a ghost `\seq` is large (the LinkedList/KeY study was + ~7 person-months for 328 LoC). Not gold-plating in principle — just expensive today; worth a + re-scoping spike to see whether a *partial* invariant (e.g. non-negativity + position bounds + proven on a static extraction of the read/write inner loops) is reachable more cheaply. + - **On every OpenJML upgrade:** re-try dropping the two spec-file deletions in + `.github/actions/setup-openjml/action.yml` (bump the cache-key fixup suffix), and re-try the + four class invariants documented in the `.jml` header. + - **Evaluated and rejected 2026-09** (do not re-open without new facts) — deductive/model-checking + alternatives beyond OpenJML: **KeY 3.0.0** — could + re-prove the same static scope with archived `.proof` files, but proof replay is + version-brittle and adds maintenance without widening the scope (generics unsupported, no + concurrency, no `Deque`/`java.util.concurrent` stubs); **VerCors 2.4.0** — only candidate + with concurrent-Java separation logic, but models locks as single-entrant, has no + volatile/JMM semantics and near-empty JDK stubs: verifying StreamBuffer means re-modeling it, + a research project; **JBMC (cbmc 6.11)** — its JDK-8 model library has no + `ArrayDeque`/`java.util.concurrent`, thread support officially limited; would only duplicate + the ESC scope, bounded; **Infer/RacerD v1.3.0** — explicitly "avoids reasoning about weak + memory and Java's volatile keyword", i.e. blind to exactly this class's design. + - **jqwik pin policy** — see [`../workspace/policies/jqwik-prompt-injection.md`](../workspace/policies/jqwik-prompt-injection.md). `jqwik.version ≤ 1.9.3` is mandatory. A standing constraint, not a task: it has to be re-checked whenever the dependency is bumped. - **`@VisibleForTesting` audit.** `StreamBuffer` has **15** package-private methods that exist so tests can reach them (`decideTrimExecution`, `shouldTrim`, `clampToMaxInt`, `decrementAvailableBytesBudget`, `calculateResultingChunks`, the five `shouldSkipTrim*`/`should*` predicates, `isAvailableBytesPositive`, `isMaxAllocSizeLessThanAvailable`, `shouldCheckEdgeCase`, `recordReadStatistics`, `shouldUpdateMaxObservedBytes`, `updateMaxObservedBytesIfNeeded`). None is annotated, and Guava is not a dependency here — so closing this means deciding between (a) adding a project-local marker annotation, which puts a new public type into the API surface of a deliberately one-class library, and (b) recording that the convention does not apply to this repo. Decide and act; do not leave it as a permanently open audit. diff --git a/pom.xml b/pom.xml index 7279626..77b519c 100644 --- a/pom.xml +++ b/pom.xml @@ -765,6 +765,99 @@ SPDX-License-Identifier: Apache-2.0 + + + jml-rac + + + ${openjml.home}/jdk/bin/java + + + + + org.apache.maven.plugins + maven-surefire-plugin + + ${openjml.jdk.java} + + -Xmx2g + ${project.build.directory}/rac-classes + + ${openjml.home}/jmlruntime.jar + + + exception + + + + **/vmlens/*.java + **/StreamBufferArchitectureTest.java + **/StreamBufferLincheckTest.java + + + + + + jcstress diff --git a/spotbugs-exclude.xml b/spotbugs-exclude.xml index c83a28f..8d71502 100644 --- a/spotbugs-exclude.xml +++ b/spotbugs-exclude.xml @@ -39,6 +39,62 @@ SPDX-License-Identifier: Apache-2.0 + + + + + + + + + + + + + + + + + + + + + + + + + + + +# JPF interleaving model-check + +Exhaustive thread-interleaving verification of `StreamBuffer`'s concurrent read/write/close protocol +with [Java PathFinder](https://github.com/javapathfinder/jpf-core). Where the jcstress +`Mode.Termination` tests (`-Pjcstress`) *stress* the blocking paths under hardware-driven schedules, +JPF *exhaustively enumerates* the interleavings of a small harness — a strictly stronger guarantee +for the schedules it covers. It is the erschöpfende ("exhaustive") counterpart flagged in +[`../../../TODO.md`](../../../TODO.md). + +This directory is **not** part of the Maven build (Maven compiles only `src/test/java`). The harness +is compiled with `javac --release 8` and executed by JPF on **JDK 11** (jpf-core's required +runtime). Nothing here reaches the shipped jar. + +## What is verified + +The harness (`JpfStreamBufferHarness.java`) runs one writer (writes two bytes, then `close()`) and +one reader (`read()` until EOF) over one real `StreamBuffer`, and JPF explores every interleaving, +reporting: + +- **deadlocks** — a thread parked forever on the semaphore (lost wakeup), +- **uncaught exceptions** — any thread dying unexpectedly, +- **byte fidelity** — the reader must receive exactly the two bytes, in order, then EOF (an explicit + `throw`, validated with a negative control so it cannot be vacuous). + +Last confirmed run: **no errors detected**, ~14,000 states, maxDepth 130. + +## Files + +| File | Role | +|---|---| +| `net/ladenthin/streambuffer/jpf/JpfStreamBufferHarness.java` | the model-checked harness (the oracle) | +| `StreamBuffer.jpf` | JPF run configuration (target + classpath) | +| `jpf-model/java/util/concurrent/atomic/AtomicLong.java` | a completed `AtomicLong` model that patches a jpf-core stub (see below) | + +## Why the AtomicLong patch + +jpf-core (pinned commit `e61e396087983cde00b1e4a5f4b3dde39c0f9f7f`) ships a 2014-era model class for +`java.util.concurrent.atomic.AtomicLong` that declares only legacy `attempt*` helpers, so a class +under model check that calls `addAndGet` (as `StreamBuffer` does for its statistics counters) dies +with `NoSuchMethodError` — even though jpf-core's native peer already implements those methods (they +appear as "orphan NativePeer method" warnings for lack of a matching model declaration). +`jpf-model/.../AtomicLong.java` is jpf-core's model class with the modern surface added; the build +copies it over the stub before compiling jpf-core. This is the only change to jpf-core, and it is a +genuine upstream deficiency worth reporting. + +## Run it locally (Docker, no JDK 11 needed on the host) + +From the repository root, with `target/classes` already built (`mvn -DskipTests compile`): + +```bash +SB="$(pwd)" # streambuffer checkout +WORK="$(mktemp -d)" +git clone https://github.com/javapathfinder/jpf-core.git "$WORK/jpf-core" +git -C "$WORK/jpf-core" checkout e61e396087983cde00b1e4a5f4b3dde39c0f9f7f +# apply the AtomicLong model patch +cp "$SB/src/test/jpf/jpf-model/java/util/concurrent/atomic/AtomicLong.java" \ + "$WORK/jpf-core/src/classes/modules/java.base/java/util/concurrent/atomic/AtomicLong.java" + +docker run --rm -v "$WORK/jpf-core:/jpf" -v "$SB:/sb" -w /jpf eclipse-temurin:11-jdk bash -lc ' + apt-get update -qq && apt-get install -y -qq git >/dev/null + git config --global --add safe.directory /jpf + sed -i "s/\r$//" gradlew # tolerate a Windows (CRLF) checkout + ./gradlew --no-daemon buildJars -x test + + cd /sb/src/test/jpf + rm -rf out streambuffer-classes lib && mkdir -p out streambuffer-classes lib + cp -r /sb/target/classes/net streambuffer-classes/ + cp "$(find ~/.m2 /root/.m2 -name "checker-qual-*.jar" 2>/dev/null | head -1)" lib/checker-qual.jar + cp "$(find ~/.m2 /root/.m2 -name "jspecify-*.jar" 2>/dev/null | head -1)" lib/jspecify.jar + cp "$(find ~/.m2 /root/.m2 -name "error_prone_annotations-*.jar" 2>/dev/null | head -1)" lib/error-prone-annotations.jar + javac --release 8 -cp streambuffer-classes -d out net/ladenthin/streambuffer/jpf/JpfStreamBufferHarness.java + java -jar /jpf/build/RunJPF.jar StreamBuffer.jpf +' +``` + +The annotation jars must be present under an `.m2` the container can see; the CI job resolves them +with `mvn dependency:copy-dependencies` instead. Expected tail: `no errors detected`. diff --git a/src/test/jpf/StreamBuffer.jpf b/src/test/jpf/StreamBuffer.jpf new file mode 100644 index 0000000..294bc1b --- /dev/null +++ b/src/test/jpf/StreamBuffer.jpf @@ -0,0 +1,22 @@ +# SPDX-FileCopyrightText: 2014-2026 Bernard Ladenthin +# +# SPDX-License-Identifier: Apache-2.0 +# +# JPF run configuration for the StreamBuffer concurrency harness. Consumed by RunJPF.jar in the +# jpf-interleavings CI job and by the local Docker recipe in README.md. The sibling directories it +# references (out/, streambuffer-classes/, lib/) are assembled next to this file at run time — they +# are build outputs, not checked in. +target = net.ladenthin.streambuffer.jpf.JpfStreamBufferHarness + +# classpath (all relative to this .jpf's directory): +# out/ - the harness, compiled with `javac --release 8` +# streambuffer-classes - the Java-8 production bytecode (a copy of target/classes/net) +# lib/*.jar - the annotation types the production bytecode references +# (checker-qual/jspecify/error-prone; RUNTIME-retained, so JPF resolves +# them during class loading — copied to stable unversioned names) +classpath = ${config_path}/out;${config_path}/streambuffer-classes;${config_path}/lib/checker-qual.jar;${config_path}/lib/jspecify.jar;${config_path}/lib/error-prone-annotations.jar + +# The default JPF search enumerates every relevant thread interleaving and reports deadlocks, +# uncaught exceptions, and assertion violations. The harness oracle uses explicit throws (not Java +# `assert`, which JPF does not reliably enable for the SUT), so it is caught regardless of this flag. +vm.enable_assertions = true diff --git a/src/test/jpf/jpf-model/java/util/concurrent/atomic/AtomicLong.java b/src/test/jpf/jpf-model/java/util/concurrent/atomic/AtomicLong.java new file mode 100644 index 0000000..dd33bf5 --- /dev/null +++ b/src/test/jpf/jpf-model/java/util/concurrent/atomic/AtomicLong.java @@ -0,0 +1,132 @@ +/* + * SPDX-FileCopyrightText: 2014 United States Government, as represented by the Administrator of the National Aeronautics and Space Administration + * SPDX-FileCopyrightText: 2026 Bernard Ladenthin + * + * SPDX-License-Identifier: Apache-2.0 + * + * Derived from the jpf-core model class java/util/concurrent/atomic/AtomicLong.java + * (github.com/javapathfinder/jpf-core): the modern addAndGet/incrementAndGet/getAndAdd surface was + * added so a class under model check can call it (the upstream stub declared only legacy helpers). + * + * Copyright (C) 2014, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * Apache License, Version 2.0 (the "License"); you may not use this file except + * in compliance with the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package java.util.concurrent.atomic; + +/** + * MJI model class for java.util.concurrent.atomic.AtomicLong. + * + *

The stock jpf-core model only declared the legacy {@code attempt*} helpers, so a class under + * model check that called the modern {@code addAndGet}/{@code incrementAndGet}/{@code getAndAdd} + * surface died with {@code NoSuchMethodError} — even though the companion native peer + * ({@code JPF_java_util_concurrent_atomic_AtomicLong}) already implemented every one of those as an + * atomic MJI method (they showed up as "orphan NativePeer method" warnings for lack of a matching + * model declaration). This model declares that surface so the peer binds; the plain-Java bodies are + * the fallback if the peer is ever absent. Backing field name {@code value} matches the peer's + * {@code env.getLongField(objRef, "value")} accessors. Not synchronized on purpose: atomicity comes + * from the peer's single-MJI-call execution, mirroring the real CAS-based class. + */ +public class AtomicLong implements java.io.Serializable { + + private static final long serialVersionUID = 1927816293512124184L; + + private long value; + + public AtomicLong (long initialValue) { + value = initialValue; + } + + public AtomicLong () { + } + + public final long get () { + return value; + } + + public final void set (long newValue) { + value = newValue; + } + + public final void lazySet (long newValue) { + value = newValue; + } + + public final long getAndSet (long newValue) { + long old = value; + value = newValue; + return old; + } + + public final boolean compareAndSet (long expect, long update) { + if (value == expect) { + value = update; + return true; + } + return false; + } + + public final boolean weakCompareAndSet (long expect, long update) { + return compareAndSet(expect, update); + } + + public final long getAndIncrement () { + return value++; + } + + public final long getAndDecrement () { + return value--; + } + + public final long getAndAdd (long delta) { + long old = value; + value += delta; + return old; + } + + public final long incrementAndGet () { + return ++value; + } + + public final long decrementAndGet () { + return --value; + } + + public final long addAndGet (long delta) { + value += delta; + return value; + } + + public final int intValue () { + return (int) value; + } + + public final long longValue () { + return value; + } + + public final float floatValue () { + return (float) value; + } + + public final double doubleValue () { + return (double) value; + } + + @Override + public String toString () { + return Long.toString(value); + } +} diff --git a/src/test/jpf/net/ladenthin/streambuffer/jpf/JpfStreamBufferHarness.java b/src/test/jpf/net/ladenthin/streambuffer/jpf/JpfStreamBufferHarness.java new file mode 100644 index 0000000..a5a75f7 --- /dev/null +++ b/src/test/jpf/net/ladenthin/streambuffer/jpf/JpfStreamBufferHarness.java @@ -0,0 +1,78 @@ +// SPDX-FileCopyrightText: 2014-2026 Bernard Ladenthin +// +// SPDX-License-Identifier: Apache-2.0 +package net.ladenthin.streambuffer.jpf; + +import java.io.IOException; +import java.io.InputStream; +import java.io.OutputStream; +import net.ladenthin.streambuffer.StreamBuffer; + +/** + * Java PathFinder harness: exhaustively model-checks the concurrent read/write/close protocol of + * {@link StreamBuffer} over ALL thread interleavings JPF can enumerate — a stronger guarantee than + * the jcstress termination tests (which sample hardware-driven schedules). This is deliberately NOT + * a JUnit test: it is compiled with {@code javac --release 8} and run under JPF (JDK 11), never by + * Maven surefire; see {@code src/test/jpf/README.md} and the {@code jpf-interleavings} job in + * {@code .github/workflows/formal-verification.yml}. + * + *

Deliberately tiny (two bytes, two worker threads) so the state space stays tractable — the + * last confirmed run explored ~14k states, maxDepth 130. JPF flags three failure classes: deadlocks + * (a thread parked forever on the semaphore), uncaught exceptions, and the explicit oracle throws + * below (byte fidelity). Keep the payload minimal; the state space explodes fast. + */ +public final class JpfStreamBufferHarness { + + private JpfStreamBufferHarness() {} + + public static void main(String[] args) throws Exception { + final StreamBuffer sb = new StreamBuffer(); + final OutputStream os = sb.getOutputStream(); + final InputStream is = sb.getInputStream(); + + final byte[] payload = {0x41, 0x42}; + + final Thread writer = new Thread(() -> { + try { + os.write(payload[0]); + os.write(payload[1]); + sb.close(); + } catch (IOException e) { + throw new AssertionError("writer must not fail", e); + } + }); + + final byte[] got = new byte[payload.length]; + final int[] count = {0}; + + final Thread reader = new Thread(() -> { + try { + int c; + while ((c = is.read()) != -1) { + if (count[0] < got.length) { + got[count[0]] = (byte) c; + } + count[0]++; + } + } catch (IOException e) { + throw new AssertionError("reader must not fail", e); + } + }); + + writer.start(); + reader.start(); + writer.join(); + reader.join(); + + // Every interleaving must deliver exactly the two written bytes, in order, then EOF. + // Explicit throws, NOT `assert`: JPF does not reliably enable Java assertions for the SUT + // (a disabled assert would make this oracle vacuous — verified with a negative control), + // whereas a thrown Throwable is always caught by JPF's NoUncaughtExceptionsProperty. + if (count[0] != payload.length) { + throw new AssertionError("read " + count[0] + " bytes, expected " + payload.length); + } + if (got[0] != payload[0] || got[1] != payload[1]) { + throw new AssertionError("byte order/content corrupted"); + } + } +} From 702b945de35f505e3175d205e068c432d9b5426e Mon Sep 17 00:00:00 2001 From: Bernard Ladenthin Date: Sun, 13 Sep 2026 01:41:26 +0200 Subject: [PATCH 2/2] fix(ci): disable JUnit @Timeout enforcement in the OpenJML RAC run RAC instrumentation slows every method by an unbounded factor, so StreamBufferTest's class-level @Timeout(20s) is not a meaningful gate under it: the large-allocation test trim_respectsMaxAllocationSize_splitsLargeBuffer passed well under 20s uninstrumented but timed out on the 2-core CI runner while RAC-instrumented (276/277 passed, the one error was a timeout, not a contract violation). Set junit.jupiter.execution.timeout.mode=disabled for the jml-rac profile only; correctness and contract checking are unaffected, only the timing gate is lifted while instrumented. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01TU5B8DDtDwKSS6ohSfoz2Y --- pom.xml | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/pom.xml b/pom.xml index 77b519c..10734a2 100644 --- a/pom.xml +++ b/pom.xml @@ -823,6 +823,17 @@ SPDX-License-Identifier: Apache-2.0 exception + + disabled