1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
|
import Debug.QuickCheck
import System.IO.Unsafe
import Control.Concurrent.MVar
import Control.Concurrent
import Control.Monad
data Action = NewEmptyMVar | NewMVar Int | TakeMVar | ReadMVar | PutMVar Int
| SwapMVar Int | IsEmptyMVar | ReturnInt Int | ReturnBool Bool
deriving (Eq,Show)
main = do
t <- myThreadId
forkIO (threadDelay 1000000 >> killThread t)
-- just in case we deadlock
testMVar
testMVar :: IO ()
testMVar = do
quickCheck prop_NewEIs_NewERet
quickCheck prop_NewIs_NewRet
quickCheck prop_NewTake_NewRet
quickCheck prop_NewEPutTake_NewERet
quickCheck prop_NewRead_NewRet
quickCheck prop_NewSwap_New
prop_NewEIs_NewERet =
[NewEmptyMVar,IsEmptyMVar] =^ [NewEmptyMVar,ReturnBool True]
prop_NewIs_NewRet n =
[NewMVar n,IsEmptyMVar] =^ [NewMVar n,ReturnBool False]
prop_NewTake_NewRet n =
[NewMVar n,TakeMVar] =^ [NewEmptyMVar,ReturnInt n]
prop_NewEPutTake_NewERet n =
[NewEmptyMVar,PutMVar n,TakeMVar] =^
[NewEmptyMVar,ReturnInt n]
prop_NewRead_NewRet n =
[NewMVar n,ReadMVar] =^ [NewMVar n,ReturnInt n]
prop_NewSwap_New m n =
[NewMVar m,SwapMVar n] =^ [NewMVar n]
perform :: [Action] -> IO ([Bool],[Int])
perform [] = return ([],[])
perform (a:as) =
case a of
ReturnInt v -> liftM (\(b,l) -> (b,v:l)) (perform as)
ReturnBool v -> liftM (\(b,l) -> (v:b,l)) (perform as)
NewEmptyMVar -> newEmptyMVar >>= \mv -> perform' mv as
NewMVar n -> newMVar n >>= \mv -> perform' mv as
_ -> error $ "Please use NewMVar or NewEmptyMVar as first "
++ "action"
perform' :: MVar Int -> [Action] -> IO ([Bool],[Int])
perform' _ [] = return ([],[])
perform' mv (a:as) =
case a of
ReturnInt v -> liftM (\(b,l) -> (b,v:l)) (perform' mv as)
ReturnBool v -> liftM (\(b,l) -> (v:b,l)) (perform' mv as)
TakeMVar -> liftM2 (\v (b,l) -> (b,v:l)) (takeMVar mv)
(perform' mv as)
ReadMVar -> liftM2 (\v (b,l) -> (b,v:l)) (readMVar mv)
(perform' mv as)
PutMVar n -> putMVar mv n >> perform' mv as
SwapMVar n -> swapMVar mv n >> perform' mv as
IsEmptyMVar -> liftM2 (\v (b,l) -> (v:b,l)) (isEmptyMVar mv)
(perform' mv as)
_ -> error $ "If you want to use " ++ show a
++ " please use the =^ operator"
actions :: Gen [Action]
actions = do
oneof [liftM (NewEmptyMVar:) (actions' True),
liftM2 (:) (liftM NewMVar arbitrary) (actions' False)]
actions' :: Bool -> Gen [Action]
actions' empty =
oneof ([return [],
liftM (IsEmptyMVar:) (actions' empty)] ++
if empty
then [liftM2 (:) (liftM PutMVar arbitrary) (actions' False)]
else []
++
if empty
then []
else [liftM (TakeMVar:) (actions' True)]
++
if empty
then []
else [liftM (ReadMVar:) (actions' False)]
++
if empty
then []
else [liftM2 (:) (liftM SwapMVar arbitrary) (actions' False)] )
(=^) :: [Action] -> [Action] -> Property
c =^ c' =
forAll (actions' (delta True c))
(\suff -> observe c suff == observe c' suff)
where observe x suff = unsafePerformIO (perform (x++suff))
(^=^) :: [Action] -> [Action] -> Property
c ^=^ c' =
forAll actions
(\pref -> forAll (actions' (delta True (pref++c)))
(\suff -> observe c pref suff ==
observe c' pref suff))
where observe x pref suff = unsafePerformIO (perform (pref++x++suff))
delta :: Bool -> [Action] -> Bool
delta b [] = b
delta b (ReturnInt _:as) = delta b as
delta b (ReturnBool _:as) = delta b as
delta _ (NewEmptyMVar:as) = delta True as
delta _ (NewMVar _:as) = delta False as
delta b (TakeMVar:as) = delta (if b
then error "take on empty MVar"
else True) as
delta b (ReadMVar:as) = delta (if b
then error "read on empty MVar"
else False) as
delta _ (PutMVar _:as) = delta False as
delta b (SwapMVar _:as) = delta (if b
then error "swap on empty MVar"
else False) as
delta b (IsEmptyMVar:as) = delta b as
|
