Add vmlens interleaving analysis tests for StreamBuffer

pom.xml

@@ -179,6 +179,21 @@ SPDX-License-Identifier: Apache-2.0
             <version>${lincheck.version}</version>
             <scope>test</scope>
         </dependency>
+        <!--
+            vmlens interleaving-analysis API. Promoted from the `vmlens` profile to the
+            main test classpath (transitive-dependency-free, so convergence-safe) so the
+            VmlensInterleavingSmokeTest compiles in every build, keeping the smoke test in
+            sync with the three sibling repos. It is only *executed* under the `vmlens`
+            profile; the managed surefire <excludes> below keeps the ordinary suite from
+            running it agent-less (a vacuous pass that prints an "agent not configured"
+            warning).
+        -->
+        <dependency>
+            <groupId>com.vmlens</groupId>
+            <artifactId>api</artifactId>
+            <version>${vmlens.version}</version>
+            <scope>test</scope>
+        </dependency>
     </dependencies>
     <build>
         <pluginManagement>
@@ -232,6 +247,19 @@ SPDX-License-Identifier: Apache-2.0
                     <groupId>org.apache.maven.plugins</groupId>
                     <artifactId>maven-surefire-plugin</artifactId>
                     <version>3.5.6</version>
+                    <configuration>
+                        <!--
+                            Tests in the `vmlens` package are meaningful only under the vmlens
+                            agent (the `vmlens` profile). Without the agent an AllInterleavings
+                            loop body never runs (a vacuous pass that prints an "agent not
+                            configured" warning), so keep the whole package out of the ordinary
+                            surefire run. The `vmlens` profile's whole-suite run still picks
+                            these up (they are not in that plugin's <excludes>).
+                        -->
+                        <excludes>
+                            <exclude>**/vmlens/*.java</exclude>
+                        </excludes>
+                    </configuration>
                 </plugin>
                 <plugin>
                     <groupId>org.apache.maven.plugins</groupId>

src/test/java/net/ladenthin/streambuffer/vmlens/StreamBufferReaderWriterInterleavingTest.java

@@ -0,0 +1,85 @@
+// SPDX-FileCopyrightText: 2014-2026 Bernard Ladenthin <bernard.ladenthin@gmail.com>
+//
+// 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}.
+ *
+ * <p>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} <em>outside</em> {@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 <em>every</em> interleaving — no byte may be lost or
+ * double-counted in the hand-off between the lock-free wait gate and the
+ * lock-protected mutation.</p>
+ *
+ * <p>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
+ * <em>termination</em>, 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 <excludes>} in {@code pom.xml}).</p>
+ */
+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<Throwable> 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()));
+            }
+        }
+    }
+}

src/test/java/net/ladenthin/streambuffer/vmlens/VmlensInterleavingSmokeTest.java

@@ -0,0 +1,57 @@
+// SPDX-FileCopyrightText: 2014-2026 Bernard Ladenthin <bernard.ladenthin@gmail.com>
+//
+// 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.
+ *
+ * <p>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.</p>
+ *
+ * <p>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 <excludes>}
+ * 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.</p>
+ */
+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));
+            }
+        }
+    }
+}