Haskell memory model

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

Haskell memory model

Li-yao Xia-2
Hello café,

What guarantees are there about shared memory concurrency in Haskell? In
particular, I'm wondering how to correctly and efficiently synchronize
mutable operations from the vector package, using stm or atomic-primops.

- Are reads/writes on vectors sequentially consistent? As a concrete
example, can the following program (a common test for relaxed memory
models) print anything?


import qualified Data.Vector.Mutable as MV
import Control.Concurrent

main :: IO ()
main = do
   v <- MV.replicate 2 0
   t <- newEmptyMVar
   forkIO $ do
     MV.write v 0 1
     x <- MV.read v 1
     putMVar t x
   forkIO $ do
     MV.write v 1 1
     x <- MV.read v 0
     putMVar t x
   a <- takeMVar t
   b <- takeMVar t
   if a == 0 && b == 0 then
     putStrLn "Relaxed!"
   else
     return ()


- Do atomic operations (via stm or atomic-primops) imply some
constraints between vector operations? As another concrete example, can
the snippet linked below ever throw an exception? One thread writes to a
vector, and another reads from it, and they communicate via stm to guess
whether the read value is safe to evaluate (in one test case the first
thread overwrites a defined value with undefined, and in the other case
it overwrites undefined with a defined value).

http://lpaste.net/362596


Regards,
Li-yao
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Haskell memory model

Ben Lippmeier-2

On 5 Mar 2018, at 2:21 am, Li-yao Xia <[hidden email]> wrote:

What guarantees are there about shared memory concurrency in Haskell? In particular, I'm wondering how to correctly and efficiently synchronize mutable operations from the vector package, using stm or atomic-primops.

- Are reads/writes on vectors sequentially consistent? As a concrete example, can the following program (a common test for relaxed memory models) print anything?

Read/Writes for single elements of a vector compile down to single machine instructions, which will be some sort of vanilla MOV on x86. The x86 architecture is free to reorder stores after writes. AIUI this is due to the write buffer [2] which holds writes before they are committed to main memory. The x86 instruction set has an MFENCE operation to force loads and stores to be visible to global memory before others, but this isn’t inserted for read/writes to mutable vectors.



- Do atomic operations (via stm or atomic-primops) imply some constraints between vector operations? 

I think the answer to this is “probably, but only incidentally”. The MFENCE instruction on x86 applies to all deferred load/store actions in the physical thread. If you can cause an MFENCE to be emitted into the instruction stream then this will also cause vector operations to be sequentialised.

See:

Ben.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Haskell memory model

Li-yao Xia-2
Thanks Ben! Your answer and links are very helpful. I'll study them
carefully.

Li-yao

On 03/05/2018 04:24 AM, Ben Lippmeier wrote:

>
>> On 5 Mar 2018, at 2:21 am, Li-yao Xia <[hidden email]
>> <mailto:[hidden email]>> wrote:
>>
>> What guarantees are there about shared memory concurrency in Haskell?
>> In particular, I'm wondering how to correctly and efficiently
>> synchronize mutable operations from the vector package, using stm or
>> atomic-primops.
>>
>> - Are reads/writes on vectors sequentially consistent? As a concrete
>> example, can the following program (a common test for relaxed memory
>> models) print anything?
>
> Read/Writes for single elements of a vector compile down to single
> machine instructions, which will be some sort of vanilla MOV on x86. The
> x86 architecture is free to reorder stores after writes. AIUI this is
> due to the write buffer [2] which holds writes before they are committed
> to main memory. The x86 instruction set has an MFENCE operation to force
> loads and stores to be visible to global memory before others, but this
> isn’t inserted for read/writes to mutable vectors.
>
> [1] https://en.wikipedia.org/wiki/Memory_ordering
> [2] https://en.wikipedia.org/wiki/Write_buffer
>
>
>> - Do atomic operations (via stm or atomic-primops) imply some
>> constraints between vector operations?
>
> I think the answer to this is “probably, but only incidentally”. The
> MFENCE instruction on x86 applies to all deferred load/store actions in
> the physical thread. If you can cause an MFENCE to be emitted into the
> instruction stream then this will also cause vector operations to be
> sequentialised.
>
> See:
> https://stackoverflow.com/questions/21506748/reasoning-about-ioref-operation-reordering-in-concurrent-programs
> http://blog.ezyang.com/2014/01/so-you-want-to-add-a-new-concurrency-primitive-to-ghc/
>
> Ben.
>
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.