The virtual machine on which the specifications execute.
- type VM a = StateT Store Effect a
- type Data = Dynamic
- type Loc = Int
- data Scheduler
- data Store
- data ThreadId
- initialStore :: Scheduler -> Store
- alloc :: VM Loc
- emptyLoc :: Loc -> VM ()
- freshThreadId :: VM ThreadId
- finishThread :: ThreadId -> VM ()
- lookupHeap :: Loc -> VM (Maybe Data)
- mainTid :: ThreadId
- printChar :: Char -> VM ()
- readChar :: VM Char
- updateHeap :: Loc -> Data -> VM ()
- updateSoup :: Executable f => ThreadId -> IOSpec f a -> VM ()
- data Effect a
- roundRobin :: Scheduler
- singleThreaded :: Scheduler
- class Functor f => Executable f where
- data Step a
- runIOSpec :: Executable f => IOSpec f a -> Scheduler -> Effect (a, Store)
- evalIOSpec :: Executable f => IOSpec f a -> Scheduler -> Effect a
- execIOSpec :: Executable f => IOSpec f a -> Scheduler -> Store
The Virtual Machine
type VM a = StateT Store Effect aSource
The VM
monad is essentially a state monad, modifying the
store. Besides returning pure values, various primitive effects
may occur, such as printing characters or failing with an error
message.
initialStore :: Scheduler -> StoreSource
Primitive operations on the VM
emptyLoc :: Loc -> VM ()Source
The emptyLoc
function removes the data stored at a given
location. This corresponds, for instance, to emptying an MVar
.
freshThreadId :: VM ThreadIdSource
The freshThreadId
function returns a previously unallocated ThreadId
.
finishThread :: ThreadId -> VM ()Source
The finishThread
function kills the thread with the specified
ThreadId
.
lookupHeap :: Loc -> VM (Maybe Data)Source
The lookupHeap
function returns the data stored at a given
heap location, if there is any.
updateHeap :: Loc -> Data -> VM ()Source
The updateHeap
function overwrites a given location with
new data.
updateSoup :: Executable f => ThreadId -> IOSpec f a -> VM ()Source
The updateSoup
function updates the process associated with a
given ThreadId
.
The observable effects on the VM
The Effect
type contains all the primitive effects that are
observable on the virtual machine.
Sample schedulers
There are two example scheduling algorithms roundRobin
and
singleThreaded
. Note that Scheduler
is also an instance of
Arbitrary
. Using QuickCheck to generate random schedulers is a
great way to maximise the number of interleavings that your tests
cover.
The roundRobin
scheduler provides a simple round-robin scheduler.
singleThreaded :: SchedulerSource
The singleThreaded
scheduler will never schedule forked
threads, always scheduling the main thread. Only use this
scheduler if your code is not concurrent.
Executing code on the VM
class Functor f => Executable f whereSource
The Executable
type class captures all the different types of
operations that can be executed in the VM
monad.
Executable Teletype | |
Executable STMS | |
Executable IORefS | The |
Executable MVarS | |
Executable ForkS | |
(Executable f, Executable g) => Executable (:+: f g) |
evalIOSpec :: Executable f => IOSpec f a -> Scheduler -> Effect aSource
The evalIOSpec
function returns the effects a computation
yields, but discards the final state of the virtual machine.
execIOSpec :: Executable f => IOSpec f a -> Scheduler -> StoreSource
The execIOSpec
returns the final Store
after executing a
computation.
Beware: this function assumes that your computation will
succeed, without any other visible Effect
. If your computation
reads a character from the teletype, for instance, it will return
an error.