packages feed

IOSpec (empty) → 0.1

raw patch · 12 files changed

+1003/−0 lines, 12 filesdep +QuickCheckdep +basedep +mtlbuild-type:Customsetup-changed

Dependencies added: QuickCheck, base, mtl

Files

+ IOSpec.cabal view
@@ -0,0 +1,32 @@+Name:		        IOSpec+Version:        	0.1+License:        	BSD3+License-file:		LICENSE+Author:			Wouter Swierstra+Maintainer:     	Wouter Swierstra <wss@cs.nott.ac.uk>+Homepage:       	http://www.cs.nott.ac.uk/~wss/repos/IOSpec+Synopsis:       	A pure specification of the IO monad.+Description:		At the moment this package consists of four +			modules:+			.+                           * "Test.IOSpec.Teletype": a specification of getChar and putChar.+			.+			   * "Test.IOSpec.IORef": a specification of most functions on IORefs.+			.+			   * "Test.IOSpec.Concurrent": specification of forkIO and MVars.+			.+			   * "Data.Stream": a library for manipulating infinite lists.+			.+			There are several well-documented examples included with the source distribution.+Category:       	Test+Build-Depends:  	base, mtl, QuickCheck +Hs-source-dirs:		src+Extra-source-files:	README+			, examples/Echo.hs+			, examples/Queues.hs+			, examples/Channels.hs+Exposed-modules:	Data.Stream+			, Test.IOSpec+			, Test.IOSpec.Teletype+			, Test.IOSpec.IORef+			, Test.IOSpec.Concurrent
+ LICENSE view
@@ -0,0 +1,32 @@+Copyright Wouter Swierstra 2006.++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials+      provided with the distribution.++    * Neither the name of Wouter Swierstra nor the names of other+      contributors may be used to endorse or promote products+      derived from this software without specific prior written+      permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README view
@@ -0,0 +1,31 @@+IOSpec version 0.1+  Author: Wouter Swierstra <wss@cs.nott.ac.uk>++IOSpec provides a library containing pure, executable specifications+of a few functions from the IO monad. ++Build instructions:++    $ runhaskell Setup.lhs configure+    $ runhaskell Setup.lhs build+    $ runhaskell Setup.lhs install++See http://www.haskell.org/ghc/docs/latest/html/Cabal/builders.html+for more instructions.++Documentation:++Please have a look at the latest documentation available from:+  http://www.cs.nott.ac.uk/~wss/repos/IOSpec++To build the Haddock API execute the following command:+    $ runhaskell Setup.lhs haddock++Check out the examples directory for the following examples:++    * Echo.hs - illustrates how to test the echo function.+    * Queues.hs - an implementation of queues using IORefs.+    * Channels.hs - an implementation of channels using MVars.++Every example contains quite some comments, explaining how to use+the library.
+ Setup.lhs view
@@ -0,0 +1,4 @@+#! /usr/bin/env runhaskell+ +> import Distribution.Simple+> main = defaultMain
+ examples/Channels.hs view
@@ -0,0 +1,84 @@+{-# OPTIONS_GHC -fglasgow-exts #-}+import Test.QuickCheck+import Control.Monad+import Data.Maybe (fromJust, isJust)+import Data.List (sort)+import Test.IOSpec.Concurrent+import Data.Dynamic++-- An implementation of channels using MVars. Simon Peyton Jones's+-- paper "Tackling the Awkward Squad" explains this implementation+-- of queues in a bit more detail.++data Data =  Cell Int (MVar Data) deriving Typeable++type Channel = (MVar (MVar Data), MVar (MVar Data))++newChan :: IOConc Channel+newChan = do read <- newEmptyMVar+	     write <- newEmptyMVar+	     hole <- newEmptyMVar+	     putMVar read hole+	     putMVar write hole+	     return (read,write)++putChan :: Channel -> Int -> IOConc ()+putChan (_,write) val = +  do newHole <- newEmptyMVar+     oldHole <- takeMVar write+     putMVar write newHole+     putMVar oldHole (Cell val newHole)++getChan :: Channel -> IOConc Int+getChan (read,write) = +  do headVar <- takeMVar read+     Cell val newHead <- takeMVar headVar+     putMVar read newHead+     return val++-- We can now check that data is never lost of duplicated.  We fork+-- off n threads that write an integer to a channel, together with n+-- threads that read from the channel and record the read value in+-- an MVar.  The main thread waits till all the threads have+-- successfully read a value. We can then check that the data+-- written to the channel is the same as the data read from it.++reader ::  Channel -> MVar [Int] -> IOConc ()+reader channel var =  do x <- getChan channel+                         xs <- takeMVar var+                         putMVar var (x:xs)++writer :: Channel -> Int -> IOConc ()+writer channel i = putChan channel i++chanTest :: [Int] -> IOConc [Int]+chanTest ints = do+  ch <- newChan+  result <- newEmptyMVar+  putMVar result []+  forM ints (\i -> forkIO (writer ch i)) +  replicateM (length ints) (forkIO (reader ch result))+  wait result ints ++wait :: MVar [Int] -> [Int] -> IOConc [Int]+wait var xs  = do+  res <- takeMVar var+  if length res == length xs +    then return res+    else putMVar var res >> wait var xs++-- To actually run concurrent programs, we must choose the scheduler+-- with which to run. At the moment, IOSpec provides a simple+-- round-robin scheduler; alternatively we can write our own+-- scheduler using "streamSched" that takes a stream of integers to+-- a scheduler.++-- Using QuickCheck to generate a random stream, we can use the+-- streamSched to implement a random scheduler -- thereby testing as+-- many interleavings as possible.+chanProp ints stream =+  sort (fromJust (runIOConc (chanTest ints) (streamSched stream))) +  ==  sort ints++main = do putStrLn "Testing channels..."+          quickCheck chanProp
+ examples/Echo.hs view
@@ -0,0 +1,45 @@+-- Note that the Prelude and Test.IOSpec.Teletype both export+-- functions called getChar and putChar. To begin with, we hide the+-- definitions in the prelude and work with the pure specification.++import Prelude hiding (getChar, putChar)+import qualified Data.Stream as Stream+import Test.IOSpec.Teletype+import Test.QuickCheck++-- The echo function, as we have always known it+echo :: IOTeletype ()+echo = getChar >>= putChar >> echo++-- It should echo any character entered at the teletype.  This is+-- the behaviour we would expect echo to have.  The Output data type+-- is defined in Test.IOSpec.Teletype and represents the observable+-- behaviour of a teletype interaction.+copy :: Stream.Stream Char -> Output ()+copy (Stream.Cons x xs) = Print x (copy xs)++-- An auxiliary function that takes the first n elements printed to+-- the teletype.+takeOutput :: Int -> Output () -> String+takeOutput 0 _ = ""+takeOutput (n + 1) (Print c xs) = c : takeOutput n xs++-- We can use QuickCheck to test if our echo function meets the+-- desired specification: that is that for every input the user+-- enters, every finite prefix of runTT echo input and copy input is+-- the same.+echoProp :: Int -> Stream.Stream Char -> Property+echoProp n input = +  n > 0 ==>  +    takeOutput n (runTT echo input) +    == takeOutput n (copy input)++instance Arbitrary Char where+  arbitrary = choose ('a','z')++main = do putStrLn "Testing echo..."+          quickCheck echoProp++-- Once we are satisfied with our definition of echo, we can change+-- our imports. Rather than importing Test.IOSpec.Teletype, we+-- import the "real" getChar and putChar, as defined in the Prelude.
+ examples/Queues.hs view
@@ -0,0 +1,129 @@+{-# OPTIONS_GHC -fglasgow-exts #-}+import Test.QuickCheck+import Test.IOSpec.IORef+import Data.Dynamic+import Control.Monad++-- We begin by giving an implementation of queues using our pure+-- specification of IORefs.++type Queue = (IORef Data, IORef Data)++data Data  = Cell Int (IORef Data) | NULL deriving Typeable++-- There is one important point here. To use the IORefs in IOSpec,+-- we need to make sure that any data we store in an IORef is an+-- instance of Typeable. Fortunately, GHC can derive instances of+-- Typeable for most data types.++-- The implementation of Queues is fairly standard. We use a linked+-- list, with special pointers to the head and tail of the queue.++emptyQueue :: IOState Queue+emptyQueue  = do  +  front <- newIORef NULL +  back <- newIORef NULL+  return (front,back)++enqueue :: Queue -> Int -> IOState ()+enqueue (front,back) x = +  do  newBack <- newIORef NULL+      let cell = Cell x newBack+      c <- readIORef back+      writeIORef back cell +      case c of+        NULL -> writeIORef front cell+        Cell y t -> writeIORef t cell++dequeue :: Queue -> IOState (Maybe Int)+dequeue (front,back) = do+  c <- readIORef front+  case c of+    NULL -> return Nothing+    (Cell x nextRef) -> do+      next <- readIORef nextRef+      writeIORef front next+      return (Just x)++-- Besides basic queue operations, we also implement queue reversal.++reverseQueue :: Queue -> IOState ()+reverseQueue (front,back) = do+  f <- readIORef front+  case f of+    NULL -> return ()+    Cell x nextRef -> do+      flipPointers NULL (Cell x nextRef)+      f <- readIORef front+      b <- readIORef back+      writeIORef front b+      writeIORef back f++flipPointers :: Data -> Data -> IOState ()+flipPointers prev NULL = return ()+flipPointers prev (Cell x next) = do+      nextCell <- readIORef next+      writeIORef next prev+      flipPointers (Cell x next) nextCell+    +-- A pair of functions that convert lists to queues and vice versa.++queueToList :: Queue -> IOState [Int]+queueToList = unfoldM dequeue++listToQueue :: [Int] -> IOState Queue+listToQueue xs = do q <- emptyQueue+                    sequence_ (map (enqueue q) xs)+                    return q++unfoldM :: Monad m => (a -> m (Maybe x)) -> a -> m [x]+unfoldM f a = do+  x <- f a+  case x of+    Nothing -> return []+    Just x -> liftM (x:) (unfoldM f a)++-- Now we can state a few properties of queues.++inversesProp :: [Int] -> Bool+inversesProp xs = xs == runIOState (listToQueue xs >>= queueToList)++revRevProp xs = runIOState revRevProg == xs+  where+  revRevProg = do q <- listToQueue xs+                  reverseQueue q+                  reverseQueue q+                  queueToList q++revProp xs = runIOState revProg == reverse xs+  where+  revProg = do q <- listToQueue xs+               reverseQueue q+               queueToList q++queueProp1 x = runIOState queueProg1 == Just x+  where+  queueProg1 = do q <- emptyQueue+                  enqueue q x+                  dequeue q++queueProp2 x y = runIOState queueProg2 == Just y+  where+  queueProg2 = do q <- emptyQueue+                  enqueue q x+                  enqueue q y+                  dequeue q+                  dequeue q++main = do putStrLn "Testing first queue property..."+          quickCheck queueProp1+          putStrLn "Testing second queue property..."+          quickCheck queueProp2+          putStrLn "Testing queueToList and listToQueue.."+          quickCheck inversesProp+          putStrLn "Testing that reverseQueue is its own inverse..."+          quickCheck revRevProp+          putStrLn "Testing reverseQueue matches the spec..."+          quickCheck revProp+-- Once we are satisfied with our implementation, we can import the+-- "real" Data.IORef instead of Test.IOSpec.IORef.
+ src/Data/Stream.hs view
@@ -0,0 +1,178 @@+-- | Streams are infinite lists. Most operations on streams are+-- completely analogous to the definition in Data.List.++module Data.Stream+   (+     Stream(..) +   , head +   , tail+   , intersperse +   , iterate+   , repeat+   , cycle+   , unfold +   , take+   , drop+   , splitAt+   , takeWhile+   , dropWhile+   , span+   , break+   , isPrefixOf+   , filter+   , partition+   , (!!)+   , zip+   , zipWith+   , unzip+   , words+   , unwords+   , lines+   , unlines+   , listToStream+   , streamToList+   )+   where++import Prelude hiding (head, tail, iterate, take, drop, takeWhile,+  dropWhile, repeat, cycle, filter, (!!), zip, unzip,+  zipWith,words,unwords,lines,unlines, break, span, splitAt)++import Control.Applicative+import Data.Char (isSpace)+import Test.QuickCheck++data Stream a = Cons a (Stream a) deriving (Show, Eq)++instance Functor Stream where+  fmap f (Cons x xs) = Cons (f x) (fmap f xs)++instance Applicative Stream where+  pure = repeat+  (<*>) = zipWith ($)++instance Arbitrary a => Arbitrary (Stream a) where+  arbitrary = do  x <- arbitrary+                  xs <- arbitrary+                  return (Cons x xs)+  coarbitrary = coarbitrary . streamToList++head :: Stream a -> a+head (Cons x _ ) = x++tail :: Stream a -> Stream a+tail (Cons _ xs) = xs++intersperse :: a -> Stream a -> Stream a+intersperse y (Cons x xs) = Cons x (Cons y (intersperse y xs))++unfold :: (c -> (a,c)) -> c -> Stream a+unfold f c = +  let (x,d) = f c +  in Cons x (unfold f d)+          +iterate :: (a -> a) -> a -> Stream a+iterate f x = Cons x (iterate f (f x))++take :: Int -> Stream a  -> [a]+take n (Cons x xs)+  | n == 0    = []+  | n > 0     =  x : (take (n - 1) xs)+  | otherwise = error "Stream.take: negative argument."++drop n xs+  | n == 0    = xs+  | n > 0     = drop (n - 1) (tail xs)+  | otherwise = error "Stream.drop: negative argument."++takeWhile :: (a -> Bool) -> Stream a -> [a]+takeWhile p (Cons x xs)+  | p x       = x : takeWhile p xs+  | otherwise = []++dropWhile :: (a -> Bool) -> Stream a -> Stream a+dropWhile p (Cons x xs)+  | p x       = dropWhile p xs+  | otherwise = Cons x xs++repeat :: a -> Stream a+repeat x = Cons x (repeat x)++cycle :: [a] -> Stream a+cycle xs = foldr Cons (cycle xs) xs++filter :: (a -> Bool) -> Stream a -> Stream a+filter p (Cons x xs)+  | p x       = Cons x (filter p xs)+  | otherwise = filter p xs++(!!) :: Int -> Stream a -> a+(!!) n (Cons x xs)+  | n == 0    = x+  | n > 0     = (!!) (n - 1) xs+  | otherwise = error "Stream.!! negative argument"++zip :: Stream a -> Stream b -> Stream (a,b)+zip (Cons x xs) (Cons y ys) = Cons (x,y) (zip xs ys)++unzip :: Stream (a,b) -> (Stream a, Stream b)+unzip (Cons (x,y) xys) = (Cons x (fst (unzip xys)),+                                Cons y (snd (unzip xys)))     ++zipWith :: (a -> b -> c) -> Stream a -> Stream b -> Stream c+zipWith f (Cons x xs) (Cons y ys) = Cons (f x y) (zipWith f xs ys)++span :: (a -> Bool) -> Stream a -> ([a], Stream a)+span p (Cons x xs)+  | p x       = let (trues, falses) = span p xs+                in (x : trues, falses)+  | otherwise = ([], Cons x xs)++break :: (a -> Bool) -> Stream a -> ([a], Stream a)+break p = span (not . p)++words :: Stream Char -> Stream String+words xs = let (w, ys) = break isSpace xs+                 in Cons w (words ys)++unwords :: Stream String -> Stream Char+unwords (Cons x xs) = foldr Cons (Cons ' ' (unwords xs)) x++lines :: Stream Char -> Stream String+lines xs = let (l, ys) = break (== '\n') xs+                 in Cons l (lines (tail ys))++unlines :: Stream String -> Stream Char+unlines (Cons x xs) = foldr Cons (Cons '\n' (unlines xs)) x++isPrefixOf :: Eq a => [a] -> Stream a -> Bool+isPrefixOf [] _ = True+isPrefixOf (y:ys) (Cons x xs)+  | y == x    = isPrefixOf ys xs+  | otherwise = False++partition :: (a -> Bool) -> Stream a -> (Stream a, Stream a)+partition p (Cons x xs) = +  let (trues,falses) = partition p xs+  in if p x then (Cons x trues, falses)+            else (trues, Cons x falses)++inits :: Stream a -> Stream ([a])+inits (Cons x xs) = Cons [] (fmap (x:) (inits xs))++tails :: Stream a -> Stream (Stream a)+tails xs = Cons xs (tails (tail xs))++splitAt :: Int -> Stream a -> ([a], Stream a)+splitAt n xs+  | n == 0    = ([],xs)+  | n > 0     = let (prefix,rest) = splitAt (n-1) (tail xs)+                in (head xs : prefix, rest)+  | otherwise = error "Stream.splitAt negative argument."++streamToList :: Stream a -> [a]+streamToList (Cons x xs) = x : streamToList xs++listToStream (x:xs) = Cons xs (listToStream xs)+listToStream []     = error "Stream.listToStream applied to finite list"+
+ src/Test/IOSpec.hs view
@@ -0,0 +1,10 @@+module Test.IOSpec+  (+    module Test.IOSpec.IORef+  , module Test.IOSpec.Concurrent+  , module Test.IOSpec.Teletype+  ) where++import Test.IOSpec.Concurrent+import Test.IOSpec.IORef+import Test.IOSpec.Teletype
+ src/Test/IOSpec/Concurrent.hs view
@@ -0,0 +1,282 @@+{-#  OPTIONS -fglasgow-exts -fno-warn-missing-fields  #-}+-- | A pure specification of basic concurrency operations.++module Test.IOSpec.Concurrent+   (+   -- * The IOConc monad+     IOConc+   , runIOConc+   -- * Supported functions+   , ThreadId+   , MVar+   , newEmptyMVar+   , takeMVar+   , putMVar+   , forkIO+   -- * Schedulers+   , Scheduler(..)+   , streamSched+   , roundRobin+   )+   where ++import Data.Dynamic+import Data.Maybe (fromJust)+import Data.List (nub)+import Control.Monad.State+import qualified Data.Stream as Stream++-- The IOConc data type and its instances+newtype ThreadId  = ThreadId Int deriving (Eq, Show)+type Data         = Dynamic+type Loc          = Int++data IOConc a = +     NewEmptyMVar (Loc -> IOConc a) +  |  TakeMVar Loc (Data -> IOConc a) +  |  PutMVar Loc Data (IOConc a)+  |  forall b . Fork  (IOConc b) (ThreadId -> IOConc  a)+  |  Return a ++instance Functor IOConc where +  fmap f (Return x) = Return (f x)+  fmap f (NewEmptyMVar io) = NewEmptyMVar (\l -> fmap f (io l))+  fmap f (TakeMVar l io) = TakeMVar l (\d -> fmap f (io d))+  fmap f (PutMVar l d io) = PutMVar l d (fmap f io)+  fmap f (Fork l io)      = Fork l (\tid -> fmap f (io tid))++instance Monad IOConc where+  return = Return+  (Return x) >>= g       = g x+  (NewEmptyMVar f) >>= g = NewEmptyMVar (\l -> f l >>= g)+  (TakeMVar l f) >>= g   = TakeMVar l (\d -> f d >>= g)+  PutMVar c d f >>= g    = PutMVar c d (f >>= g)+  Fork p1 p2 >>= g       = Fork p1 (\tid -> p2 tid >>= g)++-- | An 'MVar' is a shared, mutable variable.+newtype MVar a = MVar Loc deriving Typeable++-- | The 'newEmptyMVar' function creates a new 'MVar' that is initially empty.+newEmptyMVar        :: IOConc (MVar a)+newEmptyMVar        = NewEmptyMVar (Return . MVar)+ +-- | The 'takeMVar' function removes the value stored in an+-- 'MVar'. If the 'MVar' is empty, the thread is blocked.+takeMVar            :: Typeable a => MVar a -> IOConc a+takeMVar (MVar l)   = TakeMVar l (Return . unsafeFromDynamic)++-- | The 'putMVar' function fills an 'MVar' with a new value. If the+-- 'MVar' is not empty, the thread is blocked.+putMVar             :: Typeable a => MVar a -> a -> IOConc ()+putMVar (MVar l) d  = PutMVar l (toDyn d) (Return ())++-- | The 'forkIO' function forks off a new thread.+forkIO              :: IOConc a -> IOConc ThreadId +forkIO p            = Fork p Return++-- The scheduler and store++-- | A scheduler consists of a function that, given the number of+-- threads, returns the 'ThreadId' of the next scheduled thread,+-- together with a new scheduler.+newtype Scheduler = +  Scheduler (Int -> (ThreadId, Scheduler))++data ThreadStatus = +     forall b . Running (IOConc b) +  |  Finished++type Heap = Loc -> Maybe Data++data Store   = Store    {  fresh :: Loc+                        ,  heap :: Heap+                        ,  nextTid :: ThreadId+                        ,  soup :: ThreadId -> ThreadStatus+                        ,  scheduler :: Scheduler+                        ,  blockedThreads :: [ThreadId]+                        }++initStore :: Scheduler -> Store+initStore s   = Store  {   fresh    = 0 +                        ,  nextTid   = ThreadId 1+                        ,  scheduler = s+                        ,  blockedThreads = []+                        }++-- | The 'runIOConc' function runs a concurrent computation with a given scheduler.+-- If a deadlock occurs, Nothing is returned.++runIOConc :: IOConc a -> Scheduler -> Maybe a+runIOConc io s = evalState (interleave io) (initStore s)++-- A single step++data Status a = Stop a | Step (IOConc a) | Blocked ++step ::  IOConc a -> State Store (Status a)+step (Return a) = return (Stop a)+step (NewEmptyMVar f)+  = do  loc <- alloc+        modifyHeap (update loc Nothing)+        return (Step (f loc))+step (TakeMVar l f)  +  = do  var <- lookupHeap l+        case var of+          Nothing   ->  return Blocked+          (Just d)  ->  do  emptyMVar l+                            return (Step (f d))+step (PutMVar l d p)   +  = do  var <- lookupHeap l+        case var of+          Nothing   ->  do  fillMVar l d+                            return (Step p)+          (Just d)  ->  return Blocked+step (Fork l r)        +  = do  tid <- freshThreadId+        extendSoup l tid+        return (Step (r tid))++emptyMVar :: Loc -> State Store ()+emptyMVar l = modifyHeap (update l Nothing)++fillMVar :: Loc -> Data -> State Store ()+fillMVar l d = modifyHeap (update l (Just d))++extendSoup :: IOConc a -> ThreadId -> State Store () +extendSoup p tid = modifySoup (update tid (Running p))++-- Interleaving steps++data Process a = +     Main (IOConc a)+  |  forall b . Aux (IOConc b)++interleave :: IOConc a -> State Store (Maybe a)+interleave main  +  = do  (tid,t) <- schedule main+        case t of+          Main p -> +            do  x <- step p+                case x of+                  Stop r   ->  return (Just r)+                  Step p   ->  do resetBlockedThreads+                                  interleave p+                  Blocked  ->  do isDeadlock <- detectDeadlock+                                  if isDeadlock +                                    then return Nothing+                                    else interleave main+          Aux p -> +            do  x <- step p+                case x of+                  Stop _   ->   do  resetBlockedThreads+                                    finishThread tid+                                    interleave main+                  Step q   ->   do  resetBlockedThreads+                                    extendSoup q tid+                                    interleave main+                  Blocked  ->   do  recordBlockedThread tid+                                    interleave main++schedule :: IOConc a -> State Store (ThreadId, Process a)+schedule main = do  (ThreadId tid) <- getNextThreadId+                    if tid == 0 +                      then return (ThreadId 0, Main main)+                      else do+                        tsoup <- gets soup+                        case tsoup (ThreadId tid) of+                          Finished ->  schedule main+                          Running p -> return (ThreadId tid, Aux p)+                          ++getNextThreadId :: State Store ThreadId+getNextThreadId = do  Scheduler sch <- gets scheduler+                      (ThreadId n) <- gets nextTid+                      let (tid,s) = sch n+                      modifyScheduler (const s)+                      return tid+++-- | Given a stream of integers, 'streamSched' builds a+-- scheduler. This is especially useful if you use QuickCheck and+-- generate a random stream; the resulting random scheduler will+-- hopefully cover a large number of interleavings.++streamSched :: Stream.Stream Int -> Scheduler+streamSched xs = +  Scheduler (\k -> (ThreadId (Stream.head xs `mod` k), streamSched (Stream.tail xs)))+++-- | A simple round-robin scheduler.+roundRobin :: Scheduler+roundRobin = streamSched (Stream.unfold (\k -> (k, k+1)) 0)++-- Utilities++freshThreadId :: State Store ThreadId+freshThreadId = do tid <- gets nextTid+                   modifyTid (\(ThreadId k) -> ThreadId (k + 1))+                   return tid++alloc :: State Store Loc +alloc = do  loc <- gets fresh+            modifyFresh ((+) 1)+            return loc++lookupHeap :: Loc -> State Store (Maybe Data)+lookupHeap l = do  h <- gets heap+                   return (h l)++extendHeap :: Loc -> Data -> State Store ()+extendHeap l d  = modifyHeap (update l (Just d))++finishThread :: ThreadId -> State Store ()+finishThread tid = modifySoup (update tid Finished)++resetBlockedThreads :: State Store ()+resetBlockedThreads = modifyBlockedThreads (const [])++recordBlockedThread :: ThreadId -> State Store ()+recordBlockedThread tid = do +  tids <- gets blockedThreads+  if tid `elem` tids +    then return ()+    else modifyBlockedThreads (tid :)++detectDeadlock :: State Store Bool+detectDeadlock = do blockedThreads <- liftM length (gets blockedThreads)                   +                    (ThreadId nrThreads) <- gets nextTid+                    threadSoup <- gets soup+                    let allThreadIds = [ThreadId x | x <- [1 .. (nrThreads - 1)]]+                    let finishedThreads = length $ filter isFinished (map threadSoup allThreadIds)+                    return (blockedThreads + finishedThreads == nrThreads - 1)++isFinished :: ThreadStatus -> Bool+isFinished Finished = True+isFinished _        = False+                       ++update :: Eq a => a -> b -> (a -> b) -> (a -> b)+update l d h k+  | l == k       = d+  | otherwise    = h k++unsafeFromDynamic :: Typeable a => Dynamic -> a+unsafeFromDynamic = fromJust . fromDynamic++modifyHeap f            = do s <- get+                             put (s {heap = f (heap s)})++modifyScheduler f       = do s <- get+                             put (s {scheduler = f (scheduler s)})++modifyFresh f           = do s <- get+                             put (s {fresh = f (fresh s)})++modifyTid f             = do s <- get+                             put (s {nextTid = f (nextTid s)})+ +modifySoup f            = do s <- get+                             put (s {soup = f (soup s)})++modifyBlockedThreads f     = do s <- get+                                put (s {blockedThreads = f (blockedThreads s)})
+ src/Test/IOSpec/IORef.hs view
@@ -0,0 +1,116 @@++{-#  OPTIONS -fglasgow-exts -fno-warn-missing-fields  #-}++-- | A pure specification of mutable variables. +module Test.IOSpec.IORef +   (+    -- * The IOState monad+     IOState+   , runIOState+    -- * Manipulation of IORefs+   , IORef+   , newIORef+   , readIORef+   , writeIORef+   , modifyIORef+   ) +   where++import Control.Monad.State +import Data.Dynamic+import Data.Maybe (fromJust)++type Data           = Dynamic+type Loc            = Int++-- | The IOState monad++data IOState a  = +     NewIORef Data (Loc -> IOState a) +  |  ReadIORef Loc (Data -> IOState a)+  |  WriteIORef Loc Data (IOState  a) +  |  Return a ++instance Functor IOState where+  fmap f (NewIORef d io)     = NewIORef d (\l -> fmap f (io l))+  fmap f (ReadIORef l io)    = ReadIORef l (\d -> fmap f (io d))+  fmap f (WriteIORef l d io) = WriteIORef l d (fmap f io)+  fmap f (Return x)     = Return (f x)++instance Monad IOState where+  return                    = Return+  (Return a) >>= g          = g a+  (NewIORef d f) >>= g      = NewIORef d (\l -> f l >>= g)+  (ReadIORef l f) >>= g     = ReadIORef l (\d -> f d >>= g)+  (WriteIORef l d s) >>= g  = WriteIORef l d (s >>= g)++-- | A mutable variable in the IOState monad+newtype IORef a = IORef Loc++-- | The 'newIORef' function creates a new mutable variable.+newIORef :: Typeable a => a -> IOState (IORef a)+newIORef d = NewIORef (toDyn d) (Return . IORef)++-- | The 'readIORef' function reads the value stored in a mutable variable.+readIORef :: Typeable a => IORef a -> IOState a+readIORef (IORef l) = ReadIORef l (Return . unsafeFromDynamic)++-- | The 'writeIORef' function overwrites the value stored in an IORef.+writeIORef :: Typeable a => IORef a -> a -> IOState ()+writeIORef (IORef l) d = WriteIORef l (toDyn d) (Return ())++-- | The 'modifyIORef' function applies a function to the value stored in +-- and IORef.+modifyIORef :: Typeable a => IORef a -> (a -> a) -> IOState ()+modifyIORef ref f = readIORef ref >>= \x -> writeIORef ref (f x)++unsafeFromDynamic :: Typeable a => Dynamic -> a+unsafeFromDynamic = fromJust . fromDynamic++data Store = Store {fresh :: Loc, heap :: Heap}+type Heap = Loc -> Data ++emptyStore :: Store+emptyStore = Store {fresh = 0}++-- | The 'runIOState' function executes a computation in the `IOState' monad.+runIOState :: IOState a -> a+runIOState io = evalState (step io) emptyStore++step :: IOState a -> State Store a+step (Return a) = return a+step (NewIORef d g)      +  = do  loc <- alloc+        extendHeap loc d+        step (g loc) +step (ReadIORef l g)     +  = do  d <- lookupHeap l+        step (g d)+step (WriteIORef l d p)+  = do  extendHeap l d+        step p++alloc :: State Store Loc +alloc = do  loc <- gets fresh+            modifyFresh ((+) 1)+            return loc++lookupHeap :: Loc -> State Store Data+lookupHeap l = do  h <- gets heap+                   return (h l)++extendHeap :: Loc -> Data -> State Store ()+extendHeap l d  = modifyHeap (update l d)++modifyHeap :: (Heap -> Heap) -> State Store ()+modifyHeap f = do  s <- get+                   put (s {heap = f (heap s)})++modifyFresh :: (Loc -> Loc) -> State Store ()+modifyFresh f = do  s <- get+                    put (s {fresh = f (fresh s)})++update :: Loc -> Data -> Heap -> Heap+update l d h k+  | l == k       = d+  | otherwise    = h k
+ src/Test/IOSpec/Teletype.hs view
@@ -0,0 +1,60 @@+-- | A pure implementation of getChar and putChar.++module Test.IOSpec.Teletype+   (+   -- * The IOTeletype monad+     IOTeletype+   , Output(..)+   , runTT+   -- * Pure getChar and putChar+   , getChar+   , putChar+   ) +   where++import qualified Data.Stream as Stream+import Prelude hiding (getChar, putChar)++-- | The IOTeletype monad+data IOTeletype a = +     GetChar (Char -> IOTeletype a)+  |  PutChar Char (IOTeletype a)+  |  ReturnTeletype a++instance Functor IOTeletype where+  fmap f (GetChar tt)       = GetChar (\x -> fmap f (tt x))+  fmap f (PutChar c tt)     = PutChar c (fmap f tt)+  fmap f (ReturnTeletype x) = ReturnTeletype (f x)++instance Monad IOTeletype where+  return = ReturnTeletype+  (ReturnTeletype a)  >>= g     = g a+  (GetChar f)         >>= g     = GetChar (\c -> f c >>= g)+  (PutChar c a)       >>= g     = PutChar c (a >>= g)+++-- | Once you have constructed something of type 'IOTeletype' you+-- can run the interaction. If you pass in a stream of characters+-- entered at the teletype, it will produce a value of type 'Output'+runTT :: IOTeletype a -> Stream.Stream Char -> Output a+runTT (ReturnTeletype a) cs  = Finish a+runTT (GetChar f) cs         = runTT (f (Stream.head cs)) (Stream.tail cs)+runTT (PutChar c p) cs       = Print c (runTT p cs)++-- | The result of running a teletype interation is a (potentially+-- infinite) list of characters, that are printed to the screen. The+-- interaction can also end, and return a final value, using the+-- 'Finish' constructor.+data Output a = +     Print Char (Output a) +  |  Finish a+++-- | The getChar function can be used to read input from the teletype.+getChar    ::  IOTeletype Char +getChar    =   GetChar ReturnTeletype++-- | The getChar function can be used to print to the teletype.+putChar    ::  Char -> IOTeletype () +putChar c  =   PutChar c (ReturnTeletype ())+