0 | ||| Resource Pool
   1 | module Data.Pool
   2 |
   3 | import public Data.Pool.Internal
   4 |
   5 | import Control.Monad.Elin
   6 | import Control.Monad.MCancel
   7 | import Data.Array
   8 | import Data.Array.Mutable
   9 | import Data.Either
  10 | import Data.Linear.Ref1
  11 | import Data.Linear.Traverse1
  12 | import Data.List
  13 | import Data.SortedSet
  14 | import System.Concurrency
  15 | import System.Info
  16 | import System.Posix.Timer
  17 | import System.Posix.Timer.Prim
  18 | import Syntax.T1
  19 |
  20 | %language ElabReflection
  21 |
  22 | %default total
  23 |
  24 | %hide Data.List.Elem.get
  25 |
  26 | --------------------------------------------------------------------------------
  27 | --          Utilities
  28 | --------------------------------------------------------------------------------
  29 |
  30 | ||| Grab CLOCK_MONOTONIC.
  31 | |||
  32 | grabMonotonicTime : Elin World [Errno] (IClock CLOCK_MONOTONIC)
  33 | grabMonotonicTime = getTime CLOCK_MONOTONIC
  34 |
  35 | ||| Grab CLOCK_REALTIME.
  36 | |||
  37 | grabRealTime : Elin World [Errno] (IClock CLOCK_REALTIME)
  38 | grabRealTime = getTime CLOCK_REALTIME
  39 |
  40 | ||| Cancellation check.
  41 | |||
  42 | isCancelled :  Nat
  43 |             -> Queue Nat
  44 |             -> Bool
  45 | isCancelled _ QEnd         =
  46 |   False
  47 | isCancelled x (QNode y ys) =
  48 |   let True = x == y
  49 |         | False =>
  50 |             isCancelled x ys
  51 |     in True
  52 |
  53 | ||| Append a value into the `Queue a`.
  54 | |||
  55 | appendQ :  Queue a
  56 |         -> a
  57 |         -> Queue a
  58 | appendQ QEnd         x =
  59 |   QNode x QEnd
  60 | appendQ (QNode y ys) x =
  61 |   QNode y (appendQ ys x)
  62 |
  63 | ||| Reverse a `Queue a`.
  64 | |||
  65 | reverseQ :  Queue a
  66 |          -> Queue a
  67 | reverseQ q =
  68 |   go q QEnd
  69 |   where
  70 |     go :  Queue a
  71 |        -> Queue a
  72 |        -> Queue a
  73 |     go QEnd         acc =
  74 |       acc
  75 |     go (QNode x xs) acc =
  76 |       go xs (QNode x acc)
  77 |
  78 | ||| Append two `Queue a`.
  79 | |||
  80 | appendAll :  Queue a
  81 |           -> Queue a
  82 |           -> Queue a
  83 | appendAll QEnd         ys =
  84 |   ys
  85 | appendAll (QNode x xs) ys =
  86 |   QNode x (appendAll xs ys)
  87 |
  88 | ||| Normalize two `Queue Waiter`s.
  89 | |||
  90 | normalize :  Queue (Waiter a)
  91 |           -> Queue (Waiter a)
  92 |           -> Queue (Waiter a)
  93 | normalize QEnd q2 =
  94 |   q2
  95 | normalize q1   q2 =
  96 |   appendAll q1 q2
  97 |
  98 | ||| Dequeue first live waiter.
  99 | |||
 100 | dequeueLive :  Queue (Waiter a)
 101 |             -> SortedSet Nat
 102 |             -> (Maybe (Waiter a), Queue (Waiter a), SortedSet Nat)
 103 | dequeueLive QEnd                              cancelled =
 104 |   (Nothing, QEnd, cancelled)
 105 | dequeueLive (QNode w@(MkWaiter id wake) rest) cancelled =
 106 |   let True = contains id cancelled
 107 |         | False =>
 108 |             -- live waiter
 109 |             (Just w, rest, cancelled)
 110 |     in -- cancelled waiter
 111 |        -- consume tombstone and continue
 112 |        dequeueLive rest (delete id cancelled)
 113 |
 114 | ||| Stripe-level dequeue.
 115 | |||
 116 | dequeueStripe :  Stripe a
 117 |               -> (Maybe (Waiter a), Stripe a)
 118 | dequeueStripe (MkStripe available cache queue queuer nextid cancelled) =
 119 |   let fullq                  = normalize queue queuer
 120 |       (mw, rest, cancelled') = dequeueLive fullq cancelled
 121 |       Just w                 = mw
 122 |         | Nothing =>
 123 |            (Nothing, MkStripe available cache QEnd QEnd nextid cancelled')
 124 |     in (Just w, MkStripe available cache rest QEnd nextid cancelled')
 125 |
 126 | ||| Check to see if entry is stale.
 127 | |||
 128 | isStale :  Clock Duration
 129 |         -> IClock CLOCK_MONOTONIC
 130 |         -> Entry a
 131 |         -> Bool
 132 | isStale ttl now (MkEntry _ lastused) =
 133 |   timeDifference now lastused > ttl
 134 |
 135 | ||| Execute `Stripe a` effects after CAS commit.
 136 | |||
 137 | ||| This is the only place IO is performed for Stripe transitions.
 138 | |||
 139 | ||| Guarantees:
 140 | ||| - Effects are executed exactly once (only after successful CAS).
 141 | ||| - Ordering is preserved.
 142 | ||| - No effects are run on CAS retry.
 143 | |||
 144 | export
 145 | runEffects :  (Nat, Stripe1 World a)
 146 |            -> List (StripeEffect a)
 147 |            -> F1 World (Either (List StripeError) ())
 148 | runEffects (stripeid, (MkStripe1 striperef)) effects t =
 149 |   let effects' # t := traverse1 (runEffect (stripeid, (MkStripe1 striperef))) effects t
 150 |       effectserrs  := concat $ lefts effects'
 151 |     in case effectserrs of
 152 |          []           =>
 153 |            Right () # t
 154 |          effectserrs' =>
 155 |            Left effectserrs' # t
 156 |   where
 157 |     runEffect :  (Nat, Stripe1 World a)
 158 |               -> StripeEffect a
 159 |               -> F1 World (Either (List StripeError) ())
 160 |     runEffect _                                 None                      t =
 161 |       Right () # t
 162 |     runEffect _                                 (Wake ch val)             t =
 163 |       let () # t := ioToF1 (channelPut ch val) t
 164 |         in Right () # t
 165 |     runEffect _                                 (WakeMany pairs)          t =
 166 |       let () # t := traverse1_ (\(ch,val) => ioToF1 (channelPut ch val)) pairs t
 167 |         in Right () # t
 168 |     runEffect _                                 (FreeMany free xs)        t =
 169 |       let () # t := traverse1_ (\x => ioToF1 (free x)) xs t
 170 |         in Right () # t
 171 |     runEffect (stripeid, (MkStripe1 striperef)) (InsertWithTimestamp val) t =
 172 |       let monotonicnow # t := ioToF1 (runElinIO grabMonotonicTime) t
 173 |         in case monotonicnow of
 174 |              Left monotonicnowerr =>
 175 |                let realtimenow    # t := ioToF1 (runElinIO grabRealTime) t
 176 |                    Right realtimenow' := realtimenow
 177 |                      | Left realtimenowerr =>
 178 |                          Left [ MkStripeError stripeid "Data.Pool.runEffects.runEffect" (show monotonicnowerr) Nothing
 179 |                               , MkStripeError stripeid "Data.Pool.runEffects.runEffect" (show realtimenowerr) Nothing
 180 |                               ] # t
 181 |                  in Left [MkStripeError stripeid "Data.Pool.runEffects.runEffect" (show monotonicnowerr) (Just realtimenow')] # t
 182 |              Right monotonicnow'  =>
 183 |                let entry  := MkEntry val monotonicnow'
 184 |                    () # t := casupdate1 striperef (\(MkStripe available cache queue queuer nextid cancelled) =>
 185 |                                                      (MkStripe available (entry :: cache) queue queuer nextid cancelled, ())
 186 |                                                   ) t
 187 |                  in Right () # t
 188 |
 189 | ||| Atomically apply a `Stripe a` transition and execute its effects.
 190 | |||
 191 | ||| This is the central concurrency primitive of the `Stripe a` model.
 192 | |||
 193 | ||| Behavior:
 194 | ||| - Applies a pure state transition (`Stripe -> StripeStep`) under CAS.
 195 | ||| - Retries automatically on contention using `casupdate1`.
 196 | ||| - Extracts effects only from the successful committed transition.
 197 | ||| - Executes effects exactly once after CAS succeeds.
 198 | |||
 199 | ||| Guarantees:
 200 | ||| - Linearizability, such that the `Stripe a` transition appears atomic.
 201 | ||| - No duplicated effects (retries do not leak effects).
 202 | ||| - No IO occurs during CAS evaluation.
 203 | ||| - Effects are executed strictly after commit.
 204 | |||
 205 | ||| Design Notes:
 206 | ||| - `stepfn` must be pure (no IO, no external mutation).
 207 | ||| - All side effects must be encoded in `StripeEffect a`.
 208 | ||| - This function is the only place where `Stripe a` transitions are committed.
 209 | |||
 210 | export
 211 | casWithEffects :  (Nat, Stripe1 World a)
 212 |                -> (Stripe a -> StripeStep a)
 213 |                -> F1 World (Either (List StripeError) ())
 214 | casWithEffects (stripeid, (MkStripe1 striperef)) stepfn t =
 215 |   let effects # t := casupdate1 striperef (\stripe =>
 216 |                                             let (MkStripeStep stripe' stripeeffects) = stepfn stripe
 217 |                                               in (stripe', stripeeffects)
 218 |                                           ) t
 219 |     in runEffects (stripeid, (MkStripe1 striperef)) effects t
 220 |
 221 | --------------------------------------------------------------------------------
 222 | --          Configuration
 223 | --------------------------------------------------------------------------------
 224 |
 225 | ||| Set the number of stripes in the `PoolConfig a`.
 226 | export
 227 | setNumStripes :  (pc : PoolConfig a)
 228 |               -> (n ** (LTE 1 n, LTE n (fst (poolmaxresources pc))))
 229 |               -> PoolConfig a
 230 | setNumStripes (MkPoolConfig create free cachettl (maxres ** prfmaxres) _ pclabel) numstripes =
 231 |   MkPoolConfig create
 232 |                free
 233 |                cachettl
 234 |                (maxres ** prfmaxres)
 235 |                numstripes
 236 |                pclabel
 237 |
 238 | ||| Assign a label to the `PoolConfig a`.
 239 | export
 240 | setPoolLabel :  String
 241 |              -> PoolConfig a
 242 |              -> PoolConfig a
 243 | setPoolLabel label pc =
 244 |   { poolconfiglabel := label } pc
 245 |
 246 | --------------------------------------------------------------------------------
 247 | --          Resource Management
 248 | --------------------------------------------------------------------------------
 249 |
 250 | ||| Create a new striped resource pool.
 251 | |||
 252 | ||| Behavior:
 253 | ||| - Allocates exactly `mstripes` independent `Stripe`s.
 254 | ||| - Distributes the total capacity (`poolmaxresources`) across stripes as evenly as possible:
 255 | |||  - Each stripe receives either `base` or `base + 1` capacity.
 256 | |||  - The first `rest` stripes receive the extra unit.
 257 | ||| - Initializes each stripe with:
 258 | |||  - `available = assigned capacity`
 259 | |||  - empty cache
 260 | |||  - empty waiter queues
 261 | |||  - fresh waiter id supply
 262 | ||| - Constructs a `LocalPool1` for each stripe and stores them in a mutable array.
 263 | |||
 264 | ||| Resource Distribution:
 265 | ||| - Let:
 266 | |||  - `base = div maxres mstripes`
 267 | |||  - `rest = mod maxres mstripes`
 268 | ||| - Then:
 269 | |||  - Total capacity is preserved: sum(stripes) = maxres
 270 | |||  - Load is balanced with minimal skew (difference ≤ 1).
 271 | |||
 272 | ||| Concurrency Model:
 273 | ||| - Each stripe is independent and owns its own:
 274 | |||   - resource cache
 275 | |||   - waiter queues
 276 | |||   - capacity accounting
 277 | ||| - Threads interact with exactly one stripe at a time (via `getLocalPool`).
 278 | ||| - This minimizes contention and improves scalability.
 279 | |||
 280 | ||| Cleanup Model:
 281 | ||| - No global collector thread is created.
 282 | ||| - Resource cleanup is performed opportunistically via `cleanStripeIfNeeded`.
 283 | ||| - This ensures:
 284 | |||   - No background threads.
 285 | |||   - Cleanup proportional to usage.
 286 | |||   - Deterministic behavior (no GC reliance).
 287 | |||
 288 | ||| Guarantees:
 289 | ||| - Total capacity never exceeds `poolmaxresources`.
 290 | ||| - Each stripe starts empty but with full creation capacity.
 291 | ||| - No IO occurs during stripe initialization except allocation of refs.
 292 | ||| - Array is fully initialized before being returned.
 293 | |||
 294 | ||| Failure Conditions:
 295 | ||| - Crashes if:
 296 | |||   - An impossible index is encountered during initialization (should be unreachable).
 297 | |||   - A `Nat -> Fin` conversion fails (indicates internal inconsistency).
 298 | |||
 299 | ||| Notes:
 300 | ||| - `numstripes` is explicit, avoiding runtime dependency on capabilities.
 301 | ||| - The caller is responsible for eventual cleanup via `destroyAllResources`.
 302 | ||| - This function performs no resource creation; resources are created lazily on demand.
 303 | |||
 304 | ||| Invariants Established:
 305 | ||| - Each `LocalPool1` corresponds to exactly one stripe.
 306 | ||| - Stripe state is valid and consistent for CAS-based transitions.
 307 | ||| - Waiter queues and cancellation queues start empty.
 308 | |||
 309 | export
 310 | newPool :  (numstripes : Nat)
 311 |         -> PoolConfig a
 312 |         -> F1 World (Either (List Pool1Error) (Pool1 World numstripes a))
 313 | newPool numstripes pc@(MkPoolConfig create free cachettl (maxres ** prfmaxres) _ pclabel) t =
 314 |   let striperesources := let base = div maxres numstripes
 315 |                              rest = mod maxres numstripes
 316 |                            in zip (range Z numstripes)
 317 |                                   (distribute base rest numstripes)
 318 |       pools       # t := unsafeMArray1 numstripes t
 319 |       pools'      # t := saturateLocalPools 0 numstripes striperesources pools t
 320 |       Right ()        := pools'
 321 |         | Left errors =>
 322 |             Left errors # t
 323 |     in Right (MkPool1 pc pools) # t
 324 |   where
 325 |     range :  Nat
 326 |           -> Nat
 327 |           -> List Nat
 328 |     range start Z     =
 329 |       []
 330 |     range start (S k) =
 331 |       start :: range (S start) k
 332 |     distribute :  Nat
 333 |                -> Nat
 334 |                -> Nat
 335 |                -> List Nat
 336 |     distribute base rest Z      =
 337 |       []
 338 |     distribute base Z     (S k) =
 339 |       base :: distribute base Z k
 340 |     distribute base (S r) (S k) =
 341 |       (S base) :: distribute base r k
 342 |     saturateLocalPools :  (o, x : Nat)
 343 |                        -> {auto v : Ix x numstripes}
 344 |                        -> {auto 0 prf : LTE o $ ixToNat v}
 345 |                        -> (resources : List (Nat, Nat))
 346 |                        -> (arr : MArray World numstripes (LocalPool1 World a))
 347 |                        -> F1 World (Either (List Pool1Error) ())
 348 |     saturateLocalPools o Z     _         _   t =
 349 |       Right () # t
 350 |     saturateLocalPools o (S j) resources arr t =
 351 |       case lookup j resources of
 352 |         Nothing       =>
 353 |           let realtimenow    # t := ioToF1 (runElinIO grabRealTime) t
 354 |               Right realtimenow' := realtimenow
 355 |                 | Left realtimenowerr =>
 356 |                     let newerrors := [ MkPool1Error "Data.Pool.newPool.saturatePools" (show realtimenowerr) Nothing
 357 |                                      , MkPool1Error "Data.Pool.newPool.saturatePools" "impossible index" Nothing
 358 |                                      ]
 359 |                       in Left newerrors # t
 360 |               newerrors := [MkPool1Error "Data.Pool.newPool.saturatePools" "impossible index" (Just realtimenow')]
 361 |             in Left newerrors # t
 362 |         Just resource =>
 363 |           let striperef  # t := ref1 ( MkStripe resource
 364 |                                                 []
 365 |                                                 QEnd
 366 |                                                 QEnd
 367 |                                                 0
 368 |                                                 empty
 369 |                                      ) t
 370 |               striperef1     := MkStripe1 striperef
 371 |               localpool      := MkLocalPool1 j striperef1
 372 |               Just j'        := tryNatToFin j
 373 |                 | Nothing =>
 374 |                     let realtimenow    # t := ioToF1 (runElinIO grabRealTime) t
 375 |                         Right realtimenow' := realtimenow
 376 |                           | Left realtimenowerr =>
 377 |                               let newerrors := [ MkPool1Error "Data.Pool.newPool.saturatePools" (show realtimenowerr) Nothing
 378 |                                                , MkPool1Error "Data.Pool.newPool.saturatePools" "couldn't convert Nat to Fin" Nothing
 379 |                                                ]
 380 |                                 in Left newerrors # t
 381 |                         newerrors := [MkPool1Error "Data.Pool.newPool.saturatePools" "couldn't convert Nat to Fin" (Just realtimenow')]
 382 |                       in Left newerrors # t
 383 |               ()         # t := set arr j' localpool t
 384 |             in saturateLocalPools o j resources arr t
 385 |
 386 | ||| Select a `LocalPool1 World a` for the current thread.
 387 | |||
 388 | ||| This function deterministically maps the calling thread to one of the
 389 | ||| available stripes using a modulo-based hashing scheme.
 390 | |||
 391 | ||| Behavior:
 392 | ||| - Computes a stripe index `sid`:
 393 | |||  - If `n == 1`, always selects index `0` (fast path).
 394 | |||  - Otherwise:
 395 | |||   - Retrieves the current thread id (`getThreadId`).
 396 | |||   - Maps it into `[0, n)` via modulo arithmetic.
 397 | ||| - Converts the resulting index into a `Fin n`.
 398 | ||| - Returns the corresponding `LocalPool1` from the array.
 399 | |||
 400 | ||| Thread-to-Stripe Mapping:
 401 | ||| - Mapping is stable for a given thread id.
 402 | ||| - Different threads are distributed across stripes.
 403 | ||| - Collisions are possible but minimized under uniform thread ids.
 404 | |||
 405 | ||| Concurrency Implications:
 406 | ||| - Each thread interacts primarily with a single stripe.
 407 | ||| - Reduces contention compared to a single global pool.
 408 | ||| - Enables scalable parallel access under CAS-based updates.
 409 | |||
 410 | ||| Arithmetic Details:
 411 | ||| - Uses a custom `remInt` implementation to ensure:
 412 | |||  - Correct behavior for negative thread ids (if any).
 413 | |||  - Avoidance of undefined behavior from division/modulo edge cases.
 414 | ||| - Conversion pipeline:
 415 | |||  - Int (thread id)
 416 | |||   - modulo n
 417 | |||   - Nat
 418 | |||   - Fin n
 419 | |||
 420 | ||| Guarantees:
 421 | ||| - Always returns a valid `LocalPool1` when invariants hold.
 422 | ||| - No mutation of pool state occurs.
 423 | ||| - No blocking or waiting.
 424 | |||
 425 | ||| Failure Conditions:
 426 | ||| - Crashes if:
 427 | |||   - Conversion from `Nat` to `Fin n` fails (should be impossible if modulo is correct).
 428 | |||   - Division by zero is attempted (guarded by invariant `n >= 1`).
 429 | |||
 430 | ||| Performance:
 431 | ||| - O(1) selection.
 432 | ||| - Minimal overhead in the `n == 1` case (no IO, no modulo).
 433 | ||| - Single IO call (`getThreadId`) in the general case.
 434 | |||
 435 | ||| Design Notes:
 436 | ||| - This function is intentionally simple and deterministic.
 437 | ||| - It avoids randomness or hashing to keep behavior predictable.
 438 | ||| - Stripe selection is orthogonal to resource availability:
 439 | |||  - Load balancing is achieved probabilistically via thread distribution.
 440 | |||
 441 | ||| Invariants:
 442 | ||| - `n >= 1` (guaranteed by `PoolConfig` construction).
 443 | ||| - `pools` contains exactly `n` initialized entries.
 444 | ||| - Each index in `[0, n)` maps to a valid `LocalPool1`.
 445 | |||
 446 | ||| Relationship to the system:
 447 | ||| - This is the entry point for all pool operations:
 448 | |||  - `takeResource`
 449 | |||  - `tryTakeResource`
 450 | |||  - `putResource`
 451 | ||| - It determines which stripe's CAS state machine is used.
 452 | |||
 453 | private
 454 | getLocalPool :  {n : Nat}
 455 |              -> Pool1 World n a
 456 |              -> F1 World (Either (List Pool1Error) (LocalPool1 World a))
 457 | getLocalPool pool@(MkPool1 _ localpools) t =
 458 |   case n == 1 of
 459 |     True  =>
 460 |       let sid         := 0
 461 |           sid'        := remInt sid (cast {to=Int} n)
 462 |           Just sid''  := sid'
 463 |             | Nothing =>
 464 |                 let realtimenow    # t := ioToF1 (runElinIO grabRealTime) t
 465 |                     Right realtimenow' := realtimenow
 466 |                       | Left realtimenowerr =>
 467 |                           let newerrors := [ MkPool1Error "Data.Pool.getLocalPool" (show realtimenowerr) Nothing
 468 |                                            , MkPool1Error "Data.Pool.getLocalPool" "division by zero" Nothing
 469 |                                            ]
 470 |                             in Left newerrors # t
 471 |                     newerrors := [MkPool1Error "Data.Pool.getLocalPool" "division by zero" (Just realtimenow')]
 472 |                   in Left newerrors # t
 473 |           Just sid''' := tryNatToFin (cast {to=Nat} sid'')
 474 |             | Nothing =>
 475 |                 let realtimenow    # t := ioToF1 (runElinIO grabRealTime) t
 476 |                     Right realtimenow' := realtimenow
 477 |                       | Left realtimenowerr =>
 478 |                           let newerrors := [ MkPool1Error "Data.Pool.getLocalPool" (show realtimenowerr) Nothing
 479 |                                            , MkPool1Error "Data.Pool.getLocalPool" "couldn't convert Nat to Fin" Nothing
 480 |                                            ]
 481 |                             in Left newerrors # t
 482 |                     newerrors := [MkPool1Error "Data.Pool.getLocalPool" "couldn't convert Nat to Fin" (Just realtimenow')]
 483 |                   in Left newerrors # t
 484 |           sid'''' # t := get localpools sid''' t
 485 |         in Right sid'''' # t
 486 |     False =>
 487 |       let sid     # t := ioToF1 getThreadId t
 488 |           sid'        := remInt sid (cast {to=Int} n)
 489 |           Just sid''  := sid'
 490 |             | Nothing =>
 491 |                 let realtimenow    # t := ioToF1 (runElinIO grabRealTime) t
 492 |                     Right realtimenow' := realtimenow
 493 |                       | Left realtimenowerr =>
 494 |                           let newerrors := [ MkPool1Error "Data.Pool.getLocalPool" (show realtimenowerr) Nothing
 495 |                                            , MkPool1Error "Data.Pool.getLocalPool" "division by zero" Nothing
 496 |                                            ]
 497 |                             in Left newerrors # t
 498 |                     newerrors := [MkPool1Error "Data.Pool.getLocalPool" "division by zero" (Just realtimenow')]
 499 |                   in Left newerrors # t
 500 |           Just sid''' := tryNatToFin (cast {to=Nat} sid'')
 501 |             | Nothing =>
 502 |                 let realtimenow    # t := ioToF1 (runElinIO grabRealTime) t
 503 |                     Right realtimenow' := realtimenow
 504 |                       | Left realtimenowerr =>
 505 |                           let newerrors := [ MkPool1Error "Data.Pool.getLocalPool" (show realtimenowerr) Nothing
 506 |                                            , MkPool1Error "Data.Pool.getLocalPool" "couldn't convert Nat to Fin" Nothing
 507 |                                            ]
 508 |                             in Left newerrors # t
 509 |                     newerrors := [MkPool1Error "Data.Pool.getLocalPool" "couldn't convert Nat to Fin" (Just realtimenow')]
 510 |                   in Left newerrors # t
 511 |           sid'''' # t := get localpools sid''' t
 512 |         in Right sid'''' # t
 513 |   where
 514 |     signumInt :  Int
 515 |               -> Int
 516 |     signumInt x =
 517 |       let False = x > 0
 518 |             | True =>
 519 |                 1
 520 |           False = x < 0
 521 |             | True =>
 522 |                 -1
 523 |         in 0 
 524 |     quotInt :  Int
 525 |             -> Int
 526 |             -> Int
 527 |     quotInt x y =
 528 |       let q     = x `div` y
 529 |           r     = x `mod` y
 530 |           False = (r /= 0) && (signumInt x /= signumInt y)
 531 |             | True =>
 532 |                 q + 1
 533 |         in q
 534 |     remInt :  Int
 535 |            -> Int
 536 |            -> Maybe Int
 537 |     remInt x y =
 538 |       let False = y == 0
 539 |             | True =>
 540 |                 Nothing
 541 |         in Just $ x - (quotInt x y) * y
 542 |
 543 | ||| Deliver a value to a `Stripe a` state.
 544 | |||
 545 | ||| This function:
 546 | ||| - Updates Stripe state
 547 | ||| - Emits wake effects
 548 | |||
 549 | ||| Invariants:
 550 | ||| - Each wake corresponds to a committed state transition.
 551 | ||| - Queue ordering is preserved.
 552 | ||| - No side effects occur during evaluation.
 553 | |||
 554 | export
 555 | signal :  Stripe a
 556 |        -> WakeResult a
 557 |        -> StripeStep a
 558 | signal stripe@(MkStripe available cache queue queuer nextid cancelled) result =
 559 |   let (mw, MkStripe available' cache' queue' queuer' nextid' cancelled') = dequeueStripe stripe
 560 |       Just (MkWaiter _ wake)                                             = mw
 561 |         | Nothing =>
 562 |             case result of
 563 |               Deliver val            =>
 564 |                 MkStripeStep (MkStripe (S available') cache' queue' queuer' nextid' cancelled')
 565 |                              [InsertWithTimestamp val]
 566 |               Create                 =>
 567 |                 MkStripeStep (MkStripe available' cache' queue' queuer' nextid' cancelled')
 568 |                              [None]
 569 |               Cancelled              =>
 570 |                 MkStripeStep (MkStripe available' cache' queue' queuer' nextid' cancelled')
 571 |                              [None]
 572 |     in MkStripeStep (MkStripe available' cache' queue' queuer' nextid' cancelled')
 573 |                     [Wake wake result]
 574 |
 575 | ||| Block until a resource is delivered to this waiter.
 576 | |||
 577 | ||| Behavior:
 578 | ||| - Waits on the provided `Channel (Maybe a)` for a wakeup signal.
 579 | ||| - Returns:
 580 | |||  - `Just a` if a resource is successfully delivered.
 581 | |||  - `Nothing` if the waiter is cancelled or destroyed.
 582 | |||
 583 | ||| Cancellation:
 584 | ||| - If the waiting thread is aborted, the `cleanup` handler is invoked.
 585 | ||| - This atomically marks the waiter as cancelled by inserting its `wid` into the Stripe's `cancelled` queue.
 586 | ||| - Cancellation is lazy, cancelled waiters are skipped during dequeue.
 587 | |||
 588 | ||| Guarantees:
 589 | ||| - No busy waiting, the thread blocks on a channel.
 590 | ||| - No lost wakeups, every successful `signal` results in exactly one `channelPut` to a live waiter.
 591 | ||| - Safe under races:
 592 | |||  - If cancellation happens before wake, waiter is skipped later.
 593 | |||  -  If wake happens before cancellation, value is delivered.
 594 | ||| - Exactly-once semantics:
 595 | |||  - Each waiter receives at most one wakeup.
 596 | |||  - Each wakeup corresponds to a committed Stripe transition.
 597 | |||
 598 | ||| Design Notes:
 599 | ||| - This function performs no direct Stripe mutation except in `cleanup`.
 600 | ||| - All coordination with producers happens via `signal` + `StripeEffect`.
 601 | ||| - The `Channel (Maybe a)` encodes both success (`Just`) and termination (`Nothing`).
 602 | |||
 603 | ||| Invariants:
 604 | ||| - `wid` must be the same identifier used when enqueuing the waiter.
 605 | ||| - The channel must be single-consumer and used exactly once.
 606 | ||| - Stripe state remains the single source of truth for cancellation.
 607 | |||
 608 | export
 609 | waitForResource :  (Nat, Stripe1 World a)
 610 |                 -> Nat                    -- waiter id
 611 |                 -> Channel (WakeResult a) -- wake channel
 612 |                 -> F1 World (Either (List StripeError) (WakeResult a))
 613 | waitForResource (stripeid, (MkStripe1 striperef)) wid wake t =
 614 |   let res    # t := ioToF1 (runElinIO (waitForResource' (MkStripe1 striperef) wid wake)) t
 615 |       Right res' := res
 616 |         | Left err =>
 617 |             let realtimenow    # t := ioToF1 (runElinIO grabRealTime) t
 618 |                 Right realtimenow' := realtimenow
 619 |                   | Left realtimenowerr =>
 620 |                       let newerrors := [ MkStripeError stripeid "Data.Pool.waitForResource" (show realtimenowerr) Nothing
 621 |                                        , MkStripeError stripeid "Data.Pool.waitForResource" (show err) Nothing
 622 |                                        ]
 623 |                         in Left newerrors # t
 624 |                 newerrors := [MkStripeError stripeid "Data.Pool.waitForResource" (show err) (Just realtimenow')]
 625 |               in Left newerrors # t
 626 |     in Right res' # t
 627 |   where
 628 |     cleanup :   Stripe1 World a
 629 |              -> Nat
 630 |              -> F1' World
 631 |     cleanup (MkStripe1 mstripe) wid t =
 632 |       casupdate1 mstripe (\(MkStripe available cache queue queuer nextid cancelled) =>
 633 |                            (MkStripe available cache queue queuer nextid (insert wid cancelled), ())
 634 |                          ) t
 635 |     waitForResource'' :  Channel (WakeResult a)
 636 |                       -> F1 World (WakeResult a)
 637 |     waitForResource'' wake t =
 638 |       ioToF1 (channelGet wake) t
 639 |     waitForResource' :  MCancel (Elin World)
 640 |                      => Stripe1 World a
 641 |                      -> Nat
 642 |                      -> Channel (WakeResult a)
 643 |                      -> Elin World [Errno] (WakeResult a)
 644 |     waitForResource' mstripe wid wake =
 645 |       onAbort (runIO (waitForResource'' wake)) (runIO (cleanup mstripe wid))
 646 |
 647 | ||| Destroy a resource instead of returning it to the `Pool1 World a`.
 648 | |||
 649 | ||| Behavior:
 650 | ||| - If a waiter exists, they are woken with `Nothing`.
 651 | ||| - Otherwise, no state change occurs (resource is discarded).
 652 | |||
 653 | ||| Guarantees:
 654 | ||| - Waiters are not left blocked indefinitely.
 655 | ||| - No resource is reinserted into the cache.
 656 | |||
 657 | export
 658 | destroyResource :  (Nat, Stripe1 World a)
 659 |                 -> F1 World (Either (List StripeError) ())
 660 | destroyResource (stripeid, (MkStripe1 striperef)) t =
 661 |   let res    # t := ioToF1 (runElinIO (destroy (stripeid, (MkStripe1 striperef)))) t
 662 |       Right res' := res
 663 |         | Left err =>
 664 |             let realtimenow    # t := ioToF1 (runElinIO grabRealTime) t
 665 |                 Right realtimenow' := realtimenow
 666 |                   | Left realtimenowerr =>
 667 |                       let newerrors := [ MkStripeError stripeid "Data.Pool.destroyResource" (show realtimenowerr) Nothing
 668 |                                        , MkStripeError stripeid "Data.Pool.destoryResource" (show err) Nothing
 669 |                                        ]
 670 |                         in Left newerrors # t
 671 |                 newerrors := [MkStripeError stripeid "Data.Pool.destroyResource" (show err) (Just realtimenow')]
 672 |               in Left newerrors # t
 673 |       Right ()   := res'
 674 |         | Left errs =>
 675 |             Left errs # t
 676 |     in Right () # t
 677 |   where
 678 |     destroy' :  (Nat, Stripe1 World a)
 679 |              -> F1 World (Either (List StripeError) ())
 680 |     destroy' (stripeid, (MkStripe1 striperef)) t =
 681 |       casWithEffects (stripeid, (MkStripe1 striperef)) (\stripe => signal stripe Create) t
 682 |     destroy :  MCancel (Elin World)
 683 |             => (Nat, Stripe1 World a)
 684 |             -> Elin World [Errno] (Either (List StripeError) ())
 685 |     destroy (stripeid, (MkStripe1 striperef)) =
 686 |       uncancelable $ \_ =>
 687 |         runIO (destroy' (stripeid, (MkStripe1 striperef)))
 688 |
 689 | ||| Free resource entries in the stripe that satisfy a predicate.
 690 | |||
 691 | ||| Behavior:
 692 | ||| - Removes stale entries from cache atomically.
 693 | ||| - Emits a batched free effect.
 694 | ||| - Ensures no resource is freed twice or leaked.
 695 | |||
 696 | ||| Guarantees:
 697 | ||| - Removal is atomic with respect to Stripe.
 698 | ||| - Freeing happens after commit.
 699 | ||| - Safe under contention and retries.
 700 | |||
 701 | private
 702 | cleanStripe :  (Entry a -> Bool)
 703 |             -> (a -> IO ())
 704 |             -> (Nat, Stripe1 World a)
 705 |             -> F1 World (Either (List StripeError) ())
 706 | cleanStripe isstale free (stripeid, (MkStripe1 striperef)) t =
 707 |   let res # t := ioToF1 (runElinIO (cleanStripe' (stripeid, (MkStripe1 striperef)))) t
 708 |       Right res' := res
 709 |         | Left err =>
 710 |             let realtimenow    # t := ioToF1 (runElinIO grabRealTime) t
 711 |                 Right realtimenow' := realtimenow
 712 |                   | Left realtimenowerr =>
 713 |                       let newerrors := [ MkStripeError stripeid "Data.Pool.cleanStripe" (show realtimenowerr) Nothing
 714 |                                        , MkStripeError stripeid "Data.Pool.cleanStripe" (show err) Nothing
 715 |                                        ]
 716 |                         in Left newerrors # t
 717 |                 newerrors := [MkStripeError stripeid "Data.Pool.cleanStripe" (show err) (Just realtimenow')]
 718 |               in Left newerrors # t
 719 |       Right ()   := res'
 720 |         | Left errs =>
 721 |             Left errs # t
 722 |     in Right () # t
 723 |   where
 724 |     step :  Stripe a
 725 |          -> StripeStep a
 726 |     step (MkStripe available cache queue queuer nextid cancelled) =
 727 |       let (stale, fresh) = partition isstale cache
 728 |           freedvals      = map (\(MkEntry v _) => v) stale
 729 |         in MkStripeStep
 730 |              (MkStripe available fresh queue queuer nextid cancelled)
 731 |              ( case freedvals of
 732 |                  [] =>
 733 |                    [None]
 734 |                  xs =>
 735 |                    [FreeMany free xs]
 736 |              )
 737 |     cleanStripe'' :  (Nat, Stripe1 World a)
 738 |                   -> F1 World (Either (List StripeError) ())
 739 |     cleanStripe'' (stripeid, (MkStripe1 striperef)) t =
 740 |       casWithEffects (stripeid, (MkStripe1 striperef)) step t
 741 |     cleanStripe' :  MCancel (Elin World)
 742 |                  => (Nat, Stripe1 World a)
 743 |                  -> Elin World [Errno] (Either (List StripeError) ())
 744 |     cleanStripe' (stripeid, (MkStripe1 striperef)) =
 745 |       uncancelable $ \_ =>
 746 |         runIO (cleanStripe'' (stripeid, (MkStripe1 striperef)))
 747 |
 748 | ||| Opportunistically clean stale resources from a `Stripe1 World a`.
 749 | |||
 750 | ||| This function performs stripe-local garbage collection of cached resources
 751 | ||| based on a time-to-live (TTL) policy. It replaces the need for a global
 752 | ||| collector thread by tying cleanup to normal pool activity.
 753 | |||
 754 | ||| Behavior:
 755 | ||| - Reads the current monotonic time.
 756 | ||| - Constructs a staleness predicate using the provided TTL.
 757 | ||| - Invokes `cleanStripe` to:
 758 | |||   - Remove stale entries from the cache.
 759 | |||   - Emit `FreeMany` effects for the removed resources.
 760 | ||| - Effects are executed only after the CAS commit inside `cleanStripe`.
 761 | |||
 762 | ||| Staleness:
 763 | ||| - A resource is considered stale if:
 764 | |||  - now - lastUsed > ttl
 765 | ||| - Time is measured using `CLOCK_MONOTONIC`, ensuring:
 766 | |||  - No sensitivity to wall-clock changes.
 767 | |||  - Stable elapsed-time semantics.
 768 | |||
 769 | ||| Concurrency Model:
 770 | ||| - Cleanup is performed via `cleanStripe`, which uses CAS:
 771 | |||  - Stripe state updates are atomic.
 772 | |||  - Effects are executed exactly once after commit.
 773 | ||| - Safe under contention:
 774 | |||  - Multiple threads may attempt cleanup concurrently.
 775 | |||  - Only one successful CAS applies each transition.
 776 | |||  - No resource is freed more than once.
 777 | |||
 778 | ||| Execution Model:
 779 | ||| - This function performs IO (time retrieval) outside CAS.
 780 | ||| - The actual mutation and freeing are deferred via `StripeEffect`.
 781 | ||| - No IO occurs during CAS evaluation.
 782 | |||
 783 | ||| Usage:
 784 | ||| - Intended to be called opportunistically during:
 785 | |||  - `takeResource`
 786 | |||  - `putResource`
 787 | |||  - `tryTakeResource`
 788 | ||| - Provides amortized cleanup without background threads.
 789 | |||
 790 | ||| Guarantees:
 791 | ||| - Stale resources are eventually freed under continued usage.
 792 | ||| - No interference with active resources or waiters.
 793 | ||| - No blocking or waiting is introduced.
 794 | |||
 795 | ||| Tradeoffs:
 796 | ||| - Cleanup is activity-driven rather than time-driven.
 797 | ||| - Idle stripes may retain stale resources longer.
 798 | ||| - In exchange:
 799 | |||  - No global thread.
 800 | |||  - Lower runtime overhead.
 801 | |||  - Fully local behavior.
 802 | |||
 803 | ||| Failure Handling:
 804 | ||| - Crashes if time retrieval fails (consistent with module error policy).
 805 | |||
 806 | ||| Invariants:
 807 | ||| - Only cached resources are considered for cleanup.
 808 | ||| - Each freed resource is removed exactly once.
 809 | ||| - Stripe structure remains consistent after cleanup.
 810 | |||
 811 | private
 812 | cleanStripeIfNeeded :  (ttl : Clock Duration)
 813 |                     -> (free : a -> IO ())
 814 |                     -> (Nat, Stripe1 World a)
 815 |                     -> F1 World (Either (List StripeError) ())
 816 | cleanStripeIfNeeded ttl free (stripeid, (MkStripe1 striperef)) t =
 817 |   let now    # t := ioToF1 (runElinIO grabMonotonicTime) t
 818 |       Right now' := now
 819 |         | Left err   =>
 820 |             let realtimenow    # t := ioToF1 (runElinIO grabRealTime) t
 821 |                 Right realtimenow' := realtimenow
 822 |                   | Left realtimenowerr =>
 823 |                       let newerrors := [ MkStripeError stripeid "Data.Pool.cleanStripeIfNeeded" (show realtimenowerr) Nothing
 824 |                                        , MkStripeError stripeid "Data.Pool.cleanStripeIfNeeded" (show err) Nothing
 825 |                                        ]
 826 |                         in Left newerrors # t
 827 |                 newerrors := [MkStripeError stripeid "Data.Pool.cleanStripeIfNeeded" (show err) (Just realtimenow')]
 828 |               in Left newerrors # t
 829 |     in cleanStripe (isStale ttl now') free (stripeid, (MkStripe1 striperef)) t
 830 |
 831 | ||| Return a resource to the `Pool1 World n a`.
 832 | |||
 833 | ||| Behavior:
 834 | ||| - If a waiter exists, the resource is delivered directly.
 835 | ||| - Otherwise, it is inserted into the cache with a timestamp.
 836 | |||
 837 | ||| Guarantees:
 838 | ||| - No resource is lost.
 839 | ||| - Wakeups are ordered and deterministic.
 840 | |||
 841 | export
 842 | putResource :  Pool1 World n a
 843 |             -> (Nat, Stripe1 World a)
 844 |             -> a
 845 |             -> F1 World (Either (List StripeError) ())
 846 | putResource (MkPool1 (MkPoolConfig _ free ttl _ _ _) _) (stripeid, (MkStripe1 striperef)) val t =
 847 |   let stripecleanerrs # t := cleanStripeIfNeeded ttl free (stripeid, (MkStripe1 striperef)) t
 848 |     in casWithEffects (stripeid, (MkStripe1 striperef)) (\stripe => signal stripe (Deliver val)) t
 849 |
 850 | ||| Destroy all resources in all stripes in the `Pool1 World n a`.
 851 | |||
 852 | ||| Behavior:
 853 | ||| - Removes all cached resources from every stripe.
 854 | ||| - Frees them via the provided `freeresource` function.
 855 | ||| - Leaves wait queues untouched.
 856 | |||
 857 | ||| Guarantees:
 858 | ||| - Each resource is freed exactly once.
 859 | ||| - No IO occurs during Stripe state transitions.
 860 | ||| - Safe under contention (uses CAS + effect model).
 861 | |||
 862 | ||| Notes:
 863 | ||| - This only affects cached (idle) resources.
 864 | ||| - Resources currently checked out are NOT affected.
 865 | |||
 866 | export
 867 | destroyAllResources :  {n : Nat}
 868 |                     -> Pool1 World n a
 869 |                     -> MArray World n (LocalPool1 World a)
 870 |                     -> F1 World (Either (List StripeError) ())
 871 | destroyAllResources (MkPool1 (MkPoolConfig _ freeresource _ _ _ _) _) localpools t =
 872 |   go 0 n localpools t
 873 |   where
 874 |     go :  (o, x : Nat)
 875 |        -> {auto v : Ix x n}
 876 |        -> {auto 0 prf : LTE o $ ixToNat v}
 877 |        -> (arr : MArray World n (LocalPool1 World a))
 878 |        -> F1 World (Either (List StripeError) ())
 879 |     go o Z     _   t =
 880 |       Right () # t
 881 |     go o (S j) arr t =
 882 |       let MkLocalPool1 stripeid stripe1 # t := getIx arr j t
 883 |           cleanedstripe                 # t := cleanStripe (const True) freeresource (stripeid, stripe1) t
 884 |           Right ()                          := cleanedstripe
 885 |             | Left errs =>
 886 |                 Left errs # t
 887 |         in go o j arr t
 888 |
 889 | ||| Restore one unit of available capacity in the `Stripe a`.
 890 | |||
 891 | ||| Behavior:
 892 | ||| - Increments `available` by 1.
 893 | ||| - Does not modify cache or queue.
 894 | ||| - Emits no effects.
 895 | |||
 896 | ||| Used when resource creation fails after capacity was reserved.
 897 | |||
 898 | ||| Guarantees:
 899 | ||| - Atomic under CAS.
 900 | ||| - No IO performed.
 901 | ||| - Safe under contention.
 902 | |||
 903 | export
 904 | restoreSize :  (Nat, Stripe1 World a)
 905 |             -> F1 World (Either (List StripeError) ())
 906 | restoreSize (stripeid, (MkStripe1 striperef)) t =
 907 |   casWithEffects (stripeid, (MkStripe1 striperef)) step t
 908 |   where
 909 |     step :  Stripe a
 910 |          -> StripeStep a
 911 |     step (MkStripe available cache queue queuer nextid cancelled) =
 912 |       MkStripeStep
 913 |         (MkStripe (S available) cache queue queuer nextid cancelled)
 914 |         [None]
 915 |
 916 | ||| Acquire a resource from the `Pool1 World n a`.
 917 | |||
 918 | ||| Behavior:
 919 | ||| - Attempts to take a resource from the local stripe.
 920 | ||| - Uses a single CAS step to atomically choose between:
 921 | |||  - Reusing a cached resource.
 922 | |||  - Reserving capacity for new resource creation.
 923 | |||  - Enqueuing as a waiter when fully exhausted.
 924 | |||
 925 | ||| Fast Path (Cache Reuse):
 926 | ||| - If a cached resource exists:
 927 | |||  - Remove it from the cache.
 928 | |||  - Return it immediately.
 929 | ||| - `available` is not modified.
 930 | ||| - The resource already exists and therefore does not consume creation capacity.
 931 | |||
 932 | ||| Creation Path:
 933 | ||| - If the cache is empty but `available > 0`:
 934 | |||  - Atomically decrement `available`.
 935 | |||  - Reserve one unit of creation capacity.
 936 | |||  - Create a fresh resource outside the CAS section.
 937 | |||
 938 | ||| Wait Path:
 939 | ||| - If:
 940 | |||  - cache is empty.
 941 | |||  - and `available == 0`.
 942 | ||| - Then:
 943 | |||  - enqueue a `Waiter`.
 944 | |||  - block on `waitForResource`.
 945 | ||| - The waiter is eventually:
 946 | |||  - woken with `Just a` when a resource is returned.
 947 | |||  - or `Nothing` when capacity is restored.
 948 | |||
 949 | ||| Capacity Semantics:
 950 | ||| - `available` represents remaining creation budget.
 951 | ||| - It is decremented ONLY when creating a brand-new resource.
 952 | ||| - It is restored when:
 953 | |||  - resource creation aborts.
 954 | |||  - resources are destroyed.
 955 | |||
 956 | ||| Concurrency Guarantees:
 957 | ||| - Decision logic is atomic via CAS.
 958 | ||| - No IO occurs during CAS evaluation.
 959 | ||| - Effects execute exactly once after successful commit.
 960 | ||| - Waiters are served FIFO (excluding cancelled waiters).
 961 | ||| - No lost wakeups.
 962 | |||
 963 | ||| Invariants:
 964 | ||| - Total live resources never exceeds stripe capacity.
 965 | ||| - Cached resources are timestamped before insertion.
 966 | ||| - Waiters exist only inside Stripe state.
 967 | |||
 968 | export
 969 | takeResource :  {n : Nat}
 970 |              -> Pool1 World n a
 971 |              -> F1 World (Either (Either (List Pool1Error) (List StripeError)) (a, LocalPool1 World a))
 972 | takeResource pool@(MkPool1 poolconfig@(MkPoolConfig _ free ttl _ _ _) localpools) t =
 973 |   let lp                                                          # t := getLocalPool pool t
 974 |       Right lp'@(MkLocalPool1 stripeid stripe1@(MkStripe1 striperef)) := lp
 975 |         | Left errs =>
 976 |             Left (Left errs) # t
 977 |       cleanedstripe                                               # t := cleanStripeIfNeeded ttl free (stripeid, (MkStripe1 striperef)) t
 978 |       Right ()                                                        := cleanedstripe
 979 |         | Left errs =>
 980 |             Left (Right errs) # t
 981 |       wake                                                        # t := ioToF1 makeChannel t
 982 |       res                                                             : (List (StripeEffect a), Either a (Either () (Nat, Channel (WakeResult a))))
 983 |       (effects, res'')                                            # t :=
 984 |         casupdate1 striperef (\(MkStripe available cache queue queuer nextid cancelled) =>
 985 |                                 case cache of
 986 |                                   -- fast path
 987 |                                   MkEntry v _ :: rest =>
 988 |                                     let none : List (StripeEffect a)
 989 |                                         none    = [None]
 990 |                                         stripe' = MkStripe available
 991 |                                                            rest
 992 |                                                            queue
 993 |                                                            queuer
 994 |                                                            nextid
 995 |                                                            cancelled
 996 |                                         result : Either a (Either () (Nat, Channel (WakeResult a)))
 997 |                                         result = Left v
 998 |                                       in ( stripe'
 999 |                                          , (none, result)
1000 |                                          )
1001 |                                   -- slow path
1002 |                                   []                  =>
1003 |                                     case available == 0 of
1004 |                                       True  =>
1005 |                                         -- enqueue waiter
1006 |                                         let none : List (StripeEffect a)
1007 |                                             none    = [None]
1008 |                                             wid     = nextid
1009 |                                             waiter : Waiter a
1010 |                                             waiter  = MkWaiter wid wake
1011 |                                             stripe' = MkStripe available
1012 |                                                                cache
1013 |                                                                queue
1014 |                                                                (appendQ queuer waiter)
1015 |                                                                (S nextid)
1016 |                                                                cancelled
1017 |                                             result : Either a (Either () (Nat, Channel (WakeResult a)))
1018 |                                             result = Right (Right (wid, wake))
1019 |                                           in ( stripe'
1020 |                                              , (none, result)
1021 |                                              )
1022 |                                       False =>
1023 |                                         -- resource creation slot
1024 |                                         let none : List (StripeEffect a)
1025 |                                             none    = [None]
1026 |                                             stripe' = MkStripe (minus available 1)
1027 |                                                                cache
1028 |                                                                queue
1029 |                                                                queuer
1030 |                                                                nextid
1031 |                                                                 cancelled
1032 |                                             result : Either a (Either () (Nat, Channel (WakeResult a)))
1033 |                                             result = Right (Left ())
1034 |                                           in ( stripe'
1035 |                                              , (none, result)
1036 |                                              )
1037 |                              ) t
1038 |       -- Run effects after commit
1039 |       effects'                                                    # t := runEffects (stripeid, stripe1) effects t
1040 |       Right ()                                                        := effects'
1041 |         | Left errs =>
1042 |             Left (Right errs) # t
1043 |       Right (Right (wid, wake))                                       := res''
1044 |         | -- fast path
1045 |           Left v =>
1046 |             Right (v, lp') # t
1047 |           -- create immediately
1048 |         | Right (Left ()) =>
1049 |             let res  # t := ioToF1 (runElinIO (createWithCleanup poolconfig (stripeid, stripe1))) t
1050 |                 Left err := res
1051 |                   | Right v =>
1052 |                       Right (v, lp') # t
1053 |                 realtimenow    # t := ioToF1 (runElinIO grabRealTime) t
1054 |                 Right realtimenow' := realtimenow
1055 |                   | Left realtimenowerr =>
1056 |                       let newerrors := [ MkStripeError stripeid "Data.Pool.takeResource" (show realtimenowerr) Nothing
1057 |                                        , MkStripeError stripeid "Data.Pool.takeResource" (show err) Nothing
1058 |                                        ]
1059 |                         in Left (Right newerrors) # t
1060 |                 newerrors           := [MkStripeError stripeid "Data.Pool.takeResource" (show err) (Just realtimenow')]
1061 |               in Left (Right newerrors) # t
1062 |       wakeresult                                                  # t := waitForResource (stripeid, stripe1) wid wake t
1063 |       Right wakeresult'                                               := wakeresult
1064 |         | Left errs =>
1065 |             let realtimenow    # t := ioToF1 (runElinIO grabRealTime) t
1066 |                 Right realtimenow' := realtimenow
1067 |                   | Left realtimenowerr =>
1068 |                       let newerrors := [ MkStripeError stripeid "Data.Pool.takeResource" (show realtimenowerr) Nothing
1069 |                                        , MkStripeError stripeid "Data.Pool.takeResource" "Data.Pool.waitForResource failed" Nothing
1070 |                                        ]
1071 |                         in Left (Right $ errs ++ newerrors) # t
1072 |                 newerrors := [MkStripeError stripeid "Data.Pool.takeResource" "Data.Pool.waitForResource failed" (Just realtimenow')]
1073 |               in Left (Right $ errs ++ newerrors) # t
1074 |       -- need to create
1075 |       Create                                                          := wakeresult'
1076 |         | -- woken with resource
1077 |           Deliver v =>
1078 |             Right (v, lp') # t
1079 |         | Cancelled =>
1080 |             let realtimenow    # t := ioToF1 (runElinIO grabRealTime) t
1081 |                 Right realtimenow' := realtimenow
1082 |                   | Left realtimenowerr =>
1083 |                       let newerrors := [ MkStripeError stripeid "Data.Pool.takeResource" (show realtimenowerr) Nothing
1084 |                                        , MkStripeError stripeid "Data.Pool.takeResource" "impossible" Nothing
1085 |                                        ]
1086 |                         in Left (Right newerrors) # t
1087 |                 newerrors := [MkStripeError stripeid "Data.Pool.takeResource" "impossible" (Just realtimenow')]
1088 |               in Left (Right newerrors) # t
1089 |       res                                                         # t := ioToF1 (runElinIO (createWithCleanup poolconfig (stripeid, stripe1))) t
1090 |       Left err                                                        := res
1091 |         | Right v =>
1092 |             Right (v, lp') # t     
1093 |       realtimenow                                                 # t := ioToF1 (runElinIO grabRealTime) t
1094 |       Right realtimenow'                                              := realtimenow
1095 |         | Left realtimenowerr =>
1096 |             let newerrors := [ MkStripeError stripeid "Data.Pool.takeResource" (show realtimenowerr) Nothing
1097 |                              , MkStripeError stripeid "Data.Pool.takeResource" (show err) Nothing
1098 |                              ]
1099 |               in Left (Right newerrors) # t
1100 |       newerrors                                                       := [MkStripeError stripeid "Data.Pool.takeResource" (show err) (Just realtimenow')]
1101 |     in Left (Right newerrors) # t
1102 |   where
1103 |     createWithCleanup :  PoolConfig a
1104 |                       -> (Nat, Stripe1 World a)
1105 |                       -> Elin World [Errno] a
1106 |     createWithCleanup (MkPoolConfig createResource _ _ _ _ _) (stripeid, stripe) =
1107 |       onAbort (liftIO createResource) ( do _ <- runIO (restoreSize (stripeid, stripe))
1108 |                                            liftIO (pure ())
1109 |                                       )
1110 |
1111 | ||| Safely acquire and use a resource from the pool.
1112 | |||
1113 | ||| This is the primary high-level interface for working with `Pool1`.
1114 | ||| It ensures that resources are correctly returned or destroyed,
1115 | ||| even in the presence of exceptions or cancellation.
1116 | |||
1117 | ||| Behavior:
1118 | ||| - Acquires a resource using `takeResource`.
1119 | ||| - Executes the user action `f` with that resource.
1120 | ||| - On normal completion:
1121 | |||  - The resource is returned to the pool via `putResource`.
1122 | ||| - On exception or cancellation:
1123 | |||  - The resource is destroyed via `destroyResource`.
1124 | |||
1125 | ||| Concurrency & Masking:
1126 | ||| - The entire operation runs inside `uncancelable`, ensuring:
1127 | |||  - Resource acquisition and release cannot be interrupted.
1128 | ||| - The user action `f` is executed via `poll`, meaning:
1129 | |||  - It *can* be interrupted or cancelled.
1130 | ||| - If cancellation occurs during `f`, the cleanup handler runs.
1131 | |||
1132 | ||| Cleanup Guarantees:
1133 | ||| - Exactly one of the following happens:
1134 | |||  - `putResource` (success path)
1135 | |||  - `destroyResource` (failure or cancellation path)
1136 | ||| - No resource is leaked or returned twice.
1137 | ||| - Waiters are properly woken via Stripe effects.
1138 | |||
1139 | ||| Failure Handling:
1140 | ||| - Exceptions from `f` are propagated.
1141 | ||| - Exceptions during acquisition or cleanup cause a crash (consistent with the rest of the module’s error handling).
1142 | |||
1143 | ||| Returns:
1144 | ||| - The result of applying `f` to the acquired resource.
1145 | |||
1146 | ||| Invariants:
1147 | ||| - Resources are never duplicated or lost.
1148 | ||| - Pool state remains consistent under concurrency.
1149 | ||| - All Stripe effects are executed after CAS commit.
1150 | |||
1151 | export
1152 | withResource :  {n : Nat}
1153 |              -> Pool1 World n a
1154 |              -> (a -> IO r)
1155 |              -> F1 World (Either (Either (List Pool1Error) (List StripeError)) (Maybe r))
1156 | withResource pool@(MkPool1 _ localpools) f t =
1157 |   let res     # t := ioToF1 (runElinIO (withResource' pool f)) t
1158 |       Right res'  := res
1159 |         | Left err =>
1160 |             let realtimenow    # t := ioToF1 (runElinIO grabRealTime) t
1161 |                 Right realtimenow' := realtimenow
1162 |                   | Left realtimenowerr =>
1163 |                       let newerrors := [ MkPool1Error "Data.Pool.withResource" (show realtimenowerr) Nothing
1164 |                                        , MkPool1Error "Data.Pool.withResource" (show err) Nothing
1165 |                                        ]
1166 |                         in Left (Left newerrors) # t
1167 |                 newerrors := [MkPool1Error "Data.Pool.withResource" (show err) (Just realtimenow')]
1168 |               in Left (Left newerrors) # t
1169 |       Right res'' := res'
1170 |         | Left errs =>
1171 |             let Right stripeerrs := errs
1172 |                   | Left poolerrs =>
1173 |                       Left (Left poolerrs) # t
1174 |               in Left (Right stripeerrs) # t
1175 |       Just res''' := res''
1176 |         | Nothing =>
1177 |             Right Nothing # t
1178 |     in Right (Just res''') # t
1179 |   where
1180 |     withResource' :  {n : Nat}
1181 |                   -> MCancel (Elin World)
1182 |                   => Pool1 World n a
1183 |                   -> (a -> IO r)
1184 |                   -> Elin World [Errno] (Either (Either (List Pool1Error) (List StripeError)) (Maybe r))
1185 |     withResource' pool@(MkPool1 _ localpools) f =
1186 |       uncancelable $ \poll => do
1187 |         res <- runIO (takeResource pool)
1188 |         let Right (res', MkLocalPool1 stripeid (MkStripe1 striperef)) = res
1189 |               | Left errs => do
1190 |                   let Right stripeerrs = errs
1191 |                         | Left poolerrs =>
1192 |                             pure (Left (Left poolerrs))
1193 |                   pure (Left (Right stripeerrs))
1194 |         res'' <- onAbort (poll $ liftIO $ f res') ( do _ <- runIO (destroyResource (stripeid, (MkStripe1 striperef)))
1195 |                                                        liftIO (pure ())
1196 |                                                   )
1197 |         putr <- runIO (putResource pool (stripeid, (MkStripe1 striperef)) res')
1198 |         let Right () = putr
1199 |               | Left errs =>
1200 |                   pure (Left (Right errs))
1201 |         pure (Right (Just res''))
1202 |
1203 | ||| Attempt to take a resource without blocking.
1204 | |||
1205 | ||| Behavior:
1206 | ||| - Reads the local stripe and checks availability.
1207 | ||| - If no resources are available:
1208 | |||   - Returns `Nothing` immediately.
1209 | |||   - Does NOT enqueue a waiter.
1210 | |||   - Does NOT create a resource.
1211 | |||
1212 | ||| - If a resource is available:
1213 | |||   - Removes it atomically via CAS.
1214 | |||   - Returns `Just (resource, LocalPool1)`.
1215 | |||
1216 | ||| Guarantees:
1217 | ||| - Non-blocking: never waits on a channel.
1218 | ||| - No side effects inside CAS.
1219 | ||| - No waiter allocation.
1220 | ||| - Safe under contention via CAS retry.
1221 | |||
1222 | export
1223 | tryTakeResource :  {n : Nat}
1224 |                 -> Pool1 World n a
1225 |                 -> F1 World (Either (Either (List Pool1Error) (List StripeError)) (Maybe (a, LocalPool1 World a)))
1226 | tryTakeResource pool@(MkPool1 _ localpools) t =
1227 |   let res     # t := ioToF1 (runElinIO (tryTakeResource' pool)) t
1228 |       Right res'  := res
1229 |         | Left err =>
1230 |             let realtimenow    # t := ioToF1 (runElinIO grabRealTime) t
1231 |                 Right realtimenow' := realtimenow
1232 |                   | Left realtimenowerr =>
1233 |                       let newerrors := [ MkPool1Error "Data.Pool.tryTakeResource" (show realtimenowerr) Nothing
1234 |                                        , MkPool1Error "Data.Pool.tryTakeResource" (show err) Nothing
1235 |                                        ]
1236 |                         in Left (Left newerrors) # t
1237 |                 newerrors := [MkPool1Error "Data.Pool.tryTakeResource" (show err) (Just realtimenow')]
1238 |               in Left (Left newerrors) # t
1239 |       Right res'' := res'
1240 |         | Left errs =>
1241 |             let Right stripeerrs := errs
1242 |                   | Left poolerrs =>
1243 |                       Left (Left poolerrs) # t
1244 |               in Left (Right stripeerrs) # t
1245 |       Just res''' := res''
1246 |         | Nothing =>
1247 |             Right Nothing # t
1248 |     in Right (Just res''') # t
1249 |   where
1250 |     tryTakeResource'' :  {n : Nat}
1251 |                       -> MCancel (Elin World)
1252 |                       => Pool1 World n a
1253 |                       -> F1 World (Either (Either (List Pool1Error) (List StripeError)) (Maybe (a, LocalPool1 World a)))
1254 |     tryTakeResource'' pool@(MkPool1 (MkPoolConfig _ free ttl _ _ _) _) t =
1255 |       let lp                                                          # t := getLocalPool pool t
1256 |           Right lp'@(MkLocalPool1 stripeid stripe1@(MkStripe1 striperef)) := lp
1257 |             | Left poolerrs =>
1258 |                 Left (Left poolerrs) # t
1259 |           -- clean stripe if needed
1260 |           cleanedstripe                                               # t := cleanStripeIfNeeded ttl free (stripeid, (MkStripe1 striperef)) t
1261 |           Right ()                                                        := cleanedstripe
1262 |             | Left stripeerrs =>
1263 |                 Left (Right stripeerrs) # t
1264 |           -- attempt fast-path only
1265 |           res                                                         # t :=
1266 |             casupdate1 striperef (\(MkStripe available cache queue queuer nextid cancelled) =>
1267 |                                     case (available == 0, cache) of
1268 |                                       -- no capacity, do nothing
1269 |                                       (True, _)                    =>
1270 |                                         ( MkStripe available cache queue queuer nextid cancelled
1271 |                                         , Nothing
1272 |                                         )
1273 |                                       -- cache hit, consume
1274 |                                       (False, MkEntry v _ :: rest) =>
1275 |                                         ( MkStripe available
1276 |                                                    rest
1277 |                                                    queue
1278 |                                                    queuer
1279 |                                                    nextid
1280 |                                                    cancelled
1281 |                                         , Just v
1282 |                                         )
1283 |                                       -- available > 0, but cache empty
1284 |                                       (False, [])                  =>
1285 |                                         ( MkStripe available cache queue queuer nextid cancelled
1286 |                                         , Nothing
1287 |                                         )
1288 |                                  ) t
1289 |           Just v                                                          := res
1290 |             | Nothing =>
1291 |                 Right Nothing # t
1292 |         in Right (Just (v, lp')) # t
1293 |     tryTakeResource' :  {n : Nat}
1294 |                      -> MCancel (Elin World)
1295 |                      => Pool1 World n a
1296 |                      -> Elin World [Errno] (Either (Either (List Pool1Error) (List StripeError)) (Maybe (a, LocalPool1 World a)))
1297 |     tryTakeResource' pool =
1298 |       uncancelable $ \_ =>
1299 |         runIO (tryTakeResource'' pool)
1300 |
1301 | ||| Attempt to acquire and use a resource from the pool without blocking.
1302 | |||
1303 | ||| Behavior:
1304 | ||| - Tries to take a resource immediately using `tryTakeResource`.
1305 | ||| - If no resource is available:
1306 | |||  - Returns `Nothing` without blocking or creating a resource.
1307 | ||| - If a resource is available:
1308 | |||  - Executes the provided function `f` with the resource.
1309 | |||  - Returns `Just result` on success.
1310 | |||
1311 | ||| Resource Handling:
1312 | ||| - The acquired resource is always returned to the pool via `putResource` after successful execution of `f`.
1313 | ||| - If an exception or cancellation occurs during `f`:
1314 | |||  - The resource is destroyed using `destroyResource` instead of being returned.
1315 | |||
1316 | ||| Cancellation Semantics:
1317 | ||| - The outer operation is `uncancelable`, ensuring:
1318 | |||  - No resource is leaked between acquisition and release.
1319 | ||| - The user function `f` is executed under `poll`, meaning:
1320 | |||  - It remains cancelable.
1321 | ||| - If cancellation occurs during `f`:
1322 | |||  - The resource is safely discarded.
1323 | |||  - The pool remains in a consistent state.
1324 | |||
1325 | ||| Concurrency Guarantees:
1326 | ||| - Does not block waiting for a resource.
1327 | ||| - Does not enqueue a waiter.
1328 | ||| - All Stripe transitions (`putResource`, `destroyResource`) are performed via `casWithEffects`, ensuring:
1329 | |||  - Atomic state updates.
1330 | |||  - No duplicated side effects.
1331 | |||  - Deterministic wake behavior.
1332 | |||
1333 | ||| Failure Handling:
1334 | ||| - Any exception from `f` is propagated.
1335 | ||| - Internal pool errors result in a crash with diagnostic information.
1336 | |||
1337 | ||| Returns:
1338 | ||| - `Nothing` if no resource was immediately available.
1339 | ||| - `Just r` if a resource was acquired and `f` completed successfully.
1340 | |||
1341 | ||| Notes:
1342 | ||| - This function is the non-blocking counterpart to `withResource`.
1343 | ||| - It is useful when callers prefer to fallback rather than wait.
1344 | |||
1345 | export
1346 | tryWithResource :  {n : Nat}
1347 |                 -> Pool1 World n a
1348 |                 -> (a -> IO r)
1349 |                 -> F1 World (Either (Either (List Pool1Error) (List StripeError)) (Maybe r))
1350 | tryWithResource pool@(MkPool1 _ localpools) f t =
1351 |   let res     # t := ioToF1 (runElinIO (tryWithResource' pool f)) t
1352 |       Right res'  := res
1353 |         | Left err =>
1354 |             let realtimenow    # t := ioToF1 (runElinIO grabRealTime) t
1355 |                 Right realtimenow' := realtimenow
1356 |                   | Left realtimenowerr =>
1357 |                       let newerrors := [ MkPool1Error "Data.Pool.tryWithResource" (show realtimenowerr) Nothing
1358 |                                        , MkPool1Error "Data.Pool.tryWithResource" (show err) Nothing
1359 |                                        ]
1360 |                         in Left (Left newerrors) # t
1361 |                 newerrors := [MkPool1Error "Data.Pool.tryWithResource" (show err) (Just realtimenow')]
1362 |               in Left (Left newerrors) # t
1363 |       Right res'' := res'
1364 |         | Left errs =>
1365 |             let Right stripeerrs := errs
1366 |                   | Left poolerrs =>
1367 |                       Left (Left poolerrs) # t
1368 |               in Left (Right stripeerrs) # t
1369 |       Just res''' := res''
1370 |         | Nothing =>
1371 |             Right Nothing # t
1372 |     in Right (Just res''') # t
1373 |   where
1374 |     tryWithResource' :  {n : Nat}
1375 |                      -> MCancel (Elin World)
1376 |                      => Pool1 World n a
1377 |                      -> (a -> IO r)
1378 |                      -> Elin World [Errno] (Either (Either (List Pool1Error) (List StripeError)) (Maybe r))
1379 |     tryWithResource' pool@(MkPool1 _ localpools) f =
1380 |       uncancelable $ \poll => do
1381 |         res                                                           <- runIO (tryTakeResource pool)
1382 |         let Right res'                                                := res
1383 |               | Left errs =>
1384 |                   let Right stripeerrs := errs
1385 |                         | Left poolerrs =>
1386 |                             pure (Left (Left poolerrs))
1387 |                     in pure (Left (Right stripeerrs))
1388 |         let Just (res'', MkLocalPool1 stripeid (MkStripe1 striperef)) := res'
1389 |               | Nothing =>
1390 |                   pure (Right Nothing)
1391 |         res''' <- onAbort (poll $ liftIO $ f res'') ( do _ <- runIO (destroyResource (stripeid, (MkStripe1 striperef)))
1392 |                                                          liftIO (pure ())
1393 |                                                     )
1394 |         putr <- runIO (putResource pool (stripeid, (MkStripe1 striperef)) res'')
1395 |         let Right ()                                                  := putr
1396 |               | Left stripeerrs =>
1397 |                   pure (Left (Right stripeerrs))
1398 |         pure (Right (Just res'''))
1399 |