runEffects : Stripe1 World a -> List (StripeEffect a) -> F1' World Execute `Stripe a` effects after CAS commit.
This is the only place IO is performed for Stripe transitions.
Guarantees:
- Effects are executed exactly once (only after successful CAS).
- Ordering is preserved.
- No effects are run on CAS retry.
Totality: total
Visibility: exportcasWithEffects : Stripe1 World a -> (Stripe a -> StripeStep a) -> F1' World Atomically apply a `Stripe a` transition and execute its effects.
This is the central concurrency primitive of the `Stripe a` model.
Behavior:
- Applies a pure state transition (`Stripe -> StripeStep`) under CAS.
- Retries automatically on contention using `casupdate1`.
- Extracts effects only from the successful committed transition.
- Executes effects exactly once after CAS succeeds.
Guarantees:
- Linearizability, such that the `Stripe a` transition appears atomic.
- No duplicated effects (retries do not leak effects).
- No IO occurs during CAS evaluation.
- Effects are executed strictly after commit.
Design Notes:
- `stepfn` must be pure (no IO, no external mutation).
- All side effects must be encoded in `StripeEffect a`.
- This function is the only place where `Stripe a` transitions are committed.
Totality: total
Visibility: exportsetNumStripes : (pc : PoolConfig a) -> (n : Nat ** (LTE 1 n, LTE n (fst (poolmaxresources pc)))) -> PoolConfig a Set the number of stripes in the `PoolConfig a`.
Totality: total
Visibility: exportsetPoolLabel : String -> PoolConfig a -> PoolConfig a Assign a label to the `PoolConfig a`.
Totality: total
Visibility: exportnewPool : (numstripes : Nat) -> PoolConfig a -> F1 World (Pool1 World numstripes a) Create a new striped resource pool.
Behavior:
- Allocates exactly `mstripes` independent `Stripe`s.
- Distributes the total capacity (`poolmaxresources`) across stripes as evenly as possible:
- Each stripe receives either `base` or `base + 1` capacity.
- The first `rest` stripes receive the extra unit.
- Initializes each stripe with:
- `available = assigned capacity`
- empty cache
- empty waiter queues
- fresh waiter id supply
- Constructs a `LocalPool1` for each stripe and stores them in a mutable array.
Resource Distribution:
- Let:
- `base = div maxres mstripes`
- `rest = mod maxres mstripes`
- Then:
- Total capacity is preserved: sum(stripes) = maxres
- Load is balanced with minimal skew (difference ≤ 1).
Concurrency Model:
- Each stripe is independent and owns its own:
- resource cache
- waiter queues
- capacity accounting
- Threads interact with exactly one stripe at a time (via `getLocalPool`).
- This minimizes contention and improves scalability.
Cleanup Model:
- No global collector thread is created.
- Resource cleanup is performed opportunistically via `cleanStripeIfNeeded`.
- This ensures:
- No background threads.
- Cleanup proportional to usage.
- Deterministic behavior (no GC reliance).
Guarantees:
- Total capacity never exceeds `poolmaxresources`.
- Each stripe starts empty but with full creation capacity.
- No IO occurs during stripe initialization except allocation of refs.
- Array is fully initialized before being returned.
Failure Conditions:
- Crashes if:
- An impossible index is encountered during initialization (should be unreachable).
- A `Nat -> Fin` conversion fails (indicates internal inconsistency).
Notes:
- `numstripes` is explicit, avoiding runtime dependency on capabilities.
- The caller is responsible for eventual cleanup via `destroyAllResources`.
- This function performs no resource creation; resources are created lazily on demand.
Invariants Established:
- Each `LocalPool1` corresponds to exactly one stripe.
- Stripe state is valid and consistent for CAS-based transitions.
- Waiter queues and cancellation queues start empty.
Totality: total
Visibility: exportsignal : Stripe a -> WakeResult a -> StripeStep a Deliver a value to a `Stripe a` state.
This function:
- Updates Stripe state
- Emits wake effects
Invariants:
- Each wake corresponds to a committed state transition.
- Queue ordering is preserved.
- No side effects occur during evaluation.
Totality: total
Visibility: exportwaitForResource : Stripe1 World a -> Nat -> Channel (WakeResult a) -> F1 World (WakeResult a) Block until a resource is delivered to this waiter.
Behavior:
- Waits on the provided `Channel (Maybe a)` for a wakeup signal.
- Returns:
- `Just a` if a resource is successfully delivered.
- `Nothing` if the waiter is cancelled or destroyed.
Cancellation:
- If the waiting thread is aborted, the `cleanup` handler is invoked.
- This atomically marks the waiter as cancelled by inserting its `wid` into the Stripe's `cancelled` queue.
- Cancellation is lazy, cancelled waiters are skipped during dequeue.
Guarantees:
- No busy waiting, the thread blocks on a channel.
- No lost wakeups, every successful `signal` results in exactly one `channelPut` to a live waiter.
- Safe under races:
- If cancellation happens before wake, waiter is skipped later.
- If wake happens before cancellation, value is delivered.
- Exactly-once semantics:
- Each waiter receives at most one wakeup.
- Each wakeup corresponds to a committed Stripe transition.
Design Notes:
- This function performs no direct Stripe mutation except in `cleanup`.
- All coordination with producers happens via `signal` + `StripeEffect`.
- The `Channel (Maybe a)` encodes both success (`Just`) and termination (`Nothing`).
Invariants:
- `wid` must be the same identifier used when enqueuing the waiter.
- The channel must be single-consumer and used exactly once.
- Stripe state remains the single source of truth for cancellation.
Totality: total
Visibility: exportdestroyResource : Stripe1 World a -> F1' World Destroy a resource instead of returning it to the `Pool1 World a`.
Behavior:
- If a waiter exists, they are woken with `Nothing`.
- Otherwise, no state change occurs (resource is discarded).
Guarantees:
- Waiters are not left blocked indefinitely.
- No resource is reinserted into the cache.
Totality: total
Visibility: exportputResource : Pool1 World n a -> Stripe1 World a -> a -> F1' World Return a resource to the `Pool1 World n a`.
Behavior:
- If a waiter exists, the resource is delivered directly.
- Otherwise, it is inserted into the cache with a timestamp.
Guarantees:
- No resource is lost.
- Wakeups are ordered and deterministic.
Totality: total
Visibility: exportdestroyAllResources : Pool1 World n a -> MArray World n (LocalPool1 World a) -> F1' World Destroy all resources in all stripes in the `Pool1 World n a`.
Behavior:
- Removes all cached resources from every stripe.
- Frees them via the provided `freeresource` function.
- Leaves wait queues untouched.
Guarantees:
- Each resource is freed exactly once.
- No IO occurs during Stripe state transitions.
- Safe under contention (uses CAS + effect model).
Notes:
- This only affects cached (idle) resources.
- Resources currently checked out are NOT affected.
Totality: total
Visibility: exportrestoreSize : Stripe1 World a -> F1' World Restore one unit of available capacity in the `Stripe a`.
Behavior:
- Increments `available` by 1.
- Does not modify cache or queue.
- Emits no effects.
Used when resource creation fails after capacity was reserved.
Guarantees:
- Atomic under CAS.
- No IO performed.
- Safe under contention.
Totality: total
Visibility: exporttakeResource : Pool1 World n a -> F1 World (a, LocalPool1 World a) Acquire a resource from the `Pool1 World n a`.
Behavior:
- Attempts to take a resource from the local stripe.
- Uses a single CAS step to atomically choose between:
- Reusing a cached resource.
- Reserving capacity for new resource creation.
- Enqueuing as a waiter when fully exhausted.
Fast Path (Cache Reuse):
- If a cached resource exists:
- Remove it from the cache.
- Return it immediately.
- `available` is not modified.
- The resource already exists and therefore does not consume creation capacity.
Creation Path:
- If the cache is empty but `available > 0`:
- Atomically decrement `available`.
- Reserve one unit of creation capacity.
- Create a fresh resource outside the CAS section.
Wait Path:
- If:
- cache is empty.
- and `available == 0`.
- Then:
- enqueue a `Waiter`.
- block on `waitForResource`.
- The waiter is eventually:
- woken with `Just a` when a resource is returned.
- or `Nothing` when capacity is restored.
Capacity Semantics:
- `available` represents remaining creation budget.
- It is decremented ONLY when creating a brand-new resource.
- It is restored when:
- resource creation aborts.
- resources are destroyed.
Concurrency Guarantees:
- Decision logic is atomic via CAS.
- No IO occurs during CAS evaluation.
- Effects execute exactly once after successful commit.
- Waiters are served FIFO (excluding cancelled waiters).
- No lost wakeups.
Invariants:
- Total live resources never exceeds stripe capacity.
- Cached resources are timestamped before insertion.
- Waiters exist only inside Stripe state.
Totality: total
Visibility: exportwithResource : Pool1 World n a -> (a -> IO r) -> F1 World r Safely acquire and use a resource from the pool.
This is the primary high-level interface for working with `Pool1`.
It ensures that resources are correctly returned or destroyed,
even in the presence of exceptions or cancellation.
Behavior:
- Acquires a resource using `takeResource`.
- Executes the user action `f` with that resource.
- On normal completion:
- The resource is returned to the pool via `putResource`.
- On exception or cancellation:
- The resource is destroyed via `destroyResource`.
Concurrency & Masking:
- The entire operation runs inside `uncancelable`, ensuring:
- Resource acquisition and release cannot be interrupted.
- The user action `f` is executed via `poll`, meaning:
- It *can* be interrupted or cancelled.
- If cancellation occurs during `f`, the cleanup handler runs.
Cleanup Guarantees:
- Exactly one of the following happens:
- `putResource` (success path)
- `destroyResource` (failure or cancellation path)
- No resource is leaked or returned twice.
- Waiters are properly woken via Stripe effects.
Failure Handling:
- Exceptions from `f` are propagated.
- Exceptions during acquisition or cleanup cause a crash (consistent with the rest of the module’s error handling).
Returns:
- The result of applying `f` to the acquired resource.
Invariants:
- Resources are never duplicated or lost.
- Pool state remains consistent under concurrency.
- All Stripe effects are executed after CAS commit.
Totality: total
Visibility: exporttryTakeResource : Pool1 World n a -> F1 World (Maybe (a, LocalPool1 World a)) Attempt to take a resource without blocking.
Behavior:
- Reads the local stripe and checks availability.
- If no resources are available:
- Returns `Nothing` immediately.
- Does NOT enqueue a waiter.
- Does NOT create a resource.
- If a resource is available:
- Removes it atomically via CAS.
- Returns `Just (resource, LocalPool1)`.
Guarantees:
- Non-blocking: never waits on a channel.
- No side effects inside CAS.
- No waiter allocation.
- Safe under contention via CAS retry.
Totality: total
Visibility: exporttryWithResource : Pool1 World n a -> (a -> IO r) -> F1 World (Maybe r) Attempt to acquire and use a resource from the pool without blocking.
Behavior:
- Tries to take a resource immediately using `tryTakeResource`.
- If no resource is available:
- Returns `Nothing` without blocking or creating a resource.
- If a resource is available:
- Executes the provided function `f` with the resource.
- Returns `Just result` on success.
Resource Handling:
- The acquired resource is always returned to the pool via `putResource` after successful execution of `f`.
- If an exception or cancellation occurs during `f`:
- The resource is destroyed using `destroyResource` instead of being returned.
Cancellation Semantics:
- The outer operation is `uncancelable`, ensuring:
- No resource is leaked between acquisition and release.
- The user function `f` is executed under `poll`, meaning:
- It remains cancelable.
- If cancellation occurs during `f`:
- The resource is safely discarded.
- The pool remains in a consistent state.
Concurrency Guarantees:
- Does not block waiting for a resource.
- Does not enqueue a waiter.
- All Stripe transitions (`putResource`, `destroyResource`) are performed via `casWithEffects`, ensuring:
- Atomic state updates.
- No duplicated side effects.
- Deterministic wake behavior.
Failure Handling:
- Any exception from `f` is propagated.
- Internal pool errors result in a crash with diagnostic information.
Returns:
- `Nothing` if no resource was immediately available.
- `Just r` if a resource was acquired and `f` completed successfully.
Notes:
- This function is the non-blocking counterpart to `withResource`.
- It is useful when callers prefer to fallback rather than wait.
Totality: total
Visibility: export