Test.IOSpec.VirtualMachine

The virtual machine on which the specifications execute.

The Virtual Machine

type VM a = StateT Store Effect a

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

type Loc = Int

data Scheduler

Instances

Arbitrary Scheduler

Defined in Test.IOSpec.VirtualMachine

Methods

arbitrary :: Gen Scheduler

shrink :: Scheduler -> [Scheduler]

Show Scheduler

Defined in Test.IOSpec.VirtualMachine

Methods

showsPrec :: Int -> Scheduler -> ShowS

show :: Scheduler -> String

showList :: [Scheduler] -> ShowS

data Store

data ThreadId

Instances

Arbitrary ThreadId

Defined in Test.IOSpec.VirtualMachine

Methods

arbitrary :: Gen ThreadId

shrink :: ThreadId -> [ThreadId]

CoArbitrary ThreadId

Defined in Test.IOSpec.VirtualMachine

Methods

coarbitrary :: ThreadId -> Gen b -> Gen b

Show ThreadId

Defined in Test.IOSpec.VirtualMachine

Methods

showsPrec :: Int -> ThreadId -> ShowS

show :: ThreadId -> String

showList :: [ThreadId] -> ShowS

Eq ThreadId

Defined in Test.IOSpec.VirtualMachine

Methods

(==) :: ThreadId -> ThreadId -> Bool

(/=) :: ThreadId -> ThreadId -> Bool

initialStore :: Scheduler -> Store

Primitive operations on the VM

alloc :: VM Loc

The alloc function allocate a fresh location on the heap.

emptyLoc :: Loc -> VM ()

The emptyLoc function removes the data stored at a given location. This corresponds, for instance, to emptying an MVar.

freshThreadId :: VM ThreadId

The freshThreadId function returns a previously unallocated ThreadId.

finishThread :: ThreadId -> VM ()

The finishThread function kills the thread with the specified ThreadId.

lookupHeap :: Loc -> VM (Maybe Data)

The lookupHeap function returns the data stored at a given heap location, if there is any.

mainTid :: ThreadId

The mainTid constant is the ThreadId of the main process.

printChar :: Char -> VM ()

readChar :: VM Char

The readChar and printChar functions are the primitive counterparts of getChar and putChar in the VM monad.

updateHeap :: Loc -> Data -> VM ()

The updateHeap function overwrites a given location with new data.

updateSoup :: Executable f => ThreadId -> IOSpec f a -> VM ()

The updateSoup function updates the process associated with a given ThreadId.

The observable effects on the VM

data Effect a

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

Applicative Effect

Defined in Test.IOSpec.VirtualMachine

Methods

pure :: a -> Effect a

(<*>) :: Effect (a -> b) -> Effect a -> Effect b

liftA2 :: (a -> b -> c) -> Effect a -> Effect b -> Effect c

(*>) :: Effect a -> Effect b -> Effect b

(<*) :: Effect a -> Effect b -> Effect a

Functor Effect

Defined in Test.IOSpec.VirtualMachine

Methods

fmap :: (a -> b) -> Effect a -> Effect b

(<$) :: a -> Effect b -> Effect a

Monad Effect

Defined in Test.IOSpec.VirtualMachine

Methods

(>>=) :: Effect a -> (a -> Effect b) -> Effect b

(>>) :: Effect a -> Effect b -> Effect b

return :: a -> Effect a

Eq a => Eq (Effect a)

Defined in Test.IOSpec.VirtualMachine

Methods

(==) :: Effect a -> Effect a -> Bool

(/=) :: Effect a -> Effect a -> Bool

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

The roundRobin scheduler provides a simple round-robin scheduler.

singleThreaded :: Scheduler

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

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)

Instances

Executable ForkS

Defined in Test.IOSpec.Fork

Methods

step :: ForkS a -> VM (Step a)

Executable IORefS

The Executable instance for the IORefS monad.

Defined in Test.IOSpec.IORef

Methods

step :: IORefS a -> VM (Step a)

Executable MVarS

Defined in Test.IOSpec.MVar

Methods

step :: MVarS a -> VM (Step a)

Executable STMS

Defined in Test.IOSpec.STM

Methods

step :: STMS a -> VM (Step a)

Executable Teletype

Defined in Test.IOSpec.Teletype

Methods

step :: Teletype a -> VM (Step a)

(Executable f, Executable g) => Executable (f :+: g)

Defined in Test.IOSpec.VirtualMachine

Methods

step :: (f :+: g) a -> VM (Step a)

data Step a

Constructors

Step a

Block

runIOSpec :: Executable f => IOSpec f a -> Scheduler -> Effect (a, Store)

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 a

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

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.