Data.Pool.Internal

Resource Pool Internals

Definitions

record PoolConfig : Type -> Type

  Configuration of a Pool.
  
  Constraints:
  - poolmaxresources -> The smallest acceptable value is 1.
  - poolnumstripes -> The smallest acceptable value is 1, poolnumstripes must not be larger than poolmaxresources.
  

Totality: total
Visibility: public export
Constructor: 

MkPoolConfig : IO a -> (a -> IO ()) -> Clock Duration -> (poolmaxresources : (maxres : Nat ** LTE 1 maxres)) -> (n : Nat ** (LTE 1 n, LTE n (fst poolmaxresources))) -> String -> PoolConfig a

Projections:

.createresource : PoolConfig a -> IO a

.freeresource : PoolConfig a -> a -> IO ()

.poolcachettl : PoolConfig a -> Clock Duration

.poolconfiglabel : PoolConfig a -> String

.poolmaxresources : PoolConfig a -> (maxres : Nat ** LTE 1 maxres)

.poolnumstripes : ({rec:0} : PoolConfig a) -> (n : Nat ** (LTE 1 n, LTE n (fst (poolmaxresources {rec:0}))))

.createresource : PoolConfig a -> IO a

Totality: total
Visibility: public export

createresource : PoolConfig a -> IO a

Totality: total
Visibility: public export

.freeresource : PoolConfig a -> a -> IO ()

Totality: total
Visibility: public export

freeresource : PoolConfig a -> a -> IO ()

Totality: total
Visibility: public export

.poolcachettl : PoolConfig a -> Clock Duration

Totality: total
Visibility: public export

poolcachettl : PoolConfig a -> Clock Duration

Totality: total
Visibility: public export

.poolmaxresources : PoolConfig a -> (maxres : Nat ** LTE 1 maxres)

Totality: total
Visibility: public export

poolmaxresources : PoolConfig a -> (maxres : Nat ** LTE 1 maxres)

Totality: total
Visibility: public export

.poolnumstripes : ({rec:0} : PoolConfig a) -> (n : Nat ** (LTE 1 n, LTE n (fst (poolmaxresources {rec:0}))))

Totality: total
Visibility: public export

poolnumstripes : ({rec:0} : PoolConfig a) -> (n : Nat ** (LTE 1 n, LTE n (fst (poolmaxresources {rec:0}))))

Totality: total
Visibility: public export

.poolconfiglabel : PoolConfig a -> String

Totality: total
Visibility: public export

poolconfiglabel : PoolConfig a -> String

Totality: total
Visibility: public export

data Queue : Type -> Type

  A simple (persistent) FIFO queue.
  
  This is used to maintain an ordered collection of waiting threads.
  Elements are appended at the tail and removed from the head.
  
  Notes:
  - This representation has O(n) append.
  - Under contention (with CAS updates), appends may be retried, so this structure favors simplicity over performance.
  - It is typically used together with a secondary "reversed" queue to amortize costs (two-list queue pattern).
  

Totality: total
Visibility: public export
Constructors:

QNode : a -> Queue a -> Queue a

QEnd : Queue a

data WakeResult : Type -> Type

  Result of waking a waiting thread.
  
  This represents the outcome delivered to a blocked waiter through its wake channel.
  
  Variants:
  - `Deliver a`
   - A resource was directly handed off to the waiter.
  
  - `Create`
   - No reusable resource was available, but the waiter should proceed by creating a fresh resource using an already-reserved capacity slot.
  
  - `Cancelled`
   - The waiter was cancelled before receiving a resource.
   - This is used to distinguish cancellation from normal wakeup semantics.
  
  Design Notes:
  - This replaces the older `Maybe a` wake protocol, which overloaded `Nothing` to represent multiple meanings.
  - Explicit wake states improve clarity and correctness of the Stripe state machine.
  
  Guarantees:
  - Each waiter receives at most one `WakeResult`.
  - Wake results correspond only to committed Stripe transitions.
  - No wake result is delivered more than once.
  
  Invariants:
  - `Deliver a` carries ownership transfer of exactly one resource.
  - `Create` implies capacity has already been reserved.
  - `Cancelled` does not transfer ownership of a resource.
  

Totality: total
Visibility: public export
Constructors:

Deliver : a -> WakeResult a

Create : WakeResult a

Cancelled : WakeResult a

data Waiter : Type -> Type

  A pure waiting token representing a blocked thread.
  
  This contains no mutable state. All lifecycle tracking is handled
  by the Stripe during dequeue / cancellation.
  
  Fields:
  - `id`   : unique identifier for cancellation tracking
  - `wake` : channel used to unblock the thread
  
  Invariants:
  - Waiter is immutable
  - Wake is single-use
  - Cancellation is handled by Stripe (not locally)
  

Totality: total
Visibility: public export
Constructor: 

MkWaiter : Nat -> Channel (WakeResult a) -> Waiter a

data Entry : Type -> Type

  An existing resource currently sitting in a pool.
  

Totality: total
Visibility: public export
Constructor: 

MkEntry : a -> IClock CLOCK_MONOTONIC -> Entry a

data Stripe : Type -> Type

  Stripe is the only concurrent state machine in the system.
  
  It owns:
  - Resource availability.
  - Cached resources.
  - All waiting threads.
  - Cancellation tracking.
  
  All mutations occur via CAS on an enclosing Ref, `Stripe1 s a`.
  
  Fields:
  - `available` : number of available resources
  - `cache`     : reusable resources
  - `queue`     : primary FIFO of waiters
  - `queuer`    : secondary FIFO (amortized append)
  - `nextId`    : fresh waiter id supply
  - `cancelled` : sorted set of cancelled waiter ids
  
  Invariants:
  - Stripe is immutable between CAS updates.
  - Queue ordering is authoritative.
  - Cancelled waiters are lazily skipped.
  

Totality: total
Visibility: public export
Constructor: 

MkStripe : Nat -> List (Entry a) -> Queue (Waiter a) -> Queue (Waiter a) -> Nat -> SortedSet Nat -> Stripe a

data Stripe1 : Type -> Type -> Type

  A linear mutable stripe.
  

Totality: total
Visibility: public export
Constructor: 

MkStripe1 : Ref s (Stripe a) -> Stripe1 s a

data StripeEffect : Type -> Type

  Effects emitted by a Stripe transition.
  
  These are collected during CAS computation and executed
  only after a successful CAS commit.
  
  Guarantees:
  - No IO inside CAS.
  - No duplicated effects on retry.
  - Deterministic state transitions.
  

Totality: total
Visibility: public export
Constructors:

Wake : Channel (WakeResult a) -> WakeResult a -> StripeEffect a

WakeMany : List (Channel (WakeResult a), WakeResult a) -> StripeEffect a

InsertWithTimestamp : a -> StripeEffect a

FreeMany : (a -> IO ()) -> List a -> StripeEffect a

None : StripeEffect a

record StripeStep : Type -> Type

  Result of a Stripe state transition.
  
  Represents:
  - The new Stripe state (to be CAS'd).
  - Effects to run AFTER successful commit.
  
  Invariants:
  - This must be treated as a one-shot value.
  - If CAS fails, this MUST be discarded.
  - Effects must NEVER be run unless CAS succeeds.
  

Totality: total
Visibility: public export
Constructor: 

MkStripeStep : Stripe a -> List (StripeEffect a) -> StripeStep a

Projections:

.effects : StripeStep a -> List (StripeEffect a)

.stripe : StripeStep a -> Stripe a

.stripe : StripeStep a -> Stripe a

Totality: total
Visibility: public export

stripe : StripeStep a -> Stripe a

Totality: total
Visibility: public export

.effects : StripeStep a -> List (StripeEffect a)

Totality: total
Visibility: public export

effects : StripeStep a -> List (StripeEffect a)

Totality: total
Visibility: public export

data LocalPool1 : Type -> Type -> Type

  A single, local pool based on a linear mutable stripe.
  

Totality: total
Visibility: public export
Constructor: 

MkLocalPool1 : Nat -> Stripe1 s a -> LocalPool1 s a

data Pool1 : Type -> Nat -> Type -> Type

  Striped resource pool based on linear mutable references.
  

Totality: total
Visibility: public export
Constructor: 

MkPool1 : PoolConfig a -> MArray s n (LocalPool1 s a) -> Pool1 s n a