
  0 | module Evince.Async.Synchronized
  1 | 
  2 | import Data.Linear.Ref1
  3 | import IO.Async
  4 | import public Evince.Synchronized
  5 | 
  6 | %default total
  7 | 
  8 | -- Atomic compare-and-swap spinlock. Acquire flips the flag False -> True with
  9 | -- `caswrite1` (one atomic step), so it serializes correctly even when worker
 10 | -- threads contend (true parallelism); on failure we `cede` - yielding the
 11 | -- fiber, never blocking the worker thread - and retry. Release is *also* a
 12 | -- `caswrite1` (True -> False, which always succeeds since the holder set it),
 13 | -- not a plain write: the CAS is a memory barrier, so writes made inside the
 14 | -- critical section are published to the next acquirer (release/acquire ordering
 15 | -- across threads).
 16 | acquire : IORef Bool -> Async e [] ()
 17 | acquire ref = assert_total $ do
 18 |   got <- runIO (caswrite1 ref False True)
 19 |   if got then pure () else (cede >> acquire ref)
 20 | 
 21 | ||| Run an action with the lock held, serializing concurrent `Async` fibers
 22 | ||| (across worker threads) via the atomic CAS spinlock.
 23 | export
 24 | asyncWithLock : IORef Bool -> ({0 a : Type} -> Async e [] a -> Async e [] a)
 25 | asyncWithLock ref act = do
 26 |   acquire ref
 27 |   r <- act
 28 |   ignore $ runIO (caswrite1 ref True False)
 29 |   pure r
 30 | 
 31 | export
 32 | {e : Type} -> Synchronized (Async e []) where
 33 |   newLock = do
 34 |     ref <- newref False
 35 |     pure (MkLock (asyncWithLock ref))
 36 |