Skip to content

Commit

Permalink
inbound-governor: verify demotedToColdRemote & unregisterInboundConne…
Browse files Browse the repository at this point in the history 
…ction

Verify that both methods never return 'UnsupportedState'.  This required
to change 'demotedToColdRemote' and allow two identity transitions in
the connection manager:
```
OutboundIdleSt dataFlow → OutboundIdleeSt dataFlow
```
and
```
OutboundDupSt expired → OutboundDupSt expired
```

This makes 'demotedToColdRemote' idempotent.
  • Loading branch information
@coot
coot committed Oct 20, 2021
1 parent 1cc2319 commit 4a7bb7a
Show file tree
Hide file tree
Showing 4 changed files with 91 additions and 29 deletions.
12 changes: 6 additions & 6 deletions ouroboros-network-framework/src/Ouroboros/Network/ConnectionManager/Core.hs
View file
Expand Up @@ -1640,14 +1640,14 @@ withConnectionManager ConnectionManagerArguments {
return (UnsupportedState (UnnegotiatedSt provenance))
OutboundUniState _connId _connThread _handle ->
return (UnsupportedState OutboundUniSt)
OutboundDupState _connId _connThread _handle expired ->
return (UnsupportedState (OutboundDupSt expired))
OutboundDupState _connId _connThread _handle _expired ->
return (OperationSuccess (mkTransition connState connState))
-- one can only enter 'OutboundIdleState' if remote state is
-- already cold.
OutboundIdleState _connId _connThread _handle dataFlow ->
return (UnsupportedState (OutboundIdleSt dataFlow))
InboundIdleState _connId _connThread _handle dataFlow ->
return (UnsupportedState (InboundIdleSt dataFlow))
OutboundIdleState _connId _connThread _handle _dataFlow ->
return (OperationSuccess (mkTransition connState connState))
InboundIdleState _connId _connThread _handle _dataFlow ->
return (OperationSuccess (mkTransition connState connState))

-- @
-- DemotedToCold^{dataFlow}_{Remote}
Expand Down
3 changes: 3 additions & 0 deletions ouroboros-network-framework/src/Ouroboros/Network/ConnectionManager/Types.hs
View file
Expand Up @@ -577,6 +577,9 @@ promotedToWarmRemote =
-- This executes:
--
-- * \(DemotedToCold^{*}_{Remote}\) transition.
--
-- This method is idempotent.
--
demotedToColdRemote
:: HasResponder muxMode ~ True
=> ConnectionManager muxMode socket peerAddr handle handleError m
Expand Down
7 changes: 6 additions & 1 deletion ouroboros-network-framework/test/Test/Ouroboros/Network/ConnectionManager.hs
View file
Expand Up @@ -1736,6 +1736,8 @@ verifyAbstractTransition Transition { fromState, toState } =
(OutboundDupSt Ticking, OutboundDupSt Expired) -> True
-- @DemotedToCold^{Duplex}_{Local}@
(OutboundDupSt Expired, OutboundIdleSt Duplex) -> True
-- identity transition executed by 'demotedToColdRemote'
(OutboundIdleSt dataFlow, OutboundIdleSt dataFlow') -> dataFlow == dataFlow'

--
-- Outbound ↔ Inbound
Expand All @@ -1748,6 +1750,9 @@ verifyAbstractTransition Transition { fromState, toState } =
-- @PromotedToWarm^{Duplex}_{Remote}@
(OutboundDupSt Ticking, DuplexSt) -> True
(OutboundDupSt Expired, DuplexSt) -> True
-- can be executed by 'demotedToColdRemote'
(OutboundDupSt expired, OutboundDupSt expired')
-> expired == expired'
-- @PromotedToWarm^{Duplex}_{Local}@
(InboundSt Duplex, DuplexSt) -> True
-- @DemotedToCold^{Duplex}_{Remote}@
Expand All @@ -1769,7 +1774,7 @@ verifyAbstractTransition Transition { fromState, toState } =
-- @Negotiated^{Unidirectional}_{Inbound}
(UnnegotiatedSt Inbound, InboundIdleSt Unidirectional) -> True

-- 'unregisterOutboundConnection' might perfrom
-- 'unregisterOutboundConnection' and 'demotedToColdRemote' might perfrom
(InboundIdleSt Duplex, InboundIdleSt Duplex) -> True
-- @Awake^{Duplex}_{Remote}
(InboundIdleSt Duplex, InboundSt Duplex) -> True
Expand Down
98 changes: 76 additions & 22 deletions ouroboros-network-framework/test/Test/Ouroboros/Network/Server2.hs
View file
Expand Up @@ -77,7 +77,8 @@ import Ouroboros.Network.ConnectionHandler
import Ouroboros.Network.ConnectionManager.Core
import Ouroboros.Network.ConnectionManager.Types
import Ouroboros.Network.IOManager
import Ouroboros.Network.InboundGovernor (RemoteSt (..))
import Ouroboros.Network.InboundGovernor (InboundGovernorTrace (..),
RemoteSt (..))
import qualified Ouroboros.Network.InboundGovernor.ControlChannel as Server
import Ouroboros.Network.Mux
import Ouroboros.Network.MuxMode
Expand Down Expand Up @@ -461,6 +462,7 @@ withBidirectionalConnectionManager
-- ^ identifier (for logging)
-> Tracer m (WithName name (RemoteTransitionTrace peerAddr))
-> Tracer m (WithName name (AbstractTransitionTrace peerAddr))
-> Tracer m (WithName name (InboundGovernorTrace peerAddr))
-> Snocket m socket peerAddr
-> socket
-- ^ listening socket
Expand All @@ -478,7 +480,9 @@ withBidirectionalConnectionManager
-> Async m Void
-> m a)
-> m a
withBidirectionalConnectionManager name timeouts inboundTrTracer cmTrTracer snocket socket localAddress
withBidirectionalConnectionManager name timeouts
inboundTrTracer cmTrTracer inboundTracer
snocket socket localAddress
accumulatorInit nextRequests k = do
mainThreadId <- myThreadId
inbgovControlChannel <- Server.newControlChannel
Expand Down Expand Up @@ -541,7 +545,7 @@ withBidirectionalConnectionManager name timeouts inboundTrTracer cmTrTracer snoc
serverTracer =
WithName name `contramap` nullTracer, -- ServerTrace
serverInboundGovernorTracer =
WithName name `contramap` nullTracer, -- InboundGovernorTrace
WithName name `contramap` inboundTracer, -- InboundGovernorTrace
serverConnectionLimits = AcceptedConnectionsLimit maxBound maxBound 0,
serverConnectionManager = connectionManager,
serverInboundIdleTimeout = tProtocolIdleTimeout timeouts,
Expand Down Expand Up @@ -731,7 +735,8 @@ unidirectionalExperiment timeouts snocket socket clientAndServerData = do
withInitiatorOnlyConnectionManager
"client" timeouts nullTracer snocket Nothing nextReqs
$ \connectionManager ->
withBidirectionalConnectionManager "server" timeouts nullTracer nullTracer
withBidirectionalConnectionManager "server" timeouts
nullTracer nullTracer nullTracer
snocket socket Nothing
[accumulatorInit clientAndServerData]
noNextRequests
Expand Down Expand Up @@ -834,14 +839,14 @@ bidirectionalExperiment
nextRequests0 <- oneshotNextRequests clientAndServerData0
nextRequests1 <- oneshotNextRequests clientAndServerData1
withBidirectionalConnectionManager "node-0" timeouts
nullTracer nullTracer
nullTracer nullTracer nullTracer
snocket socket0
(Just localAddr0)
[accumulatorInit clientAndServerData0]
nextRequests0
(\connectionManager0 _serverAddr0 _serverAsync0 ->
withBidirectionalConnectionManager "node-1" timeouts
nullTracer nullTracer
nullTracer nullTracer nullTracer
snocket socket1
(Just localAddr1)
[accumulatorInit clientAndServerData1]
Expand Down Expand Up @@ -1223,6 +1228,8 @@ multinodeExperiment
(RemoteTransitionTrace peerAddr))
-> Tracer m (WithName (Name peerAddr)
(AbstractTransitionTrace peerAddr))
-> Tracer m (WithName (Name peerAddr)
(InboundGovernorTrace peerAddr))
-> Snocket m socket peerAddr
-> Snocket.AddressFamily peerAddr
-- ^ either run the main node in 'Duplex' or 'Unidirectional' mode.
Expand All @@ -1231,7 +1238,7 @@ multinodeExperiment
-> DataFlow
-> MultiNodeScript req peerAddr
-> m ()
multinodeExperiment inboundTrTracer cmTrTracer
multinodeExperiment inboundTrTracer cmTrTracer inboundTracer
snocket addrFamily serverAddr accInit
dataFlow0 (MultiNodeScript script) =
withJobPool $ \jobpool -> do
Expand Down Expand Up @@ -1354,7 +1361,7 @@ multinodeExperiment inboundTrTracer cmTrTracer
Duplex ->
Job ( withBidirectionalConnectionManager
name simTimeouts
inboundTrTracer cmTrTracer
inboundTrTracer cmTrTracer inboundTracer
snocket fd (Just localAddr) serverAcc
(mkNextRequests connVar)
( \ connectionManager _ _serverAsync -> do
Expand Down Expand Up @@ -1638,6 +1645,14 @@ verifyRemoteTransition Transition {fromState, toState} =



data Three a b c
= First a
| Second b
| Third c
deriving Show



-- | Property wrapping `multinodeExperiment`.
--
-- Note: this test validates both connection manager and inbound governor state
Expand All @@ -1648,22 +1663,27 @@ verifyRemoteTransition Transition {fromState, toState} =
prop_multinode_Sim :: Int -> ArbDataFlow -> MultiNodeScript Int TestAddr -> Property
prop_multinode_Sim serverAcc (ArbDataFlow dataFlow) script =
let evs :: Trace (SimResult ())
(Either (RemoteTransitionTrace SimAddr)
(AbstractTransitionTrace SimAddr))
(Three (RemoteTransitionTrace SimAddr)
(AbstractTransitionTrace SimAddr)
(InboundGovernorTrace SimAddr))
evs = fmap wnEvent
. Trace.filter ((MainServer ==) . wnName)
. traceSelectTraceEvents
(\ev ->
case ev of
EventLog dyn ->
fmap Left
fmap First
<$> fromDynamic
@(WithName (Name SimAddr) (RemoteTransitionTrace SimAddr))
dyn
<|> fmap Right
<|> fmap Second
<$> fromDynamic
@(WithName (Name SimAddr) (AbstractTransitionTrace SimAddr))
dyn
<|> fmap Third
<$> fromDynamic
@(WithName (Name SimAddr) (InboundGovernorTrace SimAddr))
dyn
_ ->
Nothing
)
Expand All @@ -1676,6 +1696,7 @@ prop_multinode_Sim serverAcc (ArbDataFlow dataFlow) script =
(singletonScript noAttenuation)
$ \snocket ->
multinodeExperiment (Tracer traceM)
(Tracer traceM)
(Tracer traceM)
snocket
Snocket.TestFamily
Expand All @@ -1690,10 +1711,37 @@ prop_multinode_Sim serverAcc (ArbDataFlow dataFlow) script =

in counterexample (ppScript script)
. counterexample (Trace.ppTrace show show evs)
. (\ ( l :: Trace (SimResult ()) (RemoteTransitionTrace SimAddr)
, r :: Trace (SimResult ()) (AbstractTransitionTrace SimAddr)
. (\ ( tr1 :: Trace (SimResult ()) (RemoteTransitionTrace SimAddr)
, tr2 :: Trace (SimResult ()) (AbstractTransitionTrace SimAddr)
, tr3 :: Trace (SimResult ()) (InboundGovernorTrace SimAddr)
)
->
( getAllProperty
. bifoldMap
( \ _ -> AllProperty (property True))
( \ tr -> case tr of
-- verify that 'unregisterInboundConnection' does not return
-- 'UnsupportedState'.
TrDemotedToColdRemote _ res ->
case res of
UnsupportedState {}
-> AllProperty (counterexample (show tr) False)
_ -> AllProperty (property True)

-- verify that 'demotedToColdRemote' does not return
-- 'UnsupportedState'
TrWaitIdleRemote _ res ->
case res of
UnsupportedState {}
-> AllProperty (counterexample (show tr) False)
_ -> AllProperty (property True)

_ -> AllProperty (property True)
)

$ tr3
)
.&&.
( mkProperty
. bifoldMap
( \ case
Expand Down Expand Up @@ -1728,7 +1776,7 @@ prop_multinode_Sim serverAcc (ArbDataFlow dataFlow) script =
}
)
. splitConns
$ r
$ tr2
)
.&&.
( getAllProperty
Expand All @@ -1744,7 +1792,7 @@ prop_multinode_Sim serverAcc (ArbDataFlow dataFlow) script =
. verifyRemoteTransition
$ tr
)
$ l
$ tr1
)

)
Expand Down Expand Up @@ -1807,15 +1855,21 @@ prop_multinode_Sim serverAcc (ArbDataFlow dataFlow) script =

-- Right fold of the 'Trace' which splits its results.
--
traceSplit :: Trace a (Either b c) -> (Trace a b, Trace a c)
traceSplit = go [] []
traceSplit :: Trace a (Three b c d) -> (Trace a b, Trace a c, Trace a d)
traceSplit = go [] [] []
where
-- this version seems the fastest one (faster than a strict version, DList
-- style or a coinductive definition).
go :: [b] -> [c] -> Trace a (Either b c) -> (Trace a b, Trace a c)
go bs cs (Nil a) = (foldl' (flip Cons) (Nil a) bs, foldl' (flip Cons) (Nil a) cs)
go bs cs (Cons (Left b) o) = go (b : bs) cs o
go bs cs (Cons (Right c) o) = go bs (c : cs) o
go :: [b] -> [c] -> [d]
-> Trace a (Three b c d)
-> (Trace a b, Trace a c, Trace a d)
go bs cs ds (Nil a) = ( foldl' (flip Cons) (Nil a) bs
, foldl' (flip Cons) (Nil a) cs
, foldl' (flip Cons) (Nil a) ds
)
go bs cs ds (Cons (First b) o) = go (b : bs) cs ds o
go bs cs ds (Cons (Second c) o) = go bs (c : cs) ds o
go bs cs ds (Cons (Third d) o) = go bs cs (d : ds) o


splitConns :: Trace (SimResult ()) (AbstractTransitionTrace SimAddr)
Expand Down

0 comments on commit 4a7bb7a

Please sign in to comment.