@@ -24,14 +24,16 @@ import Test.QuickCheck.Property (morallyDubiousIOProperty, Result(..), result)
24import Test.HUnit (Assertion, assertFailure)
24import Test.HUnit (Assertion, assertFailure)
25import Data.Map (Map)
25import Data.Map (Map)
26import qualified Data.Map as Map
26import qualified Data.Map as Map
27+import Control.Category ((>>>))
27import Control.Applicative ((<$>))
28import Control.Applicative ((<$>))
28import Control.Exception (Exception, throwIO)
29import Control.Exception (Exception, throwIO)
29import Control.Concurrent (forkIO, threadDelay)
30import Control.Concurrent (forkIO, threadDelay)
30import Control.Concurrent.Chan (Chan, newChan, writeChan, readChan)
31import Control.Concurrent.Chan (Chan, newChan, writeChan, readChan)
31import Control.Monad (replicateM, void)
32import Control.Monad (replicateM, void)
32−import Data.List (inits)
33+import Data.List (inits, delete)
33import Data.ByteString (ByteString)
34import Data.ByteString (ByteString)
34import Data.ByteString.Char8 (pack)
35import Data.ByteString.Char8 (pack)
36+import Data.Accessor (Accessor, accessor, (^:), (^.), (^=))
35import qualified Data.ByteString as BSS (concat)
37import qualified Data.ByteString as BSS (concat)
36import qualified Text.PrettyPrint as PP
38import qualified Text.PrettyPrint as PP
@@ -48,6 +50,11 @@ import Network.Transport.TCP.Mock.Socket (scheduleReadAction, sClose)
48-- Script infrastructure --
50-- Script infrastructure --
49--------------------------------------------------------------------------------
51--------------------------------------------------------------------------------
54+type SourceEndPointIx = Int
55+type TargetEndPointIx = Int
56+type ConnectionIx = Int
51-- | We randomly generate /scripts/ which are essentially a deep embedding of
58-- | We randomly generate /scripts/ which are essentially a deep embedding of
52-- the Transport API. These scripts are then executed and the results compared
59-- the Transport API. These scripts are then executed and the results compared
53-- against an abstract interpreter.
60-- against an abstract interpreter.
@@ -57,20 +64,20 @@ data ScriptCmd =
57 -- | @Connect i j@ creates a connection from endpoint @i@ to endpoint @j@,
64 -- | @Connect i j@ creates a connection from endpoint @i@ to endpoint @j@,
58 -- where @i@ and @j@ are indices and refer to the @i@th and @j@th endpoint
65 -- where @i@ and @j@ are indices and refer to the @i@th and @j@th endpoint
59 -- created by NewEndPoint
66 -- created by NewEndPoint
60− | Connect Int Int
67+ | Connect SourceEndPointIx TargetEndPointIx
61 -- | @Close i@ closes the @i@ connection created using 'Connect'. Note that
68 -- | @Close i@ closes the @i@ connection created using 'Connect'. Note that
62 -- closing a connection does not shift other indices; in other words, in
69 -- closing a connection does not shift other indices; in other words, in
63 -- @[Connect 0 0, Close 0, Connect 0 0, Close 0]@ the second 'Close'
70 -- @[Connect 0 0, Close 0, Connect 0 0, Close 0]@ the second 'Close'
64 -- refers to the first (already closed) connection
71 -- refers to the first (already closed) connection
65− | Close Int
72+ | Close ConnectionIx
66 -- | @Send i bs@ sends payload @bs@ on the @i@ connection created
73 -- | @Send i bs@ sends payload @bs@ on the @i@ connection created
67− | Send Int [ByteString]
74+ | Send ConnectionIx [ByteString]
68 -- | @BreakAfterReads n i j@ force-closes the socket between endpoints @i@
75 -- | @BreakAfterReads n i j@ force-closes the socket between endpoints @i@
69 -- and @j@ after @n@ reads by @i@
76 -- and @j@ after @n@ reads by @i@
71 -- We should have @i /= j@ because the TCP transport does not use sockets
78 -- We should have @i /= j@ because the TCP transport does not use sockets
72 -- for connections from an endpoint to itself
79 -- for connections from an endpoint to itself
73− | BreakAfterReads Int Int Int
80+ | BreakAfterReads Int SourceEndPointIx TargetEndPointIx
74 deriving Show
81 deriving Show
76type Script = [ScriptCmd]
83type Script = [ScriptCmd]
@@ -90,34 +97,40 @@ instance Show Script where
91instance Show (Map Int [Event]) where
98instance Show (Map Int [Event]) where
92 show = ("\n" ++) . show . eventsDoc
99 show = ("\n" ++) . show . eventsDoc
101+--------------------------------------------------------------------------------
103+--------------------------------------------------------------------------------
94-- | Execute a script
105-- | Execute a script
96-- Execute ignores error codes reported back. Instead, we verify the events
107-- Execute ignores error codes reported back. Instead, we verify the events
97-- that are posted
108-- that are posted
98−execScript :: (Transport, TransportInternals) -> Script -> IO (Map Int [Event])
109+execScript :: (Transport, TransportInternals) -> Script -> IO (Map EndPointIx [Event], VerificationState)
99execScript (transport, transportInternals) script = do
110execScript (transport, transportInternals) script = do
100 chan <- newChan
111 chan <- newChan
101− runScript chan script
112+ vst <- runScript chan script
102− collectAll chan
113+ evs <- collectAll chan
104− runScript :: Chan (Maybe (Int, Event)) -> Script -> IO ()
116+ runScript :: Chan (Maybe (EndPointIx, Event)) -> Script -> IO VerificationState
105 runScript chan = go [] []
117 runScript chan = go [] []
107− go :: [EndPoint] -> [Either (TransportError ConnectErrorCode) Connection] -> Script -> IO ()
119+ go :: [EndPoint] -> [Either (TransportError ConnectErrorCode) Connection] -> Script -> IO VerificationState
108− go _endPoints _conns [] = do
120+ go endPoints _conns [] = do
109 threadDelay 10000
121 threadDelay 10000
110 writeChan chan Nothing
122 writeChan chan Nothing
123+ return (initialVerificationState (map address endPoints))
111 go endPoints conns (NewEndPoint : cmds) = do
124 go endPoints conns (NewEndPoint : cmds) = do
112 endPoint <- throwIfLeft $ newEndPoint transport
125 endPoint <- throwIfLeft $ newEndPoint transport
113 let endPointIx = length endPoints
126 let endPointIx = length endPoints
114 _tid <- forkIO $ forwardTo chan (endPointIx, endPoint)
127 _tid <- forkIO $ forwardTo chan (endPointIx, endPoint)
115 threadDelay 10000
128 threadDelay 10000
116− go (endPoints ++ [endPoint]) conns cmds
129+ go (endPoint `snoc` endPoints) conns cmds
117 go endPoints conns (Connect fr to : cmds) = do
130 go endPoints conns (Connect fr to : cmds) = do
118 conn <- connect (endPoints !! fr) (address (endPoints !! to)) ReliableOrdered defaultConnectHints
131 conn <- connect (endPoints !! fr) (address (endPoints !! to)) ReliableOrdered defaultConnectHints
119 threadDelay 10000
132 threadDelay 10000
120− go endPoints (conns ++ [conn]) cmds
133+ go endPoints (conn `snoc` conns) cmds
121 go endPoints conns (Close connIx : cmds) = do
134 go endPoints conns (Close connIx : cmds) = do
122 case conns !! connIx of
135 case conns !! connIx of
123 Left _err -> return ()
136 Left _err -> return ()
@@ -135,7 +148,7 @@ execScript (transport, transportInternals) script = do
135 scheduleReadAction sock n (putStrLn "Closing" >> sClose sock)
148 scheduleReadAction sock n (putStrLn "Closing" >> sClose sock)
136 go endPoints conns cmds
149 go endPoints conns cmds
138− forwardTo :: Chan (Maybe (Int, Event)) -> (Int, EndPoint) -> IO ()
151+ forwardTo :: Chan (Maybe (EndPointIx, Event)) -> (EndPointIx, EndPoint) -> IO ()
139 forwardTo chan (ix, endPoint) = go
152 forwardTo chan (ix, endPoint) = go
141 go :: IO ()
154 go :: IO ()
@@ -145,7 +158,7 @@ execScript (transport, transportInternals) script = do
145 EndPointClosed -> return ()
158 EndPointClosed -> return ()
146 _ -> writeChan chan (Just (ix, ev)) >> go
159 _ -> writeChan chan (Just (ix, ev)) >> go
148− collectAll :: Chan (Maybe (Int, Event)) -> IO (Map Int [Event])
161+ collectAll :: Chan (Maybe (EndPointIx, Event)) -> IO (Map EndPointIx [Event])
149 collectAll chan = go Map.empty
162 collectAll chan = go Map.empty
151 go :: Map Int [Event] -> IO (Map Int [Event])
164 go :: Map Int [Event] -> IO (Map Int [Event])
@@ -159,41 +172,75 @@ execScript (transport, transportInternals) script = do
159 insertEvent ev Nothing = Just [ev]
172 insertEvent ev Nothing = Just [ev]
160 insertEvent ev (Just evs) = Just (ev : evs)
173 insertEvent ev (Just evs) = Just (ev : evs)
162−verify :: Script -> Map Int [Event] -> Maybe String
175+--------------------------------------------------------------------------------
163−verify = go []
176+-- Verification --
164− where
177+--------------------------------------------------------------------------------
179+data VerificationState = VerificationState {
180+ endPointAddrs :: [EndPointAddress]
181+ , _connections :: [(SourceEndPointIx, TargetEndPointIx, ConnectionId)]
182+ , _mayBreak :: [(SourceEndPointIx, TargetEndPointIx)]
185+initialVerificationState :: [EndPointAddress] -> VerificationState
186+initialVerificationState addrs = VerificationState {
187+ endPointAddrs = addrs
192+-- TODO: we currently have no way to verify addresses in ConnectionOpened
193+-- or EventConnectionLost (because we don't know the addresses of the endpoints)
165− go :: [(Int, ConnectionId)] -> Script -> Map Int [Event] -> Maybe String
194+verify :: VerificationState -> Script -> Map EndPointIx [Event] -> Maybe String
166− go _conns [] evs =
195+verify _st [] evs =
196+ -- TODO: we should compare the error events against mayBreak, but we
197+ -- cannot because we don't know the endpoint addresses
167− if concat (Map.elems evs) == []
198+ if removeErrorEvents (concat (Map.elems evs)) == []
168− then Nothing
199+ then Nothing
169− else Just $ "Unexpected events: " ++ show evs
200+ else Just $ "Unexpected events: " ++ show evs
170− go conns (NewEndPoint : cmds) evs =
201+verify st (NewEndPoint : cmds) evs =
171− go conns cmds evs
202+ verify st cmds evs
172− go conns (Connect _fr to : cmds) evs =
203+verify st (Connect fr to : cmds) evs =
173− let epEvs = evs Map.! to
204+ case destruct evs to of
175− (ConnectionOpened connId _rel _addr : epEvs') ->
205+ Just (ConnectionOpened connId _rel _addr, evs') ->
176− go (conns ++ [(to, connId)]) cmds (Map.insert to epEvs' evs)
206+ verify (connections ^: snoc (fr, to, connId) $ st) cmds evs'
178− Just $ "Missing (ConnectionOpened <<connId>> <<rel>> <<addr>>) event in " ++ show evs
208+ Just $ "Missing (ConnectionOpened <<connId>> <<rel>> <<addr>>). Got " ++ show ev
179− go conns (Close connIx : cmds) evs =
209+verify st (Close connIx : cmds) evs =
180− let (epIx, connId) = conns !! connIx
210+ let (_fr, to, connId) = st ^. connectionAt connIx in
181− epEvs = evs Map.! epIx
211+ case destruct evs to of
183− (ConnectionClosed connId' : epEvs') | connId' == connId ->
212+ Just (ConnectionClosed connId', evs') | connId' == connId ->
184− go conns cmds (Map.insert epIx epEvs' evs)
213+ verify st cmds evs'
186− Just $ "Missing (ConnectionClosed " ++ show connId ++ ") event in " ++ show evs
215+ Just $ "Missing (ConnectionClosed " ++ show connId ++ "). Got " ++ show ev
187− go conns (Send connIx payload : cmds) evs =
216+verify st (Send connIx payload : cmds) evs =
188− let (epIx, connId) = conns !! connIx
217+ let (fr, to, connId) = st ^. connectionAt connIx in
189− epEvs = evs Map.! epIx
218+ case destruct evs to of
191− (Received connId' payload' : epEvs') | connId' == connId && BSS.concat payload == BSS.concat payload' ->
219+ Just (Received connId' payload', evs') | connId' == connId && BSS.concat payload == BSS.concat payload' ->
192− go conns cmds (Map.insert epIx epEvs' evs)
220+ verify st cmds evs'
193− _ ->
221+ Just (ErrorEvent (TransportError (EventConnectionLost _addr) _), evs') | st ^. mayBreak fr to ->
194− Just $ "Missing (Received " ++ show connId ++ " " ++ show payload ++ ") event in " ++ show epEvs
224+ Just $ "Missing (Received " ++ show connId ++ " " ++ show payload ++ "). Got " ++ show ev
195− go conns (BreakAfterReads n i j : cmds) evs =
225+verify st (BreakAfterReads _n i j : cmds) evs =
196− go conns cmds evs
226+ verify (mayBreak i j ^= True $ st) cmds evs
228+connections :: Accessor VerificationState [(SourceEndPointIx, TargetEndPointIx, ConnectionId)]
229+connections = accessor _connections (\cs st -> st { _connections = cs })
231+connectionAt :: ConnectionIx -> Accessor VerificationState (SourceEndPointIx, TargetEndPointIx, ConnectionId)
232+connectionAt i = connections >>> listAccessor i
234+mayBreak :: EndPointIx -> EndPointIx -> Accessor VerificationState Bool
235+mayBreak i j = accessor
236+ (\st -> (i, j) `elem` _mayBreak st || (j, i) `elem` _mayBreak st)
237+ (\b st -> if b then st { _mayBreak = (i, j) : _mayBreak st }
238+ else st { _mayBreak = delete (i, j) . delete (j, i) $ _mayBreak st })
240+removeErrorEvents :: [Event] -> [Event]
241+removeErrorEvents [] = []
242+removeErrorEvents (ErrorEvent _ : evs) = removeErrorEvents evs
243+removeErrorEvents (ev : evs) = ev : removeErrorEvents evs
198--------------------------------------------------------------------------------
245--------------------------------------------------------------------------------
199-- Script generators --
246-- Script generators --
@@ -425,8 +472,8 @@ testScriptGen transport scriptGen =
425 forAll scriptGen $ \script ->
472 forAll scriptGen $ \script ->
426 morallyDubiousIOProperty $ do
473 morallyDubiousIOProperty $ do
427 logShow script
474 logShow script
428− evs <- execScript transport script
475+ (evs, vst) <- execScript transport script
429− return $ case verify script evs of
476+ return $ case verify vst script evs of
430 Nothing -> result { ok = Just True
477 Nothing -> result { ok = Just True
432 Just err -> result { ok = Just False
479 Just err -> result { ok = Just False
@@ -436,34 +483,11 @@ testScriptGen transport scriptGen =
436testScript :: (Transport, TransportInternals) -> Script -> Assertion
483testScript :: (Transport, TransportInternals) -> Script -> Assertion
437testScript transport script = do
484testScript transport script = do
438 logShow script
485 logShow script
439− evs <- execScript transport script
486+ (evs, vst) <- execScript transport script
440− case verify script evs of
487+ case verify vst script evs of
441− Just err -> assertFailure $ "Failed with script " ++ show script ++ ": " ++ err
488+ Just err -> assertFailure $ "Failed with script " ++ show script ++ ": " ++ err ++ "\nAll events: " ++ show evs
442 Nothing -> return ()
489 Nothing -> return ()
444−--------------------------------------------------------------------------------
446−--------------------------------------------------------------------------------
448−log :: String -> IO ()
449−log = appendFile "log" . (++ "\n")
451−logShow :: Show a => a -> IO ()
454−throwIfLeft :: Exception a => IO (Either a b) -> IO b
461−instance Arbitrary ByteString where
463− len <- chooseFrom' (NormalD { mean = 5, stdDev = 10 }) (0, 100)
464− xs <- replicateM len arbitrary
467--------------------------------------------------------------------------------
491--------------------------------------------------------------------------------
468-- Draw random values from probability distributions --
492-- Draw random values from probability distributions --
469--------------------------------------------------------------------------------
493--------------------------------------------------------------------------------
@@ -494,3 +518,38 @@ chooseFrom d (lo, hi) = findCandidate
494chooseFrom' :: Distribution d => d -> (Int, Int) -> Gen Int
518chooseFrom' :: Distribution d => d -> (Int, Int) -> Gen Int
495chooseFrom' d (lo, hi) =
519chooseFrom' d (lo, hi) =
496 round <$> chooseFrom d (fromIntegral lo, fromIntegral hi)
520 round <$> chooseFrom d (fromIntegral lo, fromIntegral hi)
522+--------------------------------------------------------------------------------
524+--------------------------------------------------------------------------------
526+log :: String -> IO ()
527+log = appendFile "log" . (++ "\n")
529+logShow :: Show a => a -> IO ()
532+throwIfLeft :: Exception a => IO (Either a b) -> IO b
539+instance Arbitrary ByteString where
541+ len <- chooseFrom' (NormalD { mean = 5, stdDev = 10 }) (0, 100)
542+ xs <- replicateM len arbitrary
545+listAccessor :: Int -> Accessor [a] a
546+listAccessor i = accessor (!! i) (error "listAccessor.set not defined")
548+snoc :: a -> [a] -> [a]
549+snoc x xs = xs ++ [x]
551+destruct :: Map EndPointIx [Event] -> EndPointIx -> Maybe (Event, Map EndPointIx [Event])
555+ ev : evs' -> Just (ev, Map.insert i evs' evs)