inbound-governor: verify inbound governor state invariant

IntersectMBO · May 6, 2024 · 1a0f009 · 1a0f009
1 parent 18e92c9
commit 1a0f009
Show file tree

Hide file tree

Showing 8 changed files with 102 additions and 15 deletions.
diff --git a/ouroboros-network-framework/demo/connection-manager.hs b/ouroboros-network-framework/demo/connection-manager.hs
@@ -279,6 +279,7 @@ withBidirectionalConnectionManager snocket makeBearer socket
                   serverTracer = ("server",) `contramap` debugTracer, -- ServerTrace
                   serverTrTracer = nullTracer,
                   serverInboundGovernorTracer = ("inbound-governor",) `contramap` debugTracer,
+                  serverDebugInboundGovernor = nullTracer,
                   serverConnectionLimits = AcceptedConnectionsLimit maxBound maxBound 0,
                   serverConnectionManager = connectionManager,
                   serverInboundIdleTimeout = Just protocolIdleTimeout,

diff --git a/ouroboros-network-framework/ouroboros-network-framework.cabal b/ouroboros-network-framework/ouroboros-network-framework.cabal
@@ -187,6 +187,7 @@ test-suite sim-tests
                      , iproute
                      , network
                      , pretty-simple
+                     , psqueues
                      , random
                      , serialise
                      , text

diff --git a/ouroboros-network-framework/sim-tests/Test/Ouroboros/Network/Server2/Sim.hs b/ouroboros-network-framework/sim-tests/Test/Ouroboros/Network/Server2/Sim.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE FlexibleContexts    #-}
 {-# LANGUAGE GADTs               #-}
 {-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE NamedFieldPuns      #-}
 {-# LANGUAGE NumericUnderscores  #-}
 {-# LANGUAGE PolyKinds           #-}
 {-# LANGUAGE RankNTypes          #-}
@@ -52,6 +53,7 @@ import Data.Map.Strict qualified as Map
 import Data.Maybe (fromMaybe)
 import Data.Monoid (Sum (..))
 import Data.Monoid.Synchronisation (FirstToFinish (..))
+import Data.OrdPSQ qualified as OrdPSQ
 import Data.Set qualified as Set
 import Data.Typeable (Typeable)
 import System.Random (StdGen, mkStdGen, split)
@@ -70,9 +72,11 @@ import Ouroboros.Network.ConnectionHandler
 import Ouroboros.Network.ConnectionId
 import Ouroboros.Network.ConnectionManager.Types
 import Ouroboros.Network.ConnectionManager.Types qualified as CM
-import Ouroboros.Network.InboundGovernor (InboundGovernorTrace (..))
+import Ouroboros.Network.InboundGovernor (DebugInboundGovernor (..),
+           InboundGovernorTrace (..))
 import Ouroboros.Network.InboundGovernor qualified as IG
-import Ouroboros.Network.InboundGovernor.State (InboundGovernorCounters (..))
+import Ouroboros.Network.InboundGovernor.State (ConnectionState (..),
+           InboundGovernorCounters (..))
 import Ouroboros.Network.Mux
 import Ouroboros.Network.MuxMode
 import Ouroboros.Network.Protocol.Handshake.Codec (noTimeLimitsHandshake,
@@ -98,6 +102,7 @@ import Ouroboros.Network.ConnectionManager.Test.Utils
            (abstractStateIsFinalTransition, allValidTransitionsNames,
            validTransitionMap, verifyAbstractTransition,
            verifyAbstractTransitionOrder)
+import Ouroboros.Network.InboundGovernor.State (InboundGovernorState (..))
 import Ouroboros.Network.InboundGovernor.Test.Utils
            (allValidRemoteTransitionsNames, remoteStrIsFinalTransition,
            validRemoteTransitionMap, verifyRemoteTransition,
@@ -126,6 +131,7 @@ tests =
     , testProperty "no unsupported state"   prop_inbound_governor_no_unsupported_state
     , testProperty "pruning"                prop_inbound_governor_pruning
     , testProperty "counters"               prop_inbound_governor_counters
+    , testProperty "InboundGovernorState"   prop_inbound_governor_state
     , testProperty "timeouts enforced"      prop_timeouts_enforced
     ]
   , testGroup "Server2"
@@ -626,6 +632,8 @@ multinodeExperiment
                           (AbstractTransitionTrace peerAddr))
     -> Tracer m (WithName (Name peerAddr)
                           (InboundGovernorTrace peerAddr))
+    -> Tracer m (WithName (Name peerAddr)
+                          (DebugInboundGovernor peerAddr))
     -> Tracer m (WithName (Name peerAddr)
                           (ConnectionManagerTrace
                             peerAddr
@@ -641,7 +649,7 @@ multinodeExperiment
     -> AcceptedConnectionsLimit
     -> MultiNodeScript req peerAddr
     -> m ()
-multinodeExperiment inboundTrTracer trTracer inboundTracer cmTracer
+multinodeExperiment inboundTrTracer trTracer inboundTracer debugTracer cmTracer
                     stdGen0 snocket makeBearer addrFamily serverAddr accInit
                     dataFlow0 acceptedConnLimit
                     (MultiNodeScript script _) =
@@ -773,7 +781,7 @@ multinodeExperiment inboundTrTracer trTracer inboundTracer cmTracer
                   Job ( withBidirectionalConnectionManager
                           name simTimeouts
                           inboundTrTracer trTracer cmTracer
-                          inboundTracer
+                          inboundTracer debugTracer
                           stdGen
                           snocket makeBearer (\_ -> pure ()) fd (Just localAddr) serverAcc
                           (mkNextRequests connVar)
@@ -1412,6 +1420,7 @@ prop_connection_manager_counters (Fixed rnd) serverAcc (ArbDataFlow dataFlow)
                 multinodeExperiment (sayTracer <> Tracer traceM)
                                     (sayTracer <> Tracer traceM)
                                     (sayTracer <> Tracer traceM)
+                                    nullTracer
                                     (   sayTracer
                                      <> Tracer traceM
                                      <> networkStateTracer getState)
@@ -1470,6 +1479,7 @@ prop_timeouts_enforced (Fixed rnd) serverAcc (ArbDataFlow dataFlow)
                              dynamicTracer
                              (tracerWithTime (Tracer traceM) <> dynamicTracer)
                              dynamicTracer
+                             nullTracer
                              dynamicTracer
 
 -- | Property wrapping `multinodeExperiment`.
@@ -1809,6 +1819,60 @@ prop_inbound_governor_counters (Fixed rnd) serverAcc (ArbDataFlow dataFlow)
                        events
                        (toNonFailing <$> attenuationMap)
 
+
+prop_inbound_governor_state :: Fixed Int
+                            -> Int
+                            -> ArbDataFlow
+                            -> AbsBearerInfo
+                            -> MultiNodeScript Int TestAddr
+                            -> Property
+prop_inbound_governor_state (Fixed rnd) serverAcc (ArbDataFlow dataFlow)
+                            defaultBearerInfo
+                            mns@(MultiNodeScript events attenuationMap) =
+  let trace = runSimTrace sim
+
+      evs :: Trace (SimResult ()) (DebugInboundGovernor SimAddr)
+      evs = traceWithNameTraceEvents trace
+
+      -- inboundGovernorEvents :: Trace (SimResult ()) (InboundGovernorTrace SimAddr)
+      -- inboundGovernorEvents = traceWithNameTraceEvents trace
+
+  in  counterexample (ppScript mns)
+    . getAllProperty
+    . bifoldMap
+       ( \ case
+           MainReturn {} -> mempty
+           _             -> AllProperty (property False)
+       )
+       (AllProperty . inboundGovernorStateInvariant)
+    $ evs
+  where
+    sim :: IOSim s ()
+    sim = multiNodeSim (mkStdGen rnd) serverAcc dataFlow
+                       defaultBearerInfo
+                       maxAcceptedConnectionsLimit
+                       events
+                       attenuationMap
+
+    inboundGovernorStateInvariant :: DebugInboundGovernor SimAddr
+                                  -> Property
+    inboundGovernorStateInvariant
+        (DebugInboundGovernor InboundGovernorState { igsConnections,
+                                                     igsMatureDuplexPeers,
+                                                     igsFreshDuplexPeers })
+        =
+        keys === keys'
+      where
+        keys  = Set.map remoteAddress
+              . Map.keysSet
+              . Map.filter (\ConnectionState { csDataFlow } -> csDataFlow == Duplex)
+              $ igsConnections
+
+        keys' = Set.fromList (OrdPSQ.keys igsFreshDuplexPeers)
+             <> Map.keysSet igsMatureDuplexPeers
+
+
+
 -- | Property wrapping `multinodeExperiment` that has a generator optimized for triggering
 -- pruning, and random generated number of connections hard limit.
 --
@@ -2102,6 +2166,7 @@ unit_server_accept_error (Fixed rnd) ioErrType =
                withBidirectionalConnectionManager "node-0" simTimeouts
                                                   nullTracer nullTracer
                                                   nullTracer nullTracer
+                                                  nullTracer
                                                   (mkStdGen rnd)
                                                   snock
                                                   makeFDBearer
@@ -2162,6 +2227,8 @@ multiNodeSimTracer :: ( Alternative (STM m), Monad m, MonadFix m
                       (WithName (Name SimAddr) (AbstractTransitionTrace SimAddr))
                    -> Tracer m
                       (WithName (Name SimAddr) (InboundGovernorTrace SimAddr))
+                   -> Tracer m
+                      (WithName (Name SimAddr) (DebugInboundGovernor SimAddr))
                    -> Tracer m
                       (WithName
                        (Name SimAddr)
@@ -2173,7 +2240,7 @@ multiNodeSimTracer :: ( Alternative (STM m), Monad m, MonadFix m
 multiNodeSimTracer stdGen serverAcc dataFlow defaultBearerInfo
                    acceptedConnLimit events attenuationMap
                    remoteTrTracer abstractTrTracer
-                   inboundGovTracer connMgrTracer = do
+                   inboundGovTracer debugTracer connMgrTracer = do
 
       let attenuationMap' = (fmap toBearerInfo <$>)
                           . Map.mapKeys ( normaliseId
@@ -2189,6 +2256,7 @@ multiNodeSimTracer stdGen serverAcc dataFlow defaultBearerInfo
                  multinodeExperiment remoteTrTracer
                                      abstractTrTracer
                                      inboundGovTracer
+                                     debugTracer
                                      connMgrTracer
                                      stdGen
                                      snocket
@@ -2223,8 +2291,8 @@ multiNodeSim :: (Serialise req, Show req, Eq req, Typeable req)
 multiNodeSim stdGen serverAcc dataFlow defaultBearerInfo
                    acceptedConnLimit events attenuationMap = do
   multiNodeSimTracer stdGen serverAcc dataFlow defaultBearerInfo acceptedConnLimit
-                     events attenuationMap dynamicTracer dynamicTracer
-                     dynamicTracer dynamicTracer
+                     events attenuationMap dynamicTracer dynamicTracer dynamicTracer
+                     (Tracer traceM) dynamicTracer
 
 
 -- | Connection terminated while negotiating it.

diff --git a/ouroboros-network-framework/src/Ouroboros/Network/InboundGovernor.hs b/ouroboros-network-framework/src/Ouroboros/Network/InboundGovernor.hs
@@ -20,6 +20,7 @@ module Ouroboros.Network.InboundGovernor
   , withInboundGovernor
     -- * Trace
   , InboundGovernorTrace (..)
+  , DebugInboundGovernor (..)
   , RemoteSt (..)
   , RemoteTransition
   , RemoteTransitionTrace
@@ -100,12 +101,13 @@ withInboundGovernor :: forall (muxMode :: MuxMode) socket initiatorCtx peerAddr
                    )
                 => Tracer m (RemoteTransitionTrace peerAddr)
                 -> Tracer m (InboundGovernorTrace peerAddr)
+                -> Tracer m (DebugInboundGovernor peerAddr)
                 -> InboundGovernorInfoChannel muxMode initiatorCtx peerAddr versionData ByteString m a b
                 -> Maybe DiffTime -- protocol idle timeout
                 -> MuxConnectionManager muxMode socket initiatorCtx (ResponderContext peerAddr) peerAddr versionData versionNumber ByteString m a b
                 -> (Async m Void -> m (PublicInboundGovernorState peerAddr versionData) -> m x)
                 -> m x
-withInboundGovernor trTracer tracer inboundInfoChannel
+withInboundGovernor trTracer tracer debugTracer inboundInfoChannel
                     inboundIdleTimeout connectionManager k = do
     -- State needs to be a TVar, otherwise, when catching the exception inside
     -- the loop we do not have access to the most recent version of the state
@@ -497,6 +499,7 @@ withInboundGovernor trTracer tracer inboundInfoChannel
 
       mask_ $ do
         atomically $ writeTVar st state'
+        traceWith debugTracer (DebugInboundGovernor state')
         case mbConnId of
           Just cid -> traceWith trTracer (mkRemoteTransitionTrace cid state state')
           Nothing  -> pure ()
@@ -614,3 +617,7 @@ data InboundGovernorTrace peerAddr
     -- ^ This case is unexpected at call site.
     | TrInboundGovernorError         !SomeException
   deriving Show
+
+
+data DebugInboundGovernor peerAddr = forall muxMode initiatorCtx versionData m a b.
+    DebugInboundGovernor (InboundGovernorState muxMode initiatorCtx peerAddr versionData m a b)
diff --git a/ouroboros-network-framework/src/Ouroboros/Network/InboundGovernor/Event.hs b/ouroboros-network-framework/src/Ouroboros/Network/InboundGovernor/Event.hs
@@ -26,16 +26,16 @@ module Ouroboros.Network.InboundGovernor.Event
 
 import Control.Applicative (Alternative)
 import Control.Concurrent.Class.MonadSTM.Strict
-import Control.Monad.Class.MonadTime.SI
 import Control.Monad.Class.MonadThrow hiding (handle)
+import Control.Monad.Class.MonadTime.SI
 
 import Data.ByteString.Lazy (ByteString)
 import Data.Functor (($>))
 import Data.Map.Strict (Map)
 import Data.Map.Strict qualified as Map
 import Data.Monoid.Synchronisation
-import Data.Set qualified as Set
 import Data.OrdPSQ (OrdPSQ)
+import Data.Set qualified as Set
 
 import Network.Mux qualified as Mux
 import Network.Mux.Types (MiniProtocolDir (..), MiniProtocolStatus (..))

diff --git a/ouroboros-network-framework/src/Ouroboros/Network/Server2.hs b/ouroboros-network-framework/src/Ouroboros/Network/Server2.hs
@@ -70,6 +70,7 @@ data ServerArguments (muxMode  :: MuxMode) socket initiatorCtx peerAddr versionD
       serverTracer                :: Tracer m (ServerTrace peerAddr),
       serverTrTracer              :: Tracer m (RemoteTransitionTrace peerAddr),
       serverInboundGovernorTracer :: Tracer m (InboundGovernorTrace peerAddr),
+      serverDebugInboundGovernor  :: Tracer m (DebugInboundGovernor peerAddr),
       serverConnectionLimits      :: AcceptedConnectionsLimit,
       serverConnectionManager     :: MuxConnectionManager muxMode socket initiatorCtx (ResponderContext peerAddr)
                                                           peerAddr versionData versionNumber bytes m a b,
@@ -137,6 +138,7 @@ with ServerArguments {
       serverTrTracer,
       serverTracer = tracer,
       serverInboundGovernorTracer = inboundGovernorTracer,
+      serverDebugInboundGovernor,
       serverConnectionLimits =
         serverLimits@AcceptedConnectionsLimit { acceptedConnectionsHardLimit = hardLimit },
       serverInboundIdleTimeout,
@@ -149,6 +151,7 @@ with ServerArguments {
       traceWith tracer (TrServerStarted localAddresses)
       withInboundGovernor serverTrTracer
                           inboundGovernorTracer
+                          serverDebugInboundGovernor
                           serverInboundInfoChannel
                           serverInboundIdleTimeout
                           serverConnectionManager

diff --git a/ouroboros-network-framework/testlib/Ouroboros/Network/ConnectionManager/Test/Experiments.hs b/ouroboros-network-framework/testlib/Ouroboros/Network/ConnectionManager/Test/Experiments.hs
@@ -80,7 +80,8 @@ import Ouroboros.Network.ConnectionManager.Types
 import Ouroboros.Network.Context
 import Ouroboros.Network.ControlMessage
 import Ouroboros.Network.Driver.Limits
-import Ouroboros.Network.InboundGovernor (InboundGovernorTrace (..))
+import Ouroboros.Network.InboundGovernor (DebugInboundGovernor (..),
+           InboundGovernorTrace (..))
 import Ouroboros.Network.Mux
 import Ouroboros.Network.MuxMode
 import Ouroboros.Network.Protocol.Handshake
@@ -429,6 +430,7 @@ withBidirectionalConnectionManager
                             peerAddr
                             (ConnectionHandlerTrace UnversionedProtocol DataFlowProtocolData)))
     -> Tracer m (WithName name (InboundGovernorTrace peerAddr))
+    -> Tracer m (WithName name (DebugInboundGovernor peerAddr))
     -> StdGen
     -> Snocket m socket peerAddr
     -> Mux.MakeBearer m socket
@@ -454,7 +456,7 @@ withBidirectionalConnectionManager
     -> m a
 withBidirectionalConnectionManager name timeouts
                                    inboundTrTracer trTracer
-                                   cmTracer inboundTracer
+                                   cmTracer inboundTracer debugTracer
                                    cmStdGen
                                    snocket makeBearer
                                    confSock socket
@@ -522,6 +524,8 @@ withBidirectionalConnectionManager name timeouts
                     WithName name `contramap` inboundTrTracer,
                   serverTracer =
                     WithName name `contramap` nullTracer, -- ServerTrace
+                  serverDebugInboundGovernor =
+                    WithName name `contramap` debugTracer,
                   serverInboundGovernorTracer =
                     WithName name `contramap` inboundTracer, -- InboundGovernorTrace
                   serverConnectionLimits = acceptedConnLimit,
@@ -722,7 +726,8 @@ unidirectionalExperiment stdGen timeouts snocket makeBearer confSock socket clie
       timeLimitsHandshake maxAcceptedConnectionsLimit
       $ \connectionManager ->
         withBidirectionalConnectionManager "server" timeouts
-                                           nullTracer nullTracer nullTracer nullTracer
+                                           nullTracer nullTracer nullTracer
+                                           nullTracer nullTracer
                                            stdGen''
                                            snocket makeBearer
                                            confSock socket Nothing
@@ -802,7 +807,7 @@ bidirectionalExperiment
       nextRequests0 <- oneshotNextRequests clientAndServerData0
       nextRequests1 <- oneshotNextRequests clientAndServerData1
       withBidirectionalConnectionManager "node-0" timeouts
-                                         nullTracer nullTracer nullTracer
+                                         nullTracer nullTracer nullTracer nullTracer
                                          nullTracer stdGen' snocket makeBearer confSock
                                          socket0 (Just localAddr0)
                                          [accumulatorInit clientAndServerData0]
@@ -811,7 +816,7 @@ bidirectionalExperiment
                                          maxAcceptedConnectionsLimit
         (\connectionManager0 _serverAddr0 _serverAsync0 -> do
           withBidirectionalConnectionManager "node-1" timeouts
-                                             nullTracer nullTracer nullTracer
+                                             nullTracer nullTracer nullTracer nullTracer
                                              nullTracer stdGen'' snocket makeBearer confSock
                                              socket1 (Just localAddr1)
                                              [accumulatorInit clientAndServerData1]

diff --git a/ouroboros-network/src/Ouroboros/Network/Diffusion/P2P.hs b/ouroboros-network/src/Ouroboros/Network/Diffusion/P2P.hs
@@ -750,6 +750,7 @@ runM Interfaces
                   serverSnocket               = diNtcSnocket,
                   serverTracer                = dtLocalServerTracer,
                   serverTrTracer              = nullTracer, -- TODO: issue #3320
+                  serverDebugInboundGovernor  = nullTracer,
                   serverInboundGovernorTracer = dtLocalInboundGovernorTracer,
                   serverInboundIdleTimeout    = Nothing,
                   serverConnectionLimits      = localConnectionLimits,
@@ -1041,6 +1042,7 @@ runM Interfaces
                   serverSnocket               = diNtnSnocket,
                   serverTracer                = dtServerTracer,
                   serverTrTracer              = dtInboundGovernorTransitionTracer,
+                  serverDebugInboundGovernor  = nullTracer,
                   serverInboundGovernorTracer = dtInboundGovernorTracer,
                   serverConnectionLimits      = daAcceptedConnectionsLimit,
                   serverConnectionManager     = connectionManager,