Added prop_connection_manager_timeouts_enforced

ouroboros-network-framework/ouroboros-network-framework.cabal

@@ -144,6 +144,7 @@ test-suite test
                      , quickcheck-instances
                      , tasty
                      , tasty-quickcheck
+                     , these
 
                      , cardano-prelude
                      , contra-tracer

ouroboros-network-framework/src/Ouroboros/Network/ConnectionManager/Types.hs

@@ -209,7 +209,7 @@ data DataFlow
 -- | Boolean like type which indicates if the timeout on 'OutboundStateDuplex'
 -- has expired.
 data TimeoutExpired = Expired | Ticking
-  deriving (Eq, Show)
+  deriving (Eq, Ord, Show)
 
 
 
@@ -654,7 +654,7 @@ data AbstractState
     | WaitRemoteIdleSt
     | TerminatingSt
     | TerminatedSt
-    deriving (Eq, Show, Typeable)
+    deriving (Eq, Ord, Show, Typeable)
 
 
 -- | Counters for tracing and analysis purposes

ouroboros-network-framework/test/Test/Ouroboros/Network/Server2.hs

@@ -27,7 +27,7 @@ module Test.Ouroboros.Network.Server2
   ( tests
   ) where
 
-import           Control.Exception (AssertionFailed, SomeAsyncException (..))
+import           Control.Exception (AssertionFailed, SomeAsyncException (..), throw)
 import           Control.Monad (replicateM, when, (>=>))
 import           Control.Monad.Class.MonadAsync
 import           Control.Monad.Class.MonadThrow
@@ -48,13 +48,15 @@ import           Data.Bitraversable
 import           Data.Bool (bool)
 import           Data.ByteString.Lazy (ByteString)
 import qualified Data.ByteString.Lazy as LBS
+import           Data.Dynamic (fromDynamic)
 import           Data.Foldable (foldMap')
 import           Data.Functor (void, ($>), (<&>))
 import           Data.List (dropWhileEnd, find, mapAccumL, intercalate, (\\), delete, foldl')
 import           Data.List.NonEmpty (NonEmpty (..))
 import qualified Data.List.Trace as Trace
+import           Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
-import           Data.Maybe (fromMaybe, fromJust, isJust)
+import           Data.Maybe (fromMaybe, fromJust, isJust, catMaybes)
 import           Data.Monoid (Sum (..))
 import           Data.Monoid.Synchronisation (FirstToFinish (..))
 import qualified Data.Set as Set
@@ -157,6 +159,8 @@ tests =
                  prop_connection_manager_counters
   , testProperty "inbound_governor_counters"
                  prop_inbound_governor_counters
+  , testProperty "connection_manager_timeouts_enforced"
+                 prop_connection_manager_timeouts_enforced
   , testGroup    "unit_server_accept_error"
     [ testProperty "throw ConnectionAborted"
                   (unit_server_accept_error IOErrConnectionAborted IOErrThrow)
@@ -2024,10 +2028,10 @@ prop_connection_manager_valid_transitions serverAcc (ArbDataFlow dataFlow)
       abstractTransitionEvents = traceWithNameTraceEvents trace
 
       connectionManagerEvents :: [ConnectionManagerTrace
-                  SimAddr
-                  (ConnectionHandlerTrace
-                    UnversionedProtocol
-                    DataFlowProtocolData)]
+                                    SimAddr
+                                    (ConnectionHandlerTrace
+                                      UnversionedProtocol
+                                      DataFlowProtocolData)]
       connectionManagerEvents = withNameTraceEvents trace
 
   in tabulate "ConnectionEvents" (map showConnectionEvents events)
@@ -2067,7 +2071,7 @@ prop_connection_manager_valid_transitions serverAcc (ArbDataFlow dataFlow)
              tpTransitions         = trs
           }
        )
-    . splitConns
+    . traceSplitConns
     $ abstractTransitionEvents
   where
     sim :: IOSim s ()
@@ -2151,7 +2155,7 @@ prop_connection_manager_valid_transition_order serverAcc (ArbDataFlow dataFlow)
            _             -> AllProperty (property False)
        )
        verifyAbstractTransitionOrder
-    . splitConns
+    . traceSplitConns
     $ abstractTransitionEvents
   where
     sim :: IOSim s ()
@@ -2366,6 +2370,112 @@ prop_connection_manager_counters serverAcc (ArbDataFlow dataFlow)
         Nothing -> throwIO (SimulationTimeout :: ExperimentError SimAddr)
         Just a  -> return a
 
+
+-- | Property wrapping `multinodeExperiment`.
+--
+-- Note: this test verifies that connection-manager timeouts are enforced.
+prop_connection_manager_timeouts_enforced :: Int
+                                          -> ArbDataFlow
+                                          -> AbsBearerInfo
+                                          -> MultiNodeScript Int TestAddr
+                                          -> Property
+prop_connection_manager_timeouts_enforced serverAcc (ArbDataFlow dataFlow)
+                                          absBi (MultiNodeScript events) =
+  let trace = runSimTrace sim
+
+      transitionSignal :: [[(Time, AbstractTransitionTrace SimAddr)]]
+      transitionSignal = splitConns
+                      $ getTraceEvents
+                      $ trace
+
+  in verifyAllTimeouts transitionSignal
+  where
+    verifyAllTimeouts :: [[(Time , AbstractTransitionTrace SimAddr)]]
+                      -> Property
+    verifyAllTimeouts [] = property True
+    verifyAllTimeouts (t:tts) =
+      counterexample ("\nConnection transition trace:\n"
+                     ++ intercalate "\n" (map show t)
+                     )
+      $ verifyTimeouts Map.empty t
+      .&&. verifyAllTimeouts tts
+
+    verifyTimeouts :: Map AbstractState Time
+                   -> [(Time , AbstractTransitionTrace SimAddr)]
+                   -> Property
+    verifyTimeouts stateMap [] =
+      counterexample
+        ("These states didn't timeout:\n"
+        ++ show stateMap
+        )
+      $ Map.null stateMap
+    verifyTimeouts stateMap ((t, TransitionTrace _ tt@(Transition from to)):xs)
+      | Map.member from stateMap =
+        let newStateMap  = Map.delete from stateMap
+            newStateMap' = Map.insert to t newStateMap
+            t'           = stateMap Map.! from
+            valid        = case from of
+              InboundIdleSt _  ->
+               counterexample
+                 (errorMsg tt t' t (tProtocolIdleTimeout simTimeouts))
+               $ diffTime t t' <= tProtocolIdleTimeout simTimeouts
+              OutboundDupSt _  ->
+               counterexample
+                 (errorMsg tt t' t (tOutboundIdleTimeout simTimeouts))
+               $ diffTime t t' <= tOutboundIdleTimeout simTimeouts
+              OutboundIdleSt _ ->
+               counterexample
+                 (errorMsg tt t' t (tOutboundIdleTimeout simTimeouts))
+               $ diffTime t t' <= tOutboundIdleTimeout simTimeouts
+              TerminatingSt    ->
+               counterexample
+                 (errorMsg tt t' t (tTimeWaitTimeout simTimeouts))
+               $ diffTime t t' <= tTimeWaitTimeout simTimeouts
+              _                -> property True
+         in case to of
+           InboundIdleSt _       -> valid .&&. verifyTimeouts newStateMap' xs
+           OutboundDupSt Ticking -> valid .&&. verifyTimeouts newStateMap' xs
+           OutboundIdleSt _      -> valid .&&. verifyTimeouts newStateMap' xs
+           TerminatingSt         -> valid .&&. verifyTimeouts newStateMap' xs
+           _                     -> verifyTimeouts newStateMap xs
+      | otherwise                =
+        let newStateMap = Map.insert to t stateMap
+         in case to of
+           InboundIdleSt _       -> verifyTimeouts newStateMap xs
+           OutboundDupSt Ticking -> verifyTimeouts newStateMap xs
+           OutboundIdleSt _      -> verifyTimeouts newStateMap xs
+           TerminatingSt         -> verifyTimeouts newStateMap xs
+           _                     -> verifyTimeouts stateMap xs
+      where
+        errorMsg trand time' time maxDiffTime=
+          ("\nAt transition: " ++ show trand ++ "\n"
+          ++ "First happened at: " ++ show time' ++ "\n"
+          ++ "Second happened at: " ++ show time ++ "\n"
+          ++ "Should only take: "
+          ++ show maxDiffTime
+          ++ ", but took:" ++ show (diffTime time time')
+          )
+
+    getTraceEvents :: forall a b. Typeable b
+                      => SimTrace a
+                      -> [(Time, b)]
+    getTraceEvents = go
+      where
+        go (SimTrace t _ _ (EventLog e) trace)
+         | Just (WithName MainServer x)
+              <- fromDynamic
+                  @(WithName (Name SimAddr) b)
+                  e = (t,x) : go trace
+        go (SimTrace _ _ _ _ trace)   =         go trace
+        go (TraceMainException _ e _) = throw e
+        go (TraceDeadlock      _   _) = [] -- expected result in many cases
+        go (TraceMainReturn    _ _ _) = []
+
+    sim :: IOSim s ()
+    sim = multiNodeSim serverAcc dataFlow
+                       (Script (toBearerInfo absBi :| [noAttenuation]))
+                       maxAcceptedConnectionsLimit events
+
 -- | Property wrapping `multinodeExperiment`.
 --
 -- Note: this test validates inbound governor state changes.
@@ -2653,10 +2763,10 @@ prop_connection_manager_pruning serverAcc
       abstractTransitionEvents = traceWithNameTraceEvents trace
 
       connectionManagerEvents :: [ConnectionManagerTrace
-                  SimAddr
-                  (ConnectionHandlerTrace
-                    UnversionedProtocol
-                    DataFlowProtocolData)]
+                                    SimAddr
+                                    (ConnectionHandlerTrace
+                                      UnversionedProtocol
+                                      DataFlowProtocolData)]
       connectionManagerEvents = withNameTraceEvents trace
 
   in tabulate "ConnectionEvents" (map showConnectionEvents events)
@@ -2696,7 +2806,7 @@ prop_connection_manager_pruning serverAcc
              tpTransitions         = trs
           }
        )
-    . splitConns
+    . traceSplitConns
     $ abstractTransitionEvents
   where
     sim :: IOSim s ()
@@ -2811,11 +2921,11 @@ prop_never_above_hardlimit serverAcc
   let trace = runSimTrace sim
 
       connectionManagerEvents :: Trace (SimResult ())
-                        (ConnectionManagerTrace
-                          SimAddr
-                          (ConnectionHandlerTrace
-                            UnversionedProtocol
-                            DataFlowProtocolData))
+                                       (ConnectionManagerTrace
+                                         SimAddr
+                                         (ConnectionHandlerTrace
+                                           UnversionedProtocol
+                                           DataFlowProtocolData))
       connectionManagerEvents = traceWithNameTraceEvents trace
 
       abstractTransitionEvents :: Trace (SimResult ()) (AbstractTransitionTrace SimAddr)
@@ -3036,9 +3146,9 @@ unit_connection_terminated_when_negotiating =
 -- the property that every connection is terminated with 'UnknownConnectionSt'.
 -- This property is verified by 'verifyAbstractTransitionOrder'.
 --
-splitConns :: Trace (SimResult ()) (AbstractTransitionTrace SimAddr)
-           -> Trace (SimResult ()) [AbstractTransition]
-splitConns =
+traceSplitConns :: Trace (SimResult ()) (AbstractTransitionTrace SimAddr)
+                -> Trace (SimResult ()) [AbstractTransition]
+traceSplitConns =
     bimap id fromJust
   . Trace.filter isJust
   -- there might be some connections in the state, push them onto the 'Trace'
@@ -3064,6 +3174,32 @@ splitConns =
       )
       Map.empty
 
+splitConns :: [(Time, AbstractTransitionTrace SimAddr)]
+           -> [[(Time, AbstractTransitionTrace SimAddr)]]
+splitConns =
+    catMaybes
+  -- there might be some connections in the state, push them onto the 'Trace'
+  . (\(s, o) -> foldr (\a as -> Just a : as) o (Map.elems s))
+  . mapAccumL
+      ( \ s (t, tt@TransitionTrace { ttPeerAddr, ttTransition }) ->
+          case ttTransition of
+            Transition _ UnknownConnectionSt ->
+              case ttPeerAddr `Map.lookup` s of
+                Nothing  -> ( Map.insert ttPeerAddr [(t, tt)] s
+                            , Nothing
+                            )
+                Just trs -> ( Map.delete ttPeerAddr s
+                            , Just (reverse $ (t, tt) : trs)
+                            )
+            _ ->            ( Map.alter ( \ case
+                                              Nothing -> Just [(t, tt)]
+                                              Just as -> Just ((t, tt) : as)
+                                        ) ttPeerAddr s
+                            , Nothing
+                            )
+      )
+      Map.empty
+
 splitRemoteConns :: Trace (SimResult ()) (RemoteTransitionTrace SimAddr)
                  -> Trace (SimResult ()) [RemoteTransition]
 splitRemoteConns =

ouroboros-network-testing/src/Ouroboros/Network/Testing/Data/Signal.hs

@@ -27,6 +27,7 @@ module Ouroboros.Network.Testing.Data.Signal (
 
   -- * Simple signal transformations
   truncateAt,
+  truncateFrom,
   stable,
   nub,
   nubBy,
@@ -210,13 +211,21 @@ stable (Signal x xs) =
   where
     sameTime (E (TS t _) _) (E (TS t' _) _) = t == t'
 
--- Truncate a 'Signal' after a given time. This is typically necessary to
+-- | Truncate a 'Signal' after a given time. This is typically necessary to
 -- check properties over finite prefixes of infinite signals.
 --
 truncateAt :: Time -> Signal a -> Signal a
 truncateAt horizon (Signal x txs) =
     Signal x (takeWhile (\(E (TS t _) _) -> t < horizon) txs)
 
+-- | Truncate a 'Signal' for a given time. This is particularly necessary to
+-- assist merging two signals starting from the least common Time tag.
+--
+-- Use carefully with infinite signals.
+--
+truncateFrom :: Time -> Signal a -> Signal a
+truncateFrom horizon (Signal x txs) =
+    Signal x (dropWhile (\(E (TS t _) _) -> t < horizon) txs)
 
 -- | Sometimes the way a signal is constructed leads to duplicate signal values
 -- which can slow down signal processing. This tidies up the signal by