mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-23 22:22:07 +03:00
53f448c0db
* Adding initial implementation of atomicModifyIORef in Data.IORef. * Updating chez003 test (IORefs) to add atomicModifyIORef. * Updating CHANGELOG_NEXT.md. * Fixing linting in libs/base/Data/IORef.idr. * Fixing expected and tests/chez/chez003/IORef.idr to more appropriately test atomicModifyIORef functionality. * Add documentation for libs/base/Data/IORef.idr. * Clean up atomicModifyIORef in libs/base/Data/IORef.idr. * Updating atomicModifyIORef implementation to drop codegen check, let client decide this. Also update test to ensure enough contention to test for true atomicity (thanks to @stefan-hoeck for help with both of these). * Remove documentation regarding backends other than chez. * Update libs/base/Data/IORef.idr Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org> * Updating CHANGELOG_NEXT.md with new function name, atomically, and updating tests/chez/chez003/IORef.idr to reflect new function. * Fix linting for libs/base/Data/IORef.idr. * Update documentation for modifyIORef in libs/base/Data/IORef.idr. --------- Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
43 lines
1.0 KiB
Idris
43 lines
1.0 KiB
Idris
import Data.IORef
|
|
import System.Concurrency
|
|
|
|
slowinc : Nat -> Nat -> Nat
|
|
slowinc 0 j = S j
|
|
slowinc (S k) j = slowinc k j
|
|
|
|
parameters (ref : IORef Nat)
|
|
(lock : Mutex)
|
|
|
|
runFastInc : Nat -> IO ()
|
|
runFastInc 0 = pure ()
|
|
runFastInc (S k) = atomically lock (modifyIORef ref S) >> runFastInc k
|
|
|
|
runSlowInc : Nat -> IO ()
|
|
runSlowInc 0 = pure ()
|
|
runSlowInc (S k) = atomically lock (modifyIORef ref (slowinc 10000)) >> runSlowInc k
|
|
|
|
main : IO ()
|
|
main
|
|
= do x <- newIORef 42
|
|
let y = x
|
|
writeIORef y 94
|
|
val <- readIORef x
|
|
printLn val
|
|
val <- readIORef y
|
|
printLn val
|
|
modifyIORef x (* 2)
|
|
val <- readIORef x
|
|
printLn val
|
|
val <- readIORef y
|
|
printLn val
|
|
lock <- makeMutex
|
|
ref <- newIORef Z
|
|
readIORef ref >>= printLn
|
|
t1 <- fork $
|
|
runFastInc ref lock 1_000_000
|
|
t2 <- fork $
|
|
runSlowInc ref lock 1_0000
|
|
threadWait t1
|
|
threadWait t2
|
|
readIORef ref >>= printLn
|