Data.LSMRRBVector.Internal

Log-Structured Merge RRB Vector Internals

Reexports

Definitions

emptyBuffer : Buffer a

  Empty mutation buffer.
  

Totality: total
Visibility: export

emptyWriteBuffers : WriteBuffers a

  Empty buffer state.
  

Totality: total
Visibility: export

bufferEmpty : Buffer a -> Bool

  Determines whether a buffer contains pending entries.
  
  Returns:
  - True when no buffered operations exist.
  - False otherwise.
  
  Properties:
  - O(1).
  

Totality: total
Visibility: export

threadContextEmpty : ThreadContext a -> Bool

  Determines whether a thread context contains buffered work.
  
  Returns:
  - True when all thread-local mutation state is empty.
  - False otherwise.
  
  Properties:
  - O(1).
  
  Notes:
  - Sequence numbers are ignored.
  - Historical sequence advancement does not imply pending work.
  

Totality: total
Visibility: export

initialRebuildMetrics : RebuildMetrics

  Empty rebuild metrics.
  
  Properties:
  - No rebuilds observed.
  - Average batch size is effectively zero.
  

Totality: total
Visibility: export

initialRebuildServiceState : RebuildServiceState

  Initial rebuild service state.
  
  Properties:
  - Service begins idle.
  - No rebuild failures recorded.
  

Totality: total
Visibility: export

updateMetrics : RebuildMetrics -> Nat -> RebuildMetrics

  Updates rebuild metrics after a successful rebuild cycle.
  
  Parameters:
  - batchsize: Number of entries processed in this cycle.
  
  Properties:
  - O(1).
  - Pure deterministic update.
  

Totality: total
Visibility: export

averageBatchSize : RebuildMetrics -> Nat

  Computes average rebuild batch size.
  
  Returns:
  - 0 when no rebuilds have occurred.
  

Totality: total
Visibility: export

registerThread : Ref World (SortedMap ThreadId (ThreadContext a)) -> ThreadId -> IO (ThreadContext a)

  Registers a thread if necessary and returns its thread context.
  
  Behavior:
  - Existing registrations are reused.
  - Missing registrations allocate fresh thread state.
  
  Properties:
  - One ThreadContext per ThreadId.
  - Preserves existing mutation state.
  

Totality: total
Visibility: export

enterGeneration : Ref World (CombinedSnapshotState a) -> ThreadId -> IO (SnapshotState a)

  Announces that a thread has entered a snapshot read section.
  
  Behavior:
  - Registers the generation currently being read.
  - Replaces any previous generation announcement.
  
  Properties:
  - O(log n).
  - One active generation per thread.
  - Used by reclamation safety checks.
  

Totality: total
Visibility: export

leaveGeneration : Ref World (CombinedSnapshotState a) -> ThreadId -> IO ()

  Announces that a thread has completed a snapshot read section.
  
  Behavior:
  - Removes thread participation state.
  - Indicates thread no longer references a snapshot.
  
  Properties:
  - O(log n).
  - Enables reclamation progress.
  

Totality: total
Visibility: export

minimumGeneration : SortedMap ThreadId ReaderState -> Maybe Generation

  Finds oldest active generation.
  
  Returns:
  - Nothing when no readers exist.
  - Just generation otherwise.
  
  Properties:
  - O(n).
  

Totality: total
Visibility: export

appendEntry : Buffer a -> Entry a -> Buffer a

  Appends an Entry onto the end of a mutation buffer.
  
  Properties:
  - O(1).
  - Preserves insertion ordering.
  

Totality: total
Visibility: export

writeOperation : WriteBuffers a -> Entry a -> WriteBuffers a

  Appends a deferred mutation into the active write buffer.
  
  Properties:
  - Frozen buffer remains unchanged.
  - O(1) amortized.
  

Totality: total
Visibility: export

enqueueOperation : Ref World (SortedMap ThreadId (ThreadContext a)) -> Ref World (CombinedSnapshotState a) -> ThreadId -> Operation a -> IO Bool

  Converts an operation into an Entry and appends it into the owning thread's active mutation buffer.
  
  Steps:
  - Acquire current timestamp.
  - Register thread if necessary.
  - Allocate Entry.
  - Increment sequence counter.
  - Append into active write buffer.
  - Increment global write pressure.
  - Mark rebuild work as pending.
  
  Properties:
  - O(log n) registry update.
  - O(1) buffer append.
  - Deterministic replay ordering.
  - Adaptive batching pressure is globally visible atomically.
  

Totality: total
Visibility: export

triggerRebuild : LSMRRBVector World a -> RebuildService Poll -> Async Poll [Errno] ()

  Sends a rebuild notification to the background rebuilder.
  
  Behavior:
  - Requests background progression toward snapshot publication.
  - Multiple requests may be coalesced.
  - Triggering occurs only after adaptive batching thresholds indicate sufficient accumulated write pressure.
  
  Notes:
  - Does not guarantee immediate rebuild execution.
  - Does not guarantee publication.
  

Totality: total
Visibility: export

scheduleIfNeeded : LSMRRBVector World a -> RebuildService Poll -> Bool -> Async Poll [Errno] ()

  Schedules rebuild work if adaptive batching has reached its target.
  
  Behavior:
  - Checks whether the current write accumulation has crossed the adaptive batch threshold.
  - Coalesces multiple concurrent scheduling attempts.
  
  Properties:
  - O(1).
  - Avoids duplicate rebuild requests.
  

Totality: total
Visibility: export

rotateBuffers : ThreadContext a -> (ThreadContext a, Buffer a)

  Extract active buffer ownership for rebuilding.
  
  Returns:
  - Updated thread context with empty active buffer
  - Extracted buffer now owned by rebuilder
  

Totality: total
Visibility: export

rotateAllBuffers : Ref World (SortedMap ThreadId (ThreadContext a)) -> IO (List (Buffer a))

  Atomically extracts active buffers from all registered threads.
  
  Behavior:
  - Replaces active buffers with empty buffers.
  - Transfers ownership of previous active buffers.
  - Removes thread registrations whose post-rotation state contains no pending work.
  
  Lifecycle:
  - Rotated thread contexts whose active buffer becomes empty are removed.
  - Because only active buffers contribute to emptiness, rebuild currently removes all rotated thread registrations.
  - Explicit thread unregistration is unnecessary.
  
  Properties:
  - Extracted entries appear exactly once.
  - Prevents unbounded registry growth.
  - O(number of registered threads).
  

Totality: total
Visibility: export

bufferEntries : Buffer a -> List (Entry a)

  Converts a buffer into a list of contained entries.
  
  Behavior:
  - Preserves insertion order.
  - Extracts buffered mutation events for rebuild processing.
  
  Properties:
  - O(n).
  - Does not modify buffer ownership.
  - Pure projection operation.
  
  Notes:
  - Intended for rebuild entry collection.
  

Totality: total
Visibility: export

collectEntries : List (Buffer a) -> List (Entry a)

  Collects entries from multiple extracted buffers.
  
  Behavior:
  - Traverses all buffers.
  - Concatenates their entries into a single list.
  
  Properties:
  - O(total entries).
  - Preserves per-buffer ordering.
  - Does not perform global ordering.
  
  Notes:
  - Intended as a preprocessing step before sorting.
  

Totality: total
Visibility: export

sortEntries : Ord (Entry a) => List (Entry a) -> List (Entry a)

  Produces a deterministic global ordering of buffered entries.
  
  Ordering:
  - timestamp
  - thread id
  - sequence number
  
  Properties:
  - O(n log n).
  - Deterministic across rebuild cycles.
  
  Notes:
  - Required before replay to ensure stable behavior under concurrent writes.
  

Totality: total
Visibility: export

applyOperation : Operation a -> RRBVector a -> RRBVector a

  Applies a single deferred mutation to an RRBVector snapshot.
  
  Behavior:
  - Executes the logical operation represented by Operation.
  - Produces a new immutable vector.
  - Does not mutate the supplied vector.
  
  Variants:
  - Append  -> append value to end
  - Prepend -> prepend value to beginning
  - Insert  -> insert value at index
  - Delete  -> remove value at index
  - Update  -> replace value at index
  
  Properties:
  - Pure.
  - Deterministic.
  - Preserves RRBVector immutability.
  
  Notes:
  - Bounds behavior is inherited from the underlying RRBVector operation.
  

Totality: total
Visibility: export

replayEntries : List (Entry a) -> RRBVector a -> RRBVector a

  Replays a sequence of buffered mutations onto an immutable snapshot.
  
  Behavior:
  - Traverses entries in order.
  - Applies each contained operation to the accumulating vector.
  - Produces a rebuilt snapshot reflecting all replayed mutations.
  
  Ordering:
  - Replay order is exactly the order of the supplied entry list.
  - Deterministic replay therefore depends on prior sorting.
  
  Properties:
  - Pure.
  - O(number of entries × operation cost).
  - Preserves snapshot immutability.
  
  Notes:
  - Typically executed after collectEntries and sortEntries.
  - Does not validate entry ordering.
  

Totality: total
Visibility: export

readSnapshotWithGeneration : LSMRRBVector World a -> ThreadId -> ((Generation, RRBVector a) -> b) -> IO b

  Reads the current immutable snapshot together with its generation.
  
  Behavior:
  - Atomically captures the current SnapshotState.
  - Registers the thread as an active reader of that generation.
  - Passes (generation, snapshot tree) to the user function.
  - Ensures reader registration is cleaned up after evaluation.
  
  Key property:
  - The generation and tree are consistent and taken from the same CAS snapshot.
  
  This enables:
  - Precise visibility reasoning.
  - Safe interaction with reclamation.
  - Deterministic debugging of snapshot lag.
  
  Complexity:
  - O(log n) for reader registration/removal.
  - O(1) snapshot access.
  

Totality: total
Visibility: export

rebuildMetrics : RebuildServiceState -> RebuildMetrics

  Returns current rebuild metrics.
  
  Properties:
  - O(1)
  - Snapshot of current service state
  

Totality: total
Visibility: export

averageRebuildBatchSize : RebuildServiceState -> Nat

  Returns average rebuild batch size.
  
  Properties:
  - O(1)
  

Totality: total
Visibility: export

adjustBatchWindow : Nat -> Nat -> Nat

  Adjusts adaptive batching window according to observed write pressure.
  
  Rules:
  - Pressure above the current window expands the window.
  - Pressure below half the current window shrinks the window.
  - Window never shrinks below 1.
  
  Properties:
  - Pure deterministic policy function.
  - Does not affect correctness.
  - Only influences rebuild batching behavior.
  

Totality: total
Visibility: export

publishSnapshot : Ref World (CombinedSnapshotState a) -> List (Entry a) -> IO Generation

  Atomically publishes a rebuilt snapshot and advances adaptive batching state.
  
  Steps:
  - Publish rebuilt immutable tree.
  - Increment snapshot generation.
  - Retire previous snapshot.
  - Reset accumulated write pressure.
  - Clear rebuild pending state.
  - Adaptively adjust batching window.
  
  Properties:
  - Snapshot publication is atomic.
  - Readers always observe a consistent snapshot/generation pair.
  - Adaptive batching state transitions are globally visible atomically.
  - Previous snapshots become eligible for reclamation.
  
  Notes:
  - Adaptive batching decisions are based on write pressure observed since the previous successful publication.
  

Totality: total
Visibility: export

reclamationCutoff : List (RetiredSnapshot a) -> SortedMap ThreadId ReaderState -> Maybe Generation

  Computes the newest retired generation that may safely be reclaimed.
  
  Behavior:
  - Determines the oldest snapshot generation currently referenced by active readers.
  - Finds the highest retired generation strictly older than that reader boundary.
  - Returns Nothing when no reclaimable generation exists.
  
  Returns:
  - Nothing: No readers exist, or no retired snapshots can be reclaimed.
  - Just g: Every retired snapshot with generation <= g may safely be reclaimed.
  
  Safety rules:
  - Readers observing generation G may still require snapshot G.
  - Readers may also require all newer generations.
  - Only snapshots strictly older than the oldest active reader generation are reclaimable.
  
  Example:
  
  Retired              <-> [1,2,3,4,5]
  Active readers       <-> [4,7]
  Oldest active reader <-> 4
  Safe reclamation     <-> [1,2,3]
  Result               <-> Just 3
  
  Properties:
  - O(number of retired snapshots + number of readers).
  - Never reclaims a snapshot visible to any active reader.
  - Computes a maximal safe reclamation boundary.
  

Totality: total
Visibility: export

reclaimSnapshots : Ref World (CombinedSnapshotState a) -> IO ()

  Reclaims retired snapshots no longer visible to active readers.
  
  Rules:
  - No readers: Reclaim everything.
  - Readers exist: retain snapshots at or newer than the oldest active reader boundary.
  
  Properties:
  - Safe generation-based reclamation.
  - Keeps only snapshots potentially observable by readers.
  - O(number of retired snapshots + number of readers).
  

Totality: total
Visibility: export

rebuildOnce : Ord (Entry a) => Ref World (SortedMap Int (ThreadContext a)) -> Ref World (CombinedSnapshotState a) -> RebuildServiceState -> Async Poll [Errno] (RebuildServiceState, (Generation, Bool))

  Executes one rebuild pass.
  
  Steps:
  - Rotate all active buffers.
  - Collect extracted entries.
  - Sort entries deterministically.
  - Publish rebuilt snapshot.
  - Reclaim retired snapshots.
  
  Returns:
  - Newly published generation when entries were processed.
  - 0 only when no entries were available and publication did not occur.
  - Whether any entries were processed.
  
  Notes:
  - Performs exactly one ownership-transfer cycle.
  - Does not guarantee complete draining.
  

Visibility: export

flushUntilEmpty : Ord (Entry a) => LSMRRBVector World a -> RebuildServiceState -> Async Poll [Errno] (RebuildServiceState, Generation)

  Repeatedly performs rebuild cycles until a rotation extracts no work.
  
  Behavior:
  - Executes rebuild cycles in sequence.
  - Each cycle atomically rotates ownership of active buffers.
  - Extracted entries are rebuilt into a published snapshot.
  - Terminates once a rotation produces no extracted entries.
  
  Visibility guarantees:
  - Flush establishes a quiescent visibility boundary at buffer rotation.
  - All writes already present in rotated buffers are incorporated before completion.
  - Writes arriving concurrently may appear either before or after completion depending on timing.
  - Flush does not stop writers or establish a global synchronization barrier.
  
  Concurrency properties:
  - Writers continue appending during rebuild execution.
  - Multiple rebuild cycles may be required if writes continue arriving.
  - Progress remains lock-free for writers.
  
  Returns:
  - Final rebuild state.
  - Most recently published generation.
  
  Notes:
  - Completion means no buffered work was visible during the final rotation.
  - This is weaker than "all writes before return".
  - Stronger linearizable flush semantics would require an explicit epoch or barrier mechanism.
  - Currently unused by rebuild request processing.
  - May serve as the implementation basis for future flush semantics.
  

Visibility: export

handleRebuildRequest : Ord (Entry a) => LSMRRBVector World a -> RebuildServiceState -> RebuildRequest -> Async Poll [Errno] ()

  Processes a rebuild request issued by the LSM write system.
  
  This service is responsible for advancing the immutable snapshot from the accumulated thread-local mutation buffers.
  
  Two modes of operation exist:
  
  Trigger:
  - Performs exactly one rebuildOnce invocation.
  - May publish at most one snapshot.
  - Additional buffered work remains for future rebuild requests.
  
  Flush:
  - Repeatedly performs rebuild cycles until all buffered writes observed at invocation time are incorporated.
  - Guarantees that all writes visible in rotated buffers during draining are reflected in the returned generation.
  - Concurrent writes may be incorporated either before or after completion.
  - May perform multiple rotations and publications internally.
  
  Concurrency guarantees:
  - Writers may continue appending during rebuild.
  - Flush only guarantees completeness relative to a quiescent cut of buffer rotation visibility.
  
  Return values:
  - Trigger returns unit acknowledgement.
  - Flush returns the final snapshot generation after draining.
  
  State transitions:
  Sleeping → RotatingBuffers → CollectingEntries → SortingEntries → PublishingSnapshot → Sleeping
  
  Notes:
  - Empty rebuild cycles do not advance generation.
  - Flush drains until a cycle produces no entries.
  - Trigger is a bounded operation, Flush is unbounded (but finite under quiescent assumptions).
  

Visibility: export

rebuilderService : Ord (Entry a) => LSMRRBVector World a -> RebuildServiceState -> List (LSMRRBVector World a -> RebuildService Poll -> RebuildServiceState -> Async Poll [Errno] ()) -> Async Poll [Errno] ()

  Constructs and launches user-supplied rebuild (writer) actions concurrently.
  
  Behavior:
  - Creates a RebuildService endpoint.
  - Routes rebuild requests into handleRebuildRequest.
  - Starts all supplied rebuild-service actions concurrently.
  
  Concurrency:
  - Actions execute in parallel.
  - All actions share the same LSMRRBVector instance.
  - All actions share the same rebuild request endpoint.
  
  Properties:
  - Service composition utility.
  - Does not itself perform rebuild work.
  - Rebuild execution occurs only when actions issue requests.
  
  Notes:
  - Used to launch rebuild workers supporting background maintenance tasks.
  

Visibility: export

lsmrrbvectorService : LSMRRBVector World a -> List (LSMRRBVector World a -> Async Poll [Errno] ()) -> Async Poll [Errno] ()

  Constructs and launches user-supplied reader actions concurrently.
  
  Behavior:
  - Executes all supplied actions in parallel.
  - Provides each action access to the shared LSMRRBVector instance.
  
  Concurrency:
  - Actions may perform reads.
  - Execution order is not specified.
  - Actions run independently.
  
  Properties:
  - Service composition utility.
  - Does not perform vector operations itself.
  
  Notes:
  - Used to launch application readers.
  

Visibility: export

rebuilderAndLSMRRBVectorService : Async Poll [Errno] () -> Async Poll [Errno] () -> Async Poll [Errno] ()

  Runs rebuild infrastructure and reader workloads together.
  
  Behavior:
  - Executes the rebuilderService (writers) and lsmrrbvectorService (readers) concurrently.
  - Allows writers and readers to operate while rebuild work proceeds in the background.
  
  Concurrency:
  - Neither service blocks the other.
  - Rebuild publication may occur concurrently with reads and writes.
  
  Properties:
  - Top-level composition utility.
  - Establishes the complete LSMRRBVector runtime.
  
  Notes:
  - Intended as the final composition point used by runEmptyWith.
  

Visibility: export