Last active
August 29, 2015 14:20
-
-
Save bohde/3a56d848aa098114799d to your computer and use it in GitHub Desktop.
QueueDeadlocking
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Here is a test runner that uses quickcheck to generate programs against | |
a concurrent queue api, to hopefully find the intentional bugs in | |
it's implementation. | |
> main :: IO () | |
> main = hspec $ do | |
> describe "queue" $ do | |
> it "should not ever allow the client to block" $ property $ \program scheduler -> do | |
> res <- interpret scheduler $ new >>= runProgram program | |
> res `shouldSatisfy` (isRight) | |
here is the output of running the tests: | |
1) queue should not ever allow the client to block | |
predicate failed on: `Left [LogEntry Main (Variable (Fresh 0)) [],LogEntry Main (Variable (Write 0)) [],LogEntry Main (Spawn 0) [],LogEntry (Thread 0) (Variable (Read 0)) [],LogEntry (Thread 0) (Variable (Write 0)) [BlockedOn Main 0],LogEntry (Thread 0) Halt [],LogEntry Main (Variable (Read 0)) []]` (after 11 tests and 5 shrinks): | |
`Fork (Op Put Halt) (Op Get (Op Put Halt))` | |
`Scheduler(...)` | |
There are three pieces of information this gives us: | |
1) the string representation of the Scheduler, which is opaque | |
2) The string representation of the Program, which is equivalent to | |
the following Haskell | |
> program var = do | |
> fork $ put var () | |
> _ <- get var () | |
> put () | |
3) The log of the scheduler running the program, which shows which | |
thread the scheduler chose, the operation the thread ran, and a | |
list of threads that are blocked on an operation. | |
Here it is formatted for easier reading: | |
> [LogEntry Main (Variable (Fresh 0)) [], | |
> LogEntry Main (Variable (Write 0)) [], | |
> LogEntry Main (Spawn 0) [], | |
> LogEntry (Thread 0) (Variable (Read 0)) [], | |
> LogEntry (Thread 0) (Variable (Write 0)) [BlockedOn Main 0], | |
> LogEntry (Thread 0) Halt [], | |
> LogEntry Main (Variable (Read 0)) []] | |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Queue where | |
import PureMVar | |
data Queue m a = Queue (MVar m [a]) | |
new :: (Monad m) => MVarT m (Queue m a) | |
new = do | |
items <- newMVar | |
putMVar items [] | |
return $ Queue items | |
put :: (Monad m) => Queue m a -> a -> MVarT m () | |
put (Queue items) a = do | |
items' <- takeMVar items | |
putMVar items $ items' ++ [a] | |
getMay :: (Monad m) => Queue m a -> MVarT m (Maybe a) | |
getMay (Queue items) = do | |
items' <- takeMVar items | |
case items' of | |
[] -> do | |
putMVar items [] | |
return Nothing | |
(a:as) -> do | |
-- putMVvar items as | |
return $ Just a |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment