System.Concurrency


   0 | ||| Concurrency primitives, e.g. threads, mutexes, etc.
   1 | |||
   2 | ||| N.B.: At the moment this is pretty fundamentally tied to the Scheme RTS.
   3 | ||| Given that different back ends will have entirely different threading
   4 | ||| models, it might be unavoidable, but we might want to think about possible
   5 | ||| primitives that back ends should support.
   6 | module System.Concurrency
   7 | 
   8 | import System.Info
   9 | 
  10 | %default total
  11 | 
  12 | 
  13 | -- Thread mailboxes
  14 | 
  15 | %foreign "scheme:blodwen-set-thread-data"
  16 | prim__setThreadData : {a : Type} -> a -> PrimIO ()
  17 | %foreign "scheme:blodwen-get-thread-data"
  18 | prim__getThreadData : (a : Type) -> PrimIO a
  19 | %foreign "scheme,chez:get-thread-id"
  20 | prim__getThreadId : PrimIO Int
  21 | 
  22 | ||| Set the data stored in a thread's parameter to the given value.
  23 | ||| Currently only supported under the scheme backends.
  24 | export
  25 | setThreadData : HasIO io => {a : Type} -> a -> io ()
  26 | setThreadData val = primIO (prim__setThreadData val)
  27 | 
  28 | ||| Get the data stored in a thread's parameter.
  29 | ||| Currently only supported under the scheme backends.
  30 | export
  31 | getThreadData : HasIO io => (a : Type) -> io a
  32 | getThreadData a = primIO (prim__getThreadData a)
  33 | 
  34 | ||| Get the thread id of the current thread (chez backend).
  35 | export
  36 | getThreadId : HasIO io => io Int
  37 | getThreadId = primIO prim__getThreadId
  38 | 
  39 | 
  40 | -- Mutexes
  41 | 
  42 | export
  43 | data Mutex : Type where [external]
  44 | 
  45 | %foreign "scheme:blodwen-make-mutex"
  46 | prim__makeMutex : PrimIO Mutex
  47 | %foreign "scheme:blodwen-mutex-acquire"
  48 | prim__mutexAcquire : Mutex -> PrimIO ()
  49 | %foreign "scheme:blodwen-mutex-release"
  50 | prim__mutexRelease : Mutex -> PrimIO ()
  51 | 
  52 | ||| Creates and returns a new mutex.
  53 | export
  54 | makeMutex : HasIO io => io Mutex
  55 | makeMutex = primIO prim__makeMutex
  56 | 
  57 | ||| Acquires the mutex identified by `mutex`. The thread blocks until the mutex
  58 | ||| has been acquired.
  59 | |||
  60 | ||| Mutexes are recursive in Posix threads terminology, which means that the
  61 | ||| calling thread can use mutex-acquire to (re)acquire a mutex it already has.
  62 | ||| In this case, an equal number of mutex-release calls is necessary to release
  63 | ||| the mutex.
  64 | export
  65 | mutexAcquire : HasIO io => Mutex -> io ()
  66 | mutexAcquire m = primIO (prim__mutexAcquire m)
  67 | 
  68 | ||| Releases the mutex identified by `mutex`. Unpredictable behavior results if
  69 | ||| the mutex is not owned by the calling thread.
  70 | export
  71 | mutexRelease : HasIO io => Mutex -> io ()
  72 | mutexRelease m = primIO (prim__mutexRelease m)
  73 | 
  74 | 
  75 | -- Condition variables
  76 | 
  77 | export
  78 | data Condition : Type where [external]
  79 | 
  80 | %foreign "scheme,racket:blodwen-make-cv"
  81 |          "scheme,chez:blodwen-make-condition"
  82 | prim__makeCondition : PrimIO Condition
  83 | %foreign "scheme,racket:blodwen-cv-wait"
  84 |          "scheme,chez:blodwen-condition-wait"
  85 | prim__conditionWait : Condition -> Mutex -> PrimIO ()
  86 | %foreign "scheme,chez:blodwen-condition-wait-timeout"
  87 | --         "scheme,racket:blodwen-cv-wait-timeout"
  88 | prim__conditionWaitTimeout : Condition -> Mutex -> Int -> PrimIO ()
  89 | %foreign "scheme,racket:blodwen-cv-signal"
  90 |          "scheme,chez:blodwen-condition-signal"
  91 | prim__conditionSignal : Condition -> PrimIO ()
  92 | %foreign "scheme,racket:blodwen-cv-broadcast"
  93 |          "scheme,chez:blodwen-condition-broadcast"
  94 | prim__conditionBroadcast : Condition -> PrimIO ()
  95 | 
  96 | 
  97 | ||| Creates and returns a new condition variable.
  98 | export
  99 | makeCondition : HasIO io => io Condition
 100 | makeCondition = primIO prim__makeCondition
 101 | 
 102 | ||| Waits up to the specified timeout for the condition identified by the
 103 | ||| condition variable `cond`. The calling thread must have acquired the mutex
 104 | ||| identified by `mutex` at the time `conditionWait` is called. The mutex is
 105 | ||| released as a side effect of the call to `conditionWait`. When a thread is
 106 | ||| later released from the condition variable by one of the procedures
 107 | ||| described below, the mutex is reacquired and `conditionWait` returns.
 108 | export
 109 | conditionWait : HasIO io => Condition -> Mutex -> io ()
 110 | conditionWait cond mutex = primIO (prim__conditionWait cond mutex)
 111 | 
 112 | ||| Variant of `conditionWait` with a timeout in microseconds.
 113 | ||| When the timeout expires, the thread is released, `mutex` is reacquired, and
 114 | ||| `conditionWaitTimeout` returns.
 115 | export
 116 | conditionWaitTimeout : HasIO io => Condition -> Mutex -> Int -> io ()
 117 | conditionWaitTimeout cond mutex timeout = primIO (prim__conditionWaitTimeout cond mutex timeout)
 118 | 
 119 | ||| Releases one of the threads waiting for the condition identified by `cond`.
 120 | export
 121 | conditionSignal : HasIO io => Condition -> io ()
 122 | conditionSignal c = primIO (prim__conditionSignal c)
 123 | 
 124 | ||| Releases all of the threads waiting for the condition identified by `cond`.
 125 | export
 126 | conditionBroadcast : HasIO io => Condition -> io ()
 127 | conditionBroadcast c = primIO (prim__conditionBroadcast c)
 128 | 
 129 | 
 130 | -- Semaphores
 131 | 
 132 | export
 133 | data Semaphore : Type where [external]
 134 | 
 135 | %foreign "scheme:blodwen-make-semaphore"
 136 | prim__makeSemaphore : Int -> PrimIO Semaphore
 137 | %foreign "scheme:blodwen-semaphore-post"
 138 | prim__semaphorePost : Semaphore -> PrimIO ()
 139 | %foreign "scheme:blodwen-semaphore-wait"
 140 | prim__semaphoreWait : Semaphore -> PrimIO ()
 141 | 
 142 | 
 143 | ||| Creates and returns a new semaphore with the counter initially set to `init`.
 144 | export
 145 | makeSemaphore : HasIO io => Int -> io Semaphore
 146 | makeSemaphore init = primIO (prim__makeSemaphore init)
 147 | 
 148 | ||| Increments the semaphore's internal counter.
 149 | export
 150 | semaphorePost : HasIO io => Semaphore -> io ()
 151 | semaphorePost sema = primIO (prim__semaphorePost sema)
 152 | 
 153 | ||| Blocks until the internal counter for semaphore sema is non-zero. When the
 154 | ||| counter is non-zero, it is decremented and `semaphoreWait` returns.
 155 | export
 156 | semaphoreWait : HasIO io => Semaphore -> io ()
 157 | semaphoreWait sema = primIO (prim__semaphoreWait sema)
 158 | 
 159 | 
 160 | -- Barriers
 161 | 
 162 | ||| A barrier enables multiple threads to synchronize the beginning of some
 163 | ||| computation.
 164 | export
 165 | data Barrier : Type where [external]
 166 | 
 167 | %foreign "scheme:blodwen-make-barrier"
 168 | prim__makeBarrier : Int -> PrimIO Barrier
 169 | %foreign "scheme:blodwen-barrier-wait"
 170 | prim__barrierWait : Barrier -> PrimIO ()
 171 | 
 172 | ||| Creates a new barrier that can block a given number of threads.
 173 | |||
 174 | ||| @ numThreads the number of threads to block
 175 | export
 176 | makeBarrier : HasIO io => (numThreads : Int) -> io Barrier
 177 | makeBarrier numThreads = primIO (prim__makeBarrier numThreads)
 178 | 
 179 | ||| Blocks the current thread until all threads have rendezvoused here.
 180 | export
 181 | barrierWait : HasIO io => Barrier -> io ()
 182 | barrierWait barrier = primIO (prim__barrierWait barrier)
 183 | 
 184 | 
 185 | -- Channels
 186 | 
 187 | export
 188 | data Channel : Type -> Type where [external]
 189 | 
 190 | %foreign "scheme:blodwen-make-channel"
 191 | prim__makeChannel : PrimIO (Channel a)
 192 | %foreign "scheme:blodwen-channel-get"
 193 | prim__channelGet : Channel a -> PrimIO a
 194 | %foreign "scheme,chez:blodwen-channel-get-non-blocking"
 195 | prim__channelGetNonBlocking : Channel a -> PrimIO (Maybe a)
 196 | %foreign "scheme,chez:blodwen-channel-get-with-timeout"
 197 | prim__channelGetWithTimeout : Channel a -> Int -> PrimIO (Maybe a)
 198 | %foreign "scheme:blodwen-channel-put"
 199 | prim__channelPut : Channel a -> a -> PrimIO ()
 200 | 
 201 | ||| Creates and returns a new `Channel`.
 202 | |||
 203 | ||| The channel can be used with `channelGet` to receive a value through the
 204 | ||| channel.
 205 | ||| The channel can be used with `channelPut` to send a value through the
 206 | ||| channel.
 207 | export
 208 | makeChannel : HasIO io => io (Channel a)
 209 | makeChannel = primIO prim__makeChannel
 210 | 
 211 | ||| Blocks until a sender is ready to provide a value through `chan`. The result
 212 | ||| is the sent value.
 213 | |||
 214 | ||| @ chan the channel to receive on
 215 | export
 216 | channelGet : HasIO io => (chan : Channel a) -> io a
 217 | channelGet chan = primIO (prim__channelGet chan)
 218 | 
 219 | ||| Non-blocking version of channelGet (chez backend).
 220 | |||
 221 | ||| @ chan the channel to receive on
 222 | partial
 223 | export
 224 | channelGetNonBlocking : HasIO io => (chan : Channel a) -> io (Maybe a)
 225 | channelGetNonBlocking chan = primIO (prim__channelGetNonBlocking chan)
 226 | 
 227 | ||| Timeout version of channelGet (chez backend).
 228 | ||| Clamps minimum timeout to 25 ms on windows.
 229 | |||
 230 | ||| @ chan the channel to receive on
 231 | ||| @ milliseconds how many milliseconds to wait until timeout
 232 | partial
 233 | export
 234 | channelGetWithTimeout : HasIO io => (chan : Channel a) -> (milliseconds : Nat) -> io (Maybe a)
 235 | channelGetWithTimeout chan milliseconds =
 236 |   case os of
 237 |     "windows" =>
 238 |       let clampedms = if milliseconds > 25 then cast milliseconds else 25
 239 |         in primIO (prim__channelGetWithTimeout chan clampedms)
 240 |     _         =>
 241 |       primIO (prim__channelGetWithTimeout chan (cast milliseconds))
 242 | 
 243 | ||| Puts a value on the given channel.
 244 | |||
 245 | ||| @ chan the `Channel` to send the value over
 246 | ||| @ val  the value to send
 247 | export
 248 | channelPut : HasIO io => (chan : Channel a) -> (val : a) -> io ()
 249 | channelPut chan val = primIO (prim__channelPut chan val)
 250 |