@@ -46,6 +46,7 @@ import Data.Unique (Unique, newUnique, hashUnique)
4646import Data.Concurrent.Queue.MichaelScott (newQ, pushL, tryPopR)
4747import Data.Set (Set)
4848import qualified Data.Set as Set
49+import GHC.Stack (currentCallStack, renderStack)
4950
5051import Network.Transport
5152import Network.Transport.TCP
@@ -53,7 +54,7 @@ import Network.Transport.TCP
5354 , defaultTCPParameters
5455 , TransportInternals(socketBetween)
5556 )
56−import Network.Transport.TCP.Mock.Socket (scheduleReadAction, sClose)
57+import Network.Transport.TCP.Mock.Socket (Socket, scheduleReadAction, sClose)
5758
5859--------------------------------------------------------------------------------
5960-- Script infrastructure --
@@ -104,12 +105,7 @@ instance Show a => Show (Variable a) where
104105
105106-- | In the implementation "bundles" are purely a conceptual idea, but in the
106107-- verifier we need to concretize this notion
107−--
108−-- Invariant: first endpoint address < second endpoint address
109−type BundleId = (EndPointAddress, EndPointAddress, Int)
110−
111−incrementBundleId :: BundleId -> BundleId
112−incrementBundleId (a, b, i) = (a, b, i + 1)
108+type BundleId = Int
113109
114110data ConnectionInfo = ConnectionInfo {
115111 source :: EndPointAddress
@@ -131,9 +127,19 @@ data RunState = RunState {
131127 , _connections :: [(Connection, ConnectionInfo)]
132128 , _expectedEvents :: Map EndPointAddress [ExpEvent]
133129 , _forwardingThreads :: [ThreadId]
130+ -- | When a connection from A to be may break, we add both (A, B, n)
131+ -- and (B, A, n) to _mayBreak. Then once we detect that from A to B
132+ -- has in fact broken we move (A, B, n), *and/or* (B, A, n), from _mayBreak
133+ -- to _broken. Note that we can detect that a connection has been broken
134+ -- in one direction even if we haven't yet detected that the connection
135+ -- has broken in the other direction.
136+ --
134137 -- | Invariant: not mayBreak && broken
135− , _mayBreak :: Set BundleId
136− , _broken :: Set BundleId
138+ , _mayBreak :: Set (EndPointAddress, EndPointAddress, BundleId)
139+ , _broken :: Set (EndPointAddress, EndPointAddress, BundleId)
140+ -- | Current bundle ID between two endpoints
141+ --
142+ -- Invariant: For all keys (A, B), A <= B
137143 , _currentBundle :: Map (EndPointAddress, EndPointAddress) BundleId
138144 }
139145
@@ -170,12 +176,14 @@ verify (transport, transportInternals) script = do
170176 endPointA <- get (endPointAtIx i)
171177 endPointB <- address <$> get (endPointAtIx j)
172178 mConn <- liftIO $ connect endPointA endPointB ReliableOrdered defaultConnectHints
173− let bundleId = currentBundle (address endPointA) endPointB
179+ let bundleId = currentBundle (address endPointA) endPointB
180+ connBroken = broken (address endPointA) endPointB
181+ connMayBreak = mayBreak (address endPointA) endPointB
174182 case mConn of
175183 Right conn -> do
176− bundleBroken <- get bundleId >>= get . broken
184+ bundleBroken <- get bundleId >>= get . connBroken
177185 currentBundleId <- if bundleBroken
178− then modify bundleId incrementBundleId >> get bundleId
186+ then modify bundleId (+ 1) >> get bundleId
179187 else get bundleId
180188 connId <- Variable <$> liftIO newUnique
181189 let connInfo = ConnectionInfo {
@@ -188,12 +196,12 @@ verify (transport, transportInternals) script = do
188196 append (expectedEventsAt endPointB) (ExpConnectionOpened connInfo)
189197 Left err -> do
190198 currentBundleId <- get bundleId
191− expectingBreak <- get $ mayBreak currentBundleId
199+ expectingBreak <- get $ connMayBreak currentBundleId
192200 if expectingBreak
193201 then do
194− set (mayBreak currentBundleId) False
195− set (broken currentBundleId) True
196− else
202+ set (connMayBreak currentBundleId) False
203+ set (connBroken currentBundleId) True
204+ else
197205 liftIO $ throwIO err
198206 runCmd (Close i) = do
199207 (conn, connInfo) <- get (connectionAt i)
@@ -202,15 +210,17 @@ verify (transport, transportInternals) script = do
202210 runCmd (Send i payload) = do
203211 (conn, connInfo) <- get (connectionAt i)
204212 mResult <- liftIO $ send conn payload
213+ let connMayBreak = mayBreak (source connInfo) (target connInfo) (connectionBundle connInfo)
214+ connBroken = broken (source connInfo) (target connInfo) (connectionBundle connInfo)
205215 case mResult of
206216 Right () -> return ()
207217 Left err -> do
208− expectingBreak <- get $ mayBreak (connectionBundle connInfo)
209− isBroken <- get $ broken (connectionBundle connInfo)
218+ expectingBreak <- get connMayBreak
219+ isBroken <- get connBroken
210220 if expectingBreak || isBroken
211221 then do
212− set (mayBreak (connectionBundle connInfo)) False
213− set (broken (connectionBundle connInfo)) True
222+ set connMayBreak False
223+ set connBroken True
214224 else
215225 liftIO $ throwIO err
216226 append (expectedEventsAt (target connInfo)) (ExpReceived connInfo payload)
@@ -219,9 +229,10 @@ verify (transport, transportInternals) script = do
219229 endPointB <- address <$> get (endPointAtIx j)
220230 liftIO $ do
221231 sock <- socketBetween transportInternals endPointA endPointB
222− scheduleReadAction sock n (sClose sock)
232+ scheduleReadAction sock n $ breakSocket sock
223233 currentBundleId <- get (currentBundle endPointA endPointB)
224− set (mayBreak currentBundleId) True
234+ set (mayBreak endPointA endPointB currentBundleId) True
235+ set (mayBreak endPointB endPointA currentBundleId) True
225236 append (expectedEventsAt endPointA) (ExpConnectionLost currentBundleId endPointB)
226237 append (expectedEventsAt endPointB) (ExpConnectionLost currentBundleId endPointA)
227238
@@ -255,6 +266,11 @@ verify (transport, transportInternals) script = do
255266 else Left ("Could not match " ++ show (st ^. expectedEvents)
256267 ++ " and " ++ show actualEvents)
257268
269+breakSocket :: Socket -> IO ()
270+breakSocket sock = do
271+ currentCallStack >>= putStrLn . renderStack
272+ sClose sock
273+
258274--------------------------------------------------------------------------------
259275-- Match expected and actual events --
260276--------------------------------------------------------------------------------
@@ -703,21 +719,19 @@ expectedEventsAt addr = expectedEvents >>> DAC.mapDefault [] addr
703719forwardingThreads :: Accessor RunState [ThreadId]
704720forwardingThreads = accessor _forwardingThreads (\ts st -> st { _forwardingThreads = ts })
705721
706−mayBreak :: BundleId -> Accessor RunState Bool
707−mayBreak bid = aux >>> DAC.set bid
722+mayBreak :: EndPointAddress -> EndPointAddress -> BundleId -> Accessor RunState Bool
723+mayBreak a b bid = aux >>> DAC.set (a, b, bid)
708724 where
709− aux :: Accessor RunState (Set BundleId)
710725 aux = accessor _mayBreak (\bs st -> st { _mayBreak = bs })
711726
712−broken :: BundleId -> Accessor RunState Bool
713−broken bid = aux >>> DAC.set bid
727+broken :: EndPointAddress -> EndPointAddress -> BundleId -> Accessor RunState Bool
728+broken a b bid = aux >>> DAC.set (a, b, bid)
714729 where
715− aux :: Accessor RunState (Set BundleId)
716730 aux = accessor _broken (\bs st -> st { _broken = bs })
717731
718732currentBundle :: EndPointAddress -> EndPointAddress -> Accessor RunState BundleId
719−currentBundle i j = aux >>> if i < j then DAC.mapDefault (i, j, 0) (i, j)
720− else DAC.mapDefault (j, i, 0) (j, i)
733+currentBundle i j = aux >>> if i < j then DAC.mapDefault 0 (i, j)
734+ else DAC.mapDefault 0 (j, i)
721735 where
722736 aux :: Accessor RunState (Map (EndPointAddress, EndPointAddress) BundleId)
723737 aux = accessor _currentBundle (\mp st -> st { _currentBundle = mp })