diff --git a/IOSpec.cabal b/IOSpec.cabal --- a/IOSpec.cabal +++ b/IOSpec.cabal @@ -1,32 +1,64 @@ Name: IOSpec -Version: 0.1.1 +Version: 0.2 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: +Description: This package consists of several modules, that give a + pure specification of functions in the IO monad: . - * "Test.IOSpec.Teletype": a specification of getChar and putChar. + * "Test.IOSpec.Fork": a pure specification of + 'forkIO'. . - * "Test.IOSpec.IORef": a specification of most functions on IORefs. + * "Test.IOSpec.IORef": a pure specification of most + functions that create and manipulate on 'IORefs'. . - * "Test.IOSpec.Concurrent": specification of forkIO and MVars. + * "Test.IOSpec.MVar": a pure specification of most + functions that create and manipulate and 'MVars'. . - * "Data.Stream": a library for manipulating infinite lists. + * "Test.IOSpec.STM": a pure specification of + 'atomically' and the 'STM' monad. . - There are several well-documented examples included with the source distribution. + * "Test.IOSpec.Teletype": a pure specification of + 'getChar', 'putChar', and several related + Prelude functions. + . + Besides these modules containing the specifications, + there are a few other important modules: + . + * "Test.IOSpec.Types": defines the 'IOSpec' type and + several amenities. + . + * "Test.IOSpec.VirtualMachine": defines a virtual + machine on which to execute pure specifications. + . + * "Test.IOSpec.Surrogate": a drop-in replacement for + the other modules. Import this and recompile your + code once you've finished testing and debugging. + . + There are several well-documented examples included + with the source distribution. Category: Testing -Build-Depends: base, mtl, QuickCheck +Build-Type: Simple +Build-Depends: base, mtl, QuickCheck < 2.0, Stream +Extensions: MultiParamTypeClasses +Ghc-options: -Wall -fglasgow-exts Hs-source-dirs: src Extra-source-files: README + , examples/Channels.hs , examples/Echo.hs , examples/Queues.hs - , examples/Channels.hs -Exposed-modules: Data.Stream - , Test.IOSpec - , Test.IOSpec.Teletype + , examples/Refs.hs + , examples/Sudoku.hs +Exposed-modules: Test.IOSpec + , Test.IOSpec.Fork , Test.IOSpec.IORef - , Test.IOSpec.Concurrent + , Test.IOSpec.MVar + , Test.IOSpec.STM + , Test.IOSpec.Surrogate + , Test.IOSpec.Teletype + , Test.IOSpec.Types + , Test.IOSpec.VirtualMachine + diff --git a/README b/README --- a/README +++ b/README @@ -1,4 +1,4 @@ -IOSpec version 0.1 +IOSpec version 0.2 Author: Wouter Swierstra IOSpec provides a library containing pure, executable specifications @@ -21,11 +21,15 @@ To build the Haddock API execute the following command: $ runhaskell Setup.lhs haddock +This will require Haddock 2.0 + 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. + * Sudoku.hs - a parallel Sudoku solver that uses STM and MVars + based on Graham Hutton's version of Richard Bird's "Solving Sudoku". Every example contains quite some comments, explaining how to use the library. diff --git a/examples/Channels.hs b/examples/Channels.hs --- a/examples/Channels.hs +++ b/examples/Channels.hs @@ -3,7 +3,7 @@ import Control.Monad import Data.Maybe (fromJust, isJust) import Data.List (sort) -import Test.IOSpec.Concurrent +import Test.IOSpec hiding (Data,putStrLn) import Data.Dynamic -- An implementation of channels using MVars. Simon Peyton Jones's @@ -14,6 +14,8 @@ type Channel = (MVar (MVar Data), MVar (MVar Data)) +type IOConc a = IOSpec (MVarS :+: ForkS) a + newChan :: IOConc Channel newChan = do read <- newEmptyMVar write <- newEmptyMVar @@ -23,14 +25,14 @@ return (read,write) putChan :: Channel -> Int -> IOConc () -putChan (_,write) val = +putChan (_,write) val = do newHole <- newEmptyMVar oldHole <- takeMVar write putMVar write newHole putMVar oldHole (Cell val newHole) getChan :: Channel -> IOConc Int -getChan (read,write) = +getChan (read,write) = do headVar <- takeMVar read Cell val newHead <- takeMVar headVar putMVar read newHead @@ -56,17 +58,24 @@ ch <- newChan result <- newEmptyMVar putMVar result [] - forM ints (\i -> forkIO (writer ch i)) + forM ints (\i -> forkIO (writer ch i)) replicateM (length ints) (forkIO (reader ch result)) - wait result ints + wait result ints wait :: MVar [Int] -> [Int] -> IOConc [Int] wait var xs = do res <- takeMVar var - if length res == length xs + if length res == length xs then return res else putMVar var res >> wait var xs + +-- When do we consider two Effects equal? In this case, we want the +-- same final result, and no other visible effects. +(===) :: Eq a => Effect a -> Effect a -> Bool +Done x === Done y = x == y +_ === _ = False + -- 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 @@ -76,9 +85,10 @@ -- 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 +chanProp :: [Int] -> Scheduler -> Bool +chanProp ints sched = + fmap sort (evalIOSpec (chanTest ints) sched) + === Done (sort ints) main = do putStrLn "Testing channels..." quickCheck chanProp diff --git a/examples/Echo.hs b/examples/Echo.hs --- a/examples/Echo.hs +++ b/examples/Echo.hs @@ -3,42 +3,56 @@ -- definitions in the prelude and work with the pure specification. import Prelude hiding (getChar, putChar) +import qualified Prelude (putStrLn) import qualified Data.Stream as Stream -import Test.IOSpec.Teletype +import Test.IOSpec hiding (putStrLn) import Test.QuickCheck +import Data.Char (ord) -- The echo function, as we have always known it -echo :: IOTeletype () +echo :: IOSpec Teletype () 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) +copy :: Effect () +copy = ReadChar (\x -> Print x copy) -- An auxiliary function that takes the first n elements printed to -- the teletype. -takeOutput :: Int -> Output () -> String +takeOutput :: Int -> Effect () -> String takeOutput 0 _ = "" takeOutput (n + 1) (Print c xs) = c : takeOutput n xs +takeOutput _ _ = error "Echo.takeOutput" +-- withInput runs an Effect, passing the argument stream of +-- characters as the characters entered to stdin. Any effects left +-- over will be either Print statements, or a final Done result. +withInput :: Stream.Stream Char -> Effect a -> Effect a +withInput stdin (Done x) = Done x +withInput stdin (Print c e) = Print c (withInput stdin e) +withInput stdin (ReadChar f) = withInput (Stream.tail stdin) + (f (Stream.head stdin)) + -- 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) +echoProp n input = + n > 0 ==> + takeOutput n (withInput input (evalIOSpec echo singleThreaded)) + == takeOutput n (withInput input copy) instance Arbitrary Char where arbitrary = choose ('a','z') + coarbitrary = variant . ord -main = do putStrLn "Testing echo..." - quickCheck echoProp +main = do + Prelude.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 diff --git a/examples/Queues.hs b/examples/Queues.hs --- a/examples/Queues.hs +++ b/examples/Queues.hs @@ -1,15 +1,17 @@ {-# OPTIONS_GHC -fglasgow-exts #-} import Test.QuickCheck -import Test.IOSpec.IORef +import Test.IOSpec hiding (putStrLn) +import Prelude hiding (putStrLn) +import qualified Prelude (putStrLn) 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) +type Queue = (IORef Cell, IORef Cell) -data Data = Cell Int (IORef Data) | NULL deriving Typeable +data Cell = Cell Int (IORef Cell) | 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 @@ -19,23 +21,23 @@ -- 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 +emptyQueue :: IOSpec IORefS Queue +emptyQueue = do + front <- newIORef NULL back <- newIORef NULL return (front,back) -enqueue :: Queue -> Int -> IOState () -enqueue (front,back) x = +enqueue :: Queue -> Int -> IOSpec IORefS () +enqueue (front,back) x = do newBack <- newIORef NULL let cell = Cell x newBack c <- readIORef back - writeIORef back cell + writeIORef back cell case c of NULL -> writeIORef front cell Cell y t -> writeIORef t cell -dequeue :: Queue -> IOState (Maybe Int) +dequeue :: Queue -> IOSpec IORefS (Maybe Int) dequeue (front,back) = do c <- readIORef front case c of @@ -47,7 +49,7 @@ -- Besides basic queue operations, we also implement queue reversal. -reverseQueue :: Queue -> IOState () +reverseQueue :: Queue -> IOSpec IORefS () reverseQueue (front,back) = do f <- readIORef front case f of @@ -59,19 +61,19 @@ writeIORef front b writeIORef back f -flipPointers :: Data -> Data -> IOState () +flipPointers :: Cell -> Cell -> IOSpec IORefS () 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 :: Queue -> IOSpec IORefS [Int] queueToList = unfoldM dequeue -listToQueue :: [Int] -> IOState Queue +listToQueue :: [Int] -> IOSpec IORefS Queue listToQueue xs = do q <- emptyQueue sequence_ (map (enqueue q) xs) return q @@ -83,31 +85,46 @@ Nothing -> return [] Just x -> liftM (x:) (unfoldM f a) --- Now we can state a few properties of queues. +-- When do we consider two Effects equal? In this case, we want the +-- same final result, and no other visible effects. +(===) :: Eq a => Effect a -> Effect a -> Bool +Done x === Done y = x == y +_ === _ = False +-- Now we can state a few properties of queues. inversesProp :: [Int] -> Bool -inversesProp xs = xs == runIOState (listToQueue xs >>= queueToList) +inversesProp xs = + (return xs) === evalIOSpec (listToQueue xs >>= queueToList) singleThreaded -revRevProp xs = runIOState revRevProg == xs +revRevProp xs = evalIOSpec revRevProg singleThreaded === return xs where revRevProg = do q <- listToQueue xs reverseQueue q reverseQueue q queueToList q -revProp xs = runIOState revProg == reverse xs +revProp xs = evalIOSpec revProg singleThreaded === return (reverse xs) where revProg = do q <- listToQueue xs reverseQueue q queueToList q -queueProp1 x = runIOState queueProg1 == Just x +fifoProp :: [Int] -> Bool +fifoProp xs = evalIOSpec enqDeq singleThreaded === return xs where + enqDeq :: IOSpec IORefS [Int] + enqDeq = do + q <- emptyQueue + forM_ xs (enqueue q) + unfoldM dequeue q + +queueProp1 x = evalIOSpec queueProg1 singleThreaded === Done (Just x) + where queueProg1 = do q <- emptyQueue enqueue q x dequeue q -queueProp2 x y = runIOState queueProg2 == Just y +queueProp2 x y = evalIOSpec queueProg2 singleThreaded === Done (Just y) where queueProg2 = do q <- emptyQueue enqueue q x @@ -115,15 +132,15 @@ dequeue q dequeue q -main = do putStrLn "Testing first queue property..." +main = do Prelude.putStrLn "Testing first queue property..." quickCheck queueProp1 - putStrLn "Testing second queue property..." + Prelude.putStrLn "Testing second queue property..." quickCheck queueProp2 - putStrLn "Testing queueToList and listToQueue.." + Prelude.putStrLn "Testing queueToList and listToQueue.." quickCheck inversesProp - putStrLn "Testing that reverseQueue is its own inverse..." + Prelude.putStrLn "Testing that reverseQueue is its own inverse..." quickCheck revRevProp - putStrLn "Testing reverseQueue matches the spec..." + Prelude.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/examples/Refs.hs b/examples/Refs.hs new file mode 100644 --- /dev/null +++ b/examples/Refs.hs @@ -0,0 +1,23 @@ +import Test.IOSpec +import Test.QuickCheck + +readOnce :: Int -> IOSpec IORefS Int +readOnce x = do ref <- newIORef x + readIORef ref + +readTwice :: Int -> IOSpec IORefS Int +readTwice x = do ref <- newIORef x + readIORef ref + readIORef ref + +readIORefProp :: Int -> Bool +readIORefProp x = + let once = evalIOSpec (readOnce x) singleThreaded + twice = evalIOSpec (readTwice x) singleThreaded + in once == twice + +main = quickCheck readIORefProp + +instance Eq a => Eq (Effect a) where + (Done x) == (Done y) = x == y + _ == _ = error "Incomparable effects." diff --git a/examples/Sudoku.hs b/examples/Sudoku.hs new file mode 100644 --- /dev/null +++ b/examples/Sudoku.hs @@ -0,0 +1,316 @@ +{-# OPTIONS_GHC -fglasgow-exts #-} + +-- Based on Graham Hutton's version of Richard Bird's Sudoku solver. +module Main where + +import Data.List +import Control.Monad + +-- Import these modules to test +import Test.IOSpec hiding (putStrLn) +import Test.QuickCheck + +-- Drop the test modules and import these when you want to release +-- import Control.Concurrent +-- import Control.Concurrent.STM + +type Grid = Matrix Value +type Matrix a = [Row a] +type Row a = [TVar a] +type Value = Char + +data Sudoku = Sudoku [[Value]] deriving (Eq,Show) + +type Concurrency = STMS :+: ForkS :+: MVarS + +-- Some pure amenities + +-- The size of the board +boxsize :: Int +boxsize = 3 + +-- The possible values of a cell +values :: [Value] +values = ['1'..'9'] + +-- A dummy value representing the empty cell +empty :: Value -> Bool +empty = (== '.') + +-- When is a cell filled in or not +single :: [a] -> Bool +single [_] = True +single _ = False + +-- Some functions that return a list of nine rows, columns, or +-- boxes of a grid. +chop :: Int -> [a] -> [[a]] +chop n [] = [] +chop n xs = take n xs : chop n (drop n xs) + +rows :: [[a]] -> [[a]] +rows = id + +cols :: [[a]] -> [[a]] +cols = transpose + +boxes :: [[a]] -> [[a]] +boxes = unpack . map cols . pack + where + pack = split . map split + split = chop boxsize + unpack = map concat . concat + +-- When does a list have no duplicates +nodups :: Eq a => [a] -> Bool +nodups [] = True +nodups (x:xs) = not (elem x xs) && nodups xs + +-- collapse takes a Grid where every cell contains a list of +-- possibilities, to a list of Grids where every cell contains a +-- single value. +collapse :: [[[a]]] -> [[[a]]] +collapse = cp . map cp + +-- cartesian product of a list of lists +cp :: [[a]] -> [[a]] +cp [] = [[]] +cp (xs:xss) = [y:ys | y <- xs, ys <- cp xss] + +-- The choices function reads in a Sudoku grid, replacing each +-- unknown entry by a TVar containing ['1' .. '9'] and each fixed +-- entry x by a TVar containing [x]. +type Choices = [Value] + +choices :: [[Value]] -> STM (Matrix Choices) +choices vs = mapM (mapM choice) vs + +choice :: Value -> STM (TVar [Value]) +choice v = do + newTVar $ + if empty v + then values + else return v + +-- find all the digits that have been filled in +findSingles :: Row Choices -> STM [Value] +findSingles [] = return [] +findSingles (xs:xss) = do + v <- readTVar xs + ss <- findSingles xss + if single v then return (v ++ ss) + else return ss + +-- cross off all the digits that have been filled in +reduce :: Row Choices -> STM () +reduce row = do + singles <- findSingles row + mapM_ (removeSingles singles) row + +removeSingles :: Choices -> TVar Choices -> STM () +removeSingles singles var = do + v <- readTVar var + writeTVar var (v `minus` singles) + +-- the prune function prunes the search space, e.g. removing '9' +-- from the cells in a row/column/box if there is already a cell +-- with a '9' in said row/column/box. Using STM makes the +-- concurrency here quite neat - we can prune the rows, columns, and +-- boxes at the same time. +prune :: Matrix Choices -> IOSpec Concurrency () +prune ms = do + rowsDone <- newEmptyMVar + colsDone <- newEmptyMVar + boxesDone <- newEmptyMVar + forkIO (pruneBy rowsDone rows ms) + forkIO (pruneBy colsDone cols ms) + forkIO (pruneBy boxesDone boxes ms) + takeMVar rowsDone + takeMVar colsDone + takeMVar boxesDone + +pruneBy :: MVar () -> (Matrix Choices -> Matrix Choices) + -> Matrix Choices -> IOSpec Concurrency () +pruneBy mvar f m = do + atomically $ mapM_ reduce (f m) + putMVar mvar () + +-- When is a matrix completely filled in? +complete :: Matrix Choices -> STM Bool +complete m = liftM (all (all single)) (mapM (mapM readTVar) m) + +-- When are we 'stuck', i.e. when there is a cell with no possible +-- choices left. +void :: Matrix Choices -> STM Bool +void m = liftM (any (any null)) (mapM (mapM readTVar) m) + +minus :: Choices -> Choices -> Choices +xs `minus` ys = if single xs then xs else xs \\ ys + +-- A board is consistent if there are no duplicates in every row, +-- column, and box. +isInconsistent :: Matrix Choices -> STM Bool +isInconsistent cm = do + rowC <- liftM (all consistent) (mapM (mapM readTVar) (rows cm)) + colC <- liftM (all consistent) (mapM (mapM readTVar) (cols cm)) + boxC <- liftM (all consistent) (mapM (mapM readTVar) (boxes cm)) + return (not (rowC && colC && boxC)) + +consistent :: [[Value]] -> Bool +consistent = nodups . concat . filter single + +-- A board is blocked if it is void or inconsistent +blocked :: Matrix Choices -> STM Bool +blocked m = liftM2 (||) (void m) (isInconsistent m) + +-- The search function checks +-- +-- * if the board is blocked, we cannot make any progress in this +-- thread +-- +-- * if the board is complete, we are done and fill in the MVar +-- waiting for the result. +-- +-- * otherwise, expand the cell with the smallest number of +-- remaining choices to make a list of boards, corresponding to the +-- possible ways to fill in that cell. We then fork off a thread to +-- try and find a solution for every board in that list. +search :: MVar [[Value]] -> Matrix Choices -> IOSpec Concurrency () +search mvar m = do + isBlocked <- atomically $ blocked m + isComplete <- atomically $ complete m + if isBlocked + then return () + else + if isComplete + then do + result <- atomically $ liftM collapse (mapM (mapM readTVar) m) + putMVar mvar (head result) + else do + ms <- expand m + mapM_ (\m -> forkIO (prune m >> search mvar m)) ms + +expand :: Matrix Choices -> IOSpec Concurrency ([Matrix Choices]) +expand matrix = do + ms <- atomically $ mapM (mapM readTVar) matrix + let mms = expand' ms + atomically $ mapM (mapM (mapM newTVar)) mms + +expand' :: [[Choices]] -> [[[Choices]]] +expand' m = + [rows1 ++ [row1 ++ [c] : row2] ++ rows2 | c <- cs] + where + (rows1,row:rows2) = break (any p) m + (row1,cs:row2) = break p row + p xs = length xs == minLength + minLength = minimum (filter (> 1) (concatMap (map length) m)) + + +-- The solve function makes an empty MVar, reads in the board, +-- prunes it, and searches for solutions. Once a solution is found, +-- it will be written to the MVar and returned. +solve :: Sudoku -> IOSpec Concurrency Sudoku +solve (Sudoku grid) = do + solution <- newEmptyMVar + matrix <- atomically $ choices grid + prune matrix + search solution matrix + sol <- takeMVar solution + return (Sudoku sol) + + +-- Examples +easy :: Sudoku +easy = Sudoku + ["2....1.38", + "........5", + ".7...6...", + ".......13", + ".981..257", + "31....8..", + "9..8...2.", + ".5..69784", + "4..25...."] + +gentle :: Sudoku +gentle = Sudoku + [".1.42...5", + "..2.71.39", + ".......4.", + "2.71....6", + "....4....", + "6....74.3", + ".7.......", + "12.73.5..", + "3...82.7."] + +diabolical :: Sudoku +diabolical = Sudoku + [".9.7..86.", + ".31..5.2.", + "8.6......", + "..7.5...6", + "...3.7...", + "5...1.7..", + "......1.9", + ".2.6..35.", + ".54..8.7."] + +solution :: [[Value]] +solution = ["295743861", + "431865927", + "876192543", + "387459216", + "612387495", + "549216738", + "763524189", + "928671354", + "154938672"] + +-- Given a sudoku puzzle, solve it and check that your solution is ok. +unsolved :: Sudoku -> Int +unsolved (Sudoku xs) = length $ filter (== '.') (concat xs) + +correctProp sudoku sched = + let + (Done computed) = evalIOSpec (solve sudoku) sched + in collect (unsolved sudoku) (isSolution computed) + +-- Determines when a sudoku has been filled in properly. +isSolution :: Sudoku -> Bool +isSolution (Sudoku grid) = + isOk (boxes grid) && isOk (cols grid) && isOk (rows grid) + where + isOk xss = all (== values) (map sort xss) + +-- To generate a random sudoku puzzle, we delete a number of cells +-- from a solved grid. +instance Arbitrary Sudoku where + arbitrary = do + xs <- arbitrary + return (Sudoku $ blankOut xs (concat solution)) + coarbitrary = error "No instance coarbitrary for Sudoku grids" + +blankOut :: [Int] -> [Value] -> [[Value]] +blankOut [] grid = chop (boxsize * boxsize) grid +blankOut (x:xs) grid = + let + y = x `mod` 81 + in blankOut xs (replace y '.' grid) + +replace :: Eq a => Int -> a -> [a] -> [a] +replace n x xs = take n xs ++ [x] ++ drop (n+1) xs + +main = do + putStrLn "Running QuickCheck tests..." + -- A few unit tests + putStrLn "Solving easy..." + quickCheck (correctProp easy) + putStrLn "Solving gentle..." + quickCheck (correctProp gentle) + putStrLn "Solving diabolical..." + quickCheck (correctProp diabolical) +-- -- QuickCheck the solver + putStrLn "Solving random tests..." + quickCheck correctProp + diff --git a/src/Data/Stream.hs b/src/Data/Stream.hs deleted file mode 100644 --- a/src/Data/Stream.hs +++ /dev/null @@ -1,178 +0,0 @@ --- | 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 --- a/src/Test/IOSpec.hs +++ b/src/Test/IOSpec.hs @@ -1,10 +1,21 @@ module Test.IOSpec ( - module Test.IOSpec.IORef - , module Test.IOSpec.Concurrent +-- * The specifications + module Test.IOSpec.Fork + , module Test.IOSpec.MVar + , module Test.IOSpec.IORef + , module Test.IOSpec.STM , module Test.IOSpec.Teletype +-- * The basic types + , module Test.IOSpec.Types +-- * The virtual machine + , module Test.IOSpec.VirtualMachine ) where -import Test.IOSpec.Concurrent +import Test.IOSpec.Fork +import Test.IOSpec.MVar import Test.IOSpec.IORef +import Test.IOSpec.STM import Test.IOSpec.Teletype +import Test.IOSpec.Types +import Test.IOSpec.VirtualMachine diff --git a/src/Test/IOSpec/Concurrent.hs b/src/Test/IOSpec/Concurrent.hs deleted file mode 100644 --- a/src/Test/IOSpec/Concurrent.hs +++ /dev/null @@ -1,282 +0,0 @@ -{-# 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/Fork.hs b/src/Test/IOSpec/Fork.hs new file mode 100644 --- /dev/null +++ b/src/Test/IOSpec/Fork.hs @@ -0,0 +1,34 @@ +-- | A pure specification of 'forkIO'. +module Test.IOSpec.Fork + ( + ForkS + , forkIO + ) + where + +import Test.IOSpec.VirtualMachine +import Test.IOSpec.Types + +-- The 'ForkS' data type and its instances. +-- +-- | An expression of type @IOSpec ForkS a@ corresponds to an 'IO' +-- computation that uses 'forkIO' and returns a value of +-- type 'a'. +-- +-- By itself, 'ForkS' is not terribly useful. You will probably want +-- to use @IOSpec (ForkS :+: MVarS)@ or @IOSpec (ForkS :+: STMS)@. +data ForkS a = + forall f b . Executable f => Fork (IOSpec f b) (ThreadId -> a) + +instance Functor ForkS where + fmap f (Fork l io) = Fork l (f . io) + +-- | The 'forkIO' function forks off a new thread. +forkIO :: (Executable f, ForkS :<: g) => IOSpec f a -> IOSpec g ThreadId +forkIO p = inject (Fork p return) + +instance Executable ForkS where + step (Fork t p) = do + tid <- freshThreadId + updateSoup tid t + return (Step (p tid)) diff --git a/src/Test/IOSpec/IORef.hs b/src/Test/IOSpec/IORef.hs --- a/src/Test/IOSpec/IORef.hs +++ b/src/Test/IOSpec/IORef.hs @@ -1,116 +1,67 @@ - -{-# OPTIONS -fglasgow-exts -fno-warn-missing-fields #-} - --- | A pure specification of mutable variables. -module Test.IOSpec.IORef +-- | A pure specification of mutable variables. +module Test.IOSpec.IORef ( - -- * The IOState monad - IOState - , runIOState - -- * Manipulation of IORefs + -- * The 'IORefS' spec + IORefS + -- * Manipulation and creation of IORefs , IORef , newIORef , readIORef , writeIORef , modifyIORef - ) + ) where -import Control.Monad.State import Data.Dynamic import Data.Maybe (fromJust) +import Test.IOSpec.Types +import Test.IOSpec.VirtualMachine -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) +-- The 'IORefS' spec. +-- | An expression of type @IOSpec IORefS a@ corresponds to an @IO@ +-- computation that uses mutable references and returns a value of +-- type @a@. +data IORefS a = + NewIORef Data (Loc -> a) + | ReadIORef Loc (Data -> a) + | WriteIORef Loc Data a -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) +instance Functor IORefS where + fmap f (NewIORef d io) = NewIORef d (f . io) + fmap f (ReadIORef l io) = ReadIORef l (f . io) + fmap f (WriteIORef l d io) = WriteIORef l d (f io) --- | A mutable variable in the IOState monad +-- | A mutable variable storing a value of type a. Note that the +-- types stored by an 'IORef' are assumed to be @Typeable@. 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) +newIORef :: (Typeable a, IORefS :<: f) => a -> IOSpec f (IORef a) +newIORef d = inject $ 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) +readIORef :: (Typeable a, IORefS :<:f ) => IORef a -> IOSpec f a +readIORef (IORef l) = inject $ ReadIORef l (return . fromJust . fromDynamic) --- | 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 'writeIORef' function overwrites the value stored in a +-- mutable variable. +writeIORef :: (Typeable a, IORefS :<: f) => IORef a -> a -> IOSpec f () +writeIORef (IORef l) d = inject $ 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 () +-- | The 'modifyIORef' function applies a function to the value stored in +-- and 'IORef'. +modifyIORef :: (Typeable a, IORefS :<: f) + => IORef a -> (a -> a) -> IOSpec f () 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)}) +-- | The 'Executable' instance for the `IORefS' monad. +instance Executable IORefS where + step (NewIORef d t) = do loc <- alloc + updateHeap loc d + return (Step (t loc)) + step (ReadIORef l t) = do Just d <- lookupHeap l + return (Step (t d)) + step (WriteIORef l d t) = do updateHeap l d + return (Step t) -update :: Loc -> Data -> Heap -> Heap -update l d h k - | l == k = d - | otherwise = h k diff --git a/src/Test/IOSpec/MVar.hs b/src/Test/IOSpec/MVar.hs new file mode 100644 --- /dev/null +++ b/src/Test/IOSpec/MVar.hs @@ -0,0 +1,71 @@ +-- | A pure specification of basic operations on MVars. + +module Test.IOSpec.MVar + ( + -- * The 'MVarS' spec + MVarS + -- * Supported functions + , MVar + , newEmptyMVar + , takeMVar + , putMVar + ) + where + +import Data.Dynamic +import Data.Maybe (fromJust) +import Test.IOSpec.Types +import Test.IOSpec.VirtualMachine + +-- The 'MVarS' data type and its instances. +-- +-- | An expression of type @IOSpec MVarS a@ corresponds to an @IO@ +-- computation that uses shared, mutable variables and returns a +-- value of type @a@. +-- +-- By itself, 'MVarS' is not terribly useful. You will probably want +-- to use @IOSpec (ForkS :+: MVarS)@. + +data MVarS a = + NewEmptyMVar (Loc -> a) + | TakeMVar Loc (Data -> a) + | PutMVar Loc Data a + +instance Functor MVarS where + fmap f (NewEmptyMVar io) = NewEmptyMVar (f . io) + fmap f (TakeMVar l io) = TakeMVar l (f . io) + fmap f (PutMVar l d io) = PutMVar l d (f io) + +-- | 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 :: (Typeable a, MVarS :<: f) => IOSpec f (MVar a) +newEmptyMVar = inject $ 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, MVarS :<: f) => MVar a -> IOSpec f a +takeMVar (MVar l) = inject $ TakeMVar l (return . fromJust . fromDynamic) + +-- | The 'putMVar' function fills an 'MVar' with a new value. If the +-- 'MVar' is not empty, the thread is blocked. +putMVar :: (Typeable a, MVarS :<: f) => MVar a -> a -> IOSpec f () +putMVar (MVar l) d = inject $ PutMVar l (toDyn d) (return ()) + +instance Executable MVarS where + step (NewEmptyMVar t) = do loc <- alloc + emptyLoc loc + return (Step (t loc)) + step (TakeMVar loc t) = do var <- lookupHeap loc + case var of + Nothing -> return Block + Just x -> do + emptyLoc loc + return (Step (t x)) + step (PutMVar loc d t) = do var <- lookupHeap loc + case var of + Nothing -> do + updateHeap loc d + return (Step t) + Just _ -> return Block diff --git a/src/Test/IOSpec/STM.hs b/src/Test/IOSpec/STM.hs new file mode 100644 --- /dev/null +++ b/src/Test/IOSpec/STM.hs @@ -0,0 +1,132 @@ +module Test.IOSpec.STM + ( + -- * The specification of STM + STMS + -- * Atomically + , atomically + -- * The STM monad + , STM + , TVar + , newTVar + , readTVar + , writeTVar + , retry + , orElse + , check + ) + where + +import Test.IOSpec.VirtualMachine +import Test.IOSpec.Types +import Data.Dynamic +import Data.Maybe (fromJust) +import Control.Monad.State + +-- The 'STMS' data type and its instances. +-- +-- | An expression of type @IOSpec 'STMS' a@ corresponds to an 'IO' +-- computation that may use 'atomically' and returns a value of type +-- @a@. +-- +-- By itself, 'STMS' is not terribly useful. You will probably want +-- to use @IOSpec (ForkS :+: STMS)@. +data STMS a = + forall b . Atomically (STM b) (b -> a) + +instance Functor STMS where + fmap f (Atomically s io) = Atomically s (f . io) + +-- | The 'atomically' function atomically executes an 'STM' action. +atomically :: (STMS :<: f) => STM a -> IOSpec f a +atomically stm = inject $ Atomically stm (return) + +instance Executable STMS where + step (Atomically stm b) = + do state <- get + case runStateT (executeSTM stm) state of + Done (Nothing,_) -> return Block + Done (Just x,finalState) -> put finalState >> return (Step (b x)) + _ -> internalError "Unsafe usage of STM" + +-- The 'STM' data type and its instances. +data STM a = + STMReturn a + | NewTVar Data (Loc -> STM a) + | ReadTVar Loc (Data -> STM a) + | WriteTVar Loc Data (STM a) + | Retry + | OrElse (STM a) (STM a) + +instance Functor STM where + fmap f (STMReturn x) = STMReturn (f x) + fmap f (NewTVar d io) = NewTVar d (fmap f . io) + fmap f (ReadTVar l io) = ReadTVar l (fmap f . io) + fmap f (WriteTVar l d io) = WriteTVar l d (fmap f io) + fmap _ Retry = Retry + fmap f (OrElse io1 io2) = OrElse (fmap f io1) (fmap f io2) + +instance Monad STM where + return = STMReturn + STMReturn a >>= f = f a + NewTVar d g >>= f = NewTVar d (\l -> g l >>= f) + ReadTVar l g >>= f = ReadTVar l (\d -> g d >>= f) + WriteTVar l d p >>= f = WriteTVar l d (p >>= f) + Retry >>= _ = Retry + OrElse p q >>= f = OrElse (p >>= f) (q >>= f) + +-- | A 'TVar' is a shared, mutable variable used by STM. +newtype TVar a = TVar Loc + +-- | The 'newTVar' function creates a new transactional variable. +newTVar :: Typeable a => a -> STM (TVar a) +newTVar d = NewTVar (toDyn d) (STMReturn . TVar) + +-- | The 'readTVar' function reads the value stored in a +-- transactional variable. +readTVar :: Typeable a => TVar a -> STM a +readTVar (TVar l) = ReadTVar l (STMReturn . fromJust . fromDynamic) + +-- | The 'writeTVar' function overwrites the value stored in a +-- transactional variable. +writeTVar :: Typeable a => TVar a -> a -> STM () +writeTVar (TVar l) d = WriteTVar l (toDyn d) (STMReturn ()) + +-- | The 'retry' function abandons a transaction and retries at some +-- later time. +retry :: STM a +retry = Retry + +-- | The 'check' function checks if its boolean argument holds. If +-- the boolean is true, it returns (); otherwise it calls 'retry'. +check :: Bool -> STM () +check True = return () +check False = retry + +-- | The 'orElse' function takes two 'STM' actions @stm1@ and @stm2@ and +-- performs @stm1@. If @stm1@ calls 'retry' it performs @stm2@. If @stm1@ +-- succeeds, on the other hand, @stm2@ is not executed. +orElse :: STM a -> STM a -> STM a +orElse p q = OrElse p q + +executeSTM :: STM a -> VM (Maybe a) +executeSTM (STMReturn x) = return (return x) +executeSTM (NewTVar d io) = do + loc <- alloc + updateHeap loc d + executeSTM (io loc) +executeSTM (ReadTVar l io) = do + (Just d) <- lookupHeap l + executeSTM (io d) +executeSTM (WriteTVar l d io) = do + updateHeap l d + executeSTM io +executeSTM Retry = return Nothing +executeSTM (OrElse p q) = do + state <- get + case runStateT (executeSTM p) state of + Done (Nothing,_) -> executeSTM q + Done (Just x,s) -> put s >> return (Just x) + _ -> internalError "Unsafe usage of STM" + +internalError :: String -> a +internalError msg = error ("IOSpec.STM: " ++ msg) diff --git a/src/Test/IOSpec/Surrogate.hs b/src/Test/IOSpec/Surrogate.hs new file mode 100644 --- /dev/null +++ b/src/Test/IOSpec/Surrogate.hs @@ -0,0 +1,31 @@ +-- | This module contains a few type signatures to help replace pure +-- specifications by their effectful counterparts. +module Test.IOSpec.Surrogate + ( + -- * The IOSpec type + IOSpec + -- * The specifications + , ForkS + , MVarS + , IORefS + , STMS + , Teletype + , (:+:) + ) + where + +-- | The @IOSpec f a@ is merely type synonym for @IO a@. Once you've +-- tested a module, you can use these definitions to avoid having to +-- change your type signatures. +-- +-- Note that because this definition of 'IOSpec' ignores its @f@ +-- argument, each of 'ForkS', 'MVarS', etc., is simply an empty data +-- type. +type IOSpec f a = IO a + +data ForkS +data MVarS +data IORefS +data STMS +data Teletype +data (f :+: g) diff --git a/src/Test/IOSpec/Teletype.hs b/src/Test/IOSpec/Teletype.hs --- a/src/Test/IOSpec/Teletype.hs +++ b/src/Test/IOSpec/Teletype.hs @@ -1,60 +1,66 @@ --- | A pure implementation of getChar and putChar. - +-- | A pure specification of getChar and putChar. module Test.IOSpec.Teletype ( -- * The IOTeletype monad - IOTeletype - , Output(..) - , runTT + Teletype -- * Pure getChar and putChar , getChar , putChar - ) + , putStr + , putStrLn + , getLine + ) 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) +import Prelude hiding (getChar, putChar, putStr, putStrLn, getLine) +import Control.Monad (forM_) +import Test.IOSpec.Types +import Test.IOSpec.VirtualMachine -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) +-- The 'Teletype' specification. +-- +-- | An expression of type 'IOSpec' 'Teletype' @a@ corresponds to an @IO@ +-- computation that may print to or read from stdout and stdin +-- respectively. +-- +-- There is a minor caveat here. I assume that stdin and stdout are +-- not buffered. This is not the standard behaviour in many Haskell +-- compilers. +data Teletype a = + GetChar (Char -> a) + | PutChar Char a +instance Functor Teletype where + fmap f (GetChar tt) = GetChar (f . tt) + fmap f (PutChar c tt) = PutChar c (f tt) --- | 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 'getChar' function can be used to read a character from the +-- teletype. +getChar :: (:<:) Teletype f => IOSpec f Char +getChar = inject (GetChar return) --- | 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 print a character to the +-- teletype. +putChar :: (Teletype :<: f) => Char -> IOSpec f () +putChar c = inject (PutChar c (return ())) +instance Executable Teletype where + step (GetChar f) = do + c <- readChar + return (Step (f c)) + step (PutChar c a) = do + printChar c + return (Step a) --- | The getChar function can be used to read input from the teletype. -getChar :: IOTeletype Char -getChar = GetChar ReturnTeletype +putStr :: (Teletype :<: f) => String -> IOSpec f () +putStr str = forM_ str putChar --- | The getChar function can be used to print to the teletype. -putChar :: Char -> IOTeletype () -putChar c = PutChar c (ReturnTeletype ()) +putStrLn :: (Teletype :<: f) => String -> IOSpec f () +putStrLn str = putStr str >> putChar '\n' +getLine :: (Teletype :<: f) => IOSpec f String +getLine = do + c <- getChar + if c == '\n' + then return [] + else getLine >>= \line -> return (c : line) diff --git a/src/Test/IOSpec/Types.hs b/src/Test/IOSpec/Types.hs new file mode 100644 --- /dev/null +++ b/src/Test/IOSpec/Types.hs @@ -0,0 +1,64 @@ +{-# OPTIONS_GHC -fallow-overlapping-instances#-} +-- | This module contains the basic data types underlying the +-- 'IOSpec' library. Most of the types and classes in this module +-- are described in +-- . +module Test.IOSpec.Types + ( + -- * The 'IOSpec' type. + IOSpec(..) + , foldIOSpec + -- * Coproducts of functors + , (:+:)(..) + -- * Injections from one functor to another + , (:<:) + , inject + ) where + +-- | A value of type 'IOSpec' @f@ @a@ is either a pure value of type @a@ +-- or some effect, determined by @f@. Crucially, 'IOSpec' @f@ is a +-- monad, provided @f@ is a functor. +data IOSpec f a = + Pure a + | Impure (f (IOSpec f a)) + +instance (Functor f) => Functor (IOSpec f) where + fmap f (Pure x) = Pure (f x) + fmap f (Impure t) = Impure (fmap (fmap f) t) + +instance (Functor f) => Monad (IOSpec f) where + return = Pure + (Pure x) >>= f = f x + (Impure t) >>= f = Impure (fmap (>>= f) t) + +-- | The fold over 'IOSpec' values. +foldIOSpec :: Functor f => (a -> b) -> (f b -> b) -> IOSpec f a -> b +foldIOSpec pure _ (Pure x) = pure x +foldIOSpec pure impure (Impure t) = impure (fmap (foldIOSpec pure impure) t) + +-- | The coproduct of functors +data (f :+: g) x = Inl (f x) | Inr (g x) + +infixr 5 :+: + +instance (Functor f, Functor g) => Functor (f :+: g) where + fmap f (Inl x) = Inl (fmap f x) + fmap f (Inr y) = Inr (fmap f y) + +-- | The (:<:) class + +class (Functor sub, Functor sup) => sub :<: sup where + inj :: sub a -> sup a + +instance Functor f => (:<:) f f where + inj = id + +instance (Functor f, Functor g) => (:<:) f (f :+: g) where + inj = Inl + +instance ((:<:) f g, Functor f, Functor g, Functor h) + => (:<:) f (h :+: g) where + inj = Inr . inj + +inject :: (g :<: f) => g (IOSpec f a) -> IOSpec f a +inject = Impure . inj diff --git a/src/Test/IOSpec/VirtualMachine.hs b/src/Test/IOSpec/VirtualMachine.hs new file mode 100644 --- /dev/null +++ b/src/Test/IOSpec/VirtualMachine.hs @@ -0,0 +1,337 @@ +-- | The virtual machine on which the specifications execute. +module Test.IOSpec.VirtualMachine + ( + -- * The Virtual Machine + VM + , Data + , Loc + , Scheduler + , Store + , ThreadId + , initialStore + -- * Primitive operations on the VM + , alloc + , emptyLoc + , freshThreadId + , finishThread + , lookupHeap + , mainTid + , printChar + , readChar + , updateHeap + , updateSoup + -- * The observable effects on the VM + , Effect (..) + -- * Sample schedulers + -- $schedulerDoc + , roundRobin + , singleThreaded + -- * Executing code on the VM + , Executable(..) + , Step(..) + , runIOSpec + , evalIOSpec + , execIOSpec + ) + where + +import Control.Monad.State +import Data.Dynamic +import Data.List +import qualified Data.Stream as Stream +import Test.IOSpec.Types +import Test.QuickCheck + +type Data = Dynamic +type Loc = Int +type Heap = Loc -> Maybe Data + +newtype ThreadId = ThreadId Int deriving (Eq, Show) + +instance Arbitrary ThreadId where + arbitrary = liftM ThreadId arbitrary + coarbitrary (ThreadId k) = coarbitrary k + +newtype Scheduler = + Scheduler (Int -> (Int, Scheduler)) + +instance Arbitrary Scheduler where + arbitrary = liftM streamSched arbitrary + coarbitrary = internalError + "Test.IOSpec: no definition of coarbitrary for Schedulers." + +instance Show Scheduler where + show _ = "Test.IOSpec.Scheduler" + + +data ThreadStatus = + forall f b . Executable f => Running (IOSpec f b) + | Finished + +type ThreadSoup = ThreadId -> ThreadStatus + +data Store = + Store { fresh :: Loc + , heap :: Heap + , nextTid :: ThreadId + , blockedThreads :: [ThreadId] + , finishedThreads :: [ThreadId] + , scheduler :: Scheduler + , threadSoup :: ThreadSoup + } + +initialStore :: Scheduler -> Store +initialStore sch = + Store { fresh = 0 + , heap = internalError "Access of unallocated memory " + , nextTid = ThreadId 1 + , blockedThreads = [] + , finishedThreads = [] + , scheduler = sch + , threadSoup = internalError "Unknown thread scheduled" + } + +-- Auxiliary functions +modifyFresh :: (Loc -> Loc) -> VM () +modifyFresh f = do s <- get + put (s {fresh = f (fresh s)}) + +modifyHeap :: (Heap -> Heap) -> VM () +modifyHeap f = do s <- get + put (s {heap = f (heap s)}) + +modifyNextTid :: (ThreadId -> ThreadId) -> VM () +modifyNextTid f = do s <- get + put (s {nextTid = f (nextTid s)}) + +modifyBlockedThreads :: ([ThreadId] -> [ThreadId]) -> VM () +modifyBlockedThreads f = do s <- get + put (s {blockedThreads = f (blockedThreads s)}) + +modifyFinishedThreads :: ([ThreadId] -> [ThreadId]) -> VM () +modifyFinishedThreads f = do s <- get + put (s {finishedThreads = f (finishedThreads s)}) + +modifyScheduler :: (Scheduler -> Scheduler) -> VM () +modifyScheduler f = do s <- get + put (s {scheduler = f (scheduler s)}) + +modifyThreadSoup :: (ThreadSoup -> ThreadSoup) -> VM () +modifyThreadSoup f = do s <- get + put (s {threadSoup = f (threadSoup s)}) + + +-- | 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 VM a = StateT Store Effect a + +-- | The 'alloc' function allocate a fresh location on the heap. +alloc :: VM Loc +alloc = do loc <- gets fresh + modifyFresh ((+) 1) + return loc + +-- | The 'emptyLoc' function removes the data stored at a given +-- location. This corresponds, for instance, to emptying an @MVar@. +emptyLoc :: Loc -> VM () +emptyLoc l = modifyHeap (update l Nothing) + +-- | The 'freshThreadId' function returns a previously unallocated 'ThreadId'. +freshThreadId :: VM ThreadId +freshThreadId = do + t <- gets nextTid + modifyNextTid (\(ThreadId n) -> ThreadId (n+1)) + return t + +-- | The 'finishThread' function kills the thread with the specified +-- 'ThreadId'. +finishThread :: ThreadId -> VM () +finishThread tid = do + modifyFinishedThreads (tid:) + modifyThreadSoup (update tid Finished) + +-- | The 'blockThread' method is used to record when a thread cannot +-- make progress. +blockThread :: ThreadId -> VM () +blockThread tid = modifyBlockedThreads (tid:) + +-- | When progress is made, the 'resetBlockedThreads' function +-- | ensures that any thread can be scheduled. +resetBlockedThreads :: VM () +resetBlockedThreads = modifyBlockedThreads (const []) + +-- | The 'lookupHeap' function returns the data stored at a given +-- heap location, if there is any. +lookupHeap :: Loc -> VM (Maybe Data) +lookupHeap l = do h <- gets heap + return (h l) + +-- | The 'mainTid' constant is the 'ThreadId' of the main process. +mainTid :: ThreadId +mainTid = ThreadId 0 + +-- | The 'readChar' and 'printChar' functions are the primitive +-- counterparts of 'getChar' and 'putChar' in the 'VM' monad. +readChar :: VM Char +readChar = StateT (\s -> (ReadChar (\c -> (Done (c,s))))) + +printChar :: Char -> VM () +printChar c = StateT (\s -> (Print c (Done ((),s)))) + +-- | The 'updateHeap' function overwrites a given location with +-- new data. +updateHeap :: Loc -> Data -> VM () +updateHeap l d = modifyHeap (update l (Just d)) + +-- | The 'updateSoup' function updates the process associated with a +-- given 'ThreadId'. +updateSoup :: Executable f => ThreadId -> IOSpec f a -> VM () +updateSoup tid p = modifyThreadSoup (update tid (Running p)) + +update :: Eq a => a -> b -> (a -> b) -> (a -> b) +update l d h k + | l == k = d + | otherwise = h k + +-- | The 'Effect' type contains all the primitive effects that are +-- observable on the virtual machine. +data Effect a = + Done a + | ReadChar (Char -> Effect a) + | Print Char (Effect a) + | Fail String + +instance Functor Effect where + fmap f (Done x) = Done (f x) + fmap f (ReadChar t) = ReadChar (\c -> fmap f (t c)) + fmap f (Print c t) = Print c (fmap f t) + fmap _ (Fail msg) = Fail msg + +instance Monad Effect where + return = Done + (Done x) >>= f = f x + (ReadChar t) >>= f = ReadChar (\c -> t c >>= f) + (Print c t) >>= f = Print c (t >>= f) + (Fail msg) >>= _ = Fail msg + +-- $schedulerDoc +-- +-- 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. + +-- | The 'roundRobin' scheduler provides a simple round-robin scheduler. +roundRobin :: Scheduler +roundRobin = streamSched (Stream.unfold (\k -> (k, k+1)) 0) + +-- | The 'singleThreaded' scheduler will never schedule forked +-- threads, always scheduling the main thread. Only use this +-- scheduler if your code is not concurrent. +singleThreaded :: Scheduler +singleThreaded = streamSched (Stream.repeat 0) + +streamSched :: Stream.Stream Int -> Scheduler +streamSched (Stream.Cons x xs) = + Scheduler (\k -> (x `mod` k, streamSched xs)) + + +-- | The 'Executable' type class captures all the different types of +-- operations that can be executed in the 'VM' monad. +class Functor f => Executable f where + step :: f a -> VM (Step a) + +data Step a = Step a | Block + +instance (Executable f, Executable g) => Executable (f :+: g) where + step (Inl x) = step x + step (Inr y) = step y + +-- The 'execVM' function essentially schedules a thread and allows +-- it to perform a single step. If the main thread is finished, it +-- returns the final result of the comptuation. +execVM :: Executable f => IOSpec f a -> VM a +execVM main = do + (tid,t) <- schedule main + case t of + (Main (Pure x)) -> resetBlockedThreads >> return x + (Main (Impure p)) -> do x <- step p + case x of + Step y -> resetBlockedThreads >> execVM y + Block -> blockThread mainTid >> execVM main + (Aux (Pure _)) -> do finishThread tid + execVM main + (Aux (Impure p)) -> do x <- step p + case x of + Step y -> resetBlockedThreads >> + updateSoup tid y >> + execVM main + Block -> blockThread tid >> + execVM main +-- A Process is the result of a call to the scheduler. +data Process a = + forall f . Executable f => Main (IOSpec f a) + | forall f b . Executable f => Aux (IOSpec f b) + +-- Gets the ThreadId of the next thread to schedule. +getNextThreadId :: VM ThreadId +getNextThreadId = do + Scheduler sch <- gets scheduler + (ThreadId total) <- gets nextTid + let allTids = [ThreadId i | i <- [0 .. total - 1]] + blockedTids <- gets blockedThreads + finishedTids <- gets finishedThreads + let activeThreads = allTids \\ (blockedTids `union` finishedTids) + let (i,s) = sch (length activeThreads) + modifyScheduler (const s) + return (activeThreads !! i) + +-- The 'schedule' function tries to schedule an active thread, +-- returning the scheduled thread's ThreadId and the process +-- associated with that id. +schedule :: Executable f => IOSpec f a -> VM (ThreadId, Process a) +schedule main = do tid <- getNextThreadId + if tid == mainTid + then return (mainTid, Main main) + else do + tsoup <- gets threadSoup + case tsoup tid of + Finished -> internalError + "Scheduled finished thread." + Running p -> return (tid, Aux p) + +-- | 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. +runIOSpec :: Executable f => IOSpec f a -> Scheduler -> Effect (a, Store) +runIOSpec io sched = runStateT + (execVM io) + (initialStore sched) + +-- | 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. +execIOSpec :: Executable f => IOSpec f a -> Scheduler -> Store +execIOSpec io sched = + case runIOSpec io sched of + Done (_,s) -> s + _ -> error $ "Failed application of Test.IOSpec.execIOSpec.\n" ++ + "Probable cause: your function uses functions such as " ++ + "putChar and getChar. Check the preconditions for calling " ++ + "this function in the IOSpec documentation." + +-- | The 'evalIOSpec' function returns the effects a computation +-- yields, but discards the final state of the virtual machine. +evalIOSpec :: Executable f => IOSpec f a -> Scheduler -> Effect a +evalIOSpec io sched = fmap fst (runIOSpec io sched) + +internalError :: String -> a +internalError msg = error ("IOSpec.VirtualMachine: " ++ msg)