Idris2Doc : Data.LSMRRBVector.Types

Data.LSMRRBVector.Types

(source)
Log-Structured Merge RRB Vector Types

Definitions

data RebuildRequest : Type
  Requests sent to the rebuild service.
  
  Trigger:
  - Indicates new buffered work exists.
  - Marks rebuild work as pending.
  - Does not initiate rebuild.

Totality: total
Visibility: public export
Constructor: 
Trigger : RebuildRequest

Hints:
Eq RebuildRequest
Show RebuildRequest
record RebuildService : (0 _ : Type) -> Type
Totality: total
Visibility: public export
Constructor: 
MkRebuildService : (RebuildRequest -> Async e [Errno] ()) -> RebuildService e

Projection: 
.run : RebuildService e -> RebuildRequest -> Async e [Errno] ()
.run : RebuildService e -> RebuildRequest -> Async e [Errno] ()
Totality: total
Visibility: public export
run : RebuildService e -> RebuildRequest -> Async e [Errno] ()
Totality: total
Visibility: public export
rebuilder : (RebuildRequest -> Async e [Errno] ()) -> Async e es (RebuildService e)
Visibility: export
Generation : Type
  Snapshot generation identifier.
  
  Represents the logical version of the currently published
  immutable snapshot.
  
  Properties:
  - Monotonically increasing.
  - Incremented only after successful publication.
  - Readers may compare generations to detect snapshot changes.
  
  Notes:
  - Does not encode time.
  - Exists purely for ordering and visibility.

Totality: total
Visibility: public export
ThreadId : Type
  A wrapper over Int for thread ids.

Totality: total
Visibility: public export
data Operation : Type -> Type
  Operation represents a deferred vector mutation.
  
  Rather than mutating the underlying RRBVector immediately, all user
  modifications are first converted into Operations and appended into
  thread-indexed shared state.
  
  Variants:
  - Prepend a
    Insert a value at the logical beginning.
  - Append a
    Insert a value at the logical end.
  - Insert Nat a
    Insert a value at a specified index.
  - Delete Nat
    Remove a value at a specified index.
  - Update Nat a
    Replace a value at a specified index.
  
  Role in LSM design:
  - Forms the deferred mutation layer.
  - Enables batching.
  - Prevents writers from mutating snapshots.
  
  Notes:
  Indices are interpreted relative to the visible snapshot together with preceding replayed operations.

Totality: total
Visibility: public export
Constructors:
Prepend : a -> Operation a
Append : a -> Operation a
Insert : Nat -> a -> Operation a
Delete : Nat -> Operation a
Update : Nat -> a -> Operation a

Hints:
Eq {arg:5479} => Eq (Operation {arg:5479})
Show {arg:5479} => Show (Operation {arg:5479})
record Entry : Type -> Type
  Entry represents a deferred mutation event.
  
  Every user write becomes an Entry before entering a thread buffer.
  
  Fields:
  - operation <-> Deferred mutation
  - timestamp <-> Wall-clock ordering hint
  - threadid  <-> Originating thread
  - sequence  <-> Monotonic per-thread counter
  
  Ordering:
  - Entries are sorted using (timestamp, threadid, sequence).
  - This guarantees deterministic replay even when timestamps collide.
  
  Role in LSM design:
  - Unit of deferred work.
  - Supports deterministic rebuild.

Totality: total
Visibility: public export
Constructor: 
MkEntry : Operation a -> IClock CLOCK_REALTIME -> Int -> Nat -> Entry a

Projections:
.operation : Entry a -> Operation a
.sequence : Entry a -> Nat
.threadid : Entry a -> Int
.timestamp : Entry a -> IClock CLOCK_REALTIME

Hints:
Eq a => Eq (Entry a)
Eq (Entry a) => Ord (Entry a)
Show a => Show (Entry a)
.operation : Entry a -> Operation a
Totality: total
Visibility: public export
operation : Entry a -> Operation a
Totality: total
Visibility: public export
.timestamp : Entry a -> IClock CLOCK_REALTIME
Totality: total
Visibility: public export
timestamp : Entry a -> IClock CLOCK_REALTIME
Totality: total
Visibility: public export
.threadid : Entry a -> Int
Totality: total
Visibility: public export
threadid : Entry a -> Int
Totality: total
Visibility: public export
.sequence : Entry a -> Nat
Totality: total
Visibility: public export
sequence : Entry a -> Nat
Totality: total
Visibility: public export
record Buffer : Type -> Type
  Single append-efficient mutation log.
  
  Represents one physical mutation buffer.

Totality: total
Visibility: public export
Constructor: 
MkBuffer : SnocList (Entry a) -> Nat -> Buffer a

Projections:
.entries : Buffer a -> SnocList (Entry a)
.length : Buffer a -> Nat

Hints:
Eq a => Eq (Buffer a)
Show a => Show (Buffer a)
.entries : Buffer a -> SnocList (Entry a)
Totality: total
Visibility: public export
entries : Buffer a -> SnocList (Entry a)
Totality: total
Visibility: public export
.length : Buffer a -> Nat
Totality: total
Visibility: public export
length : Buffer a -> Nat
Totality: total
Visibility: public export
record WriteBuffers : Type -> Type
  Thread-local mutation state.
  
  Writers append only to active.
  
  During rebuild:
  - Active buffers are extracted atomically.
  - Ownership transfers to the rebuilder.
  - Writers immediately continue on a fresh buffer.
  
  Properties:
  - O(1) amortized append.
  - No stop-the-world pauses.
  - No shared rebuild ownership.

Totality: total
Visibility: public export
Constructor: 
MkWriteBuffers : Buffer a -> WriteBuffers a

Projection: 
.active : WriteBuffers a -> Buffer a

Hints:
Eq a => Eq (WriteBuffers a)
Show a => Show (WriteBuffers a)
.active : WriteBuffers a -> Buffer a
Totality: total
Visibility: public export
active : WriteBuffers a -> Buffer a
Totality: total
Visibility: public export
record ThreadContext : Type -> Type
  ThreadContext stores per-thread mutation state.
  
  Ownership:
  - One ThreadContext exists per registered thread.
  
  Fields:
  - threadid <-> Unique thread identifier
  - sequence <-> Monotonically increasing local counter used for deterministic ordering
  - buffers  <-> Thread-owned double-buffer state
  
  Properties:
  - Per-thread logical ownership.
  - Shared registry storage.
  - Low-contention write path.

Totality: total
Visibility: public export
Constructor: 
MkThreadContext : Int -> Nat -> WriteBuffers a -> ThreadContext a

Projections:
.buffers : ThreadContext a -> WriteBuffers a
.sequence : ThreadContext a -> Nat
.threadid : ThreadContext a -> Int

Hints:
Eq a => Eq (ThreadContext a)
Show a => Show (ThreadContext a)
.threadid : ThreadContext a -> Int
Totality: total
Visibility: public export
threadid : ThreadContext a -> Int
Totality: total
Visibility: public export
.sequence : ThreadContext a -> Nat
Totality: total
Visibility: public export
sequence : ThreadContext a -> Nat
Totality: total
Visibility: public export
.buffers : ThreadContext a -> WriteBuffers a
Totality: total
Visibility: public export
buffers : ThreadContext a -> WriteBuffers a
Totality: total
Visibility: public export
data RebuildState : Type
  RebuildState represents rebuild thread progress.
  
  Lifecycle:
  
  Sleeping
       ↓
  RotatingBuffers
       ↓
  CollectingEntries
       ↓
  SortingEntries
       ↓
  PublishingSnapshot
       ↓
  Sleeping

Totality: total
Visibility: public export
Constructors:
Sleeping : RebuildState
RotatingBuffers : RebuildState
CollectingEntries : RebuildState
SortingEntries : RebuildState
PublishingSnapshot : RebuildState

Hints:
Eq RebuildState
Show RebuildState
record RebuildMetrics : Type
  Runtime rebuild statistics.
  
  Metrics are updated after successful rebuild cycles and provide lightweight visibility into rebuild behavior.
  
  Fields:
  - lastbatchsize  <-> Number of entries processed during most recent rebuild.
  - totalbatchsize <-> Total number of entries processed across all rebuilds.
  - rebuildcount   <-> Number of successful rebuild cycles.
  
  Derived values:
  - average batch size: totalbatchsize / rebuildcount
  
  Properties:
  - Updated only by the rebuild worker.
  - Does not affect correctness.
  - Intended for observability and adaptive tuning.

Totality: total
Visibility: public export
Constructor: 
MkRebuildMetrics : Nat -> Nat -> Nat -> RebuildMetrics

Projections:
.lastbatchsize : RebuildMetrics -> Nat
.rebuildcount : RebuildMetrics -> Nat
.totalbatchsize : RebuildMetrics -> Nat

Hints:
Eq RebuildMetrics
Show RebuildMetrics
.lastbatchsize : RebuildMetrics -> Nat
Totality: total
Visibility: public export
lastbatchsize : RebuildMetrics -> Nat
Totality: total
Visibility: public export
.totalbatchsize : RebuildMetrics -> Nat
Totality: total
Visibility: public export
totalbatchsize : RebuildMetrics -> Nat
Totality: total
Visibility: public export
.rebuildcount : RebuildMetrics -> Nat
Totality: total
Visibility: public export
rebuildcount : RebuildMetrics -> Nat
Totality: total
Visibility: public export
record RebuildServiceState : Type
  Controls execution of rebuild-cycle progress.
  
  Fields:
  - rebuildphase: Current phase of the rebuild pipeline.
  - rebuildmetrics: Runtime rebuild statistics.
  
  Properties:
  - Local service execution state only.
  - Mutable only by the rebuild worker.
  - Represents execution progress rather than global vector state.
  
  Notes:
  - Pending rebuild work is tracked globally through CombinedSnapshotState.rebuildpending.
  - Failure state is intentionally omitted.
  - Current rebuild operations are total and crash on unrecoverable runtime failures rather than persisting structured errors.

Totality: total
Visibility: public export
Constructor: 
MkRebuildServiceState : RebuildState -> RebuildMetrics -> RebuildServiceState

Projections:
.rebuildmetrics : RebuildServiceState -> RebuildMetrics
.rebuildphase : RebuildServiceState -> RebuildState

Hints:
Eq RebuildServiceState
Show RebuildServiceState
.rebuildphase : RebuildServiceState -> RebuildState
Totality: total
Visibility: public export
rebuildphase : RebuildServiceState -> RebuildState
Totality: total
Visibility: public export
.rebuildmetrics : RebuildServiceState -> RebuildMetrics
Totality: total
Visibility: public export
rebuildmetrics : RebuildServiceState -> RebuildMetrics
Totality: total
Visibility: public export
record ReaderState : Type
  Reader participation in generation tracking.
  
  Readers announce the snapshot generation currently being observed.
  
  Properties:
  - Updated only when entering/leaving a snapshot read section.
  - Used by reclamation to determine oldest active generation.
  - One entry per participating thread.

Totality: total
Visibility: public export
Constructor: 
MkReaderState : Generation -> ReaderState

Projection: 
.generation : ReaderState -> Generation
.generation : ReaderState -> Generation
Totality: total
Visibility: public export
generation : ReaderState -> Generation
Totality: total
Visibility: public export
record SnapshotState : Type -> Type
  Immutable published snapshot state.
  
  Represents the currently visible version of the vector.
  
  Fields:
  - generation <-> Monotonic snapshot version identifier
  - tree       <-> Immutable published RRB snapshot
  
  Publication properties:
  - Tree and generation are published atomically.
  - Readers always observe a consistent snapshot pair.
  - Eliminates visibility races between tree updates and generation updates.
  
  Lifecycle:
  
  rebuild
      ↓
  new snapshot tree
      ↓
  increment generation
      ↓
  atomic publication
      ↓
  visible to readers
  
  Notes:
  - SnapshotState is immutable once constructed.
  - Publication occurs by replacing the whole record.

Totality: total
Visibility: public export
Constructor: 
MkSnapshotState : Generation -> RRBVector a -> SnapshotState a

Projections:
.generation : SnapshotState a -> Generation
.tree : SnapshotState a -> RRBVector a
.generation : SnapshotState a -> Generation
Totality: total
Visibility: public export
generation : SnapshotState a -> Generation
Totality: total
Visibility: public export
.tree : SnapshotState a -> RRBVector a
Totality: total
Visibility: public export
tree : SnapshotState a -> RRBVector a
Totality: total
Visibility: public export
record RetiredSnapshot : Type -> Type
  Snapshot awaiting reclamation.
  
  A snapshot becomes retired after publication of a newer snapshot.
  
  Properties:
  - Immutable after retirement.
  - Safe to reclaim once no reader references its generation.

Totality: total
Visibility: public export
Constructor: 
MkRetiredSnapshot : Generation -> RRBVector a -> RetiredSnapshot a

Projections:
.generation : RetiredSnapshot a -> Generation
.tree : RetiredSnapshot a -> RRBVector a
.generation : RetiredSnapshot a -> Generation
Totality: total
Visibility: public export
generation : RetiredSnapshot a -> Generation
Totality: total
Visibility: public export
.tree : RetiredSnapshot a -> RRBVector a
Totality: total
Visibility: public export
tree : RetiredSnapshot a -> RRBVector a
Totality: total
Visibility: public export
record CombinedSnapshotState : Type -> Type
  Combined snapshot publication, reclamation, and batching state.
  
  Fields:
  - currentsnapshot: Current published immutable snapshot.
  - retiredsnapshots: Older snapshots awaiting reclamation.
  - readerstate: Active reader generation announcements.
  - writepressure: Number of writes accumulated since the last rebuild cycle.
  - rebuildpending: Indicates whether buffered work exists requiring rebuild.
  - batchwindow: Current adaptive rebuild target controlling how many writes are accumulated before rebuild behavior expands or contracts.
  
  Properties:
  - Updated atomically through CAS.
  - Shared between readers, writers, and rebuilder.
  - Adaptive batching decisions observe a globally consistent state.

Totality: total
Visibility: public export
Constructor: 
MkCombinedSnapshotState : SnapshotState a -> List (RetiredSnapshot a) -> SortedMap ThreadId ReaderState -> Nat -> Bool -> Nat -> CombinedSnapshotState a

Projections:
.batchwindow : CombinedSnapshotState a -> Nat
.currentsnapshot : CombinedSnapshotState a -> SnapshotState a
.readerstate : CombinedSnapshotState a -> SortedMap ThreadId ReaderState
.rebuildpending : CombinedSnapshotState a -> Bool
.retiredsnapshots : CombinedSnapshotState a -> List (RetiredSnapshot a)
.writepressure : CombinedSnapshotState a -> Nat
.currentsnapshot : CombinedSnapshotState a -> SnapshotState a
Totality: total
Visibility: public export
currentsnapshot : CombinedSnapshotState a -> SnapshotState a
Totality: total
Visibility: public export
.retiredsnapshots : CombinedSnapshotState a -> List (RetiredSnapshot a)
Totality: total
Visibility: public export
retiredsnapshots : CombinedSnapshotState a -> List (RetiredSnapshot a)
Totality: total
Visibility: public export
.readerstate : CombinedSnapshotState a -> SortedMap ThreadId ReaderState
Totality: total
Visibility: public export
readerstate : CombinedSnapshotState a -> SortedMap ThreadId ReaderState
Totality: total
Visibility: public export
.writepressure : CombinedSnapshotState a -> Nat
Totality: total
Visibility: public export
writepressure : CombinedSnapshotState a -> Nat
Totality: total
Visibility: public export
.rebuildpending : CombinedSnapshotState a -> Bool
Totality: total
Visibility: public export
rebuildpending : CombinedSnapshotState a -> Bool
Totality: total
Visibility: public export
.batchwindow : CombinedSnapshotState a -> Nat
Totality: total
Visibility: public export
batchwindow : CombinedSnapshotState a -> Nat
Totality: total
Visibility: public export
record LSMRRBVector : Type -> Type -> Type
  A concurrent log-structured sequence built on immutable RRBVector snapshots.
  
  Architecture:
  - Writers append deferred mutations into thread-local buffers.
  - Readers access immutable published snapshots.
  - A background rebuilder periodically merges buffered mutations into a new RRBVector snapshot.
  
  Concurrency model:
  - Readers never block writers.
  - Writers never mutate published snapshots.
  - Snapshot publication occurs atomically.
  - Retired snapshots are reclaimed using generation tracking.
  
  Internally combines:
  - Thread-local mutation logs.
  - Immutable RRBVector snapshots.
  - Background rebuild publication.
  - Generation-based reclamation.
  - Adaptive rebuild batching.
  
  Visibility:
  - Writes become visible only after rebuild and publication.
  - Readers observe a consistent immutable snapshot.
  
  Notes:
  - Optimized for high write concurrency.
  - Read performance matches the underlying RRBVector snapshot.

Totality: total
Visibility: public export
Constructor: 
MkLSMRRBVector : Ref s (SortedMap ThreadId (ThreadContext a)) -> Ref s (CombinedSnapshotState a) -> Ref s Bool -> LSMRRBVector s a

Projections:
.buffers : LSMRRBVector s a -> Ref s (SortedMap ThreadId (ThreadContext a))
.combinedsnapshotstate : LSMRRBVector s a -> Ref s (CombinedSnapshotState a)
.rebuildscheduled : LSMRRBVector s a -> Ref s Bool
.buffers : LSMRRBVector s a -> Ref s (SortedMap ThreadId (ThreadContext a))
Totality: total
Visibility: public export
buffers : LSMRRBVector s a -> Ref s (SortedMap ThreadId (ThreadContext a))
Totality: total
Visibility: public export
.combinedsnapshotstate : LSMRRBVector s a -> Ref s (CombinedSnapshotState a)
Totality: total
Visibility: public export
combinedsnapshotstate : LSMRRBVector s a -> Ref s (CombinedSnapshotState a)
Totality: total
Visibility: public export
.rebuildscheduled : LSMRRBVector s a -> Ref s Bool
Totality: total
Visibility: public export
rebuildscheduled : LSMRRBVector s a -> Ref s Bool
Totality: total
Visibility: public export
record LSMRRBVectorConfig : Type
  Configuration controlling rebuild and adaptive batching behavior.
  
  Fields:
  - initialbatchwindow: Initial adaptive batching target used before runtime adjustments occur.
  
  Properties:
  - Does not affect correctness.
  - Influences rebuild latency/throughput tradeoffs.
  - Serves as the starting point for adaptive window adjustment.
  
  Typical values:
  - 16–64: Lower latency, more frequent rebuilds.
  - 64–256: Balanced throughput and latency.
  - 256+: Higher throughput under sustained write load.

Totality: total
Visibility: public export
Constructor: 
MkLSMRRBVectorConfig : Nat -> LSMRRBVectorConfig

Projection: 
.initialbatchwindow : LSMRRBVectorConfig -> Nat
.initialbatchwindow : LSMRRBVectorConfig -> Nat
Totality: total
Visibility: public export
initialbatchwindow : LSMRRBVectorConfig -> Nat
Totality: total
Visibility: public export