Semantics of MVars and IORefs?

Hello, recently, I and a few colleagues have been wondering about the interaction between IORefs and MVars, and we can't seem to find any explicit documentation stating the behavior, so I was wondering if anyone might know the answer. The question is: is it safe to use IORefs in a multi-threaded program, provided that the uses are within a "critical section" implemented with MVars. Here is a simple program to illustrate the situation: we have two threads, each thread takes a lock, increments a counter, then releases the lock:
import Control.Concurrent import Data.IORef
main :: IO () main = do lock <- newMVar () counter <- newIORef 0 forkIO (thread lock counter) thread lock counter
thread :: MVar () -> IORef Integer -> IO a thread lock counter = do takeMVar lock value <- readIORef counter print value writeIORef counter (value + 1) putMVar lock () thread lock counter
The question is if this program has a race condition or not, due to the use of IORefs? More explicitly, the concern is if a write to an IORef in one thread is guaranteed to be seen by a read from the same IORef in another thread, provided that there is proper synchronization between the two. -Iavor

Hi Iavor,
You might be interested in what Edward has written about this:
http://blog.ezyang.com/2014/01/so-you-want-to-add-a-new-concurrency-primitiv...
I would say when we do have a memory model for GHC the program you gave
will almost certainly be correct. MVar operations should be full
synchronization operations. There are some bugs on relaxed systems with
initialization that I think are being addressed. I can't find the tickets
at the moment.
Ryan
On Fri, Oct 21, 2016 at 1:19 PM, Iavor Diatchki
Hello,
recently, I and a few colleagues have been wondering about the interaction between IORefs and MVars, and we can't seem to find any explicit documentation stating the behavior, so I was wondering if anyone might know the answer.
The question is: is it safe to use IORefs in a multi-threaded program, provided that the uses are within a "critical section" implemented with MVars. Here is a simple program to illustrate the situation: we have two threads, each thread takes a lock, increments a counter, then releases the lock:
import Control.Concurrent import Data.IORef
main :: IO () main = do lock <- newMVar () counter <- newIORef 0 forkIO (thread lock counter) thread lock counter
thread :: MVar () -> IORef Integer -> IO a thread lock counter = do takeMVar lock value <- readIORef counter print value writeIORef counter (value + 1) putMVar lock () thread lock counter
The question is if this program has a race condition or not, due to the use of IORefs? More explicitly, the concern is if a write to an IORef in one thread is guaranteed to be seen by a read from the same IORef in another thread, provided that there is proper synchronization between the two.
-Iavor
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Hi Iavor and Ryan, One ticket on memory model issues is #12469. At openSUSE we see several build failures only now because we recently switched to parallel Cabal builds. A compiled Cabal Setup that is called with -j<n> sometimes segfaults on PowerPC. Actually, if I try building package OpenGL locally on my PowerMac Setup -j<n> almost always fails with a segfault if n is the number of cores or higher. See also #12537. When building on Open(SUSE) Build Service the build fails only sometimes. We build all of LTS Haskell and a random selection of around 40 packages fail, most of them with segfaults in Setup but some with GHC panics. #12469 has examples. Peter
On 21.10.2016, at 19:56, Ryan Yates
wrote: Hi Iavor,
You might be interested in what Edward has written about this:
http://blog.ezyang.com/2014/01/so-you-want-to-add-a-new-concurrency-primitiv...
I would say when we do have a memory model for GHC the program you gave will almost certainly be correct. MVar operations should be full synchronization operations. There are some bugs on relaxed systems with initialization that I think are being addressed. I can't find the tickets at the moment.
Ryan
participants (3)
-
Iavor Diatchki
-
Peter Trommler
-
Ryan Yates