{-# 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 = Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
-> WriteBuffer n
forall (n :: * -> *).
Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
-> WriteBuffer n
WriteBuffer Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
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)
iorefId :: IORefId
iorefRef :: 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
..} a
new = do
  -- Construct the new write buffer
  let write :: Seq (BufferedWrite n)
write = BufferedWrite n -> Seq (BufferedWrite n)
forall a. a -> Seq a
singleton (BufferedWrite n -> Seq (BufferedWrite n))
-> BufferedWrite n -> Seq (BufferedWrite n)
forall a b. (a -> b) -> a -> b
$ ThreadId -> ModelIORef n a -> a -> BufferedWrite n
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' = (Seq (BufferedWrite n)
 -> Seq (BufferedWrite n) -> Seq (BufferedWrite n))
-> (ThreadId, Maybe IORefId)
-> Seq (BufferedWrite n)
-> Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
-> Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith ((Seq (BufferedWrite n)
 -> Seq (BufferedWrite n) -> Seq (BufferedWrite n))
-> Seq (BufferedWrite n)
-> Seq (BufferedWrite n)
-> Seq (BufferedWrite n)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Seq (BufferedWrite n)
-> Seq (BufferedWrite n) -> Seq (BufferedWrite n)
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) <- Ref n (Map ThreadId a, Integer, a)
-> n (Map ThreadId a, Integer, a)
forall a. Ref n a -> n a
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n (Map ThreadId a, Integer, a)
iorefRef
  Ref n (Map ThreadId a, Integer, a)
-> (Map ThreadId a, Integer, a) -> n ()
forall a. Ref n a -> a -> n ()
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n (Map ThreadId a, Integer, a)
iorefRef (ThreadId -> a -> Map ThreadId a -> Map ThreadId a
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)

  WriteBuffer n -> n (WriteBuffer n)
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
-> WriteBuffer n
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 ViewL (BufferedWrite n)
-> (Seq (BufferedWrite n) -> ViewL (BufferedWrite n))
-> Maybe (Seq (BufferedWrite n))
-> ViewL (BufferedWrite n)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ViewL (BufferedWrite n)
forall a. ViewL a
EmptyL Seq (BufferedWrite n) -> ViewL (BufferedWrite n)
forall a. Seq a -> ViewL a
viewl (Maybe (Seq (BufferedWrite n)) -> ViewL (BufferedWrite n))
-> Maybe (Seq (BufferedWrite n)) -> ViewL (BufferedWrite n)
forall a b. (a -> b) -> a -> b
$ (ThreadId, Maybe IORefId)
-> Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
-> Maybe (Seq (BufferedWrite n))
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 ()
_ <- ModelIORef n a -> a -> n (n ())
forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> a -> n (n ())
writeImmediate ModelIORef n a
ref a
a
    WriteBuffer n -> n (WriteBuffer n)
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WriteBuffer n -> n (WriteBuffer n))
-> (Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
    -> WriteBuffer n)
-> Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
-> n (WriteBuffer n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
-> WriteBuffer n
forall (n :: * -> *).
Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
-> WriteBuffer n
WriteBuffer (Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
 -> n (WriteBuffer n))
-> Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
-> n (WriteBuffer n)
forall a b. (a -> b) -> a -> b
$ (ThreadId, Maybe IORefId)
-> Seq (BufferedWrite n)
-> Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
-> Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
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 -> WriteBuffer n -> n (WriteBuffer n)
forall a. a -> n a
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
_) <- ModelIORef n a -> ThreadId -> n (a, Integer)
forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> ThreadId -> n (a, Integer)
readIORefPrim ModelIORef n a
ref ThreadId
tid
  a -> n a
forall a. a -> n a
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 :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
iorefId :: IORefId
iorefRef :: Ref n (Map ThreadId a, Integer, a)
..} ThreadId
tid = do
  (a
val, Integer
count) <- ModelIORef n a -> ThreadId -> n (a, Integer)
forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> ThreadId -> n (a, Integer)
readIORefPrim ModelIORef n a
ref ThreadId
tid
  ModelTicket a -> n (ModelTicket a)
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IORefId -> Integer -> a -> ModelTicket a
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
_) <- ModelIORef n a -> ThreadId -> n (ModelTicket a)
forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> ThreadId -> n (ModelTicket a)
readForTicket ModelIORef n a
ref ThreadId
tid

  if Integer
cc Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
cc'
  then do
    n ()
effect <- ModelIORef n a -> a -> n (n ())
forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> a -> n (n ())
writeImmediate ModelIORef n a
ref a
new
    ModelTicket a
tick'' <- ModelIORef n a -> ThreadId -> n (ModelTicket a)
forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> ThreadId -> n (ModelTicket a)
readForTicket ModelIORef n a
ref ThreadId
tid
    (Bool, ModelTicket a, n ()) -> n (Bool, ModelTicket a, n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
True, ModelTicket a
tick'', n ()
effect)
  else (Bool, ModelTicket a, n ()) -> n (Bool, ModelTicket a, n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
False, ModelTicket a
tick', () -> n ()
forall a. a -> n a
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 :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
iorefId :: IORefId
iorefRef :: Ref n (Map ThreadId a, Integer, a)
..} ThreadId
tid = do
  (Map ThreadId a
vals, Integer
count, a
def) <- Ref n (Map ThreadId a, Integer, a)
-> n (Map ThreadId a, Integer, a)
forall a. Ref n a -> n a
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n (Map ThreadId a, Integer, a)
iorefRef
  (a, Integer) -> n (a, Integer)
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> ThreadId -> Map ThreadId a -> a
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 :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
iorefId :: IORefId
iorefRef :: Ref n (Map ThreadId a, Integer, a)
..} = do
  (Map ThreadId a
_, Integer
_, a
def) <- Ref n (Map ThreadId a, Integer, a)
-> n (Map ThreadId a, Integer, a)
forall a. Ref n a -> n a
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n (Map ThreadId a, Integer, a)
iorefRef
  a -> n a
forall a. a -> n a
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 :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
iorefId :: IORefId
iorefRef :: Ref n (Map ThreadId a, Integer, a)
..} a
a = do
  (Map ThreadId a
_, Integer
count, a
_) <- Ref n (Map ThreadId a, Integer, a)
-> n (Map ThreadId a, Integer, a)
forall a. Ref n a -> n a
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n (Map ThreadId a, Integer, a)
iorefRef
  let effect :: n ()
effect = Ref n (Map ThreadId a, Integer, a)
-> (Map ThreadId a, Integer, a) -> n ()
forall a. Ref n a -> a -> n ()
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n (Map ThreadId a, Integer, a)
iorefRef (Map ThreadId a
forall k a. Map k a
M.empty, Integer
count Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1, a
a)
  n ()
effect
  n () -> n (n ())
forall a. a -> n a
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) = (Seq (BufferedWrite n) -> n ()) -> [Seq (BufferedWrite n)] -> n ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Seq (BufferedWrite n) -> n ()
flush ([Seq (BufferedWrite n)] -> n ())
-> [Seq (BufferedWrite n)] -> n ()
forall a b. (a -> b) -> a -> b
$ Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
-> [Seq (BufferedWrite n)]
forall k a. Map k a -> [a]
M.elems Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
wb where
  flush :: Seq (BufferedWrite n) -> n ()
flush = (BufferedWrite n -> n (n ())) -> Seq (BufferedWrite n) -> n ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((BufferedWrite n -> n (n ())) -> Seq (BufferedWrite n) -> n ())
-> (BufferedWrite n -> n (n ())) -> Seq (BufferedWrite n) -> n ()
forall a b. (a -> b) -> a -> b
$ \(BufferedWrite ThreadId
_ ModelIORef n a
ref a
a) -> ModelIORef n a -> a -> n (n ())
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 Threads n -> Threads n -> Threads n
forall a. Semigroup a => a -> a -> a
<> [(ThreadId, Thread n)] -> Threads n
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(ThreadId, Thread n)]
phantoms where
  phantoms :: [(ThreadId, Thread n)]
phantoms = [ ((ThreadId -> Maybe IORefId -> ThreadId)
-> (ThreadId, Maybe IORefId) -> ThreadId
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ThreadId -> Maybe IORefId -> ThreadId
commitThreadId (ThreadId, Maybe IORefId)
k, Action n -> Thread n
forall (n :: * -> *). Action n -> Thread n
mkthread Action n
c)
             | ((ThreadId, Maybe IORefId)
k, Seq (BufferedWrite n)
b) <- Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
-> [((ThreadId, Maybe IORefId), Seq (BufferedWrite n))]
forall k a. Map k a -> [(k, a)]
M.toList Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))
wb
             , Action n
c <- Maybe (Action n) -> [Action n]
forall a. Maybe a -> [a]
maybeToList (ViewL (BufferedWrite n) -> Maybe (Action n)
forall {n :: * -> *} {n :: * -> *}.
ViewL (BufferedWrite n) -> Maybe (Action n)
go (ViewL (BufferedWrite n) -> Maybe (Action n))
-> ViewL (BufferedWrite n) -> Maybe (Action n)
forall a b. (a -> b) -> a -> b
$ Seq (BufferedWrite n) -> ViewL (BufferedWrite n)
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 :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
iorefId :: IORefId
iorefRef :: Ref n (Map ThreadId a, Integer, a)
..} a
_ :< Seq (BufferedWrite n)
_) = Action n -> Maybe (Action n)
forall a. a -> Maybe a
Just (Action n -> Maybe (Action n)) -> Action n -> Maybe (Action n)
forall a b. (a -> b) -> a -> b
$ ThreadId -> IORefId -> Action n
forall (n :: * -> *). ThreadId -> IORefId -> Action n
ACommit ThreadId
tid IORefId
iorefId
  go ViewL (BufferedWrite n)
EmptyL = Maybe (Action n)
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 (Id -> ThreadId)
-> (Maybe IORefId -> Id) -> Maybe IORefId -> ThreadId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe String -> Int -> Id
Id Maybe String
forall a. Maybe a
Nothing (Int -> Id) -> (Maybe IORefId -> Int) -> Maybe IORefId -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a. Num a => a -> a
negate (Int -> Int) -> (Maybe IORefId -> Int) -> Maybe IORefId -> Int
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
10000
  go Maybe IORefId
Nothing = Int
t Int -> Int -> Int
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 = (ThreadId -> Thread n -> Bool)
-> Map ThreadId (Thread n) -> Map ThreadId (Thread n)
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey ((ThreadId -> Thread n -> Bool)
 -> Map ThreadId (Thread n) -> Map ThreadId (Thread n))
-> (ThreadId -> Thread n -> Bool)
-> Map ThreadId (Thread n)
-> Map ThreadId (Thread n)
forall a b. (a -> b) -> a -> b
$ \ThreadId
k Thread n
_ -> ThreadId
k ThreadId -> ThreadId -> Bool
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 = Blocking
-> ModelMVar n a
-> a
-> (Bool -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
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 (Action n -> Bool -> Action n
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 = Blocking
-> ModelMVar n a
-> a
-> (Bool -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
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 = Emptying
-> Blocking
-> ModelMVar n a
-> (Maybe a -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
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 (a -> Action n) -> (Maybe a -> a) -> Maybe a -> Action n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe a -> a
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 = Emptying
-> Blocking
-> ModelMVar n a
-> (Maybe a -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
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 = Emptying
-> Blocking
-> ModelMVar n a
-> (Maybe a -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
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 (a -> Action n) -> (Maybe a -> a) -> Maybe a -> Action n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe a -> a
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 = Emptying
-> Blocking
-> ModelMVar n a
-> (Maybe a -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
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)
mvarId :: MVarId
mvarRef :: Ref n (Maybe a)
mvarRef :: forall (n :: * -> *) a. ModelMVar n a -> Ref n (Maybe a)
mvarId :: forall (n :: * -> *) a. ModelMVar n a -> MVarId
..} a
a Bool -> Action n
c ThreadId
threadid Threads n
threads = Ref n (Maybe a) -> n (Maybe a)
forall a. Ref n a -> n a
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n (Maybe a)
mvarRef n (Maybe a)
-> (Maybe a -> n (Bool, Threads n, [ThreadId], n ()))
-> n (Bool, Threads n, [ThreadId], n ())
forall a b. n a -> (a -> n b) -> n b
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' = BlockedOn -> ThreadId -> Threads n -> Threads n
forall (n :: * -> *).
HasCallStack =>
BlockedOn -> ThreadId -> Threads n -> Threads n
block (MVarId -> BlockedOn
OnMVarEmpty MVarId
mvarId) ThreadId
threadid Threads n
threads
      in (Bool, Threads n, [ThreadId], n ())
-> n (Bool, Threads n, [ThreadId], n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
False, Threads n
threads', [], () -> n ()
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
    Blocking
NonBlocking ->
      (Bool, Threads n, [ThreadId], n ())
-> n (Bool, Threads n, [ThreadId], n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
False, Action n -> ThreadId -> Threads n -> Threads n
forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto (Bool -> Action n
c Bool
False) ThreadId
threadid Threads n
threads, [], () -> n ()
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
  Maybe a
Nothing -> do
    let effect :: n ()
effect = Ref n (Maybe a) -> Maybe a -> n ()
forall a. Ref n a -> a -> n ()
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n (Maybe a)
mvarRef (Maybe a -> n ()) -> Maybe a -> n ()
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just a
a
    let (Threads n
threads', [ThreadId]
woken) = BlockedOn -> Threads n -> (Threads n, [ThreadId])
forall (n :: * -> *).
BlockedOn -> Threads n -> (Threads n, [ThreadId])
wake (MVarId -> BlockedOn
OnMVarFull MVarId
mvarId) Threads n
threads
    n ()
effect
    (Bool, Threads n, [ThreadId], n ())
-> n (Bool, Threads n, [ThreadId], n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
True, Action n -> ThreadId -> Threads n -> Threads n
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 :: forall (n :: * -> *) a. ModelMVar n a -> Ref n (Maybe a)
mvarId :: forall (n :: * -> *) a. ModelMVar n a -> MVarId
mvarId :: MVarId
mvarRef :: Ref n (Maybe a)
..} Maybe a -> Action n
c ThreadId
threadid Threads n
threads = Ref n (Maybe a) -> n (Maybe a)
forall a. Ref n a -> n a
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n (Maybe a)
mvarRef n (Maybe a)
-> (Maybe a -> n (Bool, Threads n, [ThreadId], n ()))
-> n (Bool, Threads n, [ThreadId], n ())
forall a b. n a -> (a -> n b) -> n b
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 -> Ref n (Maybe a) -> Maybe a -> n ()
forall a. Ref n a -> a -> n ()
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n (Maybe a)
mvarRef Maybe a
forall a. Maybe a
Nothing
          Emptying
NonEmptying -> () -> n ()
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    let (Threads n
threads', [ThreadId]
woken) = BlockedOn -> Threads n -> (Threads n, [ThreadId])
forall (n :: * -> *).
BlockedOn -> Threads n -> (Threads n, [ThreadId])
wake (MVarId -> BlockedOn
OnMVarEmpty MVarId
mvarId) Threads n
threads
    n ()
effect
    (Bool, Threads n, [ThreadId], n ())
-> n (Bool, Threads n, [ThreadId], n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
True, Action n -> ThreadId -> Threads n -> Threads n
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' = BlockedOn -> ThreadId -> Threads n -> Threads n
forall (n :: * -> *).
HasCallStack =>
BlockedOn -> ThreadId -> Threads n -> Threads n
block (MVarId -> BlockedOn
OnMVarFull MVarId
mvarId) ThreadId
threadid Threads n
threads
      in (Bool, Threads n, [ThreadId], n ())
-> n (Bool, Threads n, [ThreadId], n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
False, Threads n
threads', [], () -> n ()
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
    Blocking
NonBlocking ->
      (Bool, Threads n, [ThreadId], n ())
-> n (Bool, Threads n, [ThreadId], n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
False, Action n -> ThreadId -> Threads n -> Threads n
forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto (Maybe a -> Action n
c Maybe a
forall a. Maybe a
Nothing) ThreadId
threadid Threads n
threads, [], () -> n ()
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())