Safe Haskell	None

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

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 = Dynamic Source

type Loc = Int Source

data Scheduler Source

Instances

Show Scheduler
Arbitrary Scheduler

data Store Source

data ThreadId Source

Instances

Eq ThreadId
Show ThreadId
Arbitrary ThreadId
CoArbitrary ThreadId

initialStore :: Scheduler -> Store Source

Primitive operations on the VM

alloc :: VM Loc Source

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 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.

mainTid :: ThreadId Source

The mainTid constant is the ThreadId of the main process.

printChar :: Char -> VM ()Source

readChar :: VM Char Source

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

Instances

Monad Effect
Functor Effect
Eq a => Eq (Effect a)

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 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

Instances

Executable Teletype
Executable STMS
Executable IORefS	The `Executable` instance for the `IORefS` monad.
Executable MVarS
Executable ForkS
(Executable f, Executable g) => Executable (:+: f g)

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 -> 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.