feat(buffers): SUT-side antithesis underflow assertions

LICENSE-3rdparty.csv

@@ -18,6 +18,8 @@ anstyle,https://github.com/rust-cli/anstyle,MIT OR Apache-2.0,The anstyle Author
 anstyle-parse,https://github.com/rust-cli/anstyle,MIT OR Apache-2.0,The anstyle-parse Authors
 anstyle-query,https://github.com/rust-cli/anstyle,MIT OR Apache-2.0,The anstyle-query Authors
 anstyle-wincon,https://github.com/rust-cli/anstyle,MIT OR Apache-2.0,The anstyle-wincon Authors
+antithesis-instrumentation,https://github.com/antithesishq/antithesis-instrumentation-rust,MIT,The antithesis-instrumentation Authors
+antithesis_sdk,https://github.com/antithesishq/antithesis-sdk-rust,MIT,The antithesis_sdk Authors
 anyhow,https://github.com/dtolnay/anyhow,MIT OR Apache-2.0,David Tolnay <dtolnay@gmail.com>
 apache-avro,https://github.com/apache/avro-rs,Apache-2.0,The apache-avro Authors
 arbitrary,https://github.com/rust-fuzz/arbitrary,MIT OR Apache-2.0,"The Rust-Fuzz Project Developers, Nick Fitzgerald <fitzgen@gmail.com>, Manish Goregaokar <manishsmail@gmail.com>, Simonas Kazlauskas <arbitrary@kazlauskas.me>, Brian L. Troutwine <brian@troutwine.us>, Corey Farwell <coreyf@rwell.org>"
@@ -427,12 +429,15 @@ lexical-util,https://github.com/Alexhuszagh/rust-lexical,MIT OR Apache-2.0,Alex
 lexical-write-float,https://github.com/Alexhuszagh/rust-lexical,MIT OR Apache-2.0,Alex Huszagh <ahuszagh@gmail.com>
 lexical-write-integer,https://github.com/Alexhuszagh/rust-lexical,MIT OR Apache-2.0,Alex Huszagh <ahuszagh@gmail.com>
 libc,https://github.com/rust-lang/libc,MIT OR Apache-2.0,The Rust Project Developers
+libloading,https://github.com/nagisa/rust_libloading,ISC,Simonas Kazlauskas <libloading@kazlauskas.me>
 libm,https://github.com/rust-lang/libm,MIT OR Apache-2.0,Jorge Aparicio <jorge@japaric.io>
 libsqlite3-sys,https://github.com/rusqlite/rusqlite,MIT,The rusqlite developers
 libz-sys,https://github.com/rust-lang/libz-sys,MIT OR Apache-2.0,"Alex Crichton <alex@alexcrichton.com>, Josh Triplett <josh@joshtriplett.org>, Sebastian Thiel <sebastian.thiel@icloud.com>"
 line-clipping,https://github.com/joshka/line-clipping,MIT OR Apache-2.0,Josh McKinney
 linked-hash-map,https://github.com/contain-rs/linked-hash-map,MIT OR Apache-2.0,"Stepan Koltsov <stepan.koltsov@gmail.com>, Andrew Paseltiner <apaseltiner@gmail.com>"
 linked_hash_set,https://github.com/alexheretic/linked-hash-set,Apache-2.0,Alex Butler <alexheretic@gmail.com>
+linkme,https://github.com/dtolnay/linkme,MIT OR Apache-2.0,David Tolnay <dtolnay@gmail.com>
+linkme-impl,https://github.com/dtolnay/linkme,MIT OR Apache-2.0,David Tolnay <dtolnay@gmail.com>
 linux-raw-sys,https://github.com/sunfishcode/linux-raw-sys,Apache-2.0 WITH LLVM-exception OR Apache-2.0 OR MIT,Dan Gohman <dev@sunfishcode.online>
 listenfd,https://github.com/mitsuhiko/listenfd,Apache-2.0,Armin Ronacher <armin.ronacher@active-4.com>
 litemap,https://github.com/unicode-org/icu4x,Unicode-3.0,The ICU4X Project Developers

lib/vector-buffers/src/lib.rs

@@ -14,6 +14,10 @@
 #[macro_use]
 extern crate tracing;
 
+// Keep the Antithesis LLVM coverage-instrumentation runtime shim linked into any
+// binary that uses this crate (e.g. the Vector SUT). No effect outside Antithesis.
+use antithesis_instrumentation as _;
+
 mod buffer_usage_data;
 
 pub mod config;

lib/vector-buffers/src/variants/disk_v2/ledger.rs

@@ -29,6 +29,37 @@ use crate::buffer_usage_data::BufferUsageHandle;
 
 pub const LEDGER_LEN: usize = align16(mem::size_of::<ArchivedLedgerState>());
 
+/// SUT-side Antithesis assertion: the in-memory `total_buffer_size` accounting
+/// atomic is never decremented by more than its current value. A violation is
+/// the root of Vector #21683 — the unsaturated `fetch_sub` wraps toward 2^64,
+/// `is_buffer_full()` then returns true forever, and the writer deadlocks.
+/// Isolated in its own function with broad `allow`s because `lib.rs` sets
+/// `#![deny(warnings)]` + `#![deny(clippy::pedantic)]` and the assertion-macro
+/// expansion need not satisfy those. No-op outside Antithesis.
+#[inline]
+#[allow(warnings, clippy::all, clippy::pedantic)]
+fn assert_total_buffer_size_no_underflow(current: u64, amount: u64) {
+    antithesis_sdk::assert_always!(
+        amount <= current,
+        "ledger total_buffer_size decrement never underflows (root of #21683)"
+    );
+}
+
+/// SUT-side Antithesis assertion: `get_total_records` computes the count as
+/// `next_writer_id.wrapping_sub(last_reader_id) - 1`. When the wrapped
+/// difference is `0` (a fully drained buffer where the reader has caught up to
+/// the writer's next id), the trailing `- 1` underflows to ~2^64 — a bogus
+/// ~18-quintillion buffered-records reading. The invariant is that the wrapped
+/// difference is always at least 1. No-op outside Antithesis.
+#[inline]
+#[allow(warnings, clippy::all, clippy::pedantic)]
+fn assert_total_records_no_underflow(next_writer_id: u64, last_reader_id: u64) {
+    antithesis_sdk::assert_always!(
+        next_writer_id.wrapping_sub(last_reader_id) >= 1,
+        "ledger get_total_records never underflows on a drained buffer (#21683 metrics)"
+    );
+}
+
 /// Error that occurred during calls to [`Ledger`].
 #[derive(Debug, Snafu)]
 pub enum LedgerLoadCreateError {
@@ -263,6 +294,7 @@ where
         let next_writer_id = self.state().get_next_writer_record_id();
         let last_reader_id = self.state().get_last_reader_record_id();
 
+        assert_total_records_no_underflow(next_writer_id, last_reader_id);
         next_writer_id.wrapping_sub(last_reader_id) - 1
     }
 
@@ -289,6 +321,10 @@ where
 
     /// Decrements the total number of bytes for all unread records in the buffer.
     pub fn decrement_total_buffer_size(&self, amount: u64) {
+        assert_total_buffer_size_no_underflow(
+            self.total_buffer_size.load(Ordering::Acquire),
+            amount,
+        );
         let last_total_buffer_size = self.total_buffer_size.fetch_sub(amount, Ordering::AcqRel);
         trace!(
             previous_buffer_size = last_total_buffer_size,

lib/vector-buffers/src/variants/disk_v2/reader.rs

@@ -27,6 +27,22 @@ use crate::{
     variants::disk_v2::{io::AsyncFile, record::try_as_record_archive},
 };
 
+/// SUT-side Antithesis assertion: when accounting for a partially-read or
+/// truncated data file, `delete_completed_data_file` computes the buffer-size
+/// adjustment as `metadata.len() - bytes_read`. If the on-disk file is shorter
+/// than the bytes we believe we read (a torn tail after a crash, or filesystem
+/// fault), this unsaturated subtraction underflows to ~2^64 and is then fed
+/// into `decrement_total_buffer_size` — a #21683-class wrap. The invariant is
+/// `bytes_read <= metadata.len()`. No-op outside Antithesis.
+#[inline]
+#[allow(warnings, clippy::all, clippy::pedantic)]
+fn assert_data_file_size_delta_no_underflow(file_len: u64, bytes_read: u64) {
+    antithesis_sdk::assert_always!(
+        bytes_read <= file_len,
+        "reader data-file size delta never underflows (reader.rs:524, #21683-class)"
+    );
+}
+
 pub(super) struct ReadToken {
     record_id: u64,
     record_bytes: usize,
@@ -521,6 +537,7 @@ where
         let decrease_amount = bytes_read.map_or_else(
             || metadata.len(),
             |bytes_read| {
+                assert_data_file_size_delta_no_underflow(metadata.len(), bytes_read);
                 let size_delta = metadata.len() - bytes_read;
                 if size_delta > 0 {
                     debug!(