idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #358 from edwinb/concurrency-fix

Browse Source 
Small concurrency fixes
This commit is contained in:
Edwin Brady 2020-06-23 19:30:56 +01:00 committed by GitHub
commit a7d5a9a7fd
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 8 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
libs/base/System/Concurrency/Raw.idr
View File

@ -55,7 +55,7 @@ data Condition : Type where [external]
prim__makeCondition : PrimIO Condition
%foreign "scheme:blodwen-condition-wait"
prim__conditionWait : Condition -> Mutex -> PrimIO ()
%foreign "scheme:blodwen-condition-wait-timoue"
%foreign "scheme:blodwen-condition-wait-timeout"
prim__conditionWaitTimeout : Condition -> Mutex -> Int -> PrimIO ()
%foreign "scheme:blodwen-condition-signal"
prim__conditionSignal : Condition -> PrimIO ()
@ -70,6 +70,7 @@ export
conditionWait : Condition -> Mutex -> IO ()
conditionWait c m = primIO (prim__conditionWait c m)
||| Timeout is in microseconds
export
conditionWaitTimeout : Condition -> Mutex -> Int -> IO ()
conditionWaitTimeout c m t = primIO (prim__conditionWaitTimeout c m t)

2
libs/prelude/PrimIO.idr
View File

@ -108,7 +108,7 @@ unsafeDestroyWorld : (1 x : %World) -> a -> a
unsafeDestroyWorld %MkWorld x = x
export
unsafePerformIO : IO a -> a
unsafePerformIO : (1 _ : IO a) -> a
unsafePerformIO (MkIO f)
= unsafeCreateWorld (\w => case f w of
MkIORes res w' => unsafeDestroyWorld w' res)

5
support/chez/support.ss
View File

@ -183,7 +183,10 @@
(define (blodwen-condition) (make-condition))
(define (blodwen-condition-wait c m) (condition-wait c m))
(define (blodwen-condition-wait-timeout c m t) (condition-wait c m t))
(define (blodwen-condition-wait-timeout c m t)
(let ((sec (div t 1000000))
(micro (mod t 1000000)))
(condition-wait c m (make-time 'time-duration (* 1000 micro) sec))))
(define (blodwen-condition-signal c) (condition-signal c))
(define (blodwen-condition-broadcast c) (condition-broadcast c))

2
support/racket/support.rkt
View File

@ -180,7 +180,7 @@
(blodwen-lock m))
(define (blodwen-condition-wait-timeout c m t)
(blodwen-unlock m) ;; consistency with interface for posix condition variables
(sync/timeout t c)
(sync/timeout (/ t 1000000) c)
(blodwen-lock m))
(define (blodwen-condition-signal c)
(channel-put c 'ready))