Idris-dev icon indicating copy to clipboard operation
Idris-dev copied to clipboard

IORef shared between multiple threads doesn't work

Open redfish64 opened this issue 7 years ago • 1 comments

I am trying to share writeable memory between threads in idris, and I can't seem to do so. Is this possible?

The following results in an error: idris20022-6: idris_rts.c:967: doCopyTo: Assertion `0' failed.

module Threads

--this doesn't work, because the waitAndRead thread can't read the ioref

import System.Concurrency.Channels
import System
import Data.IORef

waitAndRead : IORef Int -> IO ()
waitAndRead x = do
  usleep $ 500*1000
  v <- readIORef x
  putStrLn $ "V is " ++ show v



main : IO ()
main =
  do 
    x <- newIORef 0
    mpid <- spawn (waitAndRead x)
    usleep $ 100 * 1000
    case mpid of
      Just mpid => writeIORef x 1
      Nothing => putStrLn "Can't spawn!"
    usleep $ 1000 * 1000
    putStrLn "Done!"


Steps to Reproduce

Run :exec main in idris repl

Expected Behavior

V is 1 Done!

Observed Behavior

idris20022-6: idris_rts.c:967: doCopyTo: Assertion `0' failed.

redfish64 avatar May 22 '18 21:05 redfish64

Still failing with v 1.3.2 of idris with:

idris_rts.c:905: doCopyTo: Assertion `0' failed. Aborted (core dumped)

redfish64 avatar Nov 07 '19 08:11 redfish64