diff --git a/IOSpec.cabal b/IOSpec.cabal new file mode 100644 --- /dev/null +++ b/IOSpec.cabal @@ -0,0 +1,32 @@ +Name: IOSpec +Version: 0.1 +License: BSD3 +License-file: LICENSE +Author: Wouter Swierstra +Maintainer: Wouter Swierstra +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 diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -0,0 +1,31 @@ +IOSpec version 0.1 + Author: Wouter Swierstra + +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. diff --git a/Setup.lhs b/Setup.lhs new file mode 100644 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,4 @@ +#! /usr/bin/env runhaskell + +> import Distribution.Simple +> main = defaultMain diff --git a/examples/Channels.hs b/examples/Channels.hs new file mode 100644 --- /dev/null +++ b/examples/Channels.hs @@ -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 diff --git a/examples/Echo.hs b/examples/Echo.hs new file mode 100644 --- /dev/null +++ b/examples/Echo.hs @@ -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. diff --git a/examples/Queues.hs b/examples/Queues.hs new file mode 100644 --- /dev/null +++ b/examples/Queues.hs @@ -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. diff --git a/src/Data/Stream.hs b/src/Data/Stream.hs new file mode 100644 --- /dev/null +++ b/src/Data/Stream.hs @@ -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" + diff --git a/src/Test/IOSpec.hs b/src/Test/IOSpec.hs new file mode 100644 --- /dev/null +++ b/src/Test/IOSpec.hs @@ -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 diff --git a/src/Test/IOSpec/Concurrent.hs b/src/Test/IOSpec/Concurrent.hs new file mode 100644 --- /dev/null +++ b/src/Test/IOSpec/Concurrent.hs @@ -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)}) diff --git a/src/Test/IOSpec/IORef.hs b/src/Test/IOSpec/IORef.hs new file mode 100644 --- /dev/null +++ b/src/Test/IOSpec/IORef.hs @@ -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 diff --git a/src/Test/IOSpec/Teletype.hs b/src/Test/IOSpec/Teletype.hs new file mode 100644 --- /dev/null +++ b/src/Test/IOSpec/Teletype.hs @@ -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 ()) +