IOSpec-0.2.1: A pure specification of the IO monad.Source codeContentsIndex
Test.IOSpec.VirtualMachine
Contents
The Virtual Machine
Primitive operations on the VM
The observable effects on the VM
Sample schedulers
Executing code on the VM
Description
The virtual machine on which the specifications execute.
Synopsis
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
= Done a
| ReadChar (Char -> Effect a)
| Print Char (Effect a)
| Fail String
roundRobin :: Scheduler
singleThreaded :: Scheduler
class Functor f => Executable f where
step :: f a -> VM (Step a)
data Step a
= Step a
| Block
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.
type Data = DynamicSource
type Loc = IntSource
data Scheduler Source
show/hide Instances
data Store Source
data ThreadId Source
show/hide Instances
initialStore :: Scheduler -> StoreSource
Primitive operations on the VM
alloc :: VM LocSource
The alloc function allocate a fresh location on the heap.
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.
mainTid :: ThreadIdSource
The mainTid constant is the ThreadId of the main process.
printChar :: Char -> VM ()Source
readChar :: VM CharSource
The readChar and printChar functions are the primitive counterparts of getChar and putChar in the VM monad.
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
data Effect a Source
The Effect type contains all the primitive effects that are observable on the virtual machine.
Constructors
Done a
ReadChar (Char -> Effect a)
Print Char (Effect a)
Fail String
show/hide Instances
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 :: SchedulerSource
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.
Methods
step :: f a -> VM (Step a)Source
show/hide Instances
data Step a Source
Constructors
Step a
Block
runIOSpec :: Executable f => IOSpec f a -> Scheduler -> Effect (a, Store)Source
The runIOSpec function is the heart of this library. Given the scheduling algorithm you want to use, it will run a value of type IOSpec f a, returning the sequence of observable effects together with the final store.
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.

Produced by Haddock version 2.4.2