Skip to content

Commit

Permalink
Add property for checking interleaves of requestNext and findIntersect
Browse files Browse the repository at this point in the history
  • Loading branch information
KtorZ committed Jun 14, 2021
1 parent d800b16 commit 81f68cc
Show file tree
Hide file tree
Showing 2 changed files with 109 additions and 15 deletions.
93 changes: 82 additions & 11 deletions server/test/unit/Ogmios/App/Protocol/ChainSyncSpec.hs
Expand Up @@ -20,7 +20,7 @@ import Cardano.Network.Protocol.NodeToClient
, runPipelinedPeer
)
import Data.Aeson
( ToJSON (..), Value (..) )
( ToJSON (..) )
import Network.TypedProtocol.Codec
( Codec (..), PeerHasAgency (..), SomeMessage (..), runDecoder )
import Ogmios.App.Options
Expand Down Expand Up @@ -57,6 +57,7 @@ import System.Random
( StdGen, random )
import Test.App.Protocol.Util
( PeerTerminatedUnexpectedly (..)
, expectWSPFault
, expectWSPResponse
, prop_inIOSim
, withMockChannel
Expand All @@ -68,28 +69,86 @@ import Test.Hspec
import Test.Hspec.QuickCheck
( prop )
import Test.QuickCheck
( Gen, forAll, frequency )
( Gen, Property, checkCoverage, choose, cover, forAll, frequency, oneof )

import qualified Codec.Json.Wsp as Wsp
import qualified Codec.Json.Wsp.Handler as Wsp
import qualified Ouroboros.Network.Protocol.ChainSync.Type as ChainSync

type Protocol = ChainSync Block (Point Block) (Tip Block)

maxInFlight :: MaxInFlight
maxInFlight = 10
maxInFlight = 3

spec :: Spec
spec = parallel $ do
context "ChainSync" $ do
prop "Basic scenario"
$ forAll genMirror $ \mirror -> prop_inIOSim
$ withChainSyncClient $ \send receive -> do
send $ MsgRequestNext RequestNext (Wsp.Response mirror)
expectWSPResponse @"RequestNext" receive (toJSON mirror)
parallel $ prop "Basic send/recv" prop_basicSendRecv
parallel $ prop "Saturate in-flight queue" prop_manyInFlight
parallel $ prop "Interleave findIntersect with requestNext" prop_interleave
where
-- We expect that client can submit request (either 'RequestNext' or
-- 'FindIntersect') and receive a corresponding response, preseving the
-- reflection value (a.k.a mirror).
prop_basicSendRecv :: Property
prop_basicSendRecv = forAll genMirror $ \mirror ->
cover 30 (isJust mirror) "with mirror" $
cover 30 (isNothing mirror) "without mirror" $
checkCoverage (p mirror)
where
p mirror = prop_inIOSim $ withChainSyncClient $ \send receive -> do
send $ requestNext mirror
expectWSPResponse @"RequestNext" receive (toJSON mirror)

send $ findIntersect mirror []
expectWSPResponse @"FindIntersect" receive (toJSON mirror)

send $ MsgFindIntersect (FindIntersect []) (Wsp.Response mirror)
expectWSPResponse @"FindIntersect" receive (toJSON mirror)
-- The chain-sync client will pipeline requests up to a certain point.
-- Indeed, WebSockets do allow for (theorically) infinite pipelining,
-- whereas the Ouroboros framework only allow for finite one. This means
-- that the application client has to keep track of the pipelined requests,
-- and choose whether to collect response for previously sent requests, or
-- to continue pipelining new incoming requests.
--
-- There's therefore a different behavior depending on the number of requests
-- in flight, which this property captures.
prop_manyInFlight :: Property
prop_manyInFlight = forAll genMaxInFlight $ \nMax ->
cover 20 (nMax > maxInFlight) "> maxInFlight" $
cover 20 (nMax >= maxInFlight - 1 && nMax <= maxInFlight + 1) "=~ maxInFlight" $
cover 20 (nMax < maxInFlight) "< maxInFlight" $
checkCoverage (p nMax)
where
p nMax = prop_inIOSim $ withChainSyncClient $ \send receive -> do
mirrors <- forM [0 .. nMax] $ \(i :: Int) -> do
let mirror = Just $ toJSON i
mirror <$ send (requestNext mirror)
forM_ mirrors $ \mirror -> do
expectWSPResponse @"RequestNext" receive (toJSON mirror)

genMaxInFlight :: Gen MaxInFlight
genMaxInFlight = oneof
[ choose (0, maxInFlight - 1)
, choose (maxInFlight - 1, maxInFlight + 1)
, choose (maxInFlight + 1, 2 * maxInFlight)
]

type Protocol = ChainSync Block (Point Block) (Tip Block)
-- The Ouroboros typed protocol follows a strategy of correct-by-construction
-- and represents protocol as state machines, fully captured at the
-- type-level. We can't model this through a WebSocket, and clients may
-- therefore produce invalid transitions. One of them is for instance,
-- asking for an intersection while they are still requests in flight that
-- haven't been collected. In this case, Ogmios returns a client error.
prop_interleave :: Property
prop_interleave = forAll genMirror $ \mirror ->
cover 30 (isJust mirror) "with mirror" $
cover 30 (isNothing mirror) "without mirror" $
checkCoverage (p mirror)
where
p mirror = prop_inIOSim $ withChainSyncClient $ \send receive -> do
send $ requestNext Nothing
send $ findIntersect mirror []
expectWSPFault receive Wsp.FaultClient (toJSON mirror)

withChainSyncClient
:: (MonadSTM m, MonadOuroboros m)
Expand Down Expand Up @@ -151,3 +210,15 @@ chainSyncMockPeer seed codec (recv, send) = flip evalStateT seed $ forever $ do
[ (10, ChainSync.MsgIntersectFound <$> genPoint <*> genTip)
, ( 1, ChainSync.MsgIntersectNotFound <$> genTip)
]

--
-- Helpers
--

requestNext :: Wsp.Mirror -> ChainSyncMessage Block
requestNext mirror =
MsgRequestNext RequestNext (Wsp.Response mirror) (Wsp.Fault mirror)

findIntersect :: Wsp.Mirror -> [Point Block] -> ChainSyncMessage Block
findIntersect mirror points =
MsgFindIntersect (FindIntersect points) (Wsp.Response mirror) (Wsp.Fault mirror)
31 changes: 27 additions & 4 deletions server/test/unit/Test/App/Protocol/Util.hs
Expand Up @@ -8,6 +8,7 @@
module Test.App.Protocol.Util
( prop_inIOSim
, expectWSPResponse
, expectWSPFault
, withMockChannel

-- * Exceptions
Expand All @@ -19,6 +20,8 @@ import Ogmios.Prelude

import Control.Exception
( evaluate )
import Control.Monad.Class.MonadTimer
( MonadDelay )
import Control.Monad.IOSim
( runSimOrThrow )
import GHC.TypeLits
Expand All @@ -42,13 +45,14 @@ import Test.QuickCheck
import Test.QuickCheck.Monadic
( monadicIO, pick, run )

import qualified Codec.Json.Wsp as Wsp
import qualified Data.Aeson as Json

-- | Run a function in IOSim, with a 'StdGen' input which can used to compute
-- random numbers deterministically within the simulation. The random generator
-- is however randomly seeded for each property run.
prop_inIOSim
:: (forall m. (MonadSTM m, MonadOuroboros m) => StdGen -> m ())
:: (forall m. (MonadSTM m, MonadOuroboros m, MonadDelay m) => StdGen -> m ())
-> Property
prop_inIOSim action = monadicIO $ do
seed <- mkStdGen <$> pick arbitrary
Expand Down Expand Up @@ -90,11 +94,29 @@ expectWSPResponse recv wantMirror = do
let gotMethod = "methodname" `at` json
let wantMethod = Json.toJSON $ symbolVal (Proxy @method)
when (gotMethod /= Just wantMethod) $
throwIO $ UnexpectedResponse gotMethod wantMethod
throwIO $ UnexpectedResponse "methodname" gotMethod wantMethod

let gotMirror = "reflection" `at` json
when (gotMirror /= Just wantMirror) $
throwIO $ UnexpectedResponse gotMirror wantMirror
throwIO $ UnexpectedResponse "reflection" gotMirror wantMirror

expectWSPFault
:: (MonadThrow m)
=> m Json.Encoding
-> Wsp.FaultCode
-> Json.Value
-> m ()
expectWSPFault recv wantCode wantMirror = do
json <- inefficientEncodingToValue <$> recv

let gotCode = ("fault" `at` json) >>= at "code"
let wantCode' = Json.toJSON wantCode
when (gotCode /= Just wantCode') $
throwIO $ UnexpectedResponse "fault" gotCode wantCode'

let gotMirror = "reflection" `at` json
when (gotMirror /= Just wantMirror) $
throwIO $ UnexpectedResponse "reflection" gotMirror wantMirror

--
-- Exceptions
Expand All @@ -104,7 +126,8 @@ data PeerTerminatedUnexpectedly = PeerTerminatedUnexpectedly deriving Show
instance Exception PeerTerminatedUnexpectedly

data UnexpectedResponse = UnexpectedResponse
{ gotResponse :: Maybe Json.Value
{ what :: String
, gotResponse :: Maybe Json.Value
, expectedResponse :: Json.Value
} deriving Show
instance Exception UnexpectedResponse

0 comments on commit 81f68cc

Please sign in to comment.