Bug-hunt fixes: safeWrite, trim, write/close race, statistics

.github/workflows/formal-verification.yml

@@ -274,39 +274,43 @@ jobs:
           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.
+      - name: Model-check the harnesses (JDK 11)
+        # RunJPF exits 0 even when it reports "error #N", so the result is gated on the logs below,
+        # never on the exit code. Two harnesses: StreamBuffer.jpf (writer that also closes, reader) and
+        # WriteClose.jpf (writer, closer and reader in three threads -- the order of write and close,
+        # bug hunt F149, which the first one cannot see).
         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
+            net/ladenthin/streambuffer/jpf/JpfStreamBufferHarness.java \
+            net/ladenthin/streambuffer/jpf/JpfWriteCloseHarness.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
+          "$JAVA_HOME/bin/java" -jar "$GITHUB_WORKSPACE/jpf-core/build/RunJPF.jar" WriteClose.jpf \
+            | tee jpf-output-write-close.log
+      - name: Gate on the JPF results
         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"
+          echo "### JPF exhaustive interleavings" >> "$GITHUB_STEP_SUMMARY"
+          for log in src/test/jpf/jpf-output.log src/test/jpf/jpf-output-write-close.log; do
+            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 in $log) — treat as failure."
+              exit 1
+            fi
+            states="$(grep -oE 'new=[0-9]+' "$log" | head -1 || echo 'new=?')"
+            echo "$(basename "$log"): no errors detected over all enumerated schedules ($states states) — no deadlock, no uncaught exception, byte fidelity held." >> "$GITHUB_STEP_SUMMARY"
+          done
       - uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9 # v7
         if: always()
         with:
           name: jpf-output
-          path: src/test/jpf/jpf-output.log
+          path: src/test/jpf/jpf-output*.log
           if-no-files-found: ignore

.gitignore

@@ -34,7 +34,7 @@ hs_err_pid*
 src/test/jpf/out/
 src/test/jpf/streambuffer-classes/
 src/test/jpf/lib/
-src/test/jpf/jpf-output.log
+src/test/jpf/jpf-output*.log
 
 /target/
 /bin/

BUGHUNT-CHECKED.md

@@ -0,0 +1,22 @@
+
+# Bug-Hunt: geprüfte Stellen — streambuffer
+
+Jede Zeile ist eine gründlich gelesene Produktionsklasse: `Pfad` · Blob-Hash der Datei beim Prüfen · Datum ·
+Ergebnis — Notiz. Eine Klasse gilt als erledigt, solange `git rev-parse --short HEAD:<Pfad>` noch denselben
+Blob-Hash liefert; hat sich die Datei seitdem geändert, wird sie erneut geprüft und die Zeile ersetzt.
+Ergebnisse: `kein Fund`, `widerlegt` (Verdacht geprüft, Code korrekt), `unsicher` (offen, siehe
+[`BUGHUNT-FOUND.md`](BUGHUNT-FOUND.md)), `Fund Fnn` (Fehler gefunden und dort beschrieben).
+
+## Geprüft
+
+- `src/main/java/net/ladenthin/streambuffer/package-info.java` · `e30da5b` · 2026-10-17 · kein Fund — gelesen, keine Notiz
+- `src/main/java/net/ladenthin/streambuffer/StreamBuffer.java` · `5e0f51d` · 2026-10-17 · Fund F02 — streambuffer: `safeWrite` wird von gleichzeitigem `write(int)` ausgehebelt
+- `src/main/java/net/ladenthin/streambuffer/StreamBuffer.java` (Schnittstelle SBInputStream.read(byte[],int,int) ↔ waitForAtLeast) · `5e0f51d` · 2026-10-17 · kein Fund — Nach dem ersten Byte wartet `readIntoArray` über `waitForAtLeast(len-1)`, also bis zur vollen Länge oder bis zum Schließen, statt nach den verfügbaren Bytes zurückzukehren. Das ist im README (Zeile 328: „To avoid blocking, only read as many bytes as available() reports“) als Verhalten festgelegt und entspricht der Standardimplementierung von `InputStream.read(byte[],int,int)`, die ebenfalls je Byte blockiert; `len == 0` kehrt ohne Warten mit 0 zurück, ein Interrupt wird als `IOException` mit gesetztem Flag gemeldet.
+- `src/main/java/net/ladenthin/streambuffer/StreamBuffer.java` (Schnittstelle Lese-/Schreibpfad ↔ Statistik und `trim`, Nachprüfung nach F73) · `cbb7f64` · 2026-10-20 · Fund F212 — `recordReadStatistics` (1 Byte bzw. je kopiertem Block) und `totalBytesWritten`/`maxObservedBytes` laufen unter `bufferLock`, den `trim()` für seine ganze Dauer hält. Seit F73 kopiert `trim()` direkt aus der FIFO und liest oder schreibt nie über die Streams; die einzige Ein-/Ausgabe, die während eines Trims noch läuft, ist ein Schreiben oder Lesen aus dem `release()` eines Trim-Start-Signals auf dem Trim-Thread (reentranter Monitor). Die beiden `isTrimRunning`-Wächter der Statistik blendeten genau diese Nutzer-Ein-/Ausgabe aus (F212, gefixt in `00fc010`); seitdem gilt `isTrimRunning` nur noch in `shouldTrim()` und verhindert dort einen verschachtelten Trim. `skip` ist `InputStream`s Vorgabe über `read(byte[])` und wird dort gezählt. Die frühere Notiz zu `5e0f51d` (das Flag blende die eigenen internen Lese-/Schreibvorgänge von `trim` aus) beschrieb den Code vor F73 und ist durch diese Zeile ersetzt.
+- `src/main/java/net/ladenthin/streambuffer/StreamBuffer.java` (Schnittstelle `trim()` ↔ `waitForAtLeast`/`read()` über das ungeschützte `availableBytes`) · `95bac9a` · 2026-10-18 · Fund F73 — Signalisierung (max-1-Permit, `close` → Signal) ohne verlorenes Aufwecken nachgerechnet; der Trim las über den eigenen Stream und machte den Zwischenstand des Zählers sichtbar (F73). `skip`/`readAllBytes` laufen über `read(byte[],…)` und erben F03, kein eigener Fund.
+- `src/main/java/net/ladenthin/streambuffer/StreamBuffer.java` (Nachprüfung des F73-`trim()`) · `95bac9a` · 2026-10-18 · kein Fund — Einträge der Länge 0 (Position 0 = Länge) werden entnommen statt zu hängen; nach `remaining == 0` übrig bleibende leere Einträge stehen vor den neuen Blöcken, ohne die Bytefolge zu ändern; `toAllocate` ist mindestens 1, die innere Schleife endet, solange `availableBytes` dem Deque-Inhalt entspricht (Invariante aller Schreibpfade unter `bufferLock`).
+- `src/main/java/net/ladenthin/streambuffer/StreamBuffer.java` (Javadoc und Setter, Sonderwerte) · `95bac9a` · 2026-10-18 · Fund F110 — Javadoc von `clampToMaxInt` veraltet seit F73; `setMaxAllocationSize` weist `<= 0` ab, `setMaxBufferElements` nimmt jeden Wert (Entscheidung in `decideTrimExecution`)
+- `src/main/java/net/ladenthin/streambuffer/StreamBuffer.java` (`SBInputStream` ohne `skip`-Überschreibung) · `95bac9a` · 2026-10-18 · kein Fund — `InputStream.skip` liest über `read(byte[],int,int)`, zählt damit in `totalBytesRead` (wie die Javadoc „reads and skips“ sagt) und blockiert bis zu Daten oder Stromende, wie ein Lesen.
+- `src/main/java/net/ladenthin/streambuffer/StreamBuffer.java` (Probe der öffentlichen Stream-API, 18 Grenzfälle gegen den `InputStream`/`OutputStream`-Vertrag) · `95bac9a` · 2026-10-18 · kein Fund — `read(b,off,0)` liefert 0 (offen und geschlossen), `read()` geschlossen-leer −1, Restdaten nach `close()` lesbar, dann −1; `skip` negativ 0, `skip` über das Ende hinaus liefert die vorhandenen Bytes; Schreiben nach `close()` wirft `IOException`; `null`/ungültige Bereiche werfen `NullPointerException`/`IndexOutOfBoundsException` wie vom Vertrag verlangt; `readAllBytes`/`transferTo` nach `close()` vollständig; doppeltes Schließen und `flush` nach `close()` folgenlos
+- `src/main/java/net/ladenthin/streambuffer/StreamBuffer.java` (Verträge `InputStream`/`OutputStream`: `len == 0`, `skip`, Schreiben nach und während `close`) · `95bac9a` · 2026-10-18 · Verdacht notiert — `read(b, off, 0)` liefert 0 auch am Ende (`validateOffsetAndLengthToRead`), `skip` über die Standardimplementierung (siehe Zeile oben), Schreiben nach `close` wirft `IOException` (`requireNonClosed`), `write(b, off, 0)` kehrt vorher zurück; das Warten auf alle `len` Bytes ist F03 (Designentscheidung). Der damals offene Verdacht `write` parallel zu `close` (Prüfung außerhalb des Locks) ist Fund F149 (gefixt in `6ece270`), siehe BUGHUNT-FOUND.md.
+- `src/main/java/net/ladenthin/streambuffer/StreamBuffer.java` (Nachprüfung des F149-Schreib-/Schließpfads) · `cbb7f64` · 2026-10-20 · kein Fund — `writeFromArray` prüft `requireNonClosed()` innerhalb von `synchronized (bufferLock)`, bevor es puffert; `closeAll()` setzt `streamClosed` unter demselben Lock; `write(int)` läuft über `writeFromArray`. Ein Schreiben, das mit `close()` um die Wette läuft, ist damit entweder vollständig gepuffert oder scheitert mit „Stream closed“, und es hängt nie an, nachdem `close()` zurückgekehrt ist. `close()` wartet, solange ein Schreiben oder Trim auf einem anderen Thread den Lock hält, einschließlich der Signal-Freigaben innerhalb von `trim()` (Javadoc von `close()`); ein `close()` aus einem Trim-Signal auf dem Trim-Thread nimmt den Lock reentrant und lässt das auslösende Schreiben und die gepufferten Bytes unberührt, weil `trim()` `availableBytes` nicht verändert. Gepinnt von `close_fromAnotherThreadDuringAWrite_waitsUntilTheWriteIsBuffered` (Schließer auf eigenem Thread) und `trim_closeDuringTrim_triggeringWriteDoesNotThrowAndPreservesData` (Schließer im Trim-Signal).