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