From 22116b7ba94a315a56099282c9030a9128dcbd80 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 14 Jun 2026 21:50:26 +0000 Subject: [PATCH 1/2] Add vmlens smoke test for 4-repo parity streambuffer already ran vmlens over the whole suite but had no dedicated VmlensInterleavingSmokeTest; add the same one the three sibling repos carry so the deterministic "is vmlens wired up?" baseline is identical across all four. - New net.ladenthin.streambuffer.vmlens.VmlensInterleavingSmokeTest: two threads increment a shared AtomicLong inside an AllInterleavings loop, asserting the sum is always 2. - pom: promote com.vmlens:api out of the vmlens profile into the main test (transitive-dep-free, convergence-safe) so the test compiles in every build; add a managed surefire so the ordinary suite skips it (vacuous without the agent). The vmlens profile's whole-suite run still picks it up. Verified green under the vmlens agent. https://claude.ai/code/session_01HzCYFLjZZGFs4BsuUty35N --- pom.xml | 28 +++++++++ .../vmlens/VmlensInterleavingSmokeTest.java | 57 +++++++++++++++++++ 2 files changed, 85 insertions(+) create mode 100644 src/test/java/net/ladenthin/streambuffer/vmlens/VmlensInterleavingSmokeTest.java diff --git a/pom.xml b/pom.xml index 048ec23..0f98a8a 100644 --- a/pom.xml +++ b/pom.xml @@ -179,6 +179,21 @@ SPDX-License-Identifier: Apache-2.0 ${lincheck.version} test + + + com.vmlens + api + ${vmlens.version} + test + @@ -232,6 +247,19 @@ SPDX-License-Identifier: Apache-2.0 org.apache.maven.plugins maven-surefire-plugin 3.5.6 + + + + **/VmlensInterleavingSmokeTest.java + + org.apache.maven.plugins diff --git a/src/test/java/net/ladenthin/streambuffer/vmlens/VmlensInterleavingSmokeTest.java b/src/test/java/net/ladenthin/streambuffer/vmlens/VmlensInterleavingSmokeTest.java new file mode 100644 index 0000000..52382b8 --- /dev/null +++ b/src/test/java/net/ladenthin/streambuffer/vmlens/VmlensInterleavingSmokeTest.java @@ -0,0 +1,57 @@ +// SPDX-FileCopyrightText: 2014-2026 Bernard Ladenthin +// +// SPDX-License-Identifier: Apache-2.0 +package net.ladenthin.streambuffer.vmlens; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.is; + +import com.vmlens.api.AllInterleavings; +import java.util.concurrent.atomic.AtomicLong; +import org.junit.jupiter.api.Test; + +/** + * Minimal vmlens interleaving-analysis smoke test demonstrating the setup. + * + *

Two threads each increment a shared {@link AtomicLong}; because + * {@link AtomicLong#incrementAndGet()} is atomic, the final value must always be + * {@code 2} regardless of how the two threads interleave. vmlens drives the body + * of the {@link AllInterleavings} loop through every possible interleaving and + * fails if any ordering violates the invariant.

+ * + *

This test is meaningful only when executed under the vmlens java agent, + * which is wired up by the {@code vmlens} Maven profile ({@code mvn -Pvmlens + * test}). Without the agent {@link AllInterleavings#hasNext()} returns + * {@code false} and the loop body is skipped, so the ordinary surefire run + * excludes this class (see the {@code maven-surefire-plugin} {@code } + * in {@code pom.xml}). It is kept in sync with the sibling repos as a shared, + * deterministic baseline for the vmlens setup; the real interleaving coverage for + * this repo is the {@code StreamBuffer} reader/writer suite.

+ */ +public class VmlensInterleavingSmokeTest { + + /** + * Verifies that two concurrent atomic increments always sum to two under + * every thread interleaving explored by vmlens. + * + * @throws InterruptedException if joining a worker thread is interrupted + */ + @Test + public void atomicIncrementsAreLinearizable() throws InterruptedException { + try (AllInterleavings allInterleavings = new AllInterleavings("VmlensInterleavingSmokeTest.atomicIncrements")) { + while (allInterleavings.hasNext()) { + final AtomicLong counter = new AtomicLong(); + + final Thread first = new Thread(counter::incrementAndGet); + final Thread second = new Thread(counter::incrementAndGet); + + first.start(); + second.start(); + first.join(); + second.join(); + + assertThat(counter.get(), is(2L)); + } + } + } +} From abff69ef52115bcc0fc2b9a4a10eaef84e8e19de Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 10:21:09 +0000 Subject: [PATCH 2/2] Add vmlens reader/writer interleaving test for StreamBuffer MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit First real (beyond-smoke) vmlens target for this repo: a writer and a reader race on a StreamBuffer and the byte-accounting invariant totalBytesWritten == totalBytesRead + availableBytes must hold at quiescence for every interleaving. This covers the interleaving class neither existing tool reaches — Lincheck excludes read() (can't progress past a parked reader) and the jcstress close/unblock races assert only termination, not the resulting accounting (the reader's waitForAtLeast gate reads availableBytes/streamClosed outside bufferLock while the writer mutates them under it). - New net.ladenthin.streambuffer.vmlens.StreamBufferReaderWriterInterleavingTest. - pom: widen the managed surefire to the whole vmlens package (**/vmlens/*.java) so new interleaving tests are auto-excluded from the ordinary suite; the vmlens profile's whole-suite run still picks them up. Verified green under the vmlens agent. https://claude.ai/code/session_01HzCYFLjZZGFs4BsuUty35N --- pom.xml | 14 +-- ...eamBufferReaderWriterInterleavingTest.java | 85 +++++++++++++++++++ 2 files changed, 92 insertions(+), 7 deletions(-) create mode 100644 src/test/java/net/ladenthin/streambuffer/vmlens/StreamBufferReaderWriterInterleavingTest.java diff --git a/pom.xml b/pom.xml index 0f98a8a..cd0fdde 100644 --- a/pom.xml +++ b/pom.xml @@ -249,15 +249,15 @@ SPDX-License-Identifier: Apache-2.0 3.5.6 - **/VmlensInterleavingSmokeTest.java + **/vmlens/*.java diff --git a/src/test/java/net/ladenthin/streambuffer/vmlens/StreamBufferReaderWriterInterleavingTest.java b/src/test/java/net/ladenthin/streambuffer/vmlens/StreamBufferReaderWriterInterleavingTest.java new file mode 100644 index 0000000..2170964 --- /dev/null +++ b/src/test/java/net/ladenthin/streambuffer/vmlens/StreamBufferReaderWriterInterleavingTest.java @@ -0,0 +1,85 @@ +// SPDX-FileCopyrightText: 2014-2026 Bernard Ladenthin +// +// SPDX-License-Identifier: Apache-2.0 +package net.ladenthin.streambuffer.vmlens; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.is; +import static org.hamcrest.Matchers.nullValue; + +import com.vmlens.api.AllInterleavings; +import java.io.InputStream; +import java.io.OutputStream; +import java.util.concurrent.atomic.AtomicReference; +import net.ladenthin.streambuffer.StreamBuffer; +import org.junit.jupiter.api.Test; + +/** + * vmlens interleaving analysis of a concurrent reader and writer on a + * {@link StreamBuffer}. + * + *

A writer thread writes a fixed payload while a reader thread drains it. The + * reader's blocking path ({@code waitForAtLeast}) reads {@code availableBytes} and + * {@code streamClosed} outside {@code bufferLock}, while the writer + * mutates {@code availableBytes} and the byte counters under the lock and only + * then releases the wakeup semaphore. The byte-accounting invariant + * {@code totalBytesWritten == totalBytesRead + availableBytes} must therefore hold + * at quiescence for every interleaving — no byte may be lost or + * double-counted in the hand-off between the lock-free wait gate and the + * lock-protected mutation.

+ * + *

This is the interleaving class that the existing coverage does not reach: the + * Lincheck test deliberately omits {@code read} (a model checker cannot progress + * past a parked reader) and the jcstress close/unblock races assert only + * termination, not the resulting accounting. Like the rest of the + * package it runs only under the vmlens agent (see the {@code vmlens} profile and + * the {@code maven-surefire-plugin} {@code } in {@code pom.xml}).

+ */ +public class StreamBufferReaderWriterInterleavingTest { + + /** + * Drives a writer against a reader through every interleaving and asserts the + * write/read/buffered byte-accounting invariant after both threads finish. + * + * @throws InterruptedException if joining a worker thread is interrupted + */ + @Test + public void readerWriterAccountingHoldsUnderAllInterleavings() throws InterruptedException { + try (AllInterleavings allInterleavings = new AllInterleavings("StreamBuffer.readerWriterAccounting")) { + while (allInterleavings.hasNext()) { + final StreamBuffer streamBuffer = new StreamBuffer(); + final OutputStream out = streamBuffer.getOutputStream(); + final InputStream in = streamBuffer.getInputStream(); + final byte[] payload = {10, 20, 30, 40}; + final byte[] sink = new byte[payload.length]; + final AtomicReference failure = new AtomicReference<>(); + + final Thread writer = new Thread(() -> { + try { + out.write(payload); + } catch (Throwable t) { + failure.compareAndSet(null, t); + } + }); + final Thread reader = new Thread(() -> { + try { + in.read(sink, 0, sink.length); + } catch (Throwable t) { + failure.compareAndSet(null, t); + } + }); + + writer.start(); + reader.start(); + writer.join(); + reader.join(); + + assertThat(failure.get(), is(nullValue())); + assertThat(streamBuffer.getTotalBytesWritten(), is((long) payload.length)); + assertThat( + streamBuffer.getTotalBytesWritten(), + is(streamBuffer.getTotalBytesRead() + streamBuffer.getAvailableBytesExact())); + } + } + } +}