From 3302ff82bf90392a5c622ab5829f6604b9dacb5e Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 16 Oct 2026 22:47:22 +0000 Subject: [PATCH 01/43] Fix safeWrite bypass by a concurrent write(int) writeSingleByte() switched the shared field ignoreSafeWrite on around its own write. A write(byte[]) on another thread that took the lock inside that window skipped the safeWrite clone and stored the caller's array by reference, so a later change to the array reached the reader. The skip is now a parameter of the write path instead of a field. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VBFFnrhtvXiUeyxjmUc4R2 --- .../ladenthin/streambuffer/StreamBuffer.java | 40 +++++++------ .../streambuffer/StreamBufferTest.java | 59 +++++++++++++++++++ 2 files changed, 81 insertions(+), 18 deletions(-) diff --git a/src/main/java/net/ladenthin/streambuffer/StreamBuffer.java b/src/main/java/net/ladenthin/streambuffer/StreamBuffer.java index 54ebe7e1..5e0f51d3 100644 --- a/src/main/java/net/ladenthin/streambuffer/StreamBuffer.java +++ b/src/main/java/net/ladenthin/streambuffer/StreamBuffer.java @@ -99,19 +99,11 @@ public class StreamBuffer implements Closeable { * A flag to enable a safe write. If safe write is enabled, modifiable byte * arrays are cloned before they are written (put) into the FIFO. Benefit: * It cost more performance to clone a byte array, but the content is - * immutable. This may be revoked by {@link #ignoreSafeWrite}, for example a - * byte array was created internally. + * immutable. Internally created arrays that never escape (see + * {@link #writeSingleByte(int)}) are not cloned. */ private volatile boolean safeWrite = false; - /** - * A flag to disable the {@link StreamBuffer#safeWrite}. I. e. to write a byte array from - * the trim method. - * It should be used if the reference to the buffer deque is not reachable out of the scope. - * It is possible to ignore the safeWrite flag to prevent not necessary clone operations. - */ - private volatile boolean ignoreSafeWrite = false; - /** * The maximum buffer elements. A number of maximum elements to invoke the * trim method. If the buffer contains more elements as the maximum, the @@ -1021,13 +1013,8 @@ private static boolean hasNoMissingBytes(int missingBytes) { * @throws IOException if the stream is closed */ private void writeSingleByte(final int b) throws IOException { - try { - ignoreSafeWrite = true; - final byte[] single = new byte[] {(byte) b}; - writeFromArray(single, 0, single.length); - } finally { - ignoreSafeWrite = false; - } + final byte[] single = new byte[] {(byte) b}; + writeFromArray(single, 0, single.length, false); } /** @@ -1040,6 +1027,23 @@ private void writeSingleByte(final int b) throws IOException { * @throws IOException if the stream is closed */ private void writeFromArray(final byte[] b, final int off, final int len) throws IOException { + writeFromArray(b, off, len, true); + } + + /** + * Shared write path of {@link #writeFromArray(byte[], int, int)} and {@link #writeSingleByte(int)}. + * Whether the {@link #safeWrite} clone may be skipped is a parameter rather than a field: a field + * shared between threads let a concurrent {@code write(int)} switch the clone off for another + * thread's {@code write(byte[])}, which then stored the caller's array by reference. + * + * @param b the source array + * @param off the offset in the source array + * @param len the number of bytes to write + * @param cloneOnSafeWrite {@code false} if {@code b} was created internally and never escapes + * @throws IOException if the stream is closed + */ + private void writeFromArray(final byte[] b, final int off, final int len, final boolean cloneOnSafeWrite) + throws IOException { if (!validateOffsetAndLengthToWrite(b, off, len)) { return; } @@ -1050,7 +1054,7 @@ private void writeFromArray(final byte[] b, final int off, final int len) throws synchronized (bufferLock) { if (off == 0 && b.length == len) { // add the full byte[] to the buffer - if (tmpSafeWrite && !ignoreSafeWrite) { + if (tmpSafeWrite && cloneOnSafeWrite) { buffer.add(b.clone()); } else { buffer.add(b); diff --git a/src/test/java/net/ladenthin/streambuffer/StreamBufferTest.java b/src/test/java/net/ladenthin/streambuffer/StreamBufferTest.java index 062924c5..bc1b9331 100644 --- a/src/test/java/net/ladenthin/streambuffer/StreamBufferTest.java +++ b/src/test/java/net/ladenthin/streambuffer/StreamBufferTest.java @@ -1371,6 +1371,65 @@ public void concurrentReadWrite_stressTest_noCrashOrInconsistency() throws Excep // assert assertArrayEquals(written, read, "Read data should match written data"); } + + @DisplayName("write(byte[]) with safeWrite: a concurrent write(int) does not bypass the clone") + @Test + public void safeWrite_concurrentSingleByteWrite_arrayStillCloned() throws Exception { + // arrange — trim disabled so the deque keeps the caller's array reference if it is not cloned + final StreamBuffer sb = new StreamBuffer(); + sb.setSafeWrite(true); + sb.setMaxBufferElements(0); + final OutputStream os = sb.getOutputStream(); + final InputStream is = sb.getInputStream(); + final byte original = 1; + final byte mutated = 2; + final AtomicBoolean stop = new AtomicBoolean(); + final AtomicInteger mutatedBytesRead = new AtomicInteger(); + final net.jodah.concurrentunit.Waiter waiter = new net.jodah.concurrentunit.Waiter(); + + Thread singleByteWriter = new Thread(() -> { + try { + while (!stop.get()) { + os.write(0); + } + } catch (IOException e) { + waiter.fail(e); + } + }); + Thread reader = new Thread(() -> { + try { + final byte[] chunk = new byte[4096]; + int n; + while ((n = is.read(chunk, 0, 1)) != -1) { + for (int i = 0; i < n; i++) { + if (chunk[i] == mutated) { + mutatedBytesRead.incrementAndGet(); + } + } + } + } catch (IOException e) { + waiter.fail(e); + } + }); + + // act — mutate each array right after write() returned; safeWrite promises a private copy + singleByteWriter.start(); + reader.start(); + for (int i = 0; i < 200_000; i++) { + final byte[] data = new byte[8]; + Arrays.fill(data, original); + os.write(data); + Arrays.fill(data, mutated); + } + stop.set(true); + singleByteWriter.join(); + os.close(); + reader.join(); + waiter.resume(); + + // assert + assertThat("bytes changed after write() reached the reader", mutatedBytesRead.get(), is(0)); + } } @Nested From 38868b8e638b268f4b3e710a754298efb960123b Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 17 Oct 2026 08:42:46 +0000 Subject: [PATCH 02/43] Add the bug-hunt ledgers: found bugs and checked classes BUGHUNT-FOUND.md records every bug found on this working branch with its file, severity, reproduction test, status and commit. BUGHUNT-CHECKED.md lists every production class that was read in full, with the blob hash it was checked at, so a later pass re-checks only files that changed. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VBFFnrhtvXiUeyxjmUc4R2 --- BUGHUNT-CHECKED.md | 13 +++++++++++++ BUGHUNT-FOUND.md | 38 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 51 insertions(+) create mode 100644 BUGHUNT-CHECKED.md create mode 100644 BUGHUNT-FOUND.md diff --git a/BUGHUNT-CHECKED.md b/BUGHUNT-CHECKED.md new file mode 100644 index 00000000..3f6a187c --- /dev/null +++ b/BUGHUNT-CHECKED.md @@ -0,0 +1,13 @@ + +# 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 diff --git a/BUGHUNT-FOUND.md b/BUGHUNT-FOUND.md new file mode 100644 index 00000000..a6c9756e --- /dev/null +++ b/BUGHUNT-FOUND.md @@ -0,0 +1,38 @@ + +# 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 — *unsicher / nur beschrieben* + +## 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. +- **Commit:** streambuffer `fb371e0` + + +### 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. +- **Reproduktion:** keine geschrieben (Designfrage). +- **Status:** unsicher / nur beschrieben +- **Commit:** – + +## Offene Verdachte ohne Fund-ID + +- keine From 8170864604d9a020ed4585c341e57805ea203796 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 17 Oct 2026 10:55:10 +0000 Subject: [PATCH 03/43] Mark F03 as a design decision in the bug-hunt ledger Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VBFFnrhtvXiUeyxjmUc4R2 --- BUGHUNT-FOUND.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/BUGHUNT-FOUND.md b/BUGHUNT-FOUND.md index a6c9756e..4a785720 100644 --- a/BUGHUNT-FOUND.md +++ b/BUGHUNT-FOUND.md @@ -9,7 +9,7 @@ Repos plus eins. Geprüfte Klassen ohne Fund stehen in [`BUGHUNT-CHECKED.md`](BU ## Übersicht - [F02](#f02) — mittel — *gefixt* -- [F03](#f03) — mittel — *unsicher / nur beschrieben* +- [F03](#f03) — mittel — *Designentscheidung, offen für den Nutzer* ## Funde @@ -30,7 +30,7 @@ Repos plus eins. Geprüfte Klassen ohne Fund stehen in [`BUGHUNT-CHECKED.md`](BU - **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. - **Reproduktion:** keine geschrieben (Designfrage). -- **Status:** unsicher / nur beschrieben +- **Status:** Designentscheidung, offen für den Nutzer – der Loop fasst diesen Eintrag nicht an (README „second wait phase“ und die jcstress-Tests zeigen, dass das Warten auf alle `len` Bytes gewollt ist). Ändern nur auf ausdrückliche Entscheidung des Nutzers. - **Commit:** – ## Offene Verdachte ohne Fund-ID From 4c9c04dd4e48a8f9a96c244ab3594226868d57cb Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 17 Oct 2026 21:51:34 +0000 Subject: [PATCH 04/43] Update the bug-hunt ledger Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VBFFnrhtvXiUeyxjmUc4R2 --- BUGHUNT-CHECKED.md | 1 + 1 file changed, 1 insertion(+) diff --git a/BUGHUNT-CHECKED.md b/BUGHUNT-CHECKED.md index 3f6a187c..1d79b506 100644 --- a/BUGHUNT-CHECKED.md +++ b/BUGHUNT-CHECKED.md @@ -11,3 +11,4 @@ Ergebnisse: `kein Fund`, `widerlegt` (Verdacht geprüft, Code korrekt), `unsiche - `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. From ceafab5ee8168f7460bf39f76fcc49819f62a7be Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 18 Oct 2026 00:56:37 +0000 Subject: [PATCH 05/43] Update the bug-hunt ledger Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VBFFnrhtvXiUeyxjmUc4R2 --- BUGHUNT-CHECKED.md | 1 + 1 file changed, 1 insertion(+) diff --git a/BUGHUNT-CHECKED.md b/BUGHUNT-CHECKED.md index 1d79b506..adfdcb1f 100644 --- a/BUGHUNT-CHECKED.md +++ b/BUGHUNT-CHECKED.md @@ -12,3 +12,4 @@ Ergebnisse: `kein Fund`, `widerlegt` (Verdacht geprüft, Code korrekt), `unsiche - `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`) · `5e0f51d` · 2026-10-18 · kein Fund — `recordReadStatistics` (1 Byte bzw. je kopiertem Block) und `totalBytesWritten`/`maxObservedBytes` laufen unter `bufferLock`, den `trim()` für seine ganze Dauer hält; das globale Flag `isTrimRunning` kann deshalb nur die eigenen internen Lese-/Schreibvorgänge von `trim` ausblenden, nie die eines anderen Threads. `skip` ist `InputStream`s Vorgabe über `read(byte[])` und wird dort gezählt; das Lesen aus `trim` heraus nutzt den reentranten Monitor desselben Threads. From 27aaed62ffeb8fd2aedd68051e7c302fbbc085f1 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 18 Oct 2026 01:34:36 +0000 Subject: [PATCH 06/43] Keep the buffered byte count constant while trim consolidates trim() drained the buffer through its own input stream and wrote the bytes back, so the volatile availableBytes fell to zero and rose again under bufferLock. waitForAtLeast reads it twice without the lock and could return fewer bytes than requested on an open stream; read() then reported the end of a stream that still held data. trim now copies the entries directly and leaves the count untouched. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VBFFnrhtvXiUeyxjmUc4R2 --- BUGHUNT-CHECKED.md | 1 + BUGHUNT-FOUND.md | 15 ++++ README.md | 4 +- .../ladenthin/streambuffer/StreamBuffer.java | 79 ++++++++----------- .../streambuffer/StreamBufferTest.java | 41 ++++++++++ 5 files changed, 91 insertions(+), 49 deletions(-) diff --git a/BUGHUNT-CHECKED.md b/BUGHUNT-CHECKED.md index adfdcb1f..f0cc9bee 100644 --- a/BUGHUNT-CHECKED.md +++ b/BUGHUNT-CHECKED.md @@ -13,3 +13,4 @@ Ergebnisse: `kein Fund`, `widerlegt` (Verdacht geprüft, Code korrekt), `unsiche - `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`) · `5e0f51d` · 2026-10-18 · kein Fund — `recordReadStatistics` (1 Byte bzw. je kopiertem Block) und `totalBytesWritten`/`maxObservedBytes` laufen unter `bufferLock`, den `trim()` für seine ganze Dauer hält; das globale Flag `isTrimRunning` kann deshalb nur die eigenen internen Lese-/Schreibvorgänge von `trim` ausblenden, nie die eines anderen Threads. `skip` ist `InputStream`s Vorgabe über `read(byte[])` und wird dort gezählt; das Lesen aus `trim` heraus nutzt den reentranten Monitor desselben Threads. +- `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. diff --git a/BUGHUNT-FOUND.md b/BUGHUNT-FOUND.md index 4a785720..7068c620 100644 --- a/BUGHUNT-FOUND.md +++ b/BUGHUNT-FOUND.md @@ -10,6 +10,7 @@ Repos plus eins. Geprüfte Klassen ohne Fund stehen in [`BUGHUNT-CHECKED.md`](BU - [F02](#f02) — mittel — *gefixt* - [F03](#f03) — mittel — *Designentscheidung, offen für den Nutzer* +- [F73](#f73) — hoch — *gefixt* ## Funde @@ -33,6 +34,20 @@ Repos plus eins. Geprüfte Klassen ohne Fund stehen in [`BUGHUNT-CHECKED.md`](BU - **Status:** Designentscheidung, offen für den Nutzer – der Loop fasst diesen Eintrag nicht an (README „second wait phase“ und die jcstress-Tests zeigen, dass das Warten auf alle `len` Bytes gewollt ist). Ändern nur auf ausdrückliche Entscheidung des Nutzers. - **Commit:** – + +### 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. +- **Status:** gefixt +- **Commit:** (folgt) + ## Offene Verdachte ohne Fund-ID - keine diff --git a/README.md b/README.md index 38203273..9013a598 100644 --- a/README.md +++ b/README.md @@ -168,7 +168,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 +209,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(); diff --git a/src/main/java/net/ladenthin/streambuffer/StreamBuffer.java b/src/main/java/net/ladenthin/streambuffer/StreamBuffer.java index 5e0f51d3..95bac9a0 100644 --- a/src/main/java/net/ladenthin/streambuffer/StreamBuffer.java +++ b/src/main/java/net/ladenthin/streambuffer/StreamBuffer.java @@ -467,67 +467,52 @@ private void signalModification() { * write operation. The method checks itself if the buffer should be trimmed * or not. * MUST be called inside {@code synchronized(bufferLock)}. - * Sets {@link #isTrimRunning} volatile flag to prevent statistics updates during internal I/O. + * Sets the {@link #isTrimRunning} volatile flag while it runs. The buffered byte count + * ({@link #availableBytes}) stays constant throughout. * Respects {@link #maxAllocationSize} limit when allocating byte arrays. */ - // Non-atomic update on the volatile availableBytes field at the - // "availableBytes += chunk.length" line is safe because the entire method - // body runs under bufferLock (see @GuardedBy and the synchronized block - // in the caller). volatile guarantees visibility to readers outside the - // lock; bufferLock guarantees atomicity of the read-modify-write. + // Non-atomic update on the volatile positionAtCurrentBufferEntry field is + // safe because the entire method body runs under bufferLock (see @GuardedBy + // and the synchronized block in the caller). volatile guarantees visibility + // to readers outside the lock; bufferLock guarantees atomicity of the + // read-modify-write. @SuppressWarnings("NonAtomicVolatileUpdate") @GuardedBy("bufferLock") - private void trim() throws IOException { + private void trim() { if (shouldTrim()) { isTrimRunning = true; try { releaseTrimStartSignals(); /* - * Need to store more bufs, may it is not possible to read out all - * data at once. The available method only returns an int value - * instead a long value. Store all read parts of the full buffer in - * a deque. + * Copy the buffered bytes into chunks of at most maxAllocationSize + * directly from the FIFO. availableBytes is deliberately left untouched: + * waitForAtLeast(long) and available() read it without bufferLock, and + * draining it to zero and filling it up again (as reading through the + * input stream did) let a waiter observe the intermediate count, e.g. + * a read() reporting the end of an open stream that still held data. */ final Deque tmpBuffer = new ArrayDeque<>(); - - int available; - // empty the current buffer, read out all bytes - while ((available = is.available()) > 0) { - // Limit each allocation to maxAllocationSize - final int toAllocate = (int) Math.min(available, maxAllocationSize); - final byte[] buf = new byte[toAllocate]; - // read out of the buffer - // and store the result to the tmpBuffer - int read = is.read(buf); - // should never happen - assert read == toAllocate : "Read not enough bytes from buffer."; - tmpBuffer.add(buf); - } - /* - * Write all previously read parts back to the buffer directly. - * We are already holding bufferLock and the chunks were - * just produced internally, so going through SBOutputStream#write - * is unnecessary and would fail at requireNonClosed() if close() - * is invoked concurrently — discarding tmpBuffer and losing - * every byte that trim already drained. - */ - while (!tmpBuffer.isEmpty()) { - // Deque.pollFirst() may return null per the JDK contract; the - // !isEmpty guard above makes it non-null here in practice, but - // neither NullAway's flow analyzer nor the Checker Framework - // Nullness Checker bridge that loop-guard reasoning, so we make - // the non-null contract explicit. - final byte[] chunk = tmpBuffer.pollFirst(); - if (chunk == null) { - throw new java.util.NoSuchElementException( - "tmpBuffer.pollFirst() returned null despite a successful isEmpty() check" - + " (remaining=" + tmpBuffer.size() - + ", indicates a concurrent modification of tmpBuffer)."); + long remaining = availableBytes; + while (remaining > 0) { + final int toAllocate = (int) Math.min(remaining, maxAllocationSize); + final byte[] chunk = new byte[toAllocate]; + int filled = 0; + while (filled < toAllocate) { + final byte[] first = buffer.getFirst(); + final int toCopy = Math.min(first.length - positionAtCurrentBufferEntry, toAllocate - filled); + System.arraycopy(first, positionAtCurrentBufferEntry, chunk, filled, toCopy); + filled += toCopy; + positionAtCurrentBufferEntry += toCopy; + if (positionAtCurrentBufferEntry == first.length) { + buffer.pollFirst(); + positionAtCurrentBufferEntry = 0; + } } - buffer.add(chunk); - availableBytes += chunk.length; + tmpBuffer.add(chunk); + remaining -= toAllocate; } + buffer.addAll(tmpBuffer); } finally { isTrimRunning = false; releaseTrimEndSignals(); diff --git a/src/test/java/net/ladenthin/streambuffer/StreamBufferTest.java b/src/test/java/net/ladenthin/streambuffer/StreamBufferTest.java index bc1b9331..bd1f4f81 100644 --- a/src/test/java/net/ladenthin/streambuffer/StreamBufferTest.java +++ b/src/test/java/net/ladenthin/streambuffer/StreamBufferTest.java @@ -2084,6 +2084,47 @@ public void concurrentTrimAndWrite_noCrashOrCorruption() throws Exception { assertThat(is.available(), is(0)); assertThat(sb.isClosed(), is(true)); } + + @DisplayName("waitForAtLeast(): a concurrent trim never makes it return fewer bytes than requested") + @Test + @Timeout(60) + public void waitForAtLeast_concurrentTrim_neverReturnsFewerBytesThanRequested() throws Exception { + // arrange — nobody reads, so the buffered byte count can only grow; a trim consolidates + // 1000 single-byte entries at a time while the waiter reads the count without the lock + final StreamBuffer sb = new StreamBuffer(); + sb.setMaxBufferElements(1_000); + final OutputStream os = sb.getOutputStream(); + final AtomicReference violation = new AtomicReference<>(); + + Thread waiter = new Thread(() -> { + try { + while (violation.get() == null && !sb.isClosed()) { + final long seen = sb.getAvailableBytesExact(); + if (seen > 0) { + final long returned = sb.waitForAtLeast(seen); + if (returned < seen) { + violation.compareAndSet( + null, + "waitForAtLeast(" + seen + ") returned " + returned + " on an open stream"); + } + } + } + } catch (InterruptedException e) { + Thread.currentThread().interrupt(); + } + }); + + // act + waiter.start(); + for (int i = 0; i < 2_000_000 && violation.get() == null; i++) { + os.write(1); + } + os.close(); + waiter.join(); + + // assert + assertThat(violation.get(), is((String) null)); + } } @Nested From 6f2107b7e64757ced162a744280d9f0ff6954829 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 18 Oct 2026 01:34:36 +0000 Subject: [PATCH 07/43] Record the commit of F73 in the bug-hunt ledger Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VBFFnrhtvXiUeyxjmUc4R2 --- BUGHUNT-FOUND.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/BUGHUNT-FOUND.md b/BUGHUNT-FOUND.md index 7068c620..dd7c4613 100644 --- a/BUGHUNT-FOUND.md +++ b/BUGHUNT-FOUND.md @@ -46,7 +46,7 @@ Repos plus eins. Geprüfte Klassen ohne Fund stehen in [`BUGHUNT-CHECKED.md`](BU - **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. - **Status:** gefixt -- **Commit:** (folgt) +- **Commit:** streambuffer `89d2173` ## Offene Verdachte ohne Fund-ID From c92a564d8c06c7c89f059551db8b2309dc20c6e8 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 18 Oct 2026 05:52:47 +0000 Subject: [PATCH 08/43] Update the bug-hunt ledger Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VBFFnrhtvXiUeyxjmUc4R2 --- BUGHUNT-CHECKED.md | 1 + 1 file changed, 1 insertion(+) diff --git a/BUGHUNT-CHECKED.md b/BUGHUNT-CHECKED.md index f0cc9bee..35689a43 100644 --- a/BUGHUNT-CHECKED.md +++ b/BUGHUNT-CHECKED.md @@ -14,3 +14,4 @@ Ergebnisse: `kein Fund`, `widerlegt` (Verdacht geprüft, Code korrekt), `unsiche - `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`) · `5e0f51d` · 2026-10-18 · kein Fund — `recordReadStatistics` (1 Byte bzw. je kopiertem Block) und `totalBytesWritten`/`maxObservedBytes` laufen unter `bufferLock`, den `trim()` für seine ganze Dauer hält; das globale Flag `isTrimRunning` kann deshalb nur die eigenen internen Lese-/Schreibvorgänge von `trim` ausblenden, nie die eines anderen Threads. `skip` ist `InputStream`s Vorgabe über `read(byte[])` und wird dort gezählt; das Lesen aus `trim` heraus nutzt den reentranten Monitor desselben Threads. - `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`). From 3250214ad8c4f709cd2d98ad858c26161f9c08c9 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 18 Oct 2026 06:55:58 +0000 Subject: [PATCH 09/43] Update the bug-hunt ledger Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VBFFnrhtvXiUeyxjmUc4R2 --- BUGHUNT-CHECKED.md | 1 + BUGHUNT-FOUND.md | 12 ++++++++++++ 2 files changed, 13 insertions(+) diff --git a/BUGHUNT-CHECKED.md b/BUGHUNT-CHECKED.md index 35689a43..f69e0b33 100644 --- a/BUGHUNT-CHECKED.md +++ b/BUGHUNT-CHECKED.md @@ -15,3 +15,4 @@ Ergebnisse: `kein Fund`, `widerlegt` (Verdacht geprüft, Code korrekt), `unsiche - `src/main/java/net/ladenthin/streambuffer/StreamBuffer.java` (Schnittstelle Lese-/Schreibpfad ↔ Statistik und `trim`) · `5e0f51d` · 2026-10-18 · kein Fund — `recordReadStatistics` (1 Byte bzw. je kopiertem Block) und `totalBytesWritten`/`maxObservedBytes` laufen unter `bufferLock`, den `trim()` für seine ganze Dauer hält; das globale Flag `isTrimRunning` kann deshalb nur die eigenen internen Lese-/Schreibvorgänge von `trim` ausblenden, nie die eines anderen Threads. `skip` ist `InputStream`s Vorgabe über `read(byte[])` und wird dort gezählt; das Lesen aus `trim` heraus nutzt den reentranten Monitor desselben Threads. - `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`) diff --git a/BUGHUNT-FOUND.md b/BUGHUNT-FOUND.md index dd7c4613..be06ecc7 100644 --- a/BUGHUNT-FOUND.md +++ b/BUGHUNT-FOUND.md @@ -11,6 +11,7 @@ Repos plus eins. Geprüfte Klassen ohne Fund stehen in [`BUGHUNT-CHECKED.md`](BU - [F02](#f02) — mittel — *gefixt* - [F03](#f03) — mittel — *Designentscheidung, offen für den Nutzer* - [F73](#f73) — hoch — *gefixt* +- [F110](#f110) — niedrig — *nur beschrieben* ## Funde @@ -48,6 +49,17 @@ Repos plus eins. Geprüfte Klassen ohne Fund stehen in [`BUGHUNT-CHECKED.md`](BU - **Status:** gefixt - **Commit:** streambuffer `89d2173` +### 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 (`89d2173`), 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. +- **Fix:** keiner. Vorschlag: den Absatz „SAFETY GUARANTEE …“ samt Beispiel auf den verbliebenen Zweck kürzen (`available()` meldet höchstens `Integer.MAX_VALUE`, auch wenn mehr als 2 GiB gepuffert sind). +- **Reproduktion:** keine (reine Doku-Abweichung). +- **Rot-Grün-Nachweis:** entfällt. +- **Status:** nur beschrieben (Nutzerregel vom 2026-10-17: gefixt und committet wird nur mit Test; eine reine Doku-Abweichung hat keinen, wie F35) +- **Commit:** – + ## Offene Verdachte ohne Fund-ID - keine From bce62681e6e31799e27f3a10a38e0ba6a69aef41 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 18 Oct 2026 07:00:28 +0000 Subject: [PATCH 10/43] Update the bug-hunt ledger Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VBFFnrhtvXiUeyxjmUc4R2 --- BUGHUNT-CHECKED.md | 1 + 1 file changed, 1 insertion(+) diff --git a/BUGHUNT-CHECKED.md b/BUGHUNT-CHECKED.md index f69e0b33..76830b5d 100644 --- a/BUGHUNT-CHECKED.md +++ b/BUGHUNT-CHECKED.md @@ -16,3 +16,4 @@ Ergebnisse: `kein Fund`, `widerlegt` (Verdacht geprüft, Code korrekt), `unsiche - `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. From 6a13949d4a8fe6103a349234d060b297a4e63808 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 18 Oct 2026 08:14:00 +0000 Subject: [PATCH 11/43] Update the bug-hunt ledger Add the missing anchors the overview links point at. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VBFFnrhtvXiUeyxjmUc4R2 --- BUGHUNT-FOUND.md | 1 + 1 file changed, 1 insertion(+) diff --git a/BUGHUNT-FOUND.md b/BUGHUNT-FOUND.md index be06ecc7..d2fb499c 100644 --- a/BUGHUNT-FOUND.md +++ b/BUGHUNT-FOUND.md @@ -49,6 +49,7 @@ Repos plus eins. Geprüfte Klassen ohne Fund stehen in [`BUGHUNT-CHECKED.md`](BU - **Status:** gefixt - **Commit:** streambuffer `89d2173` + ### 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`) From e6d08d81bdc97eac5f805e992070cb33c3363819 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 18 Oct 2026 09:47:53 +0000 Subject: [PATCH 12/43] Update the bug-hunt ledger Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VBFFnrhtvXiUeyxjmUc4R2 --- BUGHUNT-CHECKED.md | 1 + 1 file changed, 1 insertion(+) diff --git a/BUGHUNT-CHECKED.md b/BUGHUNT-CHECKED.md index 76830b5d..4b2c42b9 100644 --- a/BUGHUNT-CHECKED.md +++ b/BUGHUNT-CHECKED.md @@ -17,3 +17,4 @@ Ergebnisse: `kein Fund`, `widerlegt` (Verdacht geprüft, Code korrekt), `unsiche - `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 From 088f1ea1acdeac76f7023e90ac7243878de178ca Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 18 Oct 2026 11:23:23 +0000 Subject: [PATCH 13/43] Update the bug-hunt ledger Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VBFFnrhtvXiUeyxjmUc4R2 --- BUGHUNT-CHECKED.md | 1 + BUGHUNT-FOUND.md | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/BUGHUNT-CHECKED.md b/BUGHUNT-CHECKED.md index 4b2c42b9..a75ceadd 100644 --- a/BUGHUNT-CHECKED.md +++ b/BUGHUNT-CHECKED.md @@ -18,3 +18,4 @@ Ergebnisse: `kein Fund`, `widerlegt` (Verdacht geprüft, Code korrekt), `unsiche - `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). Offener Verdacht: `write` parallel zu `close` (Prüfung außerhalb des Locks), siehe BUGHUNT-FOUND.md. diff --git a/BUGHUNT-FOUND.md b/BUGHUNT-FOUND.md index d2fb499c..5021b098 100644 --- a/BUGHUNT-FOUND.md +++ b/BUGHUNT-FOUND.md @@ -63,4 +63,4 @@ Repos plus eins. Geprüfte Klassen ohne Fund stehen in [`BUGHUNT-CHECKED.md`](BU ## Offene Verdachte ohne Fund-ID -- keine +- 2026-10-18 – `write` gleichzeitig mit `close` aus einem anderen Thread (`StreamBuffer.java:1035` `requireNonClosed` außerhalb von `bufferLock`, `closeAll` ohne Lock): ein `write`, der die Prüfung vor `close()` passiert, hängt seine Bytes erst danach unter dem Lock an und kehrt normal zurück. Ein Leser, der dazwischen `waitForAtLeast` mit `streamClosed == true` und `availableBytes == 0` durchläuft, meldet EOF; die Bytes liegen danach im Puffer (ein weiteres `read()` nach `-1` lieferte sie). Folge: ein erfolgreich zurückgekehrter `write` erreicht einen Leser, der bei `-1` aufhört, nie. Fix wäre `requireNonClosed` innerhalb von `bufferLock` und `streamClosed = true` unter demselben Lock (Sichtbarkeit über die beiden `volatile` Felder bleibt geordnet). Nicht umgesetzt: kein deterministischer Test ohne neue Naht zwischen Prüfung und Lock (das Fenster ist eine Handvoll Anweisungen), und der Fix berührt die OpenJML-Spezifikation (`src/main/jml`) und die PIT-Schwelle 100. Ob ein `write` parallel zu `close` überhaupt unterstützt sein soll, entscheidet der Nutzer. From 5540fb0e6bc799f39428c6569337ff14c04bde78 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 18 Oct 2026 18:37:13 +0000 Subject: [PATCH 14/43] Correct the clampToMaxInt Javadoc and the maxAllocationSize default The Javadoc of clampToMaxInt still explained the clamp through the trim() loop that read the buffer back through its own input stream; since 89d2173 trim() copies straight from the deque and the only caller is available(). The README named Integer.MAX_VALUE as the maxAllocationSize default; since f88be77 it is MAX_ARRAY_LENGTH (Integer.MAX_VALUE - 8), and the setter caps larger values to it. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VBFFnrhtvXiUeyxjmUc4R2 --- BUGHUNT-FOUND.md | 12 +++++---- README.md | 2 +- .../ladenthin/streambuffer/StreamBuffer.java | 26 +++---------------- 3 files changed, 12 insertions(+), 28 deletions(-) diff --git a/BUGHUNT-FOUND.md b/BUGHUNT-FOUND.md index 5021b098..0edd016d 100644 --- a/BUGHUNT-FOUND.md +++ b/BUGHUNT-FOUND.md @@ -11,7 +11,7 @@ Repos plus eins. Geprüfte Klassen ohne Fund stehen in [`BUGHUNT-CHECKED.md`](BU - [F02](#f02) — mittel — *gefixt* - [F03](#f03) — mittel — *Designentscheidung, offen für den Nutzer* - [F73](#f73) — hoch — *gefixt* -- [F110](#f110) — niedrig — *nur beschrieben* +- [F110](#f110) — niedrig — *gefixt (Doku)* ## Funde @@ -55,10 +55,12 @@ Repos plus eins. Geprüfte Klassen ohne Fund stehen in [`BUGHUNT-CHECKED.md`](BU - **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 (`89d2173`), 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. -- **Fix:** keiner. Vorschlag: den Absatz „SAFETY GUARANTEE …“ samt Beispiel auf den verbliebenen Zweck kürzen (`available()` meldet höchstens `Integer.MAX_VALUE`, auch wenn mehr als 2 GiB gepuffert sind). -- **Reproduktion:** keine (reine Doku-Abweichung). -- **Rot-Grün-Nachweis:** entfällt. -- **Status:** nur beschrieben (Nutzerregel vom 2026-10-17: gefixt und committet wird nur mit Test; eine reine Doku-Abweichung hat keinen, wie F35) +- **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 `89d2173` (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:** – ## Offene Verdachte ohne Fund-ID diff --git a/README.md b/README.md index 9013a598..277b4fa6 100644 --- a/README.md +++ b/README.md @@ -243,7 +243,7 @@ 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. diff --git a/src/main/java/net/ladenthin/streambuffer/StreamBuffer.java b/src/main/java/net/ladenthin/streambuffer/StreamBuffer.java index 95bac9a0..0767b82c 100644 --- a/src/main/java/net/ladenthin/streambuffer/StreamBuffer.java +++ b/src/main/java/net/ladenthin/streambuffer/StreamBuffer.java @@ -631,28 +631,10 @@ boolean shouldTrim() { * from {@code value > MAX_VALUE} vs {@code value >= MAX_VALUE} (both return * the same result when {@code value == MAX_VALUE}). * - * SAFETY GUARANTEE FOR LARGE BUFFERS: - * - * This method handles the type mismatch between: - * - {@link #availableBytes}: volatile long (0 to 2^63-1, supports future-proof large buffers) - * - InputStream.available(): int contract (0 to 2^31-1, ~2.1 billion) - * - * If availableBytes ever exceeds Integer.MAX_VALUE (e.g., 5GB+ of buffered data): - * 1. This method returns Integer.MAX_VALUE (~2.1GB) - * 2. The trim() loop reads at most maxAllocationSize (≤ MAX_ARRAY_LENGTH) bytes per iteration - * 3. Loop condition (available > 0) allows continuation - * 4. Next iteration calls available() again, reads remaining bytes - * 5. Process repeats until all availableBytes are consolidated - * - * Result: NO DATA LOSS, NO OVERFLOW - all data is processed correctly. - * - * EXAMPLE FLOW (5GB data): - * Iteration 1: available() → clamped to 2,147,483,647 bytes → read and consolidate - * Iteration 2: available() → clamped to remaining bytes → read and consolidate - * ... continues until availableBytes == 0 - * - * This design allows StreamBuffer to theoretically support buffers larger than 2GB - * while maintaining compatibility with the InputStream API contract that uses int. + *

Used by {@code available()}: {@link #availableBytes} is a {@code long} and can exceed + * {@link Integer#MAX_VALUE} when more than 2 GiB are buffered, while + * {@link java.io.InputStream#available()} returns an {@code int}. Such a value is reported as + * {@link Integer#MAX_VALUE}; the buffered data itself is unaffected. * * Package-private for direct unit testing. */ From ff4aaa45ce70f1e1ef97bc4077813ad80563ee31 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 18 Oct 2026 18:37:13 +0000 Subject: [PATCH 15/43] Record the commit of F110 in the bug-hunt ledger Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VBFFnrhtvXiUeyxjmUc4R2 --- BUGHUNT-FOUND.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/BUGHUNT-FOUND.md b/BUGHUNT-FOUND.md index 0edd016d..b9083b6a 100644 --- a/BUGHUNT-FOUND.md +++ b/BUGHUNT-FOUND.md @@ -61,7 +61,7 @@ Repos plus eins. Geprüfte Klassen ohne Fund stehen in [`BUGHUNT-CHECKED.md`](BU - **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:** – +- **Commit:** 3fc6dba ## Offene Verdachte ohne Fund-ID From 6ece27039503396572f04c9521f4df5b08583224 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 18 Oct 2026 20:06:27 +0000 Subject: [PATCH 16/43] Check streamClosed under bufferLock so a write never lands after close A write that raced close() from another thread passed requireNonClosed() before taking bufferLock, while closeAll() set the flag without the lock. The write could then append after close() had returned and still return normally, while a reader in between had already reported the end of the stream. The check now runs under bufferLock and closeAll() sets the flag under it, so such a write is either buffered before the close or fails with "Stream closed". The test parks a second writer on the buffer lock from the trim-start signal and closes while it waits; it fails without the change. A jcstress test for the same race is added for the opt-in profile run. Also document that read(byte[], off, len) waits for all len bytes, the design since the first version, and how to read what is available. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VBFFnrhtvXiUeyxjmUc4R2 --- BUGHUNT-FOUND.md | 26 ++++++- README.md | 13 +++- TODO.md | 16 ++++ .../ladenthin/streambuffer/StreamBuffer.java | 27 ++++++- .../streambuffer/StreamBufferTest.java | 74 +++++++++++++++++++ .../jcstress/WriteRacingCloseRace.java | 68 +++++++++++++++++ 6 files changed, 216 insertions(+), 8 deletions(-) create mode 100644 src/test/java/net/ladenthin/streambuffer/jcstress/WriteRacingCloseRace.java diff --git a/BUGHUNT-FOUND.md b/BUGHUNT-FOUND.md index b9083b6a..585576a1 100644 --- a/BUGHUNT-FOUND.md +++ b/BUGHUNT-FOUND.md @@ -9,9 +9,10 @@ Repos plus eins. Geprüfte Klassen ohne Fund stehen in [`BUGHUNT-CHECKED.md`](BU ## Übersicht - [F02](#f02) — mittel — *gefixt* -- [F03](#f03) — mittel — *Designentscheidung, offen für den Nutzer* +- [F03](#f03) — mittel — *Designentscheidung, dokumentiert* - [F73](#f73) — hoch — *gefixt* - [F110](#f110) — niedrig — *gefixt (Doku)* +- [F149](#f149) — mittel — *gefixt* ## Funde @@ -31,8 +32,10 @@ Repos plus eins. Geprüfte Klassen ohne Fund stehen in [`BUGHUNT-CHECKED.md`](BU - **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. -- **Reproduktion:** keine geschrieben (Designfrage). -- **Status:** Designentscheidung, offen für den Nutzer – der Loop fasst diesen Eintrag nicht an (README „second wait phase“ und die jcstress-Tests zeigen, dass das Warten auf alle `len` Bytes gewollt ist). Ändern nur auf ausdrückliche Entscheidung des Nutzers. +- **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:** – @@ -63,6 +66,21 @@ Repos plus eins. Geprüfte Klassen ohne Fund stehen in [`BUGHUNT-CHECKED.md`](BU - **Status:** gefixt (Doku) - **Commit:** 3fc6dba + +### 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“. +- **Status:** gefixt +- **Commit:** – + ## Offene Verdachte ohne Fund-ID -- 2026-10-18 – `write` gleichzeitig mit `close` aus einem anderen Thread (`StreamBuffer.java:1035` `requireNonClosed` außerhalb von `bufferLock`, `closeAll` ohne Lock): ein `write`, der die Prüfung vor `close()` passiert, hängt seine Bytes erst danach unter dem Lock an und kehrt normal zurück. Ein Leser, der dazwischen `waitForAtLeast` mit `streamClosed == true` und `availableBytes == 0` durchläuft, meldet EOF; die Bytes liegen danach im Puffer (ein weiteres `read()` nach `-1` lieferte sie). Folge: ein erfolgreich zurückgekehrter `write` erreicht einen Leser, der bei `-1` aufhört, nie. Fix wäre `requireNonClosed` innerhalb von `bufferLock` und `streamClosed = true` unter demselben Lock (Sichtbarkeit über die beiden `volatile` Felder bleibt geordnet). Nicht umgesetzt: kein deterministischer Test ohne neue Naht zwischen Prüfung und Lock (das Fenster ist eine Handvoll Anweisungen), und der Fix berührt die OpenJML-Spezifikation (`src/main/jml`) und die PIT-Schwelle 100. Ob ein `write` parallel zu `close` überhaupt unterstützt sein soll, entscheidet der Nutzer. +Keine (Stand 2026-10-18). diff --git a/README.md b/README.md index 277b4fa6..bf5bf9e9 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 @@ -325,7 +325,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 58399f07..371455a7 100644 --- a/TODO.md +++ b/TODO.md @@ -11,6 +11,22 @@ annotated, so everything below is genuinely still open. ## Open +- **Run the concurrency and formal-verification suites after the write/close fix (2026-10-18).** + `writeFromArray` now checks `streamClosed` under `bufferLock` and `closeAll()` sets it under the + same lock, so a write racing a `close()` from another thread is either buffered before the close + or fails with "Stream closed" (bug-hunt F149). The default build covers it deterministically + (`StreamBufferTest$ConcurrentWriteAndCloseTests`, red before the change) and is green with PIT + 199/199; these runs were not done and belong to the next joint CI run: + - `mvn -Pjcstress test`: the new `jcstress/WriteRacingCloseRace` (writer, closer and reader; + outcome `1, -1` is forbidden) and the existing `Close*`/`Write*` termination tests, which now + exercise a `close()` that takes `bufferLock`. + - `mvn -Pvmlens test`: the reader/writer interleaving test. + - The `formal-verification.yml` pipeline: OpenJML ESC (unchanged scope, expect the same proof + count) and RAC over the full suite with the new test, plus the `jpf-interleavings` job. + - Optional, worth it: extend the JPF harness (`src/test/jpf/`) with a third thread that closes + while the writer writes, so the write/close ordering is model-checked exhaustively; today's + harness writes and closes from the same thread and cannot see this race. + - **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 diff --git a/src/main/java/net/ladenthin/streambuffer/StreamBuffer.java b/src/main/java/net/ladenthin/streambuffer/StreamBuffer.java index 0767b82c..a51edab2 100644 --- a/src/main/java/net/ladenthin/streambuffer/StreamBuffer.java +++ b/src/main/java/net/ladenthin/streambuffer/StreamBuffer.java @@ -869,6 +869,11 @@ private int readSingleByte() throws IOException { * Implementation of {@link SBInputStream#read(byte[], int, int)}. See * {@link #availableClamped()} for why this lives in the outer class. * + *

Waits for the first byte, then for all remaining {@code len - 1} bytes + * ({@code waitForAtLeast}) unless the stream is closed first. Designed that + * way since the first version; {@link #getInputStream()} documents it for + * callers. + * * @param b the destination array * @param off the offset in the destination array * @param len the maximum number of bytes to read @@ -1014,11 +1019,12 @@ private void writeFromArray(final byte[] b, final int off, final int len, final if (!validateOffsetAndLengthToWrite(b, off, len)) { return; } - requireNonClosed(); // To be thread safe cache the safeWrite value. boolean tmpSafeWrite = isSafeWrite(); synchronized (bufferLock) { + // Checked under the lock closeAll() sets the flag under; see closeAll(). + requireNonClosed(); if (off == 0 && b.length == len) { // add the full byte[] to the buffer if (tmpSafeWrite && cloneOnSafeWrite) { @@ -1105,9 +1111,16 @@ public void close() throws IOException { /** * Invoke a close. + * + *

The flag is set under {@link #bufferLock}, the lock a write checks it under, so a write + * racing the close is either fully buffered before the close or fails with "Stream closed"; + * it never appends after the close has returned, when a reader may already have reported the + * end of the stream. */ private void closeAll() { - streamClosed = true; + synchronized (bufferLock) { + streamClosed = true; + } signalModification(); } @@ -1143,6 +1156,16 @@ public boolean isClosed() { * Closing the returned {@link java.io.InputStream InputStream} will close * the complete buffer. * + *

+ * {@link java.io.InputStream#read(byte[], int, int) read(b, off, len)} + * blocks until all {@code len} bytes are available or the buffer is + * closed; only then does it return fewer. This is stricter than the + * {@code InputStream} contract, which only waits for one byte, and differs + * from {@link java.io.PipedInputStream}. A reader that must not wait for a + * full block, such as an {@code InputStreamReader} over a request/response + * protocol, waits with {@link #waitForAnyData()} and then reads at most + * {@link java.io.InputStream#available() available()} bytes. + * * @return an input stream for reading bytes from this buffer. */ public InputStream getInputStream() { diff --git a/src/test/java/net/ladenthin/streambuffer/StreamBufferTest.java b/src/test/java/net/ladenthin/streambuffer/StreamBufferTest.java index bd1f4f81..ac2d46a3 100644 --- a/src/test/java/net/ladenthin/streambuffer/StreamBufferTest.java +++ b/src/test/java/net/ladenthin/streambuffer/StreamBufferTest.java @@ -21,6 +21,7 @@ import java.io.*; import java.time.Duration; import java.util.Arrays; +import java.util.Objects; import java.util.concurrent.CountDownLatch; import java.util.concurrent.ExecutorService; import java.util.concurrent.Semaphore; @@ -2026,6 +2027,79 @@ public void read_concurrentMultipleWritesThenClose_returnsAvailableBytes() throw } } + @Nested + @DisplayName("concurrent write and close") + class ConcurrentWriteAndCloseTests { + + /** + * A {@code write} that races a {@code close()} from another thread must either be ordered + * before the close, its bytes buffered before the close returns, or fail with + * "Stream closed". It must never append after the close has completed: a reader that saw + * the closed, empty buffer in between has already reported the end of the stream, and those + * bytes are lost to it although the write returned normally. + * + *

Deterministic: the trim-start signal runs on the trim thread while it holds the buffer + * lock, so a second writer started there parks on that lock; the close happens while it is + * parked. + */ + @DisplayName("write racing close(): never appends after close() returned") + @Test + public void write_closedWhileTheWriterWaitsForTheLock_failsInsteadOfAppendingAfterTheClose() throws Exception { + // arrange + final StreamBuffer sb = new StreamBuffer(); + final OutputStream os = sb.getOutputStream(); + sb.setMaxBufferElements(1); // the second entry triggers a trim + final AtomicBoolean fired = new AtomicBoolean(false); + final AtomicReference lateWriter = new AtomicReference<>(); + final AtomicReference lateWriteFailure = new AtomicReference<>(); + final AtomicReference availableWhenClosed = new AtomicReference<>(); + final Semaphore trimStart = new Semaphore(0) { + @Override + public void release() { + super.release(); + if (!fired.compareAndSet(false, true)) { + return; + } + final Thread writer = new Thread( + () -> { + try { + os.write(7); + } catch (IOException e) { + lateWriteFailure.set(e); + } + }, + "late-writer"); + lateWriter.set(writer); + writer.start(); + // this trim holds the buffer lock, so the late writer parks on it + final long deadline = System.nanoTime() + TimeUnit.SECONDS.toNanos(10); + while (writer.getState() != Thread.State.BLOCKED && System.nanoTime() < deadline) { + Thread.yield(); + } + try { + sb.close(); + } catch (IOException e) { + throw new UncheckedIOException(e); + } + availableWhenClosed.set(sb.getAvailableBytesExact()); + } + }; + sb.addTrimStartSignal(trimStart); + + // act + os.write(1); + os.write(2); + final Thread writer = Objects.requireNonNull(lateWriter.get(), "the trim-start signal did not fire"); + writer.join(TimeUnit.SECONDS.toMillis(10)); + + // assert + assertThat(writer.isAlive(), is(false)); + assertThat(availableWhenClosed.get(), is(2L)); + assertThat(sb.getAvailableBytesExact(), is(availableWhenClosed.get())); + assertThat("the late write must fail with 'Stream closed'", lateWriteFailure.get() != null, is(true)); + } + } + @Nested @DisplayName("concurrent trim and write") class ConcurrentTrimAndWriteTests { diff --git a/src/test/java/net/ladenthin/streambuffer/jcstress/WriteRacingCloseRace.java b/src/test/java/net/ladenthin/streambuffer/jcstress/WriteRacingCloseRace.java new file mode 100644 index 00000000..7d3cc384 --- /dev/null +++ b/src/test/java/net/ladenthin/streambuffer/jcstress/WriteRacingCloseRace.java @@ -0,0 +1,68 @@ +// SPDX-FileCopyrightText: 2014-2026 Bernard Ladenthin +// +// SPDX-License-Identifier: Apache-2.0 +package net.ladenthin.streambuffer.jcstress; + +import java.io.IOException; +import java.io.InputStream; +import java.io.OutputStream; +import net.ladenthin.streambuffer.StreamBuffer; +import org.openjdk.jcstress.annotations.Actor; +import org.openjdk.jcstress.annotations.Description; +import org.openjdk.jcstress.annotations.Expect; +import org.openjdk.jcstress.annotations.JCStressTest; +import org.openjdk.jcstress.annotations.Outcome; +import org.openjdk.jcstress.annotations.State; +import org.openjdk.jcstress.infra.results.II_Result; + +/** + * A write racing a close() from another thread, observed by a reader. + * + *

The write is either ordered before the close, so the reader gets its byte, or it fails with + * "Stream closed". A write that returns normally while the reader has already reported the end of + * the stream would lose that byte for the reader. The deterministic counterpart is + * {@code StreamBufferTest.ConcurrentWriteAndCloseTests}. + * + *

{@code r1}: 1 when the write returned normally, 0 when it threw. {@code r2}: the reader's + * {@code read()} result. + */ +@JCStressTest +@Description("A write racing close() is either delivered to the reader or fails; never both lost and successful.") +@Outcome(id = "1, 7", expect = Expect.ACCEPTABLE, desc = "write before close, reader got the byte") +@Outcome(id = "0, -1", expect = Expect.ACCEPTABLE, desc = "close before write, the write failed") +@Outcome(id = "1, -1", expect = Expect.FORBIDDEN, desc = "write succeeded but the reader already saw the end") +@State +public class WriteRacingCloseRace { + + private final StreamBuffer sb = new StreamBuffer(); + private final InputStream is = sb.getInputStream(); + private final OutputStream os = sb.getOutputStream(); + + @Actor + public void writer(II_Result r) { + try { + os.write(7); + r.r1 = 1; + } catch (IOException e) { + r.r1 = 0; + } + } + + @Actor + public void closer() { + try { + sb.close(); + } catch (IOException e) { + throw new IllegalStateException("close failed", e); + } + } + + @Actor + public void reader(II_Result r) { + try { + r.r2 = is.read(); + } catch (IOException e) { + r.r2 = -2; + } + } +} From 496e8c7a85ad251dfd276876fae6ce3a4bf39b15 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 18 Oct 2026 20:06:27 +0000 Subject: [PATCH 17/43] Record the commits of F03 and F149 in the bug-hunt ledger Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VBFFnrhtvXiUeyxjmUc4R2 --- BUGHUNT-FOUND.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/BUGHUNT-FOUND.md b/BUGHUNT-FOUND.md index 585576a1..344e4dc0 100644 --- a/BUGHUNT-FOUND.md +++ b/BUGHUNT-FOUND.md @@ -36,7 +36,7 @@ Repos plus eins. Geprüfte Klassen ohne Fund stehen in [`BUGHUNT-CHECKED.md`](BU - **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:** – +- **Commit:** 1529d3b ### F73 – streambuffer: ein gleichzeitiger `trim()` lässt `waitForAtLeast`/`read()` einen halb geleerten Puffer sehen @@ -79,7 +79,7 @@ Repos plus eins. Geprüfte Klassen ohne Fund stehen in [`BUGHUNT-CHECKED.md`](BU - **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“. - **Status:** gefixt -- **Commit:** – +- **Commit:** 1529d3b ## Offene Verdachte ohne Fund-ID From 48555ce57963fbac0338b7204465138f67f526f5 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 18 Oct 2026 23:58:41 +0000 Subject: [PATCH 18/43] Carry the open points of the bug hunt into TODO.md Everything the bug hunt left open - decided but not implemented, waiting for a decision, and the CI and hardware runs - is listed in TODO.md with a pointer to its ledger entry, so it survives the end of the session. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VBFFnrhtvXiUeyxjmUc4R2 --- TODO.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/TODO.md b/TODO.md index 371455a7..a67554ce 100644 --- a/TODO.md +++ b/TODO.md @@ -22,7 +22,8 @@ annotated, so everything below is genuinely still open. exercise a `close()` that takes `bufferLock`. - `mvn -Pvmlens test`: the reader/writer interleaving test. - The `formal-verification.yml` pipeline: OpenJML ESC (unchanged scope, expect the same proof - count) and RAC over the full suite with the new test, plus the `jpf-interleavings` job. + count) and RAC over the full suite with the new test, plus the `jpf-interleavings` job. The RAC + run also covers bug-hunt F73 (the changed `trim`), which was never run against RAC either. - Optional, worth it: extend the JPF harness (`src/test/jpf/`) with a third thread that closes while the writer writes, so the write/close ordering is model-checked exhaustively; today's harness writes and closes from the same thread and cannot see this race. From 718e18c1341ac7716b4212ad6bff29cefaa9811e Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 19 Oct 2026 08:37:09 +0000 Subject: [PATCH 19/43] Add the measurement brief for the open points of the bug hunt Every measurement and CI or hardware run the bug hunt left open, with the commands, the hypothesis, what the result decides and an answer field, so an agent can run them all at once and answer in the repository. TODO.md points to it. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VBFFnrhtvXiUeyxjmUc4R2 --- BUGHUNT-MEASUREMENTS.md | 83 +++++++++++++++++++++++++++++++++++++++++ TODO.md | 3 +- 2 files changed, 85 insertions(+), 1 deletion(-) create mode 100644 BUGHUNT-MEASUREMENTS.md diff --git a/BUGHUNT-MEASUREMENTS.md b/BUGHUNT-MEASUREMENTS.md new file mode 100644 index 00000000..77e669d1 --- /dev/null +++ b/BUGHUNT-MEASUREMENTS.md @@ -0,0 +1,83 @@ +# Messauftrag zum Bug-Hunt 2026-10-16 … 19 — streambuffer + +Dieser Auftrag sammelt die Läufe, die der Bug-Hunt offen gelassen hat. Hintergrund: `BUGHUNT-FOUND.md` +(F73, F149) und `TODO.md` („Run the concurrency and formal-verification suites after the write/close fix“). + +**Regeln für den ausführenden Agenten** + +- **Nur laufen lassen und berichten.** Keine Produktionsänderung, keine Fixes; committet wird nur diese + Datei mit den Ergebnissen. +- Arbeitsstand: Branch `ccr-90fc5f6a-vs4s0f`. +- Dateien aus `.github/shared-files.sha256` nicht verändern. +- Jeder Punkt wird beantwortet (sonst mit Grund). Zu jedem Ergebnis die Umgebung (CPU, Kerne, OS, JDK) und + die wörtlichen Ausgaben, die es tragen (jcstress-Tabelle, Beweiszahl, Testzahlen). +- Ergebnis unter **Ergebnis:**, darunter **Folgerung:**. + +--- + +## S1 jcstress: Schreiben gegen `close()` + +`writeFromArray` prüft `streamClosed` seit F149 unter `bufferLock`, `closeAll()` setzt es unter derselben +Sperre. Der neue Test `jcstress/WriteRacingCloseRace` (Schreiber, Schließer, Leser) verbietet das Ergebnis +`1, -1` (Schreiben erfolgreich, Leser sah aber schon das Ende). + +```bash +mvn -B -Pjcstress test +``` + +Den Abschnitt zu `WriteRacingCloseRace` und zu den bestehenden `Close*`/`Write*`-Tests aus dem Bericht +übernehmen (Ergebnisse je Outcome mit Häufigkeit). + +**Hypothese.** Kein `FORBIDDEN`-Ergebnis, alle übrigen Tests wie vorher. +**Entscheidet.** Ob F149 unter echter Nebenläufigkeit hält. + +**Ergebnis:** + +**Folgerung:** + +--- + +## S2 vmlens: Leser/Schreiber-Verschränkungen + +```bash +mvn -B -Pvmlens test +``` + +**Hypothese.** Grün. +**Ergebnis:** + +**Folgerung:** + +--- + +## S3 Formale Verifikation (OpenJML ESC + RAC, JPF) — deckt auch F73 ab + +Die Pipeline `formal-verification.yml` läuft auf Pull Requests und per `workflow_dispatch`; auf dem Branch +auslösen und Run-ID eintragen, oder lokal nach CLAUDE.md („Formal Verification“). Zu prüfen: + +- **ESC:** die Beweiszahl muss `ESC_EXPECTED_PROOFS` (14) sein, der Umfang ist unverändert. +- **RAC:** die ganze Suite gegen die instrumentierten Klassen, mit dem neuen Test + `StreamBufferTest$ConcurrentWriteAndCloseTests` und dem in F73 geänderten `trim` (lief nie unter RAC). +- **JPF:** der Job `jpf-interleavings`. + +**Hypothese.** ESC 14/14, RAC grün, JPF grün. +**Entscheidet.** Ob F73 und F149 die Spezifikationen und das Sperrprotokoll einhalten. + +**Ergebnis:** + +**Folgerung:** + +--- + +## S4 Optional: JPF-Harness mit einem dritten Thread, der schließt + +Das heutige Harness (`src/test/jpf/`) schreibt und schließt aus demselben Thread und sieht das Rennen aus +F149 deshalb nicht. Ein Wegwerf-Harness mit Schreiber-, Schließer- und Leser-Thread, erschöpfend modellgeprüft, +würde die Reihenfolge Schreiben/Schließen beweisen. Ergebnis und Harness-Quelltext hier eintragen, nicht +committen. + +**Entscheidet.** Ob das erweiterte Harness dauerhaft aufgenommen werden soll. + +**Ergebnis:** + +**Folgerung:** diff --git a/TODO.md b/TODO.md index a67554ce..57a10291 100644 --- a/TODO.md +++ b/TODO.md @@ -16,7 +16,8 @@ annotated, so everything below is genuinely still open. same lock, so a write racing a `close()` from another thread is either buffered before the close or fails with "Stream closed" (bug-hunt F149). The default build covers it deterministically (`StreamBufferTest$ConcurrentWriteAndCloseTests`, red before the change) and is green with PIT - 199/199; these runs were not done and belong to the next joint CI run: + 199/199; these runs were not done and belong to the next joint CI run (measurement brief with + answer fields: `BUGHUNT-MEASUREMENTS.md`, S1–S4): - `mvn -Pjcstress test`: the new `jcstress/WriteRacingCloseRace` (writer, closer and reader; outcome `1, -1` is forbidden) and the existing `Close*`/`Write*` termination tests, which now exercise a `close()` that takes `bufferLock`. From b0fc35ba13e635d78e4332f495a5b3c03cf52a0f Mon Sep 17 00:00:00 2001 From: Bernard Ladenthin Date: Mon, 19 Oct 2026 15:19:03 +0200 Subject: [PATCH 20/43] Record the results of the bug-hunt measurement brief All four points ran on a throwaway VM (8 vCPU). - S1: jcstress 604/604; WriteRacingCloseRace never shows the forbidden "1, -1" in 3.54 billion samples, so F149 holds. - S2: vmlens green (19 interleavings). - S3: ESC 14/14, JPF green, RAC green for 287 of 288 tests including the F149 test and the F73 trim. The excluded test is the 2-million-write concurrent trim test, which under RAC prints a stack trace per arraycopy (21 GB of log) and needs about two hours; the openjml-rac job would time out on it without any contract being violated. - S4: a throwaway JPF harness with separate writer, closer and reader threads finds no error with the fix and finds the race before F149. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015bvDWEYcnzbZvnHgzS2KuX --- BUGHUNT-MEASUREMENTS.md | 518 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 510 insertions(+), 8 deletions(-) diff --git a/BUGHUNT-MEASUREMENTS.md b/BUGHUNT-MEASUREMENTS.md index 77e669d1..57c5d873 100644 --- a/BUGHUNT-MEASUREMENTS.md +++ b/BUGHUNT-MEASUREMENTS.md @@ -15,6 +15,30 @@ Dieser Auftrag sammelt die Läufe, die der Bug-Hunt offen gelassen hat. Hintergr --- +## Messumgebung (Ergebnisse vom 2026-10-19) + +Ausgeführt am 2026-10-19, lokal auf einer Wegwerf-VM (kein `workflow_dispatch`, Entscheidung des Auftraggebers). +Keine Datei im Repository geändert außer dieser; die Wegwerf-Harness aus S4 lag nur auf der VM. + +**Gemeinsame Umgebung (gilt für alle Punkte)** + +- Stand: Branch `ccr-90fc5f6a-vs4s0f`, `0a3b488fd64eee785dd55433c6ff9f1ea0e52c50` („Add the measurement brief + for the open points of the bug hunt“), frisch von GitHub geklont; jeder Punkt in einer eigenen Kopie des Klons. +- Maschine: Vultr-VM, `AMD EPYC-Rome Processor` (virtualisiert, QEMU `pc-q35-8.2`), 8 vCPU = 1 Sockel × + 4 Kerne × 2 Threads, 16 GB RAM, Ubuntu 24.04.5 LTS, Kernel `6.8.0-146-generic`. +- JDK für Maven, jcstress, vmlens und den RAC-Build: Temurin `21.0.12.1+1` (`.java-version` = 21). +- JDK für JPF: Temurin `11.0.32.1+1`. +- Maven `3.9.11`. +- OpenJML `21.0.28` aus `openjml-ubuntu-24.04-21.0.28.zip`, SHA-256 gegen den Wert im Workflow geprüft + (`/tmp/openjml.zip: OK`), Fixups wie `.github/actions/setup-openjml` (die beiden JML-Dateien gelöscht, + `JAVA_VERSION` in `jdk/release` ergänzt). Der RAC-Testlauf forkt die mitgelieferte JVM von OpenJML. +- jcstress 0.16, vmlens 1.2.28, jpf-core `e61e396087983cde00b1e4a5f4b3dde39c0f9f7f` (mit dem + AtomicLong-Modell aus `src/test/jpf/jpf-model`). +- Die Punkte liefen nacheinander, jcstress (S1) allein auf der Maschine. Nur RAC-Lauf 1 (S3) lief + zeitweise neben JPF, S4 und einem gezielten RAC-Zusatzlauf. RAC-Lauf 2 lief allein. + +--- + ## S1 jcstress: Schreiben gegen `close()` `writeFromArray` prüft `streamClosed` seit F149 unter `bufferLock`, `closeAll()` setzt es unter derselben @@ -31,9 +55,96 @@ Den Abschnitt zu `WriteRacingCloseRace` und zu den bestehenden `Close*`/`Write*` **Hypothese.** Kein `FORBIDDEN`-Ergebnis, alle übrigen Tests wie vorher. **Entscheidet.** Ob F149 unter echter Nebenläufigkeit hält. -**Ergebnis:** +**Ergebnis:** `mvn -B -Pjcstress test`: `BUILD SUCCESS`, `Total time: 34:21 min`. Davor lief im selben Aufruf die +normale Surefire-Phase: `Tests run: 299, Failures: 0, Errors: 0, Skipped: 0`. + +jcstress-Konfiguration (wörtlich): + +``` + Test preset mode: "default" + Hardware CPUs in use: 8 + Spinning style: Thread.onSpinWait() + Test selection: ".*" + Forks per test: 1 normal, 5 stress + Iterations per fork: 5 + Time per iteration: 1000 ms +``` + +Gesamturteil (wörtlich): + +``` +(Results: 604 planned; 604 passed, 0 failed, 0 soft errs, 0 hard errs) + +RUN RESULTS: + Interesting tests: No matches. + + Failed tests: No matches. + + Error tests: No matches. + + All remaining tests: 8 matching test results. +``` + +Ergebnisse über alle Konfigurationen (wörtlich aus dem Bericht): + +``` +.......... [OK] net.ladenthin.streambuffer.jcstress.WriteRacingCloseRace + + RESULT SAMPLES FREQ EXPECT DESCRIPTION + 0, -1 2,341,015,301 66.14% Acceptable close before write, the write failed + 1, -1 0 0.00% Forbidden write succeeded but the reader already saw the end + 1, 7 1,198,259,507 33.86% Acceptable write before close, reader got the byte + +.......... [OK] net.ladenthin.streambuffer.jcstress.CloseDuringReadRace + + RESULT SAMPLES FREQ EXPECT DESCRIPTION + STALE 0 0.00% Forbidden Reader stuck after close() + TERMINATED 42,869 100.00% Acceptable close() unblocked the reader + +.......... [OK] net.ladenthin.streambuffer.jcstress.CloseUnblocksArrayReadRace + + RESULT SAMPLES FREQ EXPECT DESCRIPTION + STALE 0 0.00% Forbidden Array reader stuck after close() + TERMINATED 39,215 100.00% Acceptable close() unblocked the array reader + +.......... [OK] net.ladenthin.streambuffer.jcstress.CloseUnblocksWaitForAtLeastRace + + RESULT SAMPLES FREQ EXPECT DESCRIPTION + STALE 0 0.00% Forbidden waitForAtLeast stuck after close() + TERMINATED 33,728 100.00% Acceptable close() unblocked waitForAtLeast + +.......... [OK] net.ladenthin.streambuffer.jcstress.ConcurrentWriteRace + + RESULT SAMPLES FREQ EXPECT DESCRIPTION + false 0 0.00% Forbidden Torn / interleaved write + true 1,495,618,828 100.00% Acceptable Both payloads intact in some order + +.......... [OK] net.ladenthin.streambuffer.jcstress.WriteUnblocksArrayReadRace -**Folgerung:** + RESULT SAMPLES FREQ EXPECT DESCRIPTION + STALE 0 0.00% Forbidden Array reader stuck after write() + TERMINATED 33,599 100.00% Acceptable write() unblocked the array reader + +.......... [OK] net.ladenthin.streambuffer.jcstress.WriteUnblocksReadRace + + RESULT SAMPLES FREQ EXPECT DESCRIPTION + STALE 0 0.00% Forbidden Reader stuck after write() + TERMINATED 33,639 100.00% Acceptable write() unblocked the reader + +.......... [OK] net.ladenthin.streambuffer.jcstress.WriteUnblocksWaitForAtLeastRace + + RESULT SAMPLES FREQ EXPECT DESCRIPTION + STALE 0 0.00% Forbidden waitForAtLeast stuck after write() + TERMINATED 36,257 100.00% Acceptable write() unblocked waitForAtLeast +``` + +**Folgerung:** Die Hypothese gilt. Bei rund 3,54 Milliarden Proben von `WriteRacingCloseRace` kam der +verbotene Ausgang `1, -1` kein einziges Mal vor. Beide erlaubten Ausgänge traten häufig auf (66 % / 34 %), +das Rennen wurde also tatsächlich von beiden Seiten getroffen. Die sieben bestehenden `Close*`/`Write*`- +und `ConcurrentWrite*`-Tests sind grün. Auch nachdem `close()` jetzt `bufferLock` nimmt, gab es keinen +`STALE`-Ausgang und keine zerrissene Schreiboperation. F149 hält unter echter Nebenläufigkeit auf dieser +Hardware (x86, also TSO; zu ARM sagt der Lauf nichts). jcstress ist ein Stresstest und kein Beweis. Den +Beweis für die Reihenfolge Schreiben/Schließen liefert S4. --- @@ -44,9 +155,33 @@ mvn -B -Pvmlens test ``` **Hypothese.** Grün. -**Ergebnis:** +**Ergebnis:** `mvn -B -Pvmlens test`: `BUILD SUCCESS` (Exit 0). Die normale Surefire-Phase im selben Aufruf ergab +`Tests run: 299, Failures: 0, Errors: 0, Skipped: 0`. Danach lief der vmlens-Agent (`agent started, Build: 1.2.28`): -**Folgerung:** +``` +[INFO] Running net.ladenthin.streambuffer.vmlens.StreamBufferReaderWriterInterleavingTest +[INFO] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.639 s -- in net.ladenthin.streambuffer.vmlens.StreamBufferReaderWriterInterleavingTest +[INFO] Running net.ladenthin.streambuffer.vmlens.VmlensInterleavingSmokeTest +[INFO] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.096 s -- in net.ladenthin.streambuffer.vmlens.VmlensInterleavingSmokeTest +... +[INFO] Tests run: 290, Failures: 0, Errors: 0, Skipped: 0 +[INFO] See /root/sb-s2/target/vmlens-report for the vmlens report. +[INFO] BUILD SUCCESS +``` + +vmlens-Bericht (`target/vmlens-report/index.html`, als Text): + +``` +# Name Count Result +0 StreamBuffer.readerWriterAccounting 19 Success +1 VmlensInterleavingSmokeTest.atomicIncrements 2 Success +``` + +**Folgerung:** Grün, die Hypothese gilt. vmlens hat 19 Verschränkungen des Leser/Schreiber-Tests +durchlaufen, ohne Fehler und ohne gemeldetes Datenrennen. Die Lock-Änderung aus F149 (`requireNonClosed()` +unter `bufferLock`) hat die Byte-Buchhaltung zwischen Schreiber und Leser also nicht beschädigt. Der +vmlens-Test enthält kein `close()` und sagt deshalb nichts über das Rennen aus F149 selbst. Das decken S1 +und S4 ab. --- @@ -63,9 +198,219 @@ auslösen und Run-ID eintragen, oder lokal nach CLAUDE.md („Formal Verificatio **Hypothese.** ESC 14/14, RAC grün, JPF grün. **Entscheidet.** Ob F73 und F149 die Spezifikationen und das Sperrprotokoll einhalten. -**Ergebnis:** +**Ergebnis:** **ESC.** + +``` +Completed proving methods in net.ladenthin.streambuffer.StreamBuffer [26.32 secs] +Summary: + Valid: 14 + Invalid: 0 + Infeasible: 0 + Timeout: 0 + Error: 0 + Skipped: 52 + TOTAL METHODS: 66 + Classes: 0 proved of 3 + DURATION: 26.6 secs + +== Guard == +Completed clean proofs: 14 (expected: 14) +``` + +Bewiesen wurden genau die 14 Methoden aus `ESC_METHODS`, jede mit `Completed proof of … - no warnings` +(Prover `z3-5.1.0`): `calculateResultingChunks`, `clampToMaxInt`, `decideTrimExecution`, +`decrementAvailableBytesBudget`, `isAvailableBytesPositive`, `isMaxAllocSizeLessThanAvailable`, +`shouldCheckEdgeCase`, `shouldSkipTrimDueToEdgeCase`, `shouldSkipTrimDueToInvalidMaxBufferElements`, +`shouldSkipTrimDueToSmallBuffer`, `shouldSkipTrimDueToSufficientBuffer`, `shouldUpdateMaxObservedBytes`, +`validateOffsetAndLengthToRead`, `validateOffsetAndLengthToWrite`. Exit 0. + +**RAC.** + +Kompilieren mit `openjml --rac --rac-show-source=line --code-math=java --spec-math=java …`: ohne Fehler. +Guard: `RAC instrumentation present (org/jmlspecs referenced)`. + +Voller Suite-Lauf `mvn -B --no-transfer-progress -P jml-rac -Dopenjml.home=… -Dopenjml.jdk.java=…/jdk/bin/java test`: + +**Lauf 1 (ganze Suite, ohne Ausschluss) – abgebrochen, ohne Ergebnis.** Er startete um 10:36:26Z. Der +Test `StreamBufferTest$ConcurrentTrimAndWriteTests#waitForAtLeast_concurrentTrim_neverReturnsFewerBytesThanRequested` +(F73) lief unter RAC gut zwei Stunden und blieb dabei grün: + +``` +[INFO] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 7344 s -- in concurrent trim and write +``` + +(Der zweite Test der Klasse, `concurrentTrimAndWrite_noCrashOrCorruption`, braucht unter RAC 0,3 s, siehe +Lauf 2.) Der Test macht 2.000.000 Einzelbyte-`write`s mit `maxBufferElements` 1000, also rund 2.000 +Trims zu je etwa 1.000 Einträgen. Der F73-`trim` ruft für jeden Eintrag `System.arraycopy` auf. Für jeden +dieser Aufrufe gibt RAC einen Hinweis samt Stacktrace aus (≈10 KB), weil die mitgelieferte JDK-Spezifikation +eine nicht kompilierte Modellmethode benutzt: + +``` +Skipping a specification clause because it contains an uncompiled model method: 'boolean java.util.Arrays.equalArrays +java.lang.NoSuchMethodError: 'boolean java.util.Arrays.equalArrays(byte[], org.jmlspecs.lang.internal.bigint, byte[], org.jmlspecs.lang.internal.bigint, org.jmlspecs.lang.internal.bigint)' + at net.ladenthin.streambuffer.StreamBuffer.trim(StreamBuffer.java:302) + at net.ladenthin.streambuffer.StreamBuffer.writeFromArray(StreamBuffer.java:1048) + at net.ladenthin.streambuffer.StreamBuffer.writeSingleByte(StreamBuffer.java:989) + at net.ladenthin.streambuffer.StreamBuffer$SBOutputStream.write(StreamBuffer.java:1096) + at net.ladenthin.streambuffer.StreamBufferTest$ConcurrentTrimAndWriteTests.waitForAtLeast_concurrentTrim_neverReturnsFewerBytesThanRequested(StreamBufferTest.java:2194) +``` + +Bis zum Abbruch kam das 2.003.546-mal vor. Das Log wuchs auf 20.985.623.867 Bytes (196.240.539 Zeilen). +Die Laufzeit begrenzt dabei nicht der Test selbst, sondern das Durchreichen der Ausgabe über surefire. Der +Thread-Dump der surefire-Fork (`jcmd 665138 Thread.print`, 12:50:52Z) zeigt den Test-Thread beim +Schreiben auf diesem Kanal: -**Folgerung:** +``` +"main" #1 [665139] prio=5 os_prio=0 cpu=7296572.50ms elapsed=8050.14s tid=0x0000722980028030 nid=665139 runnable [0x0000722986111000] + java.lang.Thread.State: RUNNABLE + at java.io.FileOutputStream.writeBytes(java.base/Native Method) + ... + at org.apache.maven.surefire.booter.spi.EventChannelEncoder.testOutput(EventChannelEncoder.java:168) + ... + at java.lang.Throwable.printStackTrace(java.base/Throwable.java:673) +``` + +`@Timeout(60)` greift unter RAC nicht, weil das Profil `jml-rac` mit +`junit.jupiter.execution.timeout.mode=disabled` alle JUnit-Timeouts abschaltet. Um ~12:50:46Z wurde die +Fork beendet (im Dump steht ein `"SIGTERM handler"`-Thread mit `elapsed=4.86s`): Die koordinierende Sitzung hielt +den Lauf nach 2 h 14 min für hängend und schickte SIGTERM, danach SIGKILL. Das war eine Fehldeutung — zu diesem +Zeitpunkt lief schon ein späterer Test +(`MaxAllocationSizeTests.trim_recursiveTrim_onChunkOverflow_allDataPreserved`). Danach habe ich den +Maven-Prozess beendet. Lauf 1 liefert also keine Gesamtzahl. Im gefilterten Log bis zum Abbruch steht +kein einziges `Failures: [1-9]`, `Errors: [1-9]` und kein `JmlAssertionError`. + +**Lauf 2 (ganze Suite, ein Ausschluss, Obergrenze `timeout 45m`).** Alle Workflow-Schritte liefen in einer +frischen Kopie neu (Klassenpfad, RAC-Kompilat, Guard `RAC instrumentation present (org/jmlspecs referenced)`). +Ausgeschlossen war nur diese eine Testmethode, über `-Dsurefire.excludesFile=/root/rac-excludes.txt` mit +dem Inhalt + +``` +StreamBufferTest$ConcurrentTrimAndWriteTests#waitForAtLeast_concurrentTrim_neverReturnsFewerBytesThanRequested +``` + +(Die Excludes-Datei wird an die `` des Profils angehängt. `-Dtest` hätte diese ersetzt.) +Ergebnis, wörtlich: + +``` +[INFO] Running concurrent trim and write +[INFO] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.316 s -- in concurrent trim and write +[INFO] Running concurrent write and close +[INFO] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.011 s -- in concurrent write and close +[INFO] Running concurrent read/write +[INFO] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 753.6 s -- in concurrent read/write +... +[INFO] Tests run: 0, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 824.4 s -- in net.ladenthin.streambuffer.StreamBufferTest +[ERROR] Surefire is going to kill self fork JVM. The exit has elapsed 30 seconds after System.exit(0). +[INFO] Tests run: 287, Failures: 0, Errors: 0, Skipped: 0 +[INFO] BUILD SUCCESS +real 17m16.471s +EXIT=0 +``` + +Prüfung im surefire-Bericht (`TEST-net.ladenthin.streambuffer.StreamBufferTest.xml`): `tests="287" +errors="0" skipped="0" failures="0"`. Die ausgeschlossene Methode kommt 0-mal vor. Gelaufen sind unter +anderem `ConcurrentWriteAndCloseTests#write_closedWhileTheWriterWaitsForTheLock_failsInsteadOfAppendingAfterTheClose`, +`ConcurrentTrimAndWriteTests#concurrentTrimAndWrite_noCrashOrCorruption`, `TrimTests` (2), +`TrimWithPartialBufferEntryTests`, `TrimWithSafeWriteTests`, `MaxAllocationSizeTests` (18, darunter alle +`trim_*`), `BufferElementCountAndTrimStateTests`, `MaxBufferElementsZeroDisablesTrimTests`, die +`trim_*`-Tests in `ExceptionSafetyAndSignalManagementTests` und `MutationSurvivorTests` (u. a. +`trim_closeCalledDuringTrim_handlesGracefully`) sowie `ReadTests#read_afterTrimAndClose_returnsRemainingBytesThenEOF`. +Im Vergleich zum normalen Lauf (`StreamBufferTest` 288) fehlt genau die eine ausgeschlossene Methode. + +Auch Lauf 2 hatte einen langsamen Test, der aber nicht hängt: `ConcurrentReadWriteTests#safeWrite_concurrentSingleByteWrite_arrayStillCloned` +(200.000 `write(byte[8])` mit `safeWrite`). Für jedes `b.clone()` unter `bufferLock` gibt RAC einmal +`java.lang.NoSuchMethodError: 'boolean java.util.Arrays.equalArrays(byte[], byte[])'` samt Stacktrace aus. +Das kam genau 200.000-mal vor, die Klasse brauchte 753,6 s. Ein Thread-Dump während des Laufs zeigt `main` +RUNNABLE beim Erzeugen eines Stacktraces, Schreiber und Leser BLOCKED auf `bufferLock`. Der Fortschritt +war messbar (13:09:40Z 179.711, 13:13:42Z 200.000 der 200.000 Schreibvorgänge), danach lief der Test +grün durch. Ein zweiter Ausschluss war deshalb nicht nötig. Die Meldung `[ERROR] Surefire is going to kill +self fork JVM …` betrifft das Herunterfahren nach dem letzten Test: Laut Dump wartete die Fork auf die +Bestätigung des Exits, während Maven noch den Ausgabe-Rückstau las. + +Wie in Lauf 1 meldet RAC einmal in `thread interruption during read()` +`JML undefined exceptional postcondition - exception thrown` / +`java.lang.ClassCastException: class java.lang.InterruptedException cannot be cast to class java.lang.IllegalArgumentException`. +RAC wertet die Klausel `signals (IllegalArgumentException e) bytes <= 0;` von `waitForAtLeast` auch dann +aus, wenn eine `InterruptedException` geworfen wurde. Das sieht nach einem OpenJML-Fehler bei der +`signals`-Typprüfung aus, nicht nach einer verletzten Vorgabe. Mit `rac=exception` würde eine Verletzung +werfen, der Test blieb aber grün. + +Gezielter Zusatzlauf (gleiche RAC-Klassen, gleiches Profil, nur +`-Dtest=StreamBufferTest$ConcurrentWriteAndCloseTests,…$TrimTests,…$TrimWithPartialBufferEntryTests,…$TrimWithSafeWriteTests,…$MaxAllocationSizeTests,…$BufferElementCountAndTrimStateTests,…$MaxBufferElementsZeroDisablesTrimTests`), +gestartet, um den neuen F149-Test und die `trim`-Tests früh unter RAC zu sehen: + +``` +[INFO] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.367 s -- in trim() +[INFO] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.007 s -- in maxBufferElements=0 disables trim +[INFO] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.052 s -- in buffer element count and trim state +[INFO] Tests run: 18, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 3.653 s -- in maxAllocationSize: getter, setter, trim behavior +[INFO] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.011 s -- in concurrent write and close +[INFO] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.016 s -- in trim() — partial buffer entry +[INFO] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.021 s -- in trim() with safeWrite enabled +[INFO] Tests run: 28, Failures: 0, Errors: 0, Skipped: 0 +[INFO] BUILD SUCCESS +real 0m15.966s +``` + +**JPF (`jpf-interleavings`).** + +Produktionsklassen mit JDK 21 gebaut (`BUILD SUCCESS`). Annotation-JARs bereitgestellt +(`checker-qual-4.3.1.jar`, `error_prone_annotations-2.50.0.jar`, `jspecify-1.0.1.jar`). jpf-core mit +JDK 11 gebaut (`BUILD SUCCESSFUL in 20s`). Harness mit `javac --release 8` übersetzt und unter JDK 11 +geprüft: + +``` +JavaPathfinder core system v8.0 (rev e61e396087983cde00b1e4a5f4b3dde39c0f9f7f) - (C) 2005-2014 United States Government. All rights reserved. + +====================================================== system under test +net.ladenthin.streambuffer.jpf.JpfStreamBufferHarness.main() + +====================================================== results +no errors detected + +====================================================== statistics +elapsed time: 00:00:02 +states: new=13616,visited=17704,backtracked=31320,end=30 +search: maxDepth=127,constraints=0 +choice generators: thread=13614 (signal=0,lock=1453,sharedRef=6979,threadApi=652,reschedule=4250), data=0 +heap: new=11650,released=6631,maxLive=718,gcCycles=31184 +instructions: 853148 +max memory: 300MB +loaded code: classes=122,methods=3245 + +== Gate == +states: new=13616 +``` + +Das Gate des Workflows ist bestanden (kein `^error #`, `no errors detected` vorhanden). Exit 0. + +**Folgerung:** - **ESC 14/14.** Die Beweiszahl stimmt mit `ESC_EXPECTED_PROOFS` überein, der Umfang ist unverändert + (die 14 Methoden aus `ESC_METHODS`). F73 und F149 haben keinen der bewiesenen statischen Helfer berührt. +- **RAC grün, mit einem Ausschluss.** Ausgeschlossen war nur + `ConcurrentTrimAndWriteTests#waitForAtLeast_concurrentTrim_neverReturnsFewerBytesThanRequested`. Die + übrigen 287 Tests laufen gegen die instrumentierten Klassen grün, ohne eine einzige Vertragsverletzung + (`rac=exception`). Darunter sind der neue F149-Test `ConcurrentWriteAndCloseTests` und alle `trim`-Tests, + also auch der in F73 geänderte `trim`, der damit zum ersten Mal unter RAC lief. Der ausgeschlossene Test + lief in Lauf 1 ebenfalls grün (`Tests run: 2, Failures: 0 … 7344 s`). Ein vollständiger Lauf aller 288 + Tests in einem Stück liegt aber nicht vor, weil Lauf 1 (irrtümlich als hängend) abgebrochen wurde. +- **Für die CI wichtig, eine Messung und keine Vorhersage aus einem CI-Lauf.** Im Job `openjml-rac` + (`timeout-minutes: 30`, Runner mit 2 Kernen) passt der F73-Test unter RAC nicht ins Zeitlimit. Lokal + brauchte er auf 8 vCPU allein 7.344 s und erzeugte rund 21 GB Log. Der Job würde also vermutlich rot + (Timeout), ohne dass ein Vertrag verletzt ist. Die Ursache ist kein Hänger: Der Test ist für den + Produktionspfad bemessen (2 Mio. Writes, `@Timeout(60)`), RAC schaltet die Timeouts ab und gibt pro + `System.arraycopy`/`clone` einen Stacktrace aus. Abhilfe wäre zu entscheiden (Test im Profil `jml-rac` + ausschließen oder kleiner skalieren). Das ist hier nicht gemacht, weil der Auftrag keine Änderungen erlaubt. +- **JPF grün** (`no errors detected`, 13.616 Zustände, maxDepth 127, wie dokumentiert „~14,000 states, + maxDepth 130“). +- Insgesamt halten F73 und F149 die Spezifikationen und das bestehende Sperrprotokoll ein, soweit ESC, + RAC und das heutige JPF-Harness reichen. Die Reihenfolge Schreiben/Schließen deckt erst S4 ab. +- **Nebenbefund, nicht Teil des Auftrags:** `StreamBufferProperties` (jqwik, 5 `@Property`) erscheint in + keinem surefire-Lauf, weder im normalen (`Tests run: 299` = `StreamBufferTest` 288 + + `StreamBufferArchitectureTest` 10 + `StreamBufferLincheckTest` 1) noch unter vmlens oder RAC. Der + Klassenname passt nicht auf die Standard-Includes von surefire (`*Test`, `*Tests`, `Test*`, `*TestCase`), + und die pom setzt keine eigenen Includes. CLAUDE.md („picked up by Surefire as a JUnit 6 engine“) und der + Kommentar im Profil `jml-rac` („… and the jqwik properties (StreamBufferProperties)“) sagen etwas anderes. + Nicht weiter untersucht. --- @@ -78,6 +423,163 @@ committen. **Entscheidet.** Ob das erweiterte Harness dauerhaft aufgenommen werden soll. -**Ergebnis:** +**Ergebnis:** Die Wegwerf-Harness `JpfWriteCloseHarness` wurde nur auf der VM angelegt (`/root/s4src`, Arbeitskopien +`/root/s4-*`) und nicht ins Repository übernommen. Sie lief mit derselben jpf-core-Build und denselben +Annotation-JARs wie der JPF-Job oben, mit `--release 8` übersetzt und unter JDK 11 geprüft. Es gibt drei +Threads: Der Schreiber schreibt zwei Einzelbytes, der Schließer ruft `sb.close()` auf, der Leser liest +bis `-1`. Das Orakel nach dem Join prüft: + +- Ein `write` nach einem gescheiterten `write` darf nicht mehr gelingen. +- Der Leser erhält **genau** die Bytes, deren `write` normal zurückkehrte, in der richtigen Reihenfolge. + +Dazu kommen die JPF-Eigenschaften Deadlock und nicht gefangene Exception. + +Konfiguration `WriteClose.jpf`: + +``` +target = net.ladenthin.streambuffer.jpf.JpfWriteCloseHarness +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 +vm.enable_assertions = true +``` + +Quelltext: + +```java +// Throwaway JPF harness for BUGHUNT-MEASUREMENTS.md S4 -- NOT committed. +package net.ladenthin.streambuffer.jpf; + +import java.io.IOException; +import java.io.InputStream; +import java.io.OutputStream; +import net.ladenthin.streambuffer.StreamBuffer; + +/** + * Writer, closer and reader in three separate threads over one StreamBuffer (bug-hunt F149). + * The writer writes two single bytes; each write either succeeds or fails with "Stream closed". + * Oracle over every interleaving JPF enumerates: + * - no deadlock, no uncaught exception (JPF properties); + * - once a write failed, every later write fails too (close is sticky); + * - the reader, which reads until -1, receives EXACTLY the bytes whose write returned normally, + * in order -- a successful write is ordered before the close and never lost for the reader. + */ +public final class JpfWriteCloseHarness { + + private JpfWriteCloseHarness() {} + + 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 boolean[] ok = new boolean[payload.length]; + + final Thread writer = new Thread(() -> { + for (int i = 0; i < payload.length; i++) { + try { + os.write(payload[i]); + ok[i] = true; + } catch (IOException e) { + ok[i] = false; + } + } + }); + + final Thread closer = new Thread(() -> { + try { + sb.close(); + } catch (IOException e) { + throw new AssertionError("close must not fail", e); + } + }); + + final byte[] got = new byte[payload.length + 1]; + 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(); + closer.start(); + reader.start(); + writer.join(); + closer.join(); + reader.join(); + + int succeeded = 0; + for (int i = 0; i < payload.length; i++) { + if (ok[i]) { + if (i != succeeded) { + throw new AssertionError("write " + i + " succeeded after an earlier write failed"); + } + succeeded++; + } + } + if (count[0] != succeeded) { + throw new AssertionError("reader got " + count[0] + " bytes, but " + succeeded + + " writes returned normally (F149: write succeeded after the reader saw EOF)"); + } + for (int i = 0; i < succeeded; i++) { + if (got[i] != payload[i]) { + throw new AssertionError("byte " + i + " corrupted"); + } + } + } +} +``` + +Lauf gegen den Stand des Branches (`0a3b488`, mit F149-Fix): + +``` +====================================================== system under test +net.ladenthin.streambuffer.jpf.JpfWriteCloseHarness.main() + +====================================================== results +no errors detected + +====================================================== statistics +elapsed time: 00:00:15 +states: new=75438,visited=151499,backtracked=226937,end=72 +search: maxDepth=135,constraints=0 +choice generators: thread=75433 (signal=0,lock=6451,sharedRef=39211,threadApi=1358,reschedule=26614), data=0 +heap: new=93087,released=49976,maxLive=751,gcCycles=216153 +instructions: 5688950 +max memory: 250MB +loaded code: classes=126,methods=3283 +``` + +Negativkontrolle: dieselbe Harness gegen die Produktionsklassen **vor** dem F149-Fix (`1529d3b^` = +`b54b620`, mit JDK 21 gebaut). Damit ist gezeigt, dass das Orakel nicht leer ist: + +``` +====================================================== error 1 +gov.nasa.jpf.vm.NoUncaughtExceptionsProperty +java.lang.AssertionError: reader got 1 bytes, but 2 writes returned normally (F149: write succeeded after the reader saw EOF) + +====================================================== results +error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.AssertionError: reader got 1 bytes, but ..." + +====================================================== statistics +elapsed time: 00:00:01 +states: new=3956,visited=5948,backtracked=9836,end=18 +``` -**Folgerung:** +**Folgerung:** Mit dem Fix ist die Harness über alle von JPF aufgezählten Verschränkungen fehlerfrei +(75.438 neue Zustände, 15 s). Ohne den Fix findet JPF das Rennen aus F149 nach 3.956 Zuständen in 1 s: +Der Leser meldet `-1` nach einem Byte, danach kehrt der zweite `write` normal zurück. Die Harness sieht +also genau den Fehler, den das heutige Harness nicht sehen kann, und beweist für dieses kleine Modell +(zwei Bytes, ein Schließer) die Reihenfolge Schreiben/Schließen. Kosten: etwa 5,5-mal so viele Zustände +wie das heutige Harness (13.616), Laufzeit weiter im Sekundenbereich. Aus Sicht der Messung spricht nichts +dagegen, sie dauerhaft aufzunehmen, etwa als zweites `target` im Job `jpf-interleavings`. Die Entscheidung +liegt beim Nutzer. From 10356bdfb651f703f278a207b8c78bcd86ac05aa Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 19 Oct 2026 14:38:31 +0000 Subject: [PATCH 21/43] Model-check the order of write and close with a third JPF harness JpfStreamBufferHarness writes and closes from one thread, so it could not see bug-hunt finding F149 (a write passing the closed check outside the lock and adding its bytes after the reader saw the end). The new harness runs writer, closer and reader in three threads: no errors over 75,438 states with the fix, and against the classes before F149 it reports "reader got 1 bytes, but 2 writes returned normally" after 3,956 states. The jpf-interleavings job runs and gates both. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VBFFnrhtvXiUeyxjmUc4R2 --- .github/workflows/formal-verification.yml | 44 ++++--- .gitignore | 2 +- CLAUDE.md | 8 +- TODO.md | 3 - src/test/jpf/README.md | 18 ++- src/test/jpf/WriteClose.jpf | 12 ++ .../jpf/JpfWriteCloseHarness.java | 114 ++++++++++++++++++ 7 files changed, 172 insertions(+), 29 deletions(-) create mode 100644 src/test/jpf/WriteClose.jpf create mode 100644 src/test/jpf/net/ladenthin/streambuffer/jpf/JpfWriteCloseHarness.java 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/CLAUDE.md b/CLAUDE.md index c003a7cf..81e3eedb 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -69,9 +69,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 diff --git a/TODO.md b/TODO.md index 57a10291..7634e151 100644 --- a/TODO.md +++ b/TODO.md @@ -25,9 +25,6 @@ annotated, so everything below is genuinely still open. - The `formal-verification.yml` pipeline: OpenJML ESC (unchanged scope, expect the same proof count) and RAC over the full suite with the new test, plus the `jpf-interleavings` job. The RAC run also covers bug-hunt F73 (the changed `trim`), which was never run against RAC either. - - Optional, worth it: extend the JPF harness (`src/test/jpf/`) with a third thread that closes - while the writer writes, so the write/close ordering is model-checked exhaustively; today's - harness writes and closes from the same thread and cannot see this race. - **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 diff --git a/src/test/jpf/README.md b/src/test/jpf/README.md index e14016d0..dd8be948 100644 --- a/src/test/jpf/README.md +++ b/src/test/jpf/README.md @@ -28,7 +28,18 @@ reporting: - **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. +Last confirmed run: **no errors detected**, 13,616 states, maxDepth 130. + +A second harness (`JpfWriteCloseHarness.java`, run configuration `WriteClose.jpf`) puts the writer, +a separate closer and the reader in three threads, so a write can race the close — which the first +harness cannot show, since its writer closes after its own writes. The writer writes two single +bytes, each of which either succeeds or fails with "Stream closed"; JPF checks over every +interleaving that a write after a failed write fails too, and that the reader receives **exactly** +the bytes whose write returned normally, in order. That is the property bug-hunt finding F149 broke +(a write passed the closed check outside the lock and added its bytes after the reader had already +seen the end). Last confirmed run: **no errors detected**, 75,438 states (~15–25 s); against the +production classes before the F149 fix (`1529d3b^`) it reports "reader got 1 bytes, but 2 writes +returned normally" after 3,956 states, so the oracle is not vacuous. ## Files @@ -36,6 +47,8 @@ Last confirmed run: **no errors detected**, ~14,000 states, maxDepth 130. |---|---| | `net/ladenthin/streambuffer/jpf/JpfStreamBufferHarness.java` | the model-checked harness (the oracle) | | `StreamBuffer.jpf` | JPF run configuration (target + classpath) | +| `net/ladenthin/streambuffer/jpf/JpfWriteCloseHarness.java` | the write/close harness (writer, closer, reader) | +| `WriteClose.jpf` | its JPF run configuration (same 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 @@ -74,8 +87,9 @@ docker run --rm -v "$WORK/jpf-core:/jpf" -v "$SB:/sb" -w /jpf eclipse-temurin:11 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 + javac --release 8 -cp streambuffer-classes -d out net/ladenthin/streambuffer/jpf/*.java java -jar /jpf/build/RunJPF.jar StreamBuffer.jpf + java -jar /jpf/build/RunJPF.jar WriteClose.jpf ' ``` diff --git a/src/test/jpf/WriteClose.jpf b/src/test/jpf/WriteClose.jpf new file mode 100644 index 00000000..23102f30 --- /dev/null +++ b/src/test/jpf/WriteClose.jpf @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2014-2026 Bernard Ladenthin +# +# SPDX-License-Identifier: Apache-2.0 +# +# JPF run configuration for the write/close harness (bug hunt F149): writer, closer and reader in +# three threads. Same classpath layout as StreamBuffer.jpf; consumed by RunJPF.jar in the +# jpf-interleavings CI job and by the local recipe in README.md. +target = net.ladenthin.streambuffer.jpf.JpfWriteCloseHarness + +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 + +vm.enable_assertions = true diff --git a/src/test/jpf/net/ladenthin/streambuffer/jpf/JpfWriteCloseHarness.java b/src/test/jpf/net/ladenthin/streambuffer/jpf/JpfWriteCloseHarness.java new file mode 100644 index 00000000..00c46f2f --- /dev/null +++ b/src/test/jpf/net/ladenthin/streambuffer/jpf/JpfWriteCloseHarness.java @@ -0,0 +1,114 @@ +// 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 for the order of {@code write} and {@code close()} (bug hunt F149): a + * writer, a closer and a reader in three separate threads over one {@link StreamBuffer}. Like + * {@link JpfStreamBufferHarness} 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}. + * + *

{@link JpfStreamBufferHarness} writes and closes from one thread, so a write can never race the + * close there, and it could not see F149: {@code writeFromArray} checked {@code streamClosed} outside + * {@code bufferLock}, so a write could pass the check, lose the lock to {@code close()}, and then add + * its bytes after the reader had already seen the end of the stream -- the write returned normally + * and its bytes were lost. Here the writer writes two single bytes, each of which either succeeds or + * fails with "Stream closed", and the reader reads until {@code -1}. Over every interleaving JPF + * enumerates: + * + *

    + *
  • no deadlock and no uncaught exception (JPF's own properties); + *
  • once a write failed, every later write fails too (close is sticky); + *
  • the reader receives exactly the bytes whose write returned normally, in order: a successful + * write is ordered before the close and never lost for the reader. + *
+ * + *

Measured with the pinned jpf-core: with the F149 fix no errors over 75,438 states (about 15 s); + * against the production classes before the fix ({@code 1529d3b^}) JPF finds the race after 3,956 + * states: "reader got 1 bytes, but 2 writes returned normally". Keep the payload at two bytes; the + * state space grows fast. + */ +public final class JpfWriteCloseHarness { + + private JpfWriteCloseHarness() {} + + 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 boolean[] ok = new boolean[payload.length]; + + final Thread writer = new Thread(() -> { + for (int i = 0; i < payload.length; i++) { + try { + os.write(payload[i]); + ok[i] = true; + } catch (IOException e) { + ok[i] = false; + } + } + }); + + final Thread closer = new Thread(() -> { + try { + sb.close(); + } catch (IOException e) { + throw new AssertionError("close must not fail", e); + } + }); + + // One slot more than the payload, so a reader that sees a byte too many is caught too. + final byte[] got = new byte[payload.length + 1]; + 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(); + closer.start(); + reader.start(); + writer.join(); + closer.join(); + reader.join(); + + // Explicit throws rather than `assert`, as in JpfStreamBufferHarness: JPF reports an uncaught + // AssertionError regardless of whether assertions are enabled for the system under test. + int succeeded = 0; + for (int i = 0; i < payload.length; i++) { + if (ok[i]) { + if (i != succeeded) { + throw new AssertionError("write " + i + " succeeded after an earlier write failed"); + } + succeeded++; + } + } + if (count[0] != succeeded) { + throw new AssertionError("reader got " + count[0] + " bytes, but " + succeeded + + " writes returned normally (F149: write succeeded after the reader saw EOF)"); + } + for (int i = 0; i < succeeded; i++) { + if (got[i] != payload[i]) { + throw new AssertionError("byte " + i + " corrupted"); + } + } + } +} From 6f924d28a97379bdfde821e2249d8a592bccf18c Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 19 Oct 2026 15:00:31 +0000 Subject: [PATCH 22/43] Scale the stress loops down under RAC instead of running into the job timeout Under RAC every System.arraycopy and clone prints a ~10 KB stack trace for an uncompiled model method of the bundled JDK specification, so the concurrent-trim test's 2 million writes took 7,344 s and 21 GB of log and the safeWrite test 753 s, with every contract holding (measured). The jml-rac profile sets streambuffer.test.rac, and both loops run 5,000 and 2,000 iterations there: 30 s and 24 s under RAC; the default build keeps 2,000,000 and 200,000. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VBFFnrhtvXiUeyxjmUc4R2 --- pom.xml | 9 ++++++ .../streambuffer/StreamBufferTest.java | 28 +++++++++++++++++-- 2 files changed, 35 insertions(+), 2 deletions(-) diff --git a/pom.xml b/pom.xml index f02c6aa8..fb1a21aa 100644 --- a/pom.xml +++ b/pom.xml @@ -834,6 +834,15 @@ SPDX-License-Identifier: Apache-2.0 is lifted. JUnit reads this config parameter from a system property. --> disabled + + true + + **/Test*.java + **/*Test.java + **/*Tests.java + **/*TestCase.java + **/*Properties.java + @@ -843,6 +857,14 @@ SPDX-License-Identifier: Apache-2.0 job's timeout, with every contract holding. --> true + + 100 true