QSM

io-sim/io-sim.cabal

@@ -97,6 +97,27 @@ library
   if flag(asserts)
      ghc-options:      -fno-ignore-asserts
 
+library qsm
+  import:              warnings
+  hs-source-dirs:      qsm
+  exposed-modules:     Test.StateMachine.IOSim.Execute
+                       Test.StateMachine.IOSim.Generate
+                       Test.StateMachine.IOSim.Types
+                       Test.StateMachine.IOSim
+
+  reexported-modules:  Test.StateMachine.Types.Rank2
+
+  build-depends:       base,
+                       io-sim,
+                       QuickCheck,
+                       mtl,
+                       containers,
+                       pretty-show,
+                       io-classes,
+                       quickcheck-state-machine:no-vendored-treediff,
+  default-extensions:  ImportQualifiedPost
+  default-language:    Haskell2010
+
 test-suite test
   import:              test-warnings
   type:                exitcode-stdio-1.0
@@ -144,3 +165,28 @@ benchmark bench
                        -Wpartial-fields
                        -Widentities
                        -Wredundant-constraints
+
+test-suite qsm-test
+  import:              test-warnings
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      qsm-test
+  main-is: Main.hs
+
+  other-modules:       BasicTest.Template
+                       BasicTest.Correct
+                       BasicTest.NoIncr
+                       BasicTest.Racy
+                       BasicTest.InternalFork
+                       BasicTest.InternalForkAtomic
+                       Exception.Deadlocks
+                       Exception.TryPutMVar
+                       Exception.WithMVar
+
+  default-language:    Haskell2010
+  default-extensions:  ImportQualifiedPost
+  build-depends:       base,
+                       io-sim:qsm,
+                       io-classes,
+                       QuickCheck,
+                       tasty,
+                       tasty-quickcheck

io-sim/qsm-test/BasicTest/Correct.hs

@@ -0,0 +1,54 @@
+-- |
+
+module BasicTest.Correct where
+
+import BasicTest.Template
+import Control.Concurrent.Class.MonadSTM
+import Test.QuickCheck
+import Test.StateMachine.IOSim
+
+{-------------------------------------------------------------------------------
+  SUT
+-------------------------------------------------------------------------------}
+
+newtype AtomicCounter m = AtomicCounter (TVar m Int)
+
+newSUT :: MonadLabelledSTM m => m (AtomicCounter m)
+newSUT = do
+    ref <- atomically $ do
+      tv <- newTVar 0
+      labelTVar tv "TheCounter"
+      pure tv
+    return (AtomicCounter ref)
+
+incr :: MonadSTM m => AtomicCounter m -> m ()
+incr (AtomicCounter ref) =
+  atomically $ do
+    i <- readTVar ref
+    writeTVar ref (i + 1)
+
+get :: MonadSTM m => AtomicCounter m -> m Int
+get (AtomicCounter ref) = readTVarIO ref
+
+semantics :: MonadSTM m => AtomicCounter m -> Cmd Concrete -> m (Resp Concrete)
+semantics sut Incr = do
+  incr sut *> pure Void
+semantics sut Get = do
+  GetR <$> get sut
+
+transition :: Model r -> Cmd r -> Resp r -> Model r
+transition (Model m) Incr _ = Model (m + 1)
+transition m Get _          = m
+
+sm :: StateMachine Model Cmd AtomicCounter Resp
+sm = StateMachine initModel transition precondition postcondition Nothing
+     generator shrinker newSUT semantics mock
+
+prop_sequential :: Property
+prop_sequential = forAllCommands sm Nothing $ runSequential sm
+
+prop_sequential' :: Property
+prop_sequential' = forAllCommands sm Nothing $ runSequentialPOR sm
+
+prop_parallel :: Property
+prop_parallel = forAllParallelCommands sm Nothing $ runParallel sm

io-sim/qsm-test/BasicTest/InternalFork.hs

@@ -0,0 +1,59 @@
+-- |
+
+module BasicTest.InternalFork where
+
+import BasicTest.Template
+import Control.Concurrent.Class.MonadSTM
+import Control.Monad.Class.MonadAsync
+import Test.QuickCheck
+import Test.StateMachine.IOSim
+
+{-------------------------------------------------------------------------------
+  SUT
+-------------------------------------------------------------------------------}
+
+newtype AtomicCounter m = AtomicCounter (TVar m Int)
+
+newSUT :: MonadLabelledSTM m => m (AtomicCounter m)
+newSUT = do
+    ref <- atomically $ do
+      tv <- newTVar 0
+      labelTVar tv "TheCounter"
+      pure tv
+    return (AtomicCounter ref)
+
+incr :: MonadAsync m => AtomicCounter m -> m ()
+incr (AtomicCounter ref) = do
+   t1 <- async f
+   t2 <- async f
+   wait t1 >> wait t2
+  where f = do
+          i <- readTVarIO ref
+          atomically $ writeTVar ref (i + 1)
+
+get :: (MonadSTM m) => AtomicCounter m -> m Int
+get (AtomicCounter ref) = readTVarIO ref
+
+semantics :: MonadAsync m => AtomicCounter m -> Cmd Concrete -> m (Resp Concrete)
+semantics sut Incr = do
+  incr sut *> pure Void
+semantics sut Get = do
+  GetR <$> get sut
+
+transition :: Model r -> Cmd r -> Resp r -> Model r
+-- each increment will increment by 2
+transition (Model m) Incr _ = Model (m + 2)
+transition m Get _          = m
+
+sm :: StateMachine Model Cmd AtomicCounter Resp
+sm = StateMachine initModel transition precondition postcondition Nothing
+     generator shrinker newSUT semantics mock
+
+prop_sequential :: Property
+prop_sequential = forAllCommands sm Nothing $ runSequential sm
+
+prop_sequential' :: Property
+prop_sequential' = forAllCommands sm Nothing $ runSequentialPOR sm
+
+prop_parallel :: Property
+prop_parallel = forAllParallelCommands sm Nothing $ runParallel sm

io-sim/qsm-test/BasicTest/InternalForkAtomic.hs

@@ -0,0 +1,59 @@
+-- |
+
+module BasicTest.InternalForkAtomic where
+
+import BasicTest.Template
+import Control.Concurrent.Class.MonadSTM
+import Control.Monad.Class.MonadAsync
+import Test.QuickCheck
+import Test.StateMachine.IOSim
+
+{-------------------------------------------------------------------------------
+  SUT
+-------------------------------------------------------------------------------}
+
+newtype AtomicCounter m = AtomicCounter (TVar m Int)
+
+newSUT :: MonadLabelledSTM m => m (AtomicCounter m)
+newSUT = do
+    ref <- atomically $ do
+      tv <- newTVar 0
+      labelTVar tv "TheCounter"
+      pure tv
+    return (AtomicCounter ref)
+
+incr :: MonadAsync m => AtomicCounter m -> m ()
+incr (AtomicCounter ref) = do
+   t1 <- async f
+   t2 <- async f
+   wait t1 >> wait t2
+  where f = atomically $ do
+          i <- readTVar ref
+          writeTVar ref (i + 1)
+
+get :: (MonadSTM m) => AtomicCounter m -> m Int
+get (AtomicCounter ref) = readTVarIO ref
+
+semantics :: MonadAsync m => AtomicCounter m -> Cmd Concrete -> m (Resp Concrete)
+semantics sut Incr = do
+  incr sut *> pure Void
+semantics sut Get = do
+  GetR <$> get sut
+
+transition :: Model r -> Cmd r -> Resp r -> Model r
+-- each increment will increment by 2
+transition (Model m) Incr _ = Model (m + 2)
+transition m Get _          = m
+
+sm :: StateMachine Model Cmd AtomicCounter Resp
+sm = StateMachine initModel transition precondition postcondition Nothing
+     generator shrinker newSUT semantics mock
+
+prop_sequential :: Property
+prop_sequential = forAllCommands sm Nothing $ runSequential sm
+
+prop_sequential' :: Property
+prop_sequential' = forAllCommands sm Nothing $ runSequentialPOR sm
+
+prop_parallel :: Property
+prop_parallel = forAllParallelCommands sm Nothing $ runParallel sm

io-sim/qsm-test/BasicTest/NoIncr.hs

@@ -0,0 +1,49 @@
+-- |
+
+module BasicTest.NoIncr where
+
+import BasicTest.Template
+import Control.Concurrent.Class.MonadSTM
+import Test.QuickCheck
+import Test.StateMachine.IOSim
+
+{-------------------------------------------------------------------------------
+  SUT
+-------------------------------------------------------------------------------}
+
+newtype AtomicCounter m = AtomicCounter (TVar m Int)
+
+newSUT :: MonadLabelledSTM m => m (AtomicCounter m)
+newSUT = do
+    ref <- atomically $ do
+      tv <- newTVar 0
+      labelTVar tv "TheCounter"
+      pure tv
+    return (AtomicCounter ref)
+
+incr :: MonadSTM m => AtomicCounter m -> m ()
+incr (AtomicCounter ref) =
+  atomically $ do
+    i <- readTVar ref
+    -- Deliberate bug, no increment
+    writeTVar ref i
+
+get :: MonadSTM m => AtomicCounter m -> m Int
+get (AtomicCounter ref) = readTVarIO ref
+
+semantics :: MonadSTM m => AtomicCounter m -> Cmd Concrete -> m (Resp Concrete)
+semantics sut Incr = do
+  incr sut *> pure Void
+semantics sut Get = do
+  GetR <$> get sut
+
+transition :: Model r -> Cmd r -> Resp r -> Model r
+transition (Model m) Incr _ = Model (m + 1)
+transition m Get _          = m
+
+sm :: StateMachine Model Cmd AtomicCounter Resp
+sm = StateMachine initModel transition precondition postcondition Nothing
+     generator shrinker newSUT semantics mock
+
+prop_sequential :: Property
+prop_sequential = forAllCommands sm Nothing $ runSequential sm

io-sim/qsm-test/BasicTest/Racy.hs

@@ -0,0 +1,53 @@
+-- |
+
+module BasicTest.Racy where
+
+import BasicTest.Template
+import Control.Concurrent.Class.MonadSTM
+import Test.QuickCheck
+import Test.StateMachine.IOSim
+
+{-------------------------------------------------------------------------------
+  SUT
+-------------------------------------------------------------------------------}
+
+newtype AtomicCounter m = AtomicCounter (TVar m Int)
+
+newSUT :: MonadLabelledSTM m => m (AtomicCounter m)
+newSUT = do
+    ref <- atomically $ do
+      tv <- newTVar 0
+      labelTVar tv "TheCounter"
+      pure tv
+    return (AtomicCounter ref)
+
+incr :: MonadSTM m => AtomicCounter m -> m ()
+incr (AtomicCounter ref) = do
+  i <- readTVarIO ref
+  atomically $ writeTVar ref (i + 1)
+
+get :: MonadSTM m => AtomicCounter m -> m Int
+get (AtomicCounter ref) = readTVarIO ref
+
+semantics :: MonadSTM m => AtomicCounter m -> Cmd Concrete -> m (Resp Concrete)
+semantics sut Incr = do
+  incr sut *> pure Void
+semantics sut Get = do
+  GetR <$> get sut
+
+transition :: Model r -> Cmd r -> Resp r -> Model r
+transition (Model m) Incr _ = Model (m + 1)
+transition m Get _          = m
+
+sm :: StateMachine Model Cmd AtomicCounter Resp
+sm = StateMachine initModel transition precondition postcondition Nothing
+     generator shrinker newSUT semantics mock
+
+prop_sequential :: Property
+prop_sequential = forAllCommands sm Nothing $ runSequential sm
+
+prop_sequential' :: Property
+prop_sequential' = forAllCommands sm Nothing $ runSequentialPOR sm
+
+prop_parallel :: Property
+prop_parallel = forAllParallelCommands sm Nothing $ runParallel sm