Idris线程间共享可写内存失败：是否支持该操作？

首先直接给你答案：Idris的IORef并不支持跨线程共享访问，这就是你运行代码时触发idris_rts.c:967: doCopyTo: Assertion 0' failed`错误的原因。

为什么你的代码会崩溃？ #

你在主线程创建了IORef x，然后把它传递给通过spawn启动的子线程，接着主线程修改这个IORef，子线程尝试读取它。但Idris的IORef内存管理模型从设计上就假设它只会在单个线程内被访问，跨线程的直接读写会破坏运行时的内存安全约束，最终触发底层的断言失败。

那怎么在Idris线程间安全共享可变状态？ #

Idris标准库推荐使用**通道（Channels）**来做线程间的通信和状态同步。如果确实需要共享可变状态，最佳实践是用一个专门的线程来持有IORef，其他线程通过通道发送"命令"来请求修改或读取状态——这样就保证了IORef始终只在单个线程内被访问，从根源上避免了线程安全问题。

下面是两种可行的实现方案：

方案1：直接用通道传递更新后的值

如果你的场景只是需要把更新后的值传递给子线程，直接用通道就足够了：

module Threads

import System.Concurrency.Channels
import System

waitAndRead : Channel Int -> IO ()
waitAndRead chan = do
  usleep $ 500*1000
  -- 从通道接收主线程更新后的值
  Just v <- readChannel chan
    | Nothing => putStrLn "Channel closed unexpectedly"
  putStrLn $ "V is " ++ show v

main : IO ()
main = do
  chan <- newChannel
  mpid <- spawn (waitAndRead chan)
  usleep $ 100 * 1000
  case mpid of
    Just _ => writeChannel chan 1
    Nothing => putStrLn "Failed to spawn thread!"
  usleep $ 1000 * 1000
  putStrLn "Done!"

方案2：用"状态管理线程"共享可变状态

如果需要更复杂的共享状态操作（比如多次读写、多线程交互），可以创建一个专门的线程来管理IORef，其他线程通过通道发送请求：

module Threads

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

-- 定义状态操作的消息类型：要么读取状态，要么更新状态
data StateCmd = ReadState (Channel Int) | UpdateState Int

-- 状态管理线程：独自持有IORef，处理来自通道的命令
stateManager : IORef Int -> Channel StateCmd -> IO ()
stateManager ref cmdChan = do
  Just cmd <- readChannel cmdChan
    | Nothing => putStrLn "State manager shutting down"
  case cmd of
    ReadState replyChan => do
      currentVal <- readIORef ref
      writeChannel replyChan currentVal
      stateManager ref cmdChan  -- 继续处理下一个命令
    UpdateState newVal => do
      writeIORef ref newVal
      stateManager ref cmdChan

waitAndRead : Channel StateCmd -> IO ()
waitAndRead cmdChan = do
  usleep $ 500*1000
  -- 创建回复通道，用于接收状态值
  replyChan <- newChannel
  -- 发送读取状态的请求
  writeChannel cmdChan (ReadState replyChan)
  -- 等待回复
  Just v <- readChannel replyChan
    | Nothing => putStrLn "Failed to receive state"
  putStrLn $ "V is " ++ show v

main : IO ()
main = do
  initialRef <- newIORef 0
  cmdChan <- newChannel
  -- 启动状态管理线程
  _ <- spawn (stateManager initialRef cmdChan)
  -- 启动读取线程
  mpid <- spawn (waitAndRead cmdChan)
  usleep $ 100 * 1000
  case mpid of
    Just _ => writeChannel cmdChan (UpdateState 1)
    Nothing => putStrLn "Failed to spawn thread!"
  usleep $ 1000 * 1000
  putStrLn "Done!"

总结 #

Idris不支持直接跨线程共享IORef，因为它的运行时没有为IORef提供线程安全的访问机制。要在线程间安全处理可变状态，必须借助通道这类并发原语，通过消息传递的方式来同步状态操作。

内容的提问来源于stack exchange，提问作者redfish64