{-# LANGUAGE ExistentialQuantification, TypeOperators #-}
module Test.IOSpec.VirtualMachine
(
VM
, Data
, Loc
, Scheduler
, Store
, ThreadId
, initialStore
, alloc
, emptyLoc
, freshThreadId
, finishThread
, lookupHeap
, mainTid
, printChar
, readChar
, updateHeap
, updateSoup
, Effect (..)
, roundRobin
, singleThreaded
, Executable(..)
, Step(..)
, runIOSpec
, evalIOSpec
, execIOSpec
)
where
import Control.Monad.State
import Data.Dynamic
import Data.List
import qualified Data.Stream as Stream
import Test.IOSpec.Types
import Test.QuickCheck
import Control.Monad (liftM, ap)
type Data = Dynamic
type Loc = Int
type Heap = Loc -> Maybe Data
newtype ThreadId = ThreadId Int deriving (ThreadId -> ThreadId -> Bool
(ThreadId -> ThreadId -> Bool)
-> (ThreadId -> ThreadId -> Bool) -> Eq ThreadId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ThreadId -> ThreadId -> Bool
== :: ThreadId -> ThreadId -> Bool
$c/= :: ThreadId -> ThreadId -> Bool
/= :: ThreadId -> ThreadId -> Bool
Eq, Int -> ThreadId -> ShowS
[ThreadId] -> ShowS
ThreadId -> String
(Int -> ThreadId -> ShowS)
-> (ThreadId -> String) -> ([ThreadId] -> ShowS) -> Show ThreadId
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ThreadId -> ShowS
showsPrec :: Int -> ThreadId -> ShowS
$cshow :: ThreadId -> String
show :: ThreadId -> String
$cshowList :: [ThreadId] -> ShowS
showList :: [ThreadId] -> ShowS
Show)
instance Arbitrary ThreadId where
arbitrary :: Gen ThreadId
arbitrary = (Int -> ThreadId) -> Gen Int -> Gen ThreadId
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> ThreadId
ThreadId Gen Int
forall a. Arbitrary a => Gen a
arbitrary
instance CoArbitrary ThreadId where
coarbitrary :: forall b. ThreadId -> Gen b -> Gen b
coarbitrary (ThreadId Int
k) = Int -> Gen b -> Gen b
forall b. Int -> Gen b -> Gen b
forall a b. CoArbitrary a => a -> Gen b -> Gen b
coarbitrary Int
k
newtype Scheduler =
Scheduler (Int -> (Int, Scheduler))
instance Arbitrary Scheduler where
arbitrary :: Gen Scheduler
arbitrary = (Stream Int -> Scheduler) -> Gen (Stream Int) -> Gen Scheduler
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Stream Int -> Scheduler
streamSched Gen (Stream Int)
forall a. Arbitrary a => Gen a
arbitrary
instance Show Scheduler where
show :: Scheduler -> String
show Scheduler
_ = String
"Test.IOSpec.Scheduler"
data ThreadStatus =
forall f b . Executable f => Running (IOSpec f b)
| Finished
type ThreadSoup = ThreadId -> ThreadStatus
data Store =
Store { Store -> Int
fresh :: Loc
, Store -> Heap
heap :: Heap
, Store -> ThreadId
nextTid :: ThreadId
, Store -> [ThreadId]
blockedThreads :: [ThreadId]
, Store -> [ThreadId]
finishedThreads :: [ThreadId]
, Store -> Scheduler
scheduler :: Scheduler
, Store -> ThreadSoup
threadSoup :: ThreadSoup
}
initialStore :: Scheduler -> Store
initialStore :: Scheduler -> Store
initialStore Scheduler
sch =
Store { fresh :: Int
fresh = Int
0
, heap :: Heap
heap = String -> Heap
forall a. String -> a
internalError String
"Access of unallocated memory "
, nextTid :: ThreadId
nextTid = Int -> ThreadId
ThreadId Int
1
, blockedThreads :: [ThreadId]
blockedThreads = []
, finishedThreads :: [ThreadId]
finishedThreads = []
, scheduler :: Scheduler
scheduler = Scheduler
sch
, threadSoup :: ThreadSoup
threadSoup = String -> ThreadSoup
forall a. String -> a
internalError String
"Unknown thread scheduled"
}
modifyFresh :: (Loc -> Loc) -> VM ()
modifyFresh :: (Int -> Int) -> VM ()
modifyFresh Int -> Int
f = do Store
s <- StateT Store Effect Store
forall s (m :: * -> *). MonadState s m => m s
get
Store -> VM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Store
s {fresh = f (fresh s)})
modifyHeap :: (Heap -> Heap) -> VM ()
modifyHeap :: (Heap -> Heap) -> VM ()
modifyHeap Heap -> Heap
f = do Store
s <- StateT Store Effect Store
forall s (m :: * -> *). MonadState s m => m s
get
Store -> VM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Store
s {heap = f (heap s)})
modifyNextTid :: (ThreadId -> ThreadId) -> VM ()
modifyNextTid :: (ThreadId -> ThreadId) -> VM ()
modifyNextTid ThreadId -> ThreadId
f = do Store
s <- StateT Store Effect Store
forall s (m :: * -> *). MonadState s m => m s
get
Store -> VM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Store
s {nextTid = f (nextTid s)})
modifyBlockedThreads :: ([ThreadId] -> [ThreadId]) -> VM ()
modifyBlockedThreads :: ([ThreadId] -> [ThreadId]) -> VM ()
modifyBlockedThreads [ThreadId] -> [ThreadId]
f = do Store
s <- StateT Store Effect Store
forall s (m :: * -> *). MonadState s m => m s
get
Store -> VM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Store
s {blockedThreads = f (blockedThreads s)})
modifyFinishedThreads :: ([ThreadId] -> [ThreadId]) -> VM ()
modifyFinishedThreads :: ([ThreadId] -> [ThreadId]) -> VM ()
modifyFinishedThreads [ThreadId] -> [ThreadId]
f = do Store
s <- StateT Store Effect Store
forall s (m :: * -> *). MonadState s m => m s
get
Store -> VM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Store
s {finishedThreads = f (finishedThreads s)})
modifyScheduler :: (Scheduler -> Scheduler) -> VM ()
modifyScheduler :: (Scheduler -> Scheduler) -> VM ()
modifyScheduler Scheduler -> Scheduler
f = do Store
s <- StateT Store Effect Store
forall s (m :: * -> *). MonadState s m => m s
get
Store -> VM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Store
s {scheduler = f (scheduler s)})
modifyThreadSoup :: (ThreadSoup -> ThreadSoup) -> VM ()
modifyThreadSoup :: (ThreadSoup -> ThreadSoup) -> VM ()
modifyThreadSoup ThreadSoup -> ThreadSoup
f = do Store
s <- StateT Store Effect Store
forall s (m :: * -> *). MonadState s m => m s
get
Store -> VM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Store
s {threadSoup = f (threadSoup s)})
type VM a = StateT Store Effect a
alloc :: VM Loc
alloc :: VM Int
alloc = do Int
loc <- (Store -> Int) -> VM Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Store -> Int
fresh
(Int -> Int) -> VM ()
modifyFresh (Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) Int
1)
Int -> VM Int
forall a. a -> StateT Store Effect a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
loc
emptyLoc :: Loc -> VM ()
emptyLoc :: Int -> VM ()
emptyLoc Int
l = (Heap -> Heap) -> VM ()
modifyHeap (Int -> Maybe Data -> Heap -> Heap
forall a b. Eq a => a -> b -> (a -> b) -> a -> b
update Int
l Maybe Data
forall a. Maybe a
Nothing)
freshThreadId :: VM ThreadId
freshThreadId :: VM ThreadId
freshThreadId = do
ThreadId
t <- (Store -> ThreadId) -> VM ThreadId
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Store -> ThreadId
nextTid
(ThreadId -> ThreadId) -> VM ()
modifyNextTid (\(ThreadId Int
n) -> Int -> ThreadId
ThreadId (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1))
ThreadId -> VM ThreadId
forall a. a -> StateT Store Effect a
forall (m :: * -> *) a. Monad m => a -> m a
return ThreadId
t
finishThread :: ThreadId -> VM ()
finishThread :: ThreadId -> VM ()
finishThread ThreadId
tid = do
([ThreadId] -> [ThreadId]) -> VM ()
modifyFinishedThreads (ThreadId
tidThreadId -> [ThreadId] -> [ThreadId]
forall a. a -> [a] -> [a]
:)
(ThreadSoup -> ThreadSoup) -> VM ()
modifyThreadSoup (ThreadId -> ThreadStatus -> ThreadSoup -> ThreadSoup
forall a b. Eq a => a -> b -> (a -> b) -> a -> b
update ThreadId
tid ThreadStatus
Finished)
blockThread :: ThreadId -> VM ()
blockThread :: ThreadId -> VM ()
blockThread ThreadId
tid = ([ThreadId] -> [ThreadId]) -> VM ()
modifyBlockedThreads (ThreadId
tidThreadId -> [ThreadId] -> [ThreadId]
forall a. a -> [a] -> [a]
:)
resetBlockedThreads :: VM ()
resetBlockedThreads :: VM ()
resetBlockedThreads = ([ThreadId] -> [ThreadId]) -> VM ()
modifyBlockedThreads ([ThreadId] -> [ThreadId] -> [ThreadId]
forall a b. a -> b -> a
const [])
lookupHeap :: Loc -> VM (Maybe Data)
lookupHeap :: Int -> VM (Maybe Data)
lookupHeap Int
l = do Heap
h <- (Store -> Heap) -> StateT Store Effect Heap
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Store -> Heap
heap
Maybe Data -> VM (Maybe Data)
forall a. a -> StateT Store Effect a
forall (m :: * -> *) a. Monad m => a -> m a
return (Heap
h Int
l)
mainTid :: ThreadId
mainTid :: ThreadId
mainTid = Int -> ThreadId
ThreadId Int
0
readChar :: VM Char
readChar :: VM Char
readChar = (Store -> Effect (Char, Store)) -> VM Char
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT (\Store
s -> ((Char -> Effect (Char, Store)) -> Effect (Char, Store)
forall a. (Char -> Effect a) -> Effect a
ReadChar (\Char
c -> ((Char, Store) -> Effect (Char, Store)
forall a. a -> Effect a
Done (Char
c,Store
s)))))
printChar :: Char -> VM ()
printChar :: Char -> VM ()
printChar Char
c = (Store -> Effect ((), Store)) -> VM ()
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT (\Store
s -> (Char -> Effect ((), Store) -> Effect ((), Store)
forall a. Char -> Effect a -> Effect a
Print Char
c (((), Store) -> Effect ((), Store)
forall a. a -> Effect a
Done ((),Store
s))))
updateHeap :: Loc -> Data -> VM ()
updateHeap :: Int -> Data -> VM ()
updateHeap Int
l Data
d = (Heap -> Heap) -> VM ()
modifyHeap (Int -> Maybe Data -> Heap -> Heap
forall a b. Eq a => a -> b -> (a -> b) -> a -> b
update Int
l (Data -> Maybe Data
forall a. a -> Maybe a
Just Data
d))
updateSoup :: Executable f => ThreadId -> IOSpec f a -> VM ()
updateSoup :: forall (f :: * -> *) a.
Executable f =>
ThreadId -> IOSpec f a -> VM ()
updateSoup ThreadId
tid IOSpec f a
p = (ThreadSoup -> ThreadSoup) -> VM ()
modifyThreadSoup (ThreadId -> ThreadStatus -> ThreadSoup -> ThreadSoup
forall a b. Eq a => a -> b -> (a -> b) -> a -> b
update ThreadId
tid (IOSpec f a -> ThreadStatus
forall (f :: * -> *) b. Executable f => IOSpec f b -> ThreadStatus
Running IOSpec f a
p))
update :: Eq a => a -> b -> (a -> b) -> (a -> b)
update :: forall a b. Eq a => a -> b -> (a -> b) -> a -> b
update a
l b
d a -> b
h a
k
| a
l a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
k = b
d
| Bool
otherwise = a -> b
h a
k
data Effect a =
Done a
| ReadChar (Char -> Effect a)
| Print Char (Effect a)
| Fail String
instance Functor Effect where
fmap :: forall a b. (a -> b) -> Effect a -> Effect b
fmap a -> b
f (Done a
x) = b -> Effect b
forall a. a -> Effect a
Done (a -> b
f a
x)
fmap a -> b
f (ReadChar Char -> Effect a
t) = (Char -> Effect b) -> Effect b
forall a. (Char -> Effect a) -> Effect a
ReadChar (\Char
c -> (a -> b) -> Effect a -> Effect b
forall a b. (a -> b) -> Effect a -> Effect b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (Char -> Effect a
t Char
c))
fmap a -> b
f (Print Char
c Effect a
t) = Char -> Effect b -> Effect b
forall a. Char -> Effect a -> Effect a
Print Char
c ((a -> b) -> Effect a -> Effect b
forall a b. (a -> b) -> Effect a -> Effect b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Effect a
t)
fmap a -> b
_ (Fail String
msg) = String -> Effect b
forall a. String -> Effect a
Fail String
msg
instance Applicative Effect where
pure :: forall a. a -> Effect a
pure = a -> Effect a
forall a. a -> Effect a
Done
<*> :: forall a b. Effect (a -> b) -> Effect a -> Effect b
(<*>) = Effect (a -> b) -> Effect a -> Effect b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Monad Effect where
return :: forall a. a -> Effect a
return = a -> Effect a
forall a. a -> Effect a
Done
(Done a
x) >>= :: forall a b. Effect a -> (a -> Effect b) -> Effect b
>>= a -> Effect b
f = a -> Effect b
f a
x
(ReadChar Char -> Effect a
t) >>= a -> Effect b
f = (Char -> Effect b) -> Effect b
forall a. (Char -> Effect a) -> Effect a
ReadChar (\Char
c -> Char -> Effect a
t Char
c Effect a -> (a -> Effect b) -> Effect b
forall a b. Effect a -> (a -> Effect b) -> Effect b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Effect b
f)
(Print Char
c Effect a
t) >>= a -> Effect b
f = Char -> Effect b -> Effect b
forall a. Char -> Effect a -> Effect a
Print Char
c (Effect a
t Effect a -> (a -> Effect b) -> Effect b
forall a b. Effect a -> (a -> Effect b) -> Effect b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Effect b
f)
(Fail String
msg) >>= a -> Effect b
_ = String -> Effect b
forall a. String -> Effect a
Fail String
msg
instance Eq a => Eq (Effect a) where
(Done a
x) == :: Effect a -> Effect a -> Bool
== (Done a
y) = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y
(ReadChar Char -> Effect a
f) == (ReadChar Char -> Effect a
g) =
(Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Char
x -> Char -> Effect a
f Char
x Effect a -> Effect a -> Bool
forall a. Eq a => a -> a -> Bool
== Char -> Effect a
g Char
x) [Char
forall a. Bounded a => a
minBound .. Char
forall a. Bounded a => a
maxBound]
(Print Char
c Effect a
t) == (Print Char
d Effect a
u) = Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
d Bool -> Bool -> Bool
&& Effect a
t Effect a -> Effect a -> Bool
forall a. Eq a => a -> a -> Bool
== Effect a
u
(Fail String
s) == (Fail String
t) = String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
t
Effect a
_ == Effect a
_ = Bool
False
roundRobin :: Scheduler
roundRobin :: Scheduler
roundRobin = Stream Int -> Scheduler
streamSched ((Int -> (Int, Int)) -> Int -> Stream Int
forall c a. (c -> (a, c)) -> c -> Stream a
Stream.unfold (\Int
k -> (Int
k, Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)) Int
0)
singleThreaded :: Scheduler
singleThreaded :: Scheduler
singleThreaded = Stream Int -> Scheduler
streamSched (Int -> Stream Int
forall a. a -> Stream a
Stream.repeat Int
0)
streamSched :: Stream.Stream Int -> Scheduler
streamSched :: Stream Int -> Scheduler
streamSched (Stream.Cons Int
x Stream Int
xs) =
(Int -> (Int, Scheduler)) -> Scheduler
Scheduler (\Int
k -> (Int
x Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
k, Stream Int -> Scheduler
streamSched Stream Int
xs))
class Functor f => Executable f where
step :: f a -> VM (Step a)
data Step a = Step a | Block
instance (Executable f, Executable g) => Executable (f :+: g) where
step :: forall a. (:+:) f g a -> VM (Step a)
step (Inl f a
x) = f a -> VM (Step a)
forall a. f a -> VM (Step a)
forall (f :: * -> *) a. Executable f => f a -> VM (Step a)
step f a
x
step (Inr g a
y) = g a -> VM (Step a)
forall a. g a -> VM (Step a)
forall (f :: * -> *) a. Executable f => f a -> VM (Step a)
step g a
y
execVM :: Executable f => IOSpec f a -> VM a
execVM :: forall (f :: * -> *) a. Executable f => IOSpec f a -> VM a
execVM IOSpec f a
main = do
(ThreadId
tid,Process a
t) <- IOSpec f a -> VM (ThreadId, Process a)
forall (f :: * -> *) a.
Executable f =>
IOSpec f a -> VM (ThreadId, Process a)
schedule IOSpec f a
main
case Process a
t of
(Main (Pure a
x)) -> VM ()
resetBlockedThreads VM () -> VM a -> VM a
forall a b.
StateT Store Effect a
-> StateT Store Effect b -> StateT Store Effect b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> VM a
forall a. a -> StateT Store Effect a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
(Main (Impure f (IOSpec f a)
p)) -> do Step (IOSpec f a)
x <- f (IOSpec f a) -> VM (Step (IOSpec f a))
forall a. f a -> VM (Step a)
forall (f :: * -> *) a. Executable f => f a -> VM (Step a)
step f (IOSpec f a)
p
case Step (IOSpec f a)
x of
Step IOSpec f a
y -> VM ()
resetBlockedThreads VM () -> VM a -> VM a
forall a b.
StateT Store Effect a
-> StateT Store Effect b -> StateT Store Effect b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IOSpec f a -> VM a
forall (f :: * -> *) a. Executable f => IOSpec f a -> VM a
execVM IOSpec f a
y
Step (IOSpec f a)
Block -> ThreadId -> VM ()
blockThread ThreadId
mainTid VM () -> VM a -> VM a
forall a b.
StateT Store Effect a
-> StateT Store Effect b -> StateT Store Effect b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IOSpec f a -> VM a
forall (f :: * -> *) a. Executable f => IOSpec f a -> VM a
execVM IOSpec f a
main
(Aux (Pure b
_)) -> do ThreadId -> VM ()
finishThread ThreadId
tid
IOSpec f a -> VM a
forall (f :: * -> *) a. Executable f => IOSpec f a -> VM a
execVM IOSpec f a
main
(Aux (Impure f (IOSpec f b)
p)) -> do Step (IOSpec f b)
x <- f (IOSpec f b) -> VM (Step (IOSpec f b))
forall a. f a -> VM (Step a)
forall (f :: * -> *) a. Executable f => f a -> VM (Step a)
step f (IOSpec f b)
p
case Step (IOSpec f b)
x of
Step IOSpec f b
y -> VM ()
resetBlockedThreads VM () -> VM () -> VM ()
forall a b.
StateT Store Effect a
-> StateT Store Effect b -> StateT Store Effect b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
ThreadId -> IOSpec f b -> VM ()
forall (f :: * -> *) a.
Executable f =>
ThreadId -> IOSpec f a -> VM ()
updateSoup ThreadId
tid IOSpec f b
y VM () -> VM a -> VM a
forall a b.
StateT Store Effect a
-> StateT Store Effect b -> StateT Store Effect b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
IOSpec f a -> VM a
forall (f :: * -> *) a. Executable f => IOSpec f a -> VM a
execVM IOSpec f a
main
Step (IOSpec f b)
Block -> ThreadId -> VM ()
blockThread ThreadId
tid VM () -> VM a -> VM a
forall a b.
StateT Store Effect a
-> StateT Store Effect b -> StateT Store Effect b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
IOSpec f a -> VM a
forall (f :: * -> *) a. Executable f => IOSpec f a -> VM a
execVM IOSpec f a
main
data Process a =
forall f . Executable f => Main (IOSpec f a)
| forall f b . Executable f => Aux (IOSpec f b)
getNextThreadId :: VM ThreadId
getNextThreadId :: VM ThreadId
getNextThreadId = do
Scheduler Int -> (Int, Scheduler)
sch <- (Store -> Scheduler) -> StateT Store Effect Scheduler
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Store -> Scheduler
scheduler
(ThreadId Int
total) <- (Store -> ThreadId) -> VM ThreadId
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Store -> ThreadId
nextTid
let allTids :: [ThreadId]
allTids = [Int -> ThreadId
ThreadId Int
i | Int
i <- [Int
0 .. Int
total Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]
[ThreadId]
blockedTids <- (Store -> [ThreadId]) -> StateT Store Effect [ThreadId]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Store -> [ThreadId]
blockedThreads
[ThreadId]
finishedTids <- (Store -> [ThreadId]) -> StateT Store Effect [ThreadId]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Store -> [ThreadId]
finishedThreads
let activeThreads :: [ThreadId]
activeThreads = [ThreadId]
allTids [ThreadId] -> [ThreadId] -> [ThreadId]
forall a. Eq a => [a] -> [a] -> [a]
\\ ([ThreadId]
blockedTids [ThreadId] -> [ThreadId] -> [ThreadId]
forall a. Eq a => [a] -> [a] -> [a]
`union` [ThreadId]
finishedTids)
let (Int
i,Scheduler
s) = Int -> (Int, Scheduler)
sch ([ThreadId] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ThreadId]
activeThreads)
(Scheduler -> Scheduler) -> VM ()
modifyScheduler (Scheduler -> Scheduler -> Scheduler
forall a b. a -> b -> a
const Scheduler
s)
ThreadId -> VM ThreadId
forall a. a -> StateT Store Effect a
forall (m :: * -> *) a. Monad m => a -> m a
return ([ThreadId]
activeThreads [ThreadId] -> Int -> ThreadId
forall a. HasCallStack => [a] -> Int -> a
!! Int
i)
schedule :: Executable f => IOSpec f a -> VM (ThreadId, Process a)
schedule :: forall (f :: * -> *) a.
Executable f =>
IOSpec f a -> VM (ThreadId, Process a)
schedule IOSpec f a
main = do ThreadId
tid <- VM ThreadId
getNextThreadId
if ThreadId
tid ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
mainTid
then (ThreadId, Process a) -> VM (ThreadId, Process a)
forall a. a -> StateT Store Effect a
forall (m :: * -> *) a. Monad m => a -> m a
return (ThreadId
mainTid, IOSpec f a -> Process a
forall a (f :: * -> *). Executable f => IOSpec f a -> Process a
Main IOSpec f a
main)
else do
ThreadSoup
tsoup <- (Store -> ThreadSoup) -> StateT Store Effect ThreadSoup
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Store -> ThreadSoup
threadSoup
case ThreadSoup
tsoup ThreadId
tid of
ThreadStatus
Finished -> String -> VM (ThreadId, Process a)
forall a. String -> a
internalError
String
"Scheduled finished thread."
Running IOSpec f b
p -> (ThreadId, Process a) -> VM (ThreadId, Process a)
forall a. a -> StateT Store Effect a
forall (m :: * -> *) a. Monad m => a -> m a
return (ThreadId
tid, IOSpec f b -> Process a
forall a (f :: * -> *) b. Executable f => IOSpec f b -> Process a
Aux IOSpec f b
p)
runIOSpec :: Executable f => IOSpec f a -> Scheduler -> Effect (a, Store)
runIOSpec :: forall (f :: * -> *) a.
Executable f =>
IOSpec f a -> Scheduler -> Effect (a, Store)
runIOSpec IOSpec f a
io Scheduler
sched = StateT Store Effect a -> Store -> Effect (a, Store)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT
(IOSpec f a -> StateT Store Effect a
forall (f :: * -> *) a. Executable f => IOSpec f a -> VM a
execVM IOSpec f a
io)
(Scheduler -> Store
initialStore Scheduler
sched)
execIOSpec :: Executable f => IOSpec f a -> Scheduler -> Store
execIOSpec :: forall (f :: * -> *) a.
Executable f =>
IOSpec f a -> Scheduler -> Store
execIOSpec IOSpec f a
io Scheduler
sched =
case IOSpec f a -> Scheduler -> Effect (a, Store)
forall (f :: * -> *) a.
Executable f =>
IOSpec f a -> Scheduler -> Effect (a, Store)
runIOSpec IOSpec f a
io Scheduler
sched of
Done (a
_,Store
s) -> Store
s
Effect (a, Store)
_ -> String -> Store
forall a. HasCallStack => String -> a
error (String -> Store) -> String -> Store
forall a b. (a -> b) -> a -> b
$ String
"Failed application of Test.IOSpec.execIOSpec.\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
"Probable cause: your function uses functions such as " String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
"putChar and getChar. Check the preconditions for calling " String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
"this function in the IOSpec documentation."
evalIOSpec :: Executable f => IOSpec f a -> Scheduler -> Effect a
evalIOSpec :: forall (f :: * -> *) a.
Executable f =>
IOSpec f a -> Scheduler -> Effect a
evalIOSpec IOSpec f a
io Scheduler
sched = ((a, Store) -> a) -> Effect (a, Store) -> Effect a
forall a b. (a -> b) -> Effect a -> Effect b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, Store) -> a
forall a b. (a, b) -> a
fst (IOSpec f a -> Scheduler -> Effect (a, Store)
forall (f :: * -> *) a.
Executable f =>
IOSpec f a -> Scheduler -> Effect (a, Store)
runIOSpec IOSpec f a
io Scheduler
sched)
internalError :: String -> a
internalError :: forall a. String -> a
internalError String
msg = String -> a
forall a. HasCallStack => String -> a
error (String
"IOSpec.VirtualMachine: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
msg)