Safe Haskell | None |
---|---|
Language | Haskell98 |
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 a Source
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 -> Store Source
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 ThreadId Source
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.
roundRobin :: Scheduler Source
The roundRobin
scheduler provides a simple round-robin scheduler.
singleThreaded :: Scheduler Source
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 where Source
The Executable
type class captures all the different types of
operations that can be executed in the VM
monad.
Executable Teletype Source | |
Executable STMS Source | |
Executable IORefS Source | The |
Executable MVarS Source | |
Executable ForkS Source | |
(Executable f, Executable g) => Executable ((:+:) f g) Source |
evalIOSpec :: Executable f => IOSpec f a -> Scheduler -> Effect a Source
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 -> Store Source
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.