{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RecordWildCards #-}

-- |
-- Module      : Test.DejaFu.Conc.Internal.Memory
-- Copyright   : (c) 2016--2019 Michael Walker
-- License     : MIT
-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
-- Stability   : experimental
-- Portability : BangPatterns, GADTs, FlexibleContexts, LambdaCase, RecordWildCards
--
-- Operations over @IORef@s and @MVar@s. This module is NOT considered
-- to form part of the public interface of this library.
--
-- Relaxed memory operations over @IORef@s are implemented with an
-- explicit write buffer: one per thread for TSO, and one per
-- thread/variable combination for PSO. Unsynchronised writes append
-- to this buffer, and periodically separate threads commit from these
-- buffers to the \"actual\" @IORef@.
--
-- This model comes from /Dynamic Partial Order Reduction for Relaxed
-- Memory Models/, N. Zhang, M. Kusano, and C. Wang (2015).
module Test.DejaFu.Conc.Internal.Memory where

import           Data.Map.Strict                     (Map)
import qualified Data.Map.Strict                     as M
import           Data.Maybe                          (maybeToList)
import           Data.Monoid                         ((<>))
import           Data.Sequence                       (Seq, ViewL(..), singleton,
                                                      viewl, (><))
import           GHC.Stack                           (HasCallStack)

import           Test.DejaFu.Conc.Internal.Common
import           Test.DejaFu.Conc.Internal.Threading
import           Test.DejaFu.Internal
import           Test.DejaFu.Types

--------------------------------------------------------------------------------
-- * Manipulating @IORef@s

-- | In non-sequentially-consistent memory models, non-synchronised
-- writes get buffered.
--
-- The @IORefId@ parameter is only used under PSO. Under TSO each
-- thread has a single buffer.
newtype WriteBuffer n = WriteBuffer
  { forall (n :: * -> *).
WriteBuffer n
-> Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
buffer :: Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n)) }

-- | A buffered write is a reference to the variable, and the value to
-- write. Universally quantified over the value type so that the only
-- thing which can be done with it is to write it to the reference.
data BufferedWrite n where
  BufferedWrite :: ThreadId -> ModelIORef n a -> a -> BufferedWrite n

-- | An empty write buffer.
emptyBuffer :: WriteBuffer n
emptyBuffer :: forall (n :: * -> *). WriteBuffer n
emptyBuffer = forall (n :: * -> *).
Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
-> WriteBuffer n
WriteBuffer forall k a. Map k a
M.empty

-- | Add a new write to the end of a buffer.
bufferWrite :: MonadDejaFu n => WriteBuffer n -> (ThreadId, Maybe IORefId) -> ModelIORef n a -> a -> n (WriteBuffer n)
bufferWrite :: forall (n :: * -> *) a.
MonadDejaFu n =>
WriteBuffer n
-> (ThreadId, Maybe IORefId)
-> ModelIORef n a
-> a
-> n (WriteBuffer n)
bufferWrite (WriteBuffer Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
wb) k :: (ThreadId, Maybe IORefId)
k@(ThreadId
tid, Maybe IORefId
_) ref :: ModelIORef n a
ref@ModelIORef{IORefId
Ref n (Map ThreadId a, Integer, a)
iorefRef :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
iorefRef :: Ref n (Map ThreadId a, Integer, a)
iorefId :: IORefId
..} a
new = do
  -- Construct the new write buffer
  let write :: Seq (BufferedWrite n)
write = forall a. a -> Seq a
singleton forall a b. (a -> b) -> a -> b
$ forall (n :: * -> *) a.
ThreadId -> ModelIORef n a -> a -> BufferedWrite n
BufferedWrite ThreadId
tid ModelIORef n a
ref a
new
  let buffer' :: Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
buffer' = forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Seq a -> Seq a -> Seq a
(><)) (ThreadId, Maybe IORefId)
k Seq (BufferedWrite n)
write Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
wb

  -- Write the thread-local value to the @IORef@'s update map.
  (Map ThreadId a
locals, Integer
count, a
def) <- forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n (Map ThreadId a, Integer, a)
iorefRef
  forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n (Map ThreadId a, Integer, a)
iorefRef (forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert ThreadId
tid a
new Map ThreadId a
locals, Integer
count, a
def)

  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (n :: * -> *).
Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
-> WriteBuffer n
WriteBuffer Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
buffer')

-- | Commit the write at the head of a buffer.
commitWrite :: MonadDejaFu n => WriteBuffer n -> (ThreadId, Maybe IORefId) -> n (WriteBuffer n)
commitWrite :: forall (n :: * -> *).
MonadDejaFu n =>
WriteBuffer n -> (ThreadId, Maybe IORefId) -> n (WriteBuffer n)
commitWrite w :: WriteBuffer n
w@(WriteBuffer Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
wb) (ThreadId, Maybe IORefId)
k = case forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. ViewL a
EmptyL forall a. Seq a -> ViewL a
viewl forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (ThreadId, Maybe IORefId)
k Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
wb of
  BufferedWrite ThreadId
_ ModelIORef n a
ref a
a :< Seq (BufferedWrite n)
rest -> do
    n ()
_ <- forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> a -> n (n ())
writeImmediate ModelIORef n a
ref a
a
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: * -> *).
Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
-> WriteBuffer n
WriteBuffer forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (ThreadId, Maybe IORefId)
k Seq (BufferedWrite n)
rest Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
wb
  ViewL (BufferedWrite n)
EmptyL -> forall (f :: * -> *) a. Applicative f => a -> f a
pure WriteBuffer n
w

-- | Read from a @IORef@, returning a newer thread-local non-committed
-- write if there is one.
readIORef :: MonadDejaFu n => ModelIORef n a -> ThreadId -> n a
readIORef :: forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> ThreadId -> n a
readIORef ModelIORef n a
ref ThreadId
tid = do
  (a
val, Integer
_) <- forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> ThreadId -> n (a, Integer)
readIORefPrim ModelIORef n a
ref ThreadId
tid
  forall (f :: * -> *) a. Applicative f => a -> f a
pure a
val

-- | Read from a @IORef@, returning a @Ticket@ representing the current
-- view of the thread.
readForTicket :: MonadDejaFu n => ModelIORef n a -> ThreadId -> n (ModelTicket a)
readForTicket :: forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> ThreadId -> n (ModelTicket a)
readForTicket ref :: ModelIORef n a
ref@ModelIORef{IORefId
Ref n (Map ThreadId a, Integer, a)
iorefRef :: Ref n (Map ThreadId a, Integer, a)
iorefId :: IORefId
iorefRef :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
..} ThreadId
tid = do
  (a
val, Integer
count) <- forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> ThreadId -> n (a, Integer)
readIORefPrim ModelIORef n a
ref ThreadId
tid
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. IORefId -> Integer -> a -> ModelTicket a
ModelTicket IORefId
iorefId Integer
count a
val)

-- | Perform a compare-and-swap on a @IORef@ if the ticket is still
-- valid. This is strict in the \"new\" value argument.
casIORef :: MonadDejaFu n => ModelIORef n a -> ThreadId -> ModelTicket a -> a -> n (Bool, ModelTicket a, n ())
casIORef :: forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a
-> ThreadId -> ModelTicket a -> a -> n (Bool, ModelTicket a, n ())
casIORef ModelIORef n a
ref ThreadId
tid (ModelTicket IORefId
_ Integer
cc a
_) !a
new = do
  tick' :: ModelTicket a
tick'@(ModelTicket IORefId
_ Integer
cc' a
_) <- forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> ThreadId -> n (ModelTicket a)
readForTicket ModelIORef n a
ref ThreadId
tid

  if Integer
cc forall a. Eq a => a -> a -> Bool
== Integer
cc'
  then do
    n ()
effect <- forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> a -> n (n ())
writeImmediate ModelIORef n a
ref a
new
    ModelTicket a
tick'' <- forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> ThreadId -> n (ModelTicket a)
readForTicket ModelIORef n a
ref ThreadId
tid
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
True, ModelTicket a
tick'', n ()
effect)
  else forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
False, ModelTicket a
tick', forall (f :: * -> *) a. Applicative f => a -> f a
pure ())

-- | Read the local state of a @IORef@.
readIORefPrim :: MonadDejaFu n => ModelIORef n a -> ThreadId -> n (a, Integer)
readIORefPrim :: forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> ThreadId -> n (a, Integer)
readIORefPrim ModelIORef{IORefId
Ref n (Map ThreadId a, Integer, a)
iorefRef :: Ref n (Map ThreadId a, Integer, a)
iorefId :: IORefId
iorefRef :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
..} ThreadId
tid = do
  (Map ThreadId a
vals, Integer
count, a
def) <- forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n (Map ThreadId a, Integer, a)
iorefRef
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k a. Ord k => a -> k -> Map k a -> a
M.findWithDefault a
def ThreadId
tid Map ThreadId a
vals, Integer
count)

-- | Read the global state of a @IORef@.
readIORefGlobal :: MonadDejaFu n => ModelIORef n a -> n a
readIORefGlobal :: forall (n :: * -> *) a. MonadDejaFu n => ModelIORef n a -> n a
readIORefGlobal ModelIORef{IORefId
Ref n (Map ThreadId a, Integer, a)
iorefRef :: Ref n (Map ThreadId a, Integer, a)
iorefId :: IORefId
iorefRef :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
..} = do
  (Map ThreadId a
_, Integer
_, a
def) <- forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n (Map ThreadId a, Integer, a)
iorefRef
  forall (f :: * -> *) a. Applicative f => a -> f a
pure a
def

-- | Write and commit to a @IORef@ immediately, clearing the update map
-- and incrementing the write count.
writeImmediate :: MonadDejaFu n => ModelIORef n a -> a -> n (n ())
writeImmediate :: forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> a -> n (n ())
writeImmediate ModelIORef{IORefId
Ref n (Map ThreadId a, Integer, a)
iorefRef :: Ref n (Map ThreadId a, Integer, a)
iorefId :: IORefId
iorefRef :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
..} a
a = do
  (Map ThreadId a
_, Integer
count, a
_) <- forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n (Map ThreadId a, Integer, a)
iorefRef
  let effect :: n ()
effect = forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n (Map ThreadId a, Integer, a)
iorefRef (forall k a. Map k a
M.empty, Integer
count forall a. Num a => a -> a -> a
+ Integer
1, a
a)
  n ()
effect
  forall (f :: * -> *) a. Applicative f => a -> f a
pure n ()
effect

-- | Flush all writes in the buffer.
writeBarrier :: MonadDejaFu n => WriteBuffer n -> n ()
writeBarrier :: forall (n :: * -> *). MonadDejaFu n => WriteBuffer n -> n ()
writeBarrier (WriteBuffer Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
wb) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Seq (BufferedWrite n) -> n ()
flush forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
M.elems Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
wb where
  flush :: Seq (BufferedWrite n) -> n ()
flush = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall a b. (a -> b) -> a -> b
$ \(BufferedWrite ThreadId
_ ModelIORef n a
ref a
a) -> forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> a -> n (n ())
writeImmediate ModelIORef n a
ref a
a

-- | Add phantom threads to the thread list to commit pending writes.
addCommitThreads :: WriteBuffer n -> Threads n -> Threads n
addCommitThreads :: forall (n :: * -> *). WriteBuffer n -> Threads n -> Threads n
addCommitThreads (WriteBuffer Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
wb) Threads n
ts = Threads n
ts forall a. Semigroup a => a -> a -> a
<> forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(ThreadId, Thread n)]
phantoms where
  phantoms :: [(ThreadId, Thread n)]
phantoms = [ (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ThreadId -> Maybe IORefId -> ThreadId
commitThreadId (ThreadId, Maybe IORefId)
k, forall (n :: * -> *). Action n -> Thread n
mkthread Action n
c)
             | ((ThreadId, Maybe IORefId)
k, Seq (BufferedWrite n)
b) <- forall k a. Map k a -> [(k, a)]
M.toList Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
wb
             , Action n
c <- forall a. Maybe a -> [a]
maybeToList (forall {n :: * -> *} {n :: * -> *}.
ViewL (BufferedWrite n) -> Maybe (Action n)
go forall a b. (a -> b) -> a -> b
$ forall a. Seq a -> ViewL a
viewl Seq (BufferedWrite n)
b)
             ]
  go :: ViewL (BufferedWrite n) -> Maybe (Action n)
go (BufferedWrite ThreadId
tid ModelIORef{IORefId
Ref n (Map ThreadId a, Integer, a)
iorefRef :: Ref n (Map ThreadId a, Integer, a)
iorefId :: IORefId
iorefRef :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
..} a
_ :< Seq (BufferedWrite n)
_) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (n :: * -> *). ThreadId -> IORefId -> Action n
ACommit ThreadId
tid IORefId
iorefId
  go ViewL (BufferedWrite n)
EmptyL = forall a. Maybe a
Nothing

-- | The ID of a commit thread.
commitThreadId :: ThreadId -> Maybe IORefId -> ThreadId
commitThreadId :: ThreadId -> Maybe IORefId -> ThreadId
commitThreadId (ThreadId (Id Maybe String
_ Int
t)) = Id -> ThreadId
ThreadId forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe String -> Int -> Id
Id forall a. Maybe a
Nothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => a -> a
negate forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe IORefId -> Int
go where
  go :: Maybe IORefId -> Int
go (Just (IORefId (Id Maybe String
_ Int
c))) = Int
t forall a. Num a => a -> a -> a
+ Int
1 forall a. Num a => a -> a -> a
+ Int
c forall a. Num a => a -> a -> a
* Int
10000
  go Maybe IORefId
Nothing = Int
t forall a. Num a => a -> a -> a
+ Int
1

-- | Remove phantom threads.
delCommitThreads :: Threads n -> Threads n
delCommitThreads :: forall (n :: * -> *). Threads n -> Threads n
delCommitThreads = forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey forall a b. (a -> b) -> a -> b
$ \ThreadId
k Thread n
_ -> ThreadId
k forall a. Ord a => a -> a -> Bool
>= ThreadId
initialThread

--------------------------------------------------------------------------------
-- * Manipulating @MVar@s

-- these are a bit clearer than a Bool
data Blocking = Blocking | NonBlocking
data Emptying = Emptying | NonEmptying

-- | Put into a @MVar@, blocking if full.
putIntoMVar :: MonadDejaFu n
  => ModelMVar n a
  -> a
  -> Action n
  -> ThreadId
  -> Threads n
  -> n (Bool, Threads n, [ThreadId], n ())
putIntoMVar :: forall (n :: * -> *) a.
MonadDejaFu n =>
ModelMVar n a
-> a
-> Action n
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
putIntoMVar ModelMVar n a
cvar a
a Action n
c = forall (n :: * -> *) a.
MonadDejaFu n =>
Blocking
-> ModelMVar n a
-> a
-> (Bool -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
mutMVar Blocking
Blocking ModelMVar n a
cvar a
a (forall a b. a -> b -> a
const Action n
c)

-- | Try to put into a @MVar@, not blocking if full.
tryPutIntoMVar :: MonadDejaFu n
  => ModelMVar n a
  -> a
  -> (Bool -> Action n)
  -> ThreadId
  -> Threads n
  -> n (Bool, Threads n, [ThreadId], n ())
tryPutIntoMVar :: forall (n :: * -> *) a.
MonadDejaFu n =>
ModelMVar n a
-> a
-> (Bool -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
tryPutIntoMVar = forall (n :: * -> *) a.
MonadDejaFu n =>
Blocking
-> ModelMVar n a
-> a
-> (Bool -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
mutMVar Blocking
NonBlocking

-- | Read from a @MVar@, blocking if empty.
readFromMVar :: (MonadDejaFu n, HasCallStack)
  => ModelMVar n a
  -> (a -> Action n)
  -> ThreadId
  -> Threads n
  -> n (Bool, Threads n, [ThreadId], n ())
readFromMVar :: forall (n :: * -> *) a.
(MonadDejaFu n, HasCallStack) =>
ModelMVar n a
-> (a -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
readFromMVar ModelMVar n a
cvar a -> Action n
c = forall (n :: * -> *) a.
MonadDejaFu n =>
Emptying
-> Blocking
-> ModelMVar n a
-> (Maybe a -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
seeMVar Emptying
NonEmptying Blocking
Blocking ModelMVar n a
cvar (a -> Action n
c forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasCallStack => Maybe a -> a
efromJust)

-- | Try to read from a @MVar@, not blocking if empty.
tryReadFromMVar :: MonadDejaFu n
  => ModelMVar n a
  -> (Maybe a -> Action n)
  -> ThreadId
  -> Threads n
  -> n (Bool, Threads n, [ThreadId], n ())
tryReadFromMVar :: forall (n :: * -> *) a.
MonadDejaFu n =>
ModelMVar n a
-> (Maybe a -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
tryReadFromMVar = forall (n :: * -> *) a.
MonadDejaFu n =>
Emptying
-> Blocking
-> ModelMVar n a
-> (Maybe a -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
seeMVar Emptying
NonEmptying Blocking
NonBlocking

-- | Take from a @MVar@, blocking if empty.
takeFromMVar :: (MonadDejaFu n, HasCallStack)
  => ModelMVar n a
  -> (a -> Action n)
  -> ThreadId
  -> Threads n
  -> n (Bool, Threads n, [ThreadId], n ())
takeFromMVar :: forall (n :: * -> *) a.
(MonadDejaFu n, HasCallStack) =>
ModelMVar n a
-> (a -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
takeFromMVar ModelMVar n a
cvar a -> Action n
c = forall (n :: * -> *) a.
MonadDejaFu n =>
Emptying
-> Blocking
-> ModelMVar n a
-> (Maybe a -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
seeMVar Emptying
Emptying Blocking
Blocking ModelMVar n a
cvar (a -> Action n
c forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasCallStack => Maybe a -> a
efromJust)

-- | Try to take from a @MVar@, not blocking if empty.
tryTakeFromMVar :: MonadDejaFu n
  => ModelMVar n a
  -> (Maybe a -> Action n)
  -> ThreadId
  -> Threads n
  -> n (Bool, Threads n, [ThreadId], n ())
tryTakeFromMVar :: forall (n :: * -> *) a.
MonadDejaFu n =>
ModelMVar n a
-> (Maybe a -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
tryTakeFromMVar = forall (n :: * -> *) a.
MonadDejaFu n =>
Emptying
-> Blocking
-> ModelMVar n a
-> (Maybe a -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
seeMVar Emptying
Emptying Blocking
NonBlocking

-- | Mutate a @MVar@, in either a blocking or nonblocking way.
mutMVar :: MonadDejaFu n
  => Blocking
  -> ModelMVar n a
  -> a
  -> (Bool -> Action n)
  -> ThreadId
  -> Threads n
  -> n (Bool, Threads n, [ThreadId], n ())
mutMVar :: forall (n :: * -> *) a.
MonadDejaFu n =>
Blocking
-> ModelMVar n a
-> a
-> (Bool -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
mutMVar Blocking
blocking ModelMVar{MVarId
Ref n (Maybe a)
mvarRef :: forall (n :: * -> *) a. ModelMVar n a -> Ref n (Maybe a)
mvarId :: forall (n :: * -> *) a. ModelMVar n a -> MVarId
mvarRef :: Ref n (Maybe a)
mvarId :: MVarId
..} a
a Bool -> Action n
c ThreadId
threadid Threads n
threads = forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n (Maybe a)
mvarRef forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Just a
_ -> case Blocking
blocking of
    Blocking
Blocking ->
      let threads' :: Threads n
threads' = forall (n :: * -> *).
HasCallStack =>
BlockedOn -> ThreadId -> Threads n -> Threads n
block (MVarId -> BlockedOn
OnMVarEmpty MVarId
mvarId) ThreadId
threadid Threads n
threads
      in forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
False, Threads n
threads', [], forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
    Blocking
NonBlocking ->
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
False, forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto (Bool -> Action n
c Bool
False) ThreadId
threadid Threads n
threads, [], forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
  Maybe a
Nothing -> do
    let effect :: n ()
effect = forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n (Maybe a)
mvarRef forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just a
a
    let (Threads n
threads', [ThreadId]
woken) = forall (n :: * -> *).
BlockedOn -> Threads n -> (Threads n, [ThreadId])
wake (MVarId -> BlockedOn
OnMVarFull MVarId
mvarId) Threads n
threads
    n ()
effect
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
True, forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto (Bool -> Action n
c Bool
True) ThreadId
threadid Threads n
threads', [ThreadId]
woken, n ()
effect)

-- | Read a @MVar@, in either a blocking or nonblocking
-- way.
seeMVar :: MonadDejaFu n
  => Emptying
  -> Blocking
  -> ModelMVar n a
  -> (Maybe a -> Action n)
  -> ThreadId
  -> Threads n
  -> n (Bool, Threads n, [ThreadId], n ())
seeMVar :: forall (n :: * -> *) a.
MonadDejaFu n =>
Emptying
-> Blocking
-> ModelMVar n a
-> (Maybe a -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
seeMVar Emptying
emptying Blocking
blocking ModelMVar{MVarId
Ref n (Maybe a)
mvarRef :: Ref n (Maybe a)
mvarId :: MVarId
mvarRef :: forall (n :: * -> *) a. ModelMVar n a -> Ref n (Maybe a)
mvarId :: forall (n :: * -> *) a. ModelMVar n a -> MVarId
..} Maybe a -> Action n
c ThreadId
threadid Threads n
threads = forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n (Maybe a)
mvarRef forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  val :: Maybe a
val@(Just a
_) -> do
    let effect :: n ()
effect = case Emptying
emptying of
          Emptying
Emptying -> forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n (Maybe a)
mvarRef forall a. Maybe a
Nothing
          Emptying
NonEmptying -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    let (Threads n
threads', [ThreadId]
woken) = forall (n :: * -> *).
BlockedOn -> Threads n -> (Threads n, [ThreadId])
wake (MVarId -> BlockedOn
OnMVarEmpty MVarId
mvarId) Threads n
threads
    n ()
effect
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
True, forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto (Maybe a -> Action n
c Maybe a
val) ThreadId
threadid Threads n
threads', [ThreadId]
woken, n ()
effect)
  Maybe a
Nothing -> case Blocking
blocking of
    Blocking
Blocking ->
      let threads' :: Threads n
threads' = forall (n :: * -> *).
HasCallStack =>
BlockedOn -> ThreadId -> Threads n -> Threads n
block (MVarId -> BlockedOn
OnMVarFull MVarId
mvarId) ThreadId
threadid Threads n
threads
      in forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
False, Threads n
threads', [], forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
    Blocking
NonBlocking ->
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
False, forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto (Maybe a -> Action n
c forall a. Maybe a
Nothing) ThreadId
threadid Threads n
threads, [], forall (f :: * -> *) a. Applicative f => a -> f a
pure ())