[ base ] Add atomically function (idris-lang#3380)

* 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 <[email protected]>

* 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 <[email protected]>

CHANGELOG_NEXT.md

@@ -217,6 +217,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 * Added implementations of `Foldable` and `Traversable` for `Control.Monad.Identity`
 
+* Added `Data.IORef.atomically` for the chez backend.
+
 #### Contrib
 
 * `Data.List.Lazy` was moved from `contrib` to `base`.

libs/base/Data/IORef.idr

@@ -1,5 +1,8 @@
 module Data.IORef
 
+import System.Concurrency
+import System.Info
+
 %default total
 
 -- Implemented externally
@@ -14,29 +17,50 @@ export
 data IORef : Type -> Type where
      MkRef : Mut a -> IORef a
 
+||| Create a new IORef.
 export
 newIORef : HasIO io => a -> io (IORef a)
 newIORef val
     = do m <- primIO (prim__newIORef val)
          pure (MkRef m)
 
+||| Read the value of an IORef.
 %inline
 export
 readIORef : HasIO io => IORef a -> io a
 readIORef (MkRef m) = primIO (prim__readIORef m)
 
+||| Write a new value into an IORef.
+||| This function does not create a memory barrier and can be reordered with other independent reads and writes within a thread,
+||| which may cause issues for multithreaded execution.
 %inline
 export
 writeIORef : HasIO io => IORef a -> (val : a) -> io ()
 writeIORef (MkRef m) val = primIO (prim__writeIORef m val)
 
+||| Write a new value into an IORef.
+||| This function does not create a memory barrier and can be reordered with other independent reads and writes within a thread,
+||| which may cause issues for multithreaded execution.
 %inline
 export
 writeIORef1 : HasLinearIO io => IORef a -> (1 val : a) -> io ()
 writeIORef1 (MkRef m) val = primIO1 (prim__writeIORef m val)
 
+||| Mutate the contents of an IORef, combining readIORef and writeIORef.
+||| This is not an atomic update, consider using atomically when operating in a multithreaded environment.
 export
 modifyIORef : HasIO io => IORef a -> (a -> a) -> io ()
 modifyIORef ref f
     = do val <- readIORef ref
          writeIORef ref (f val)
+
+||| This function atomically runs its argument according to the provided mutex.
+||| It can for instance be used to modify the contents of an IORef `ref` with a function `f`
+||| in a safe way in a multithreaded program by using `atomically lock (modifyIORef ref f)`
+||| provided that other threads also rely on the same `lock` to modify `ref`.
+export
+atomically : HasIO io => Mutex -> io () -> io ()
+atomically lock act
+    = do mutexAcquire lock
+         act
+         mutexRelease lock

tests/chez/chez003/IORef.idr

@@ -1,4 +1,20 @@
 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
@@ -14,3 +30,13 @@ main
          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

tests/chez/chez003/expected

@@ -2,3 +2,5 @@
 94
 188
 188
+0
+1010000