diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml index d89f9f95..639dba6b 100644 --- a/.github/workflows/formal-verification.yml +++ b/.github/workflows/formal-verification.yml @@ -274,9 +274,11 @@ 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" @@ -284,29 +286,31 @@ jobs: 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 diff --git a/.gitignore b/.gitignore index 5de12ed1..a2c6376b 100644 --- a/.gitignore +++ b/.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/ diff --git a/BUGHUNT-CHECKED.md b/BUGHUNT-CHECKED.md new file mode 100644 index 00000000..40c739a7 --- /dev/null +++ b/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:` 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). diff --git a/BUGHUNT-FOUND.md b/BUGHUNT-FOUND.md new file mode 100644 index 00000000..a76fbb1d --- /dev/null +++ b/BUGHUNT-FOUND.md @@ -0,0 +1,120 @@ + +# Bug-Hunt: gefundene Fehler — streambuffer + +Fortlaufendes Fundbuch der Fehlersuche auf dem Arbeitsbranch `ccr-90fc5f6a-vs4s0f`. Jeder Fund hat eine +globale ID (`Fnn`, über alle drei Repos eindeutig), Datei:Zeile, Schwere, Beschreibung, Reproduktion (Testname), +Status und Commit. Neue Funde werden **unten angehängt**; die nächste freie ID ist die höchste ID in allen drei +Repos plus eins. Geprüfte Klassen ohne Fund stehen in [`BUGHUNT-CHECKED.md`](BUGHUNT-CHECKED.md). + +## Übersicht + +- [F02](#f02) — mittel — *gefixt* +- [F03](#f03) — mittel — *Designentscheidung, dokumentiert* +- [F73](#f73) — hoch — *gefixt* +- [F110](#f110) — niedrig — *gefixt (Doku)* +- [F149](#f149) — mittel — *gefixt* +- [F212](#f212) — niedrig — *gefixt* +- [F268](#f268) — mittel — *gefixt* + +## Funde + + +### F02 – streambuffer: `safeWrite` wird von gleichzeitigem `write(int)` ausgehebelt +- **Zeit:** 2026-10-16 23:05 UTC +- **Datei:** `src/main/java/net/ladenthin/streambuffer/StreamBuffer.java:1015` (`writeSingleByte`), `:1057` (Klon-Entscheidung in `writeFromArray`) +- **Schwere:** mittel +- **Beschreibung:** `writeSingleByte()` setzte das **instanzweite** `volatile` Feld `ignoreSafeWrite=true` um seinen eigenen Schreibvorgang. Läuft auf einem anderen Thread gleichzeitig `write(byte[])` mit `setSafeWrite(true)` und bekommt den Lock in diesem Fenster, wird das Array **nicht** geklont, sondern per Referenz in die Deque gelegt. Ändert der Aufrufer sein Array danach (genau das, wovor `safeWrite` schützen soll), liest der Leser die geänderten Bytes. Klassen-Javadoc erlaubt gleichzeitige Aufrufe; ein Test im Repo spricht von „concurrent writers“. +- **Reproduktion:** `StreamBufferTest$ConcurrentReadWriteTests#safeWrite_concurrentSingleByteWrite_arrayStillCloned` – vor dem Fix rot (geänderte Bytes beim Leser), danach grün; ganze `StreamBufferTest` 286/286 grün. +- **Status:** gefixt (Feld entfernt, Klon-Erlaubnis als Parameter der privaten Schreibmethode). Nicht geprüft: OpenJML-ESC/RAC-Pipeline (die privaten Schreibmethoden stehen nicht in der `.jml`), PIT, jcstress. +- **Nachgemessen:** Messauftrag `BUGHUNT-MEASUREMENTS.md` in `0620aa7`, lokal gelaufen 2026-10-19: jcstress (S1) und vmlens (S2) grün, ESC 14/14 und RAC grün (S3); PIT 199/199 getötet (Review 2026-10-20). Die „Nicht geprüft“-Liste oben ist damit erledigt. +- **Nachtrag (Branch-Review 2026-10-20):** der Reproduktionstest `safeWrite_concurrentSingleByteWrite_arrayStillCloned` konnte leer bestehen: er rief nur `Waiter.resume()`, das in ConcurrentUnit 0.4.6 nichts zurückwirft (das tut nur `await`), und ein Leser, der vorzeitig stirbt, ließ die einzige Prüfung „0 geänderte Bytes“ grün. Jetzt halten beide Hintergrund-Threads jede `Throwable` in einer `AtomicReference` fest, Einzelbyte-Schreiber und Leser zählen ihre Bytes, und der Test prüft „kein Fehler“ sowie „gelesen == 8·n + Einzelbytes“. Gegenprobe mit einer eingeschleusten `IOException` im Lesepfad (`readIntoArray`): die alte Fassung grün, die neue rot („Expected: is null but: was “ und „Expected: is <1812184L> but: was <0L>“); ohne Einschleusung grün. Der ältere Test `concurrentReadWrite_stressTest_noCrashOrInconsistency` ruft nach `resume()` jetzt `await(1, SECONDS, 0)`, sodass die Ursache eines toten Lesers auf dem Test-Thread erscheint (vorher nur ein `assertArrayEquals`-Fehlschlag ohne Ursache); sein falscher Kommentar ist korrigiert. +- **Commit:** streambuffer `3302ff8` + + +### F03 – streambuffer: `read(byte[],off,len)` wartet auf **alle** `len` Bytes (Abweichung vom `InputStream`-Vertrag) +- **Zeit:** 2026-10-16 23:10 UTC +- **Datei:** `src/main/java/net/ladenthin/streambuffer/StreamBuffer.java:912` (`readIntoArray`, „second wait phase“ `waitForAtLeast(missingBytes)`) +- **Schwere:** mittel (falls nicht gewollt) / keine (falls gewollt) +- **Beschreibung:** Nach dem ersten Byte wartet `readIntoArray` mit `waitForAtLeast(len-1)`, bis der Rest **vollständig** da ist oder der Stream geschlossen wird. `InputStream.read(byte[],int,int)` verlangt nur, bis mindestens ein Byte verfügbar ist zu blockieren, und dann zurückzugeben, was da ist. Praktische Folge: Ein `InputStreamReader`/`BufferedReader` (liest in 8-KiB-Blöcken) über einem offenen StreamBuffer hängt bei einem Request/Response-Protokoll, bis 8 KiB zusammengekommen sind oder geschlossen wird. README („second wait phase“) und die jcstress-Tests zeigen, dass das Verhalten bewusst so gebaut ist – darum kein Fix, nur zur Entscheidung. +- **Historie:** So gebaut seit dem ersten Commit des Nutzers (`9da0dcd`, 2014-09-15): `tryWaitForEnoughBytes(missingBytes)`, Javadoc „blocks until the stream is closed or enough bytes are available“; `16f1df7` (2026-06-03) benannte es nur in `waitForAtLeast` um. Einen Monat später ergänzte der Nutzer `blockDataAvailable()` (`7a780d5`, 2014-10-31, heute `waitForAnyData()`), um ohne volle Blöcke auf Daten zu warten – beides war zusammen gedacht. Festgeschrieben durch `jcstress/WriteUnblocksArrayReadRace`, `CloseUnblocksArrayReadRace` und `read_arrayThreadInterruptedWhileWaitingForSecondByte_throwsIOException`; dokumentiert war es nirgends, und das README nannte die Streams „full … compatibility“. +- **Entscheidung des Nutzers (Variante A):** Verhalten bleibt, Dokumentation ergänzt: Javadoc von `getInputStream()` und `readIntoArray`, README „Full `InputStream`/`OutputStream` Compatibility“ (eine bewusste Abweichung) und „Deadlock Behavior → Read“ (Semantik, Unterschied zu `PipedInputStream`, Folge für `InputStreamReader`, Muster `waitForAnyData()` + `available()`). +- **Reproduktion:** keine (Designfrage). +- **Status:** Designentscheidung, dokumentiert +- **Commit:** 6ece270 + + +### F73 – streambuffer: ein gleichzeitiger `trim()` lässt `waitForAtLeast`/`read()` einen halb geleerten Puffer sehen +- **Zeit:** 2026-10-18 01:35 UTC +- **Datei:** `src/main/java/net/ladenthin/streambuffer/StreamBuffer.java:496` (`trim`), `:794` (`waitForAtLeast`) +- **Schwere:** hoch +- **Beschreibung:** `trim()` (läuft im Schreib-Thread unter `bufferLock`) leerte den Puffer, indem es über den eigenen `InputStream` las, und schrieb die Bytes danach zurück. Dabei sank das `volatile` Feld `availableBytes` Schritt für Schritt bis 0 und stieg dann wieder. `waitForAtLeast(long)` liest das Feld **ohne** Lock und zweimal: einmal in der Schleifenbedingung, einmal für den Rückgabewert. Fällt ein Trim dazwischen, gibt die Methode weniger zurück als verlangt, obwohl der Stream offen ist und keine Daten verbraucht wurden – entgegen ihrer Javadoc („blocks until at least `bytes` bytes are available, or the stream is closed“). Folgen über die privaten Lesepfade: `read()` prüft `waitForAnyData() < 1` und meldet bei einem Zwischenwert 0 das **Ende eines offenen Streams, der noch Daten hält** (ein Leser bricht ab, die Daten gehen verloren); `read(byte[],…)` liefert verkürzt. Ein `close()` aus einem dritten Thread während eines Trims ergibt über den `streamClosed`-Zweig dasselbe. Ausgelöst wird es im Normalbetrieb: jeder Schreibvorgang, der mehr als `maxBufferElements` (Vorgabe 100) Einträge erzeugt, trimmt. +- **Fix:** `trim()` kopiert die Einträge direkt aus der Deque in Blöcke zu höchstens `maxAllocationSize` (Ausgangsposition `positionAtCurrentBufferEntry` berücksichtigt) und lässt `availableBytes` unverändert. Kein Lesen über den Stream mehr, `throws IOException` und der Null-Check des Zwischenpuffers entfallen. README (Trim-Abschnitt, Statistik) nachgezogen; die Zeile zum längst entfernten `ignoreSafeWrite`-Flag (aus F02) war ohnehin veraltet. +- **Reproduktion:** `StreamBufferTest$ConcurrentTrimAndWriteTests#waitForAtLeast_concurrentTrim_neverReturnsFewerBytesThanRequested` – niemand liest, `maxBufferElements` 1000, Schreiber schreibt Einzelbytes, ein Wartender ruft `waitForAtLeast(gesehen)` und prüft, dass nicht weniger zurückkommt. Mit Fix ist das deterministisch (ohne Leser sinkt `availableBytes` nie), ohne Fix ein Stresstest, der in Millisekunden rot wird. +- **Rot-Grün-Nachweis:** ohne Fix rot in 4 von 4 Läufen („Expected: is null but: was "waitForAtLeast(998) returned 997 on an open stream"“, ebenso 44001→44000, 4001→4000, 989→988), 28 ms bis zum Fund; mit Fix grün in 3 von 3 Läufen (2/2 der Klasse); Gegenprobe per `git stash` wieder rot, nach `pop` grün. Breit: `StreamBufferTest` 287/287, `StreamBufferArchitectureTest` 10/10, `StreamBufferProperties` 5/5; `spotbugs:check` grün; PIT 199/199 getötet (Test strength 100 %). +- **Nicht geprüft:** OpenJML-RAC/ESC (`trim` steht nicht in der `.jml`, kein ESC-Ziel), jcstress- und vmlens-Profil, Lincheck. +- **CI-Bedarf:** die Pipeline `formal-verification.yml` (RAC-Lauf der Suite gegen den geänderten `trim`) einmal mitlaufen lassen. +- **Nachgemessen:** Messauftrag `BUGHUNT-MEASUREMENTS.md` in `0620aa7`, lokal gelaufen 2026-10-19: RAC der ganzen Suite gegen den geänderten `trim` grün ohne Vertragsverletzung, ESC 14/14, JPF grün, jcstress und vmlens grün (S1–S3); Lincheck läuft in jedem `mvn test` mit. „Nicht geprüft“ und „CI-Bedarf“ oben sind damit erledigt; die RAC-Laufzeit des Trim-Stresstests führte zur Skalierung unter `-Pjml-rac`. +- **Nachtrag (Branch-Review 2026-10-20):** der Test `write_wrappingStreamThrows_bufferStaysUsable` (früher `trim_ignoreSafeWriteFlagResetDuringWriteException_streamRecoverable`, auf diesem Branch umbenannt) ist **gelöscht**, nicht nur umbenannt. Sein `getOutputStream()`-Wrapper warf vor jedem Aufruf des echten Streams, die geprüfte Fehlermeldung war die des Tests selbst; schon vor F73 erreichte der Wrapper den Trim nie (`trim()` schrieb über das private Feld `os`). Die verbliebenen Erholungsschritte (ein Safe-Write mit echtem Trim, dann ein Lesen mit mehr als 0 Bytes) prüfen `trim_withSafeWriteEnabled_preservesDataIntegrity` und `trim_withSafeWrite_allDataPreserved` strenger; einen Fehler im echten Trim samt Zurücksetzen von `isTrimRunning` und Erholung prüfen `trim_signalReleaseExceptionDuringStart_streamRecoverable` und `trim_signalReleaseExceptionDuringEnd_flagAlreadyResetExceptionPropagates`. `StreamBufferTest` danach 289/289 grün. +- **Status:** gefixt +- **Commit:** streambuffer `27aaed6` + + +### F110 – streambuffer: Javadoc von `clampToMaxInt` beschreibt die `trim()`-Schleife vor F73 +- **Zeit:** 2026-10-18 09:10 UTC +- **Datei:** `src/main/java/net/ladenthin/streambuffer/StreamBuffer.java:634` (Javadoc von `clampToMaxInt`) +- **Schwere:** niedrig +- **Beschreibung:** Die Javadoc begründet die Klemmung mit dem Ablauf von `trim()`: „The trim() loop reads at most maxAllocationSize bytes per iteration … Loop condition (available > 0) … Next iteration calls available() again“, samt Beispiel für 5 GB. So arbeitete `trim()` bis F73 (`27aaed6`), das den Puffer über den eigenen Eingabestrom leerte. Seit F73 kopiert `trim()` direkt aus dem Deque und liest `availableBytes`, ohne `available()` oder `clampToMaxInt`; einziger Aufrufer ist jetzt `availableClamped()` (`InputStream.available()`). Die Javadoc beschreibt also Code, den es nicht mehr gibt – eine Abweichung, die mein eigener Fix F73 hinterlassen hat. Der Code ist korrekt. +- **Historie:** Der Absatz „SAFETY GUARANTEE …“ kam mit `d3b9731` (2026-04-15) und stimmte damals: `trim()` lief über `while ((available = is.available()) > 0)`. Mein F73-Fix `27aaed6` (2026-10-18) hat `trim()` auf das direkte Kopieren aus dem Deque umgestellt und die Javadoc übersehen. JML-Spezifikation und ESC-Beweis betreffen nur die Funktion und bleiben gültig. +- **Gleiche Art, mitbehoben:** README „Default: `Integer.MAX_VALUE`“ bei `maxAllocationSize` (seit `80d8c71`, 2026-04-15); seit `f88be77` (2026-09-30) ist der Default `MAX_ARRAY_LENGTH = Integer.MAX_VALUE - 8` und der Setter klemmt darauf. Code richtig, README veraltet. +- **Fix:** Entscheidung des Nutzers (Variante A): Javadoc auf den verbliebenen Zweck gekürzt (`available()` meldet höchstens `Integer.MAX_VALUE`, wenn mehr als 2 GiB gepuffert sind), README nennt den richtigen Default. `clampToMaxInt` bleibt (ESC-Beweisumfang samt Zählung). +- **Reproduktion:** keine (reine Doku-Abweichung); `clampToMaxInt` ist durch die bestehenden direkten Tests und den ESC-Beweis abgedeckt. +- **Rot-Grün-Nachweis:** – (Doku-Korrektur, Freigabe des Nutzers für Doku ohne roten Test) +- **Status:** gefixt (Doku) +- **Commit:** 5540fb0 + + +### F149 – streambuffer: ein `write`, der mit `close()` aus einem anderen Thread zusammentrifft, hängt nach dem `close` an und kehrt normal zurück +- **Zeit:** 2026-10-18 21:00 UTC +- **Datei:** `src/main/java/net/ladenthin/streambuffer/StreamBuffer.java` (`writeFromArray`: `requireNonClosed()` vor `synchronized (bufferLock)`; `closeAll()`: Flag ohne Lock) +- **Schwere:** mittel (Datenverlust für einen Leser, der bei `-1` aufhört; nur bei `close()` aus einem dritten Thread während eines laufenden `write`) +- **Beschreibung:** Der Schreiber besteht `requireNonClosed()`, ein anderer Thread schließt, ein Leser sieht „geschlossen, 0 Bytes“ und meldet `-1`, danach hängt der Schreiber an und kehrt ohne Exception zurück. Ein erfolgreicher `write` muss vor dem `close` eingeordnet werden, also ist das nicht linearisierbar. Ein Leser, der nach `-1` noch einmal liest, bekäme die Bytes. +- **Historie:** Seit dem ersten Commit (`9da0dcd`, 2014) steht die Prüfung vor dem Lock. Die Absicht des Projekts zeigt `e61f359` (2026-05-07, Wettlauf `trim()`/`close()`): eine Exception bei einem unbeteiligten `write` und stillschweigend verworfene Bytes wurden als Fehler behoben (`trim_closeCalledDuringTrim_handlesGracefully`, `37132b3`, `8924e88`). Das README verspricht „Parallel close without deadlock“. Weder die JPF-Prüfung (Schreiber und Schließer im selben Thread) noch Lincheck (ohne blockierendes `read`) decken den Fall ab. +- **Fix:** Entscheidung des Nutzers (Variante A). `requireNonClosed()` steht jetzt in `synchronized (bufferLock)`, und `closeAll()` setzt `streamClosed` unter demselben Lock (das Signal danach). Ein `write` ist damit entweder vor dem `close` vollständig gepuffert – `waitForAtLeast` liest beim geschlossenen Stream `availableBytes` neu und sieht ihn – oder er wirft „Stream closed“. Kosten: ein `close()` wartet auf einen laufenden `write` oder `trim()`. +- **Reproduktion:** `StreamBufferTest$ConcurrentWriteAndCloseTests#write_closedWhileTheWriterWaitsForTheLock_failsInsteadOfAppendingAfterTheClose`, deterministisch ohne Reflexion: Das Trim-Start-Signal läuft im Trim-Thread, der `bufferLock` hält; dort wird ein zweiter Schreiber gestartet, der am Lock parkt (`Thread.State.BLOCKED`), und während er parkt, wird geschlossen. Erwartet: nach dem `close` bleibt der Puffer bei 2 Bytes, der späte `write` scheitert. +- **Rot-Grün-Nachweis:** ohne Fix rot („Expected: is <2L> but: was <3L>“ – der späte `write` hängte nach dem `close` an), mit Fix grün; Gegenprobe per `git stash` des Produktionscodes wieder rot, nach `pop` grün. Breit: 304 Tests grün (`StreamBufferTest`, jqwik, Lincheck, Architektur), SpotBugs, Javadoc, PIT 199/199. +- **Zusätzlich angelegt, nicht ausgeführt:** `jcstress/WriteRacingCloseRace` (Schreiber, Schließer, Leser; Ausgang `1, -1` verboten). +- **CI-Bedarf:** `mvn -Pjcstress test`, `mvn -Pvmlens test`, die Formal-Verification-Pipeline (ESC, RAC, JPF) – alles in `TODO.md`, „Run the concurrency and formal-verification suites after the write/close fix“. +- **Nachgemessen:** Messauftrag `BUGHUNT-MEASUREMENTS.md` in `0620aa7`, lokal gelaufen 2026-10-19: jcstress `WriteRacingCloseRace` grün bei rund 3,54 Milliarden Proben (S1), vmlens grün (S2), ESC 14/14, RAC und JPF grün (S3), dazu die neue JPF-Harness `JpfWriteCloseHarness` mit drei Threads (S4): mit dem Fix fehlerfrei über 75.438 Zustände, gegen `6ece270^` rot nach 3.956. Sie läuft seither im Job `jpf-interleavings`. Der TODO-Punkt aus „CI-Bedarf“ ist danach gelöscht worden. +- **Nachtrag (Branch-Review 2026-10-20):** der Rot-Grün-Nachweis oben nahm beide Hälften des Fixes auf einmal zurück; der Reproduktionstest ruft `close()` im Trim-Start-Signal auf dem Thread, der `bufferLock` schon hält (reentrant), und bleibt grün, wenn nur der Lock in `closeAll()` fehlt. Neu: `ConcurrentWriteAndCloseTests#close_fromAnotherThreadDuringAWrite_waitsUntilTheWriteIsBuffered` startet den Schließer im Signal als eigenen Thread und hält dort dessen Zustand, `isClosed()` und den Pufferstand fest (geprüft wird erst nach dem `write`): der Schließer muss `BLOCKED` sein, der Stream noch offen, 2 Bytes gepuffert, danach geschlossen mit 2 Bytes. Gegen `closeAll()` allein (Lock dort entfernt, `requireNonClosed()` unter dem Lock in `writeFromArray` belassen) rot in 3 von 3 Läufen („Expected: is but: was “, einmal „… was “, dazu „Expected: is but: was “), der bestehende Test blieb dabei grün; mit Fix grün in 5 von 5 Läufen, `StreamBufferTest` 290/290. +- **Status:** gefixt +- **Commit:** 6ece270 + + +### F212 – streambuffer: I/O aus einem Trim-Start-Signal fehlt in den Statistiken +- **Zeit:** 2026-10-20 20:31 UTC +- **Datei:** `src/main/java/net/ladenthin/streambuffer/StreamBuffer.java` (`writeFromArray`: `if (!isTrimRunning)` um `totalBytesWritten`/`updateMaxObservedBytesIfNeeded`; `recordReadStatistics`: `if (!isTrimRunning)` um `totalBytesRead`; Javadoc von `isTrimRunning`) +- **Schwere:** niedrig (falsche Zähler, nur für I/O aus einem Trim-Start-Signal auf dem Trim-Thread) +- **Historie:** Gefunden beim Review des Branches am 2026-10-20 (Fund S1-2). Vor F73 (`27aaed6`) leerte `trim()` den Puffer über den eigenen `InputStream` und schrieb ihn zurück; die beiden Wächter hielten diese interne I/O aus den Zählern. Seit F73 kopiert `trim()` direkt aus der Deque, die Wächter schlossen nur noch einen Fall aus: ein `write`/`read`, den ein Trim-Start-Signal in seinem `release()` auf dem Trim-Thread macht (`bufferLock` ist reentrant). Die mit F73 umgeschriebene Javadoc von `isTrimRunning` schrieb diesen Ausschluss fest („nor be counted in the statistics“). +- **Beschreibung:** Ein solcher `write` erhöhte `availableBytes`, aber weder `totalBytesWritten` noch `maxObservedBytes`; ein solcher `read` senkte `availableBytes`, ohne `totalBytesRead` zu erhöhen. Das widerspricht der Javadoc von `getTotalBytesWritten`/`getTotalBytesRead` („by user I/O operations“), dem README („the statistics always reflect user I/O only“) und der Invariante `totalBytesWritten == totalBytesRead + available` (`StreamBufferProperties`): nach dem Auslesen standen 12 gelesene gegen 9 geschriebene Bytes. +- **Fix:** Die beiden Wächter um die Statistik entfallen, der in `shouldTrim()` bleibt (er verhindert den verschachtelten Trim). Javadoc von `isTrimRunning` und `recordReadStatistics` angepasst, zwei veraltete Testkommentare („trim internally reads and writes …“) korrigiert. Die JML-Spezifikation deckt keine der drei Methoden ab, daher keine Spiegelung nötig; README und Getter-Javadoc stimmen jetzt mit dem Code überein. +- **Tests:** `StreamBufferTest$StatisticsTests#statistics_writeFromTrimStartHook_isCounted` (Hook schreibt `{10,11,12}` beim ersten Trim; danach `getTotalBytesWritten()` und `getMaxObservedBytes()` 12, nach dem Auslesen `getTotalBytesRead()` 12 und gleich `getTotalBytesWritten()`), `#statistics_readFromTrimStartHook_isCounted` (Hook liest ein Byte; `getTotalBytesRead()` 1, geschrieben 9, verfügbar 8). +- **Rot-Grün-Nachweis:** ohne Fix rot („Expected: is <12L> but: was <9L>“ dreimal im Schreibtest – geschrieben, maxObserved und geschrieben gegen gelesen –, „Expected: is <1L> but: was <0L>“ im Lesetest), mit Fix grün (`StatisticsTests` 15/15). Breit: ganze Suite grün (306/306: `StreamBufferTest`, jqwik, Lincheck, Architektur), SpotBugs ohne Befund, PIT 197/197 (vorher 199: die beiden Mutanten der entfernten Wächter entfallen). +- **Status:** gefixt +- **Commit:** 00fc010 + + +### F268 – streambuffer: ein `OutOfMemoryError` mitten im `trim()` verliert gepufferte Bytes +- **Zeit:** 2026-10-21 22:58 UTC +- **Datei:** `src/main/java/net/ladenthin/streambuffer/StreamBuffer.java` (`trim()`: Allokation der Blöcke; neue Naht `allocateTrimChunk(int)`) +- **Schwere:** mittel (Datenverlust bei Speichermangel während einer Konsolidierung mit mehr als einem Block; bis dahin nur über `maxAllocationSize` erreichbar oder bei einem Puffer nahe der Array-Obergrenze) +- **Historie:** Gefunden beim Opus-Review des PR #189 am 2026-10-21. Seit F73 (`27aaed6`) kopiert `trim()` die Einträge direkt aus der Deque in Blöcke von höchstens `maxAllocationSize` Bytes. Jeder Block wurde erst allokiert, wenn der vorige fertig kopiert war – und dessen Quelleinträge waren dann schon per `pollFirst()` aus der Deque entfernt. +- **Beschreibung:** Schlug die Allokation eines späteren Blocks mit `OutOfMemoryError` fehl, lief der Error aus `write()` hinaus (das `finally` setzte `isTrimRunning` zurück und löste die Trim-End-Signale), aber die Deque enthielt nur noch die nicht kopierten Einträge, während `availableBytes` unverändert alle Bytes zählte. Ein nachfolgendes `read()` lief auf `buffer.getFirst()` einer leeren Deque (`NoSuchElementException`) oder lieferte die falschen Bytes; `available()` versprach Daten, die weg waren. +- **Fix:** `trim()` allokiert jetzt jeden Block, bevor es die Deque anfasst, und kopiert erst danach. Schlägt eine Allokation fehl, ist der Puffer genau so, wie der auslösende `write` ihn hinterlassen hat (Einträge, Reihenfolge, `availableBytes`), und der nächste `write` trimmt erneut. Die eine Allokationsstelle ist die paketprivate Naht `allocateTrimChunk(int)` (`return new byte[size]`): kein toter Aufruf im Produktivcode, und ein Test im selben Paket überschreibt sie und lässt genau die n-te Allokation fehlschlagen, ohne einen Heap, der das real tut. Keine JML-Spiegelung nötig: die `.jml` deklariert `trim()` nicht, die Naht liegt außerhalb der ESC-Liste (14 Beweise unverändert). Javadoc von `trim()`, README (`maxAllocationSize`) und CHANGELOG ergänzt. +- **Tests:** `StreamBufferTest$TrimTests#trim_allocationOfALaterChunkFails_bufferStaysConsistent` – drei 4-Byte-Einträge, `maxBufferElements` 2, `maxAllocationSize` 8, die zweite Allokation wirft; danach `getAvailableBytesExact()` 12, `getBufferElementCount()` 3, Trim-End-Signal 1 Permit, Error mit der Testmeldung; ein vierter Eintrag trimmt zu zwei 8-Byte-Blöcken (4 Allokationen), `read` liefert alle 16 Bytes in Reihenfolge. +- **Rot-Grün-Nachweis:** Naht zuerst in die alte Schleife eingezogen, Test rot („Expected: is <3> but: was <1>“ – zwei Einträge schon gepollt, der Zähler stand noch auf 12); nach dem Umbau grün (`TrimTests` 3/3). Breit: ganze Suite grün (307/307: `StreamBufferTest`, jqwik, Lincheck, Architektur), Javadoc-Jar gebaut, SpotBugs ohne Befund, PIT 198/198 (vorher 197: der eine Mutant der neuen Naht, „return null“, stirbt am Kopierschritt). +- **Status:** gefixt +- **Commit:** 1b85963 + +## Offene Verdachte ohne Fund-ID + +Keine (Stand 2026-10-18). diff --git a/CHANGELOG.md b/CHANGELOG.md index a357cd60..fd5bf037 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -22,6 +22,12 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 (fixups v3); RAC 285/285 against the unmodified 21.0.29 distribution. The class-invariant blocker is narrowed down: RAC miscompiles an unqualified call from an inner-class method to an outer instance method (`writeSingleByte(b)` in `SBOutputStream`), see TODO.md. +- **Documented: `read(byte[], off, len)` waits for all `len` bytes** (or for `close()`), a deliberate + deviation from the `InputStream` contract that has been the design since the first version but was + stated nowhere. The Javadoc of `getInputStream()` and the README ("Full `InputStream`/`OutputStream` + Compatibility", "Deadlock Behavior → Read") now say so, with the `waitForAnyData()` + `available()` + pattern for request/response protocols; the README's `maxAllocationSize` default reads + `Integer.MAX_VALUE - 8`, as the code has it. - Build tooling: spotbugs-maven-plugin 4.10.4.1 -> 4.10.5.0 (SpotBugs 4.10.5, the first release that reads JSpecify; nothing to report here), in step with the sibling repositories. - Build and test tooling bumped in step with the sibling repositories: Spotless 3.10.4 and Checker @@ -84,8 +90,45 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - Release Process prompt template moved from `CHANGELOG.md` to `docs/RELEASE.md`. - `maxAllocationSize` defaults to `Integer.MAX_VALUE - 8` (was `Integer.MAX_VALUE`); `setMaxAllocationSize` clamps larger values to it. +- **Tests that could pass without checking anything are tightened.** The jqwik properties + (`StreamBufferProperties`) now run in every build: their class name matched none of Surefire's + default include patterns, so they ran nowhere; under `-Pjml-rac` they use 100 tries instead of 1000. + The concurrent `safeWrite` test records every failure of its background threads and checks the byte + count, since `Waiter.resume()` never rethrows and a reader that died early left it green. A test + whose wrapping output stream threw before it reached the buffer is removed (its message was the + test's own). A new test pins that `close()` waits for a write on another thread, the half of the + write/close fix the existing single-threaded test does not see. The close-during-trim tests describe + the current `trim()`, which copies straight from the FIFO, instead of a read phase and a write-back + through the streams. +- **Formal verification: a third JPF harness** (`WriteClose.jpf`) model-checks writer, closer and + reader in three threads, i.e. the order of write and close, which the existing harness cannot see. + Under RAC the two stress loops of `StreamBufferTest` are scaled down (`streambuffer.test.rac`): + RAC prints a stack trace for every `System.arraycopy`/`clone` (OpenJML/OpenJML#1050), and unscaled + the job ran into its timeout with every contract holding. ### Fixed +- **`safeWrite` could be bypassed by a concurrent `write(int)`.** A single-byte write set an + instance-wide flag that told an array write running on another thread not to clone its array, so + with `setSafeWrite(true)` the caller's array could land in the buffer by reference and later changes + to it reached the reader. The flag is gone; whether to clone is a parameter of the private write path. +- **A concurrent `trim()` no longer lets a reader see a half-emptied buffer.** `trim()` drained the + buffer through its own input stream and wrote the bytes back, so the buffered count fell to 0 and rose + again while `read()` and `waitForAtLeast` read it without the lock: a reader could get fewer bytes + than requested, or end of stream, on an open stream. `trim()` now copies the entries straight from the + FIFO into blocks of at most `maxAllocationSize` and leaves the count unchanged. +- **A `trim()` whose allocation fails no longer loses buffered bytes.** The consolidation allocated its + blocks one at a time, each after the entries of the previous block had already been polled from the + FIFO, so an `OutOfMemoryError` on a later block left the buffer with those entries gone while the + byte count still included them: a reader then failed or read the wrong bytes. Every block is now + allocated before the FIFO is touched, so the error propagates out of the write with the buffer + exactly as that write left it, and the next write trims again. The allocation goes through one + package-private seam (`allocateTrimChunk`), which is how the test provokes the failure. +- **A `write` racing `close()` from another thread can no longer land after the close.** The closed + check ran before the lock was taken and `close()` set the flag without it, so a writer that had passed + the check could append after a reader had seen "closed, 0 bytes" and reported end of stream. The check + now runs under `bufferLock` and `close()` sets the flag under the same lock: a write is either fully + buffered before the close or fails with "Stream closed"; `close()` waits for a write or `trim()` in + progress on another thread. - **CI: the GitHub `snapshot` pre-release holds exactly the current build, and the release assets include the pom.** `gh release upload --clobber` replaces same-named assets and never removes any other, so the `snapshot` release accumulated: the 1.2.0-SNAPSHOT jar and javadoc jar (unsigned, from before the @@ -108,6 +151,12 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 passes `-Dmaven.repository.credentialScope=id`, Maven's own switch back to id-only matching, until a setup-java release can write `` (`mvn-server-repository-origins`, merged upstream but not yet released). +- **Statistics count the I/O of a trim start signal.** A write or read made from a trim start + signal's `release()` on the trim thread changed the buffered count but was left out of + `getTotalBytesWritten()`, `getMaxObservedBytes()` and `getTotalBytesRead()`, contrary to their + Javadoc and to `written == read + available`. The guards dated from when `trim()` read and wrote + through the streams itself; it copies straight from the FIFO now, so every counted byte is user + I/O. `isTrimRunning` still prevents a nested trim. - `trim()` with more than 2 GB buffered no longer allocates `new byte[Integer.MAX_VALUE]`, which the JVM always rejects ("Requested array size exceeds VM limit"). Allocations are capped at `Integer.MAX_VALUE - 8`, the JDK's `SOFT_MAX_ARRAY_LENGTH`. diff --git a/CLAUDE.md b/CLAUDE.md index ec116e2a..020566e1 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -44,7 +44,10 @@ mvn test-compile exec:java \ `-prof gc` reports `gc.alloc.rate.norm` (bytes allocated per op) — useful for spotting hidden allocations on the read/write hot paths. `-prof async` produces flamegraphs and requires async-profiler installed locally; CI does not run it. `mvn test` also runs: -- **jqwik properties** (`StreamBufferProperties`) — picked up by Surefire as a JUnit 6 engine. +- **jqwik properties** (`StreamBufferProperties`) — a JUnit Platform engine; Surefire runs the class + only because `pom.xml` adds `**/*Properties.java` to its include patterns (until 2026-10-19 it ran + in no build, since the name matches none of Surefire's defaults). Under `-Pjml-rac` they run with + 100 tries instead of 1000 (`jqwik.tries.default`). - **Lincheck** linearizability test (`StreamBufferLincheckTest`) over the non-blocking subset (`write`, `available`, `close`, `isClosed`). **Opt-in jcstress concurrency stress tests:** @@ -69,9 +72,11 @@ deliberately not part of the synchronous Publish pipeline and never a required c 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 + PathFinder exhaustively model-checks the concurrent read/write/close protocol with two harnesses: + `StreamBuffer.jpf` (a writer that closes after its writes, a reader) and `WriteClose.jpf` (writer, + closer and reader in three threads -- the order of write and close, which the first cannot see; + red before bug-hunt fix F149). Requires JDK 11; builds jpf-core from a pinned commit with a + one-file `AtomicLong` model patch; the harnesses are 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 @@ -149,6 +154,11 @@ mvn -P jml-rac -Dopenjml.home= -Dopenjml.jdk.java=/jdk/bin/jav [OpenJML/Specs#29](https://github.com/OpenJML/Specs/pull/29) + [OpenJML/OpenJML#982](https://github.com/OpenJML/OpenJML/pull/982)). Both fixes are in 21.0.29; the suite passes against the unmodified distribution (285/285). +- Under `-Pjml-rac` the stress loops of `StreamBufferTest` and the jqwik tries are scaled down + (`streambuffer.test.rac`, `jqwik.tries.default` 100): RAC prints a ~10 KB stack trace for every + `System.arraycopy`/`clone` (an uncompiled model method of the bundled JDK spec, + [OpenJML/OpenJML#1050](https://github.com/OpenJML/OpenJML/issues/1050)), and unscaled the job ran + into its timeout with every contract holding. Do not remove the scaling before a release fixes it. - 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. diff --git a/README.md b/README.md index 38203273..a583b84e 100644 --- a/README.md +++ b/README.md @@ -129,7 +129,7 @@ Instead of a fixed circular buffer, `StreamBuffer` uses a `Deque` that g ### Full `InputStream`/`OutputStream` Compatibility -`StreamBuffer` exposes a standard `InputStream` (via `getInputStream()`) and a standard `OutputStream` (via `getOutputStream()`). Both are full subclass implementations and can be used anywhere those types are accepted. +`StreamBuffer` exposes a standard `InputStream` (via `getInputStream()`) and a standard `OutputStream` (via `getOutputStream()`). Both are full subclass implementations and can be used anywhere those types are accepted. One deliberate difference: `read(byte[], off, len)` waits for **all** `len` bytes (or `close()`), see [Read](#read). ### Thread Safety @@ -137,6 +137,7 @@ The `InputStream` and `OutputStream` can be used concurrently from different thr - All `Deque` accesses are guarded by a `bufferLock` object. - State fields (`streamClosed`, `safeWrite`, `availableBytes`, `positionAtCurrentBufferEntry`, `maxBufferElements`, `maxAllocationSize`, `isTrimRunning`, `maxObservedBytes`) are `volatile`; the cumulative counters `totalBytesWritten` and `totalBytesRead` are `final AtomicLong` (atomic read-modify-write under concurrent I/O). +- `close()` takes the same lock, so it waits for a write or trim in progress on another thread: a write racing the close is either fully buffered or fails with "Stream closed", never appended after a reader saw the end of the stream. A trim copies every buffered byte, so with a large buffer that wait can be noticeable. - A `Semaphore signalModification` blocks reading threads until data is written or the stream is closed, avoiding busy-waiting. External semaphores can be registered via `addSignal` for thread-decoupled notification. ### No Write Deadlock @@ -168,7 +169,7 @@ sb.setMaxBufferElements(50); // trim when more than 50 elements are queued sb.setMaxBufferElements(0); // disable trimming entirely ``` -Trimming is triggered by writes, not by `setMaxBufferElements`. The trim internally bypasses `safeWrite` (via an `ignoreSafeWrite` flag) because the byte arrays it produces are not reachable from outside the buffer. +Trimming is triggered by writes, not by `setMaxBufferElements`. The trim copies the buffered arrays directly into the consolidated ones, without going through the streams, so `safeWrite` does not apply (the arrays it produces are not reachable from outside the buffer) and the buffered byte count stays constant while it runs: a concurrent `waitForAtLeast` or `available()` never sees a partly drained buffer. If `maxAllocationSize` is set (see below), trim may produce multiple smaller chunks instead of one. Trim is also skipped automatically when consolidation would not reduce the chunk count below `maxBufferElements` — for example, when `maxAllocationSize` is small enough that the resulting chunk count would still exceed the threshold. This prevents repeated no-op trims on every write. @@ -209,7 +210,7 @@ Signals are stored in a `CopyOnWriteArrayList` for thread-safe iteration. The "m ### Statistics Tracking -`StreamBuffer` tracks cumulative I/O statistics for the bytes flowing through the user-facing API. Internal reads and writes performed by the trim operation are excluded — `isTrimRunning` is checked before updating the counters so the statistics always reflect user I/O only. +`StreamBuffer` tracks cumulative I/O statistics for the bytes flowing through the user-facing API. The trim operation is excluded: it consolidates the buffered arrays directly, without reading or writing through the streams, so the statistics always reflect user I/O only. ```java StreamBuffer sb = new StreamBuffer(); @@ -243,9 +244,10 @@ sb.setMaxAllocationSize(1024 * 1024); // cap each consolidated chunk at 1 MiB long current = sb.getMaxAllocationSize(); ``` -- Default: `Integer.MAX_VALUE` (effectively one chunk per trim pass). +- Default: `Integer.MAX_VALUE - 8`, the largest array the JVM reliably allocates (effectively one chunk per trim pass); larger values passed to `setMaxAllocationSize` are capped to it. - Throws `IllegalArgumentException` if the value is ≤ 0. - Trim is skipped automatically when the resulting chunk count would not be smaller than the current `Deque` size — this prevents repeated no-op trims when `maxAllocationSize` is very small. +- Every chunk of a trim pass is allocated before any buffered entry is consolidated. If an allocation fails with `OutOfMemoryError`, the write that triggered the trim throws it and the buffer is left exactly as that write left it (entries, order and byte count), so every byte stays readable and the next write trims again. ### Trim Observer Signals @@ -325,7 +327,16 @@ External observers register `java.util.concurrent.Semaphore` objects via `addSig ### Read -If no data is available and the stream is not closed, `read()` blocks the calling thread. To avoid blocking, only read as many bytes as `available()` reports. The `waitForAnyData()` and `waitForAtLeast(long)` methods can be used to wait for data before reading. +If no data is available and the stream is not closed, `read()` blocks the calling thread. `read(byte[], off, len)` goes further: after the first byte it keeps waiting until **all** `len` bytes are buffered, and returns fewer only when the stream is closed. That is stricter than the `InputStream` contract (block until at least one byte) and unlike `PipedInputStream`; it has been the design since the first version. + +To avoid blocking, only read as many bytes as `available()` reports. The `waitForAnyData()` and `waitForAtLeast(long)` methods can be used to wait for data before reading: + +```java +sb.waitForAnyData(); // returns once at least one byte is buffered (or closed) +int n = is.read(buf, 0, Math.min(buf.length, Math.max(1, is.available()))); +``` + +This matters for wrappers that read in blocks, such as `InputStreamReader`/`BufferedReader` (8 KiB): over an open buffer in a request/response protocol they wait until a whole block has arrived. ### Write diff --git a/TODO.md b/TODO.md index 2d0ade85..4ed4977c 100644 --- a/TODO.md +++ b/TODO.md @@ -56,6 +56,28 @@ annotated, so everything below is genuinely still open. against the unmodified 21.0.29 distribution. - Missing `JAVA_VERSION` key in the bundled `jdk/release`: missing in 21.0.28 (reported in #1012), **present again in 21.0.29**; the guarded repair step is a no-op there and stays as a guard. + - **RAC evaluates a `signals (E e)` clause for an exception of another type — confirmed OpenJML + bug, reported in [OpenJML/OpenJML#1050](https://github.com/OpenJML/OpenJML/issues/1050)** (2026-10-19; reproduced on 21.0.28 and on `dev-21` `529ac454da`, + `BUGHUNT-MEASUREMENTS.md`, „OpenJML-Verdachtsfälle (RAC)“, in commit `0620aa7`, removed since). The spec + of `waitForAtLeast` allows `InterruptedException` (`signals_only IllegalArgumentException, + InterruptedException`) and constrains only the other one (`signals (IllegalArgumentException e) + bytes <= 0`). When a read is interrupted, RAC prints `JML undefined exceptional postcondition - + exception thrown` with `ClassCastException: InterruptedException cannot be cast to + IllegalArgumentException` (stack at `waitForAnyData`, which calls `waitForAtLeast`). By JML's + semantics the clause only applies when the exception is an instance of `E`, so nothing should be + reported. Confirmed: the call-site check casts without an `instanceof` guard when the predicate + folds to `false` for the actual argument (`waitForAtLeast(1L)`), `JmlAssertionAdder.applyHelper`. + Harmless here (reported, not thrown, under `rac=exception`; the test stays green). To do: re-run + once a release carries the fix. + - **RAC prints a full stack trace per call for an uncompiled model method — confirmed OpenJML + usability defect, reported in [OpenJML/OpenJML#1050](https://github.com/OpenJML/OpenJML/issues/1050)** (2026-10-19, same issue; 1000 `arraycopy` = 1000 traces, also + on `dev-21`; compiling with `-quiet` silences it). Every `System.arraycopy` and `clone` under RAC logs + `Skipping a specification clause because it contains an uncompiled model method: 'boolean + java.util.Arrays.equalArrays` plus a `NoSuchMethodError` stack trace (about 10 KB), once per + call rather than once per clause. That is what made the concurrent-trim test take 7,344 s and + 21 GB of log; worked around by scaling the stress loops under `-Pjml-rac` + (`StreamBufferTest.iterations`) and running jqwik with 100 tries there. Once fixed upstream, the + scaling can go. - **Invariants + non-static inner classes break RAC — confirmed OpenJML bug, reported in [OpenJML/OpenJML#1012](https://github.com/OpenJML/OpenJML/issues/1012).** RAC checks the outer class's invariant inside the inner class's constructor and reads the field on the inner class → `NoSuchFieldError` at runtime (21.0.27 and 21.0.28). @@ -104,9 +126,11 @@ annotated, so everything below is genuinely still open. ~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. + - **On every OpenJML upgrade:** re-try the four class invariants documented in the `.jml` + header (no bundled spec is deleted at install any more since fixups v3, so there is nothing + to re-try in `.github/actions/setup-openjml/action.yml`), and, once #1050 is fixed, drop the + RAC scaling (`streambuffer.test.rac` and `jqwik.tries.default` in the `jml-rac` profile, + `StreamBufferTest.iterations`). - **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 diff --git a/pom.xml b/pom.xml index f02c6aa8..4dd8029a 100644 --- a/pom.xml +++ b/pom.xml @@ -298,6 +298,20 @@ SPDX-License-Identifier: Apache-2.0 **/vmlens/*.java + + + **/Test*.java + **/*Test.java + **/*Tests.java + **/*TestCase.java + **/*Properties.java + @@ -834,6 +848,24 @@ SPDX-License-Identifier: Apache-2.0 is lifted. JUnit reads this config parameter from a system property. --> disabled + + true + + 100