Lightweight verification of multithreaded programs.

See Step.hs - it is quite obvious.

See Main.hs for several more examples - Peterson lock, deadlock etc.

We can also record traces in addition to states. It is not hard to add wait/notify (aka wait/pulseall), atomics, exceptions, thread interrupts.

Example:

module Main where

import Step

incrementer v = compile [
  Label "loop" $ Get v,
  Arith $ \(IntValue a:s) -> [(IntValue (a+1):s)], 
  Set v, 
  Jmp "loop"
  ]

i = initState [("a", IntValue 1), ("b", IntValue 1)] [] (compile [
  Spawn "a" (incrementer "a"),
  Spawn "b" (incrementer "b")
  ])


*Main Data.List Control.Monad> mapM_ print $ nub $ map fst $ runStep (replicateM 15 stepState) i
(fromList [("a",IntValue 4),("b",IntValue 1)],fromList [],[(Pid 0,"entry","<finished>"),(Pid 1,"a","1"),(Pid 2,"b","0")])
(fromList [("a",IntValue 4),("b",IntValue 1)],fromList [],[(Pid 0,"entry","<finished>"),(Pid 1,"a","0"),(Pid 2,"b","1")])
(fromList [("a",IntValue 4),("b",IntValue 1)],fromList [],[(Pid 0,"entry","<finished>"),(Pid 1,"a","3"),(Pid 2,"b","2")])
(fromList [("a",IntValue 3),("b",IntValue 2)],fromList [],[(Pid 0,"entry","<finished>"),(Pid 1,"a","2"),(Pid 2,"b","3")])
(fromList [("a",IntValue 3),("b",IntValue 2)],fromList [],[(Pid 0,"entry","<finished>"),(Pid 1,"a","1"),(Pid 2,"b","0")])
(fromList [("a",IntValue 3),("b",IntValue 2)],fromList [],[(Pid 0,"entry","<finished>"),(Pid 1,"a","0"),(Pid 2,"b","1")])
(fromList [("a",IntValue 3),("b",IntValue 2)],fromList [],[(Pid 0,"entry","<finished>"),(Pid 1,"a","3"),(Pid 2,"b","2")])
(fromList [("a",IntValue 2),("b",IntValue 3)],fromList [],[(Pid 0,"entry","<finished>"),(Pid 1,"a","2"),(Pid 2,"b","3")])
(fromList [("a",IntValue 2),("b",IntValue 3)],fromList [],[(Pid 0,"entry","<finished>"),(Pid 1,"a","1"),(Pid 2,"b","0")])
(fromList [("a",IntValue 2),("b",IntValue 3)],fromList [],[(Pid 0,"entry","<finished>"),(Pid 1,"a","0"),(Pid 2,"b","1")])
(fromList [("a",IntValue 2),("b",IntValue 3)],fromList [],[(Pid 0,"entry","<finished>"),(Pid 1,"a","3"),(Pid 2,"b","2")])
(fromList [("a",IntValue 1),("b",IntValue 4)],fromList [],[(Pid 0,"entry","<finished>"),(Pid 1,"a","2"),(Pid 2,"b","3")])
(fromList [("a",IntValue 1),("b",IntValue 4)],fromList [],[(Pid 0,"entry","<finished>"),(Pid 1,"a","1"),(Pid 2,"b","0")])
(fromList [("a",IntValue 1),("b",IntValue 4)],fromList [],[(Pid 0,"entry","<finished>"),(Pid 1,"a","0"),(Pid 2,"b","1")])
(fromList [("a",IntValue 4),("b",IntValue 1)],fromList [],[(Pid 0,"entry","1"),(Pid 1,"b","2")]