1
- {-# LANGUAGE DeriveGeneric #-}
2
- {-# LANGUAGE FlexibleContexts #-}
3
- {-# LANGUAGE LambdaCase #-}
4
- {-# LANGUAGE RankNTypes #-}
5
- {-# LANGUAGE ScopedTypeVariables #-}
1
+ {-# LANGUAGE DeriveGeneric #-}
2
+ {-# LANGUAGE FlexibleContexts #-}
3
+ {-# LANGUAGE LambdaCase #-}
4
+ {-# LANGUAGE RankNTypes #-}
5
+ {-# LANGUAGE PartialTypeSignatures #-}
6
+ {-# LANGUAGE ScopedTypeVariables #-}
6
7
7
8
{-# OPTIONS_GHC -Wno-unused-top-binds #-}
8
9
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
10
+ {-# OPTIONS_GHC -Wno-partial-type-signatures #-}
9
11
10
12
module Test.Control.Monad.IOSimPOR (tests ) where
11
13
12
14
import Data.Fixed (Micro )
13
- import Data.Foldable (foldl' )
15
+ import Data.Foldable (foldl' , traverse_ )
14
16
import Data.Functor (($>) )
15
17
import Data.IORef
16
18
import qualified Data.List as List
@@ -26,8 +28,9 @@ import Control.Monad
26
28
import Control.Monad.Fix
27
29
import Control.Parallel
28
30
29
- import Control.Monad.Class.MonadFork
30
31
import Control.Concurrent.Class.MonadSTM
32
+ import Control.Monad.Class.MonadAsync
33
+ import Control.Monad.Class.MonadFork
31
34
import Control.Monad.Class.MonadSay
32
35
import Control.Monad.Class.MonadTest
33
36
import Control.Monad.Class.MonadThrow
@@ -258,39 +261,47 @@ sortTasks (x:y:xs) | x>y = [y:x:xs] ++ ((x:) <$> sortTasks (y:xs))
258
261
sortTasks (x: xs) = (x: ) <$> sortTasks xs
259
262
sortTasks [] = []
260
263
261
- interpret :: forall s . TVar (IOSim s ) Int -> TVar (IOSim s ) [ThreadId (IOSim s )] -> Task -> IOSim s (ThreadId (IOSim s ))
262
- interpret r t (Task steps) = forkIO $ do
263
- context <- atomically $ do
264
+ interpret :: forall s .
265
+ TVar (IOSim s ) Int
266
+ -> TVar (IOSim s ) [ThreadId (IOSim s )]
267
+ -> Task
268
+ -> IOSim s (Async (IOSim s ) () )
269
+ interpret r t (Task steps) = async $ do
270
+ (ts, timer) <- atomically $ do
264
271
ts <- readTVar t
265
- when ( null ts) retry
272
+ check ( not ( null ts))
266
273
timer <- newTVar Nothing
267
274
return (ts,timer)
268
- mapM_ (interpretStep context) steps
269
- where interpretStep _ (WhenSet m n) = atomically $ do
270
- a <- readTVar r
271
- when (a/= m) retry
272
- writeTVar r n
273
- interpretStep (ts,_) (ThrowTo i) = throwTo (ts !! i) (ExitFailure 0 )
274
- interpretStep _ (Delay i) = threadDelay (fromIntegral i)
275
- interpretStep (_,timer) (Timeout tstep) = do
276
- timerVal <- atomically $ readTVar timer
277
- case (timerVal,tstep) of
278
- (_,NewTimeout n) -> do tout <- newTimeout (fromIntegral n)
279
- atomically $ writeTVar timer (Just tout)
280
- (Just tout,CancelTimeout ) -> cancelTimeout tout
281
- (Just tout,AwaitTimeout ) -> atomically $ awaitTimeout tout >> return ()
282
- (Nothing ,_) -> return ()
275
+ mapM_ (interpretStep ts timer) steps
276
+ where
277
+ interpretStep :: [ThreadId (IOSim s )]
278
+ -> TVar (IOSim s ) (Maybe _ ) -- Timeout is not exported
279
+ -> Step
280
+ -> IOSim s ()
281
+ interpretStep _ _ (WhenSet m n) = atomically $ do
282
+ readTVar r >>= check . (== m)
283
+ writeTVar r n
284
+ interpretStep ts _ (ThrowTo i) = throwTo (ts !! i) (ExitFailure 0 )
285
+ interpretStep _ _ (Delay i) = threadDelay (fromIntegral i)
286
+ interpretStep _ timer (Timeout tstep) = do
287
+ timerVal <- readTVarIO timer
288
+ case (timerVal,tstep) of
289
+ (_,NewTimeout n) -> do tout <- newTimeout (fromIntegral n)
290
+ atomically $ writeTVar timer (Just tout)
291
+ (Just tout,CancelTimeout ) -> cancelTimeout tout
292
+ (Just tout,AwaitTimeout ) -> atomically $ awaitTimeout tout >> return ()
293
+ (Nothing ,_) -> return ()
283
294
284
295
runTasks :: [Task ] -> IOSim s (Int ,Int )
285
296
runTasks tasks = do
286
297
let m = maximum [maxTaskValue t | Task t <- tasks]
287
- r <- atomically $ newTVar m
288
- t <- atomically $ newTVar []
298
+ r <- newTVarIO m
299
+ t <- newTVarIO []
289
300
exploreRaces
290
301
ts <- mapM (interpret r t) tasks
291
- atomically $ writeTVar t ts
292
- threadDelay 1000000000 -- allow the SUT threads to run
293
- a <- atomically $ readTVar r
302
+ atomically $ writeTVar t (asyncThreadId <$> ts)
303
+ traverse_ wait ts -- allow the SUT threads to run
304
+ a <- readTVarIO r
294
305
return (m,a)
295
306
296
307
maxTaskValue :: [Step ] -> Int
@@ -301,22 +312,24 @@ maxTaskValue [] = 0
301
312
propSimulates :: Tasks -> Property
302
313
propSimulates (Tasks tasks) =
303
314
any (not . null . (\ (Task steps)-> steps)) tasks ==>
304
- let Right (m,a) = runSim (runTasks tasks) in
305
- m>= a
315
+ let trace = runSimTrace (runTasks tasks) in
316
+ case traceResult False trace of
317
+ Right (m,a) -> property (m >= a)
318
+ Left x -> counterexample (ppTrace trace)
319
+ $ counterexample (show x) True
306
320
307
321
propExploration :: Tasks -> Property
308
322
propExploration (Tasks tasks) =
309
- -- Debug.trace ("\nTasks:\n"++ show tasks) $
310
323
any (not . null . (\ (Task steps)-> steps)) tasks ==>
311
324
traceNoDuplicates $ \ addTrace ->
312
325
-- traceCounter $ \addTrace ->
313
326
exploreSimTrace id (runTasks tasks) $ \ _ trace ->
314
- -- Debug.trace (("\nTrace:\n"++) . splitTrace . noExceptions $ show trace) $
315
327
addTrace trace $
316
328
counterexample (splitTrace . noExceptions $ show trace) $
317
329
case traceResult False trace of
318
- Right (m,a) -> property $ m>= a
319
- Left e -> counterexample (show e) False
330
+ Right (m,a) -> property (m >= a)
331
+ Left e -> counterexample (ppTrace trace)
332
+ $ counterexample (show e) True
320
333
321
334
-- Testing propPermutations n should collect every permutation of [1..n] once only.
322
335
-- Test manually, and supply a small value of n.
@@ -331,11 +344,11 @@ propPermutations n =
331
344
332
345
doit :: Int -> IOSim s [Int ]
333
346
doit n = do
334
- r <- atomically $ newTVar []
335
- exploreRaces
336
- mapM_ (\ i -> forkIO $ atomically $ modifyTVar r (++ [i])) [1 .. n]
337
- threadDelay 1
338
- atomically $ readTVar r
347
+ r <- atomically $ newTVar []
348
+ exploreRaces
349
+ mapM_ (\ i -> forkIO $ atomically $ modifyTVar r (++ [i])) [1 .. n]
350
+ threadDelay 1
351
+ atomically $ readTVar r
339
352
340
353
ordered :: Ord a => [a ] -> Bool
341
354
ordered xs = and (zipWith (<) xs (drop 1 xs))
0 commit comments