Skip to content

Commit

Permalink
Merge #1107
Browse files Browse the repository at this point in the history
1107: Test for unexpected message delays r=nfrisby a=nfrisby

This test confirms that our current test suite is not introducing any unexpected message delays, where _message delays_ is analogous to that from the paper https://eprint.iacr.org/2017/573/20171115:001835.

Issues #229 and #230 will cause this property to fail; they'll have to refine it somehow.

Co-authored-by: Nicolas Frisby <[email protected]>
  • Loading branch information
iohk-bors[bot] and nfrisby authored Oct 7, 2019
2 parents 6cbde59 + 478ddde commit 6016f49
Show file tree
Hide file tree
Showing 13 changed files with 235 additions and 81 deletions.
30 changes: 30 additions & 0 deletions ouroboros-consensus/src/Ouroboros/Consensus/Block.hs
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,9 @@ module Ouroboros.Consensus.Block (
, headerPoint
-- * Supported blocks
, SupportedBlock
-- * EBBs
, IsEBB (..)
, toIsEBB
) where

import Cardano.Prelude (NoUnexpectedThunks)
Expand All @@ -24,6 +27,7 @@ import Data.FingerTree.Strict (Measured (..))
import Ouroboros.Network.Block

import Ouroboros.Consensus.Protocol.Abstract
import Ouroboros.Consensus.Util.Condense

{-------------------------------------------------------------------------------
Link block to its header
Expand Down Expand Up @@ -81,3 +85,29 @@ class ( GetHeader blk
, SupportedHeader (BlockProtocol blk) (Header blk)
, NoUnexpectedThunks (Header blk)
) => SupportedBlock blk

{-------------------------------------------------------------------------------
EBBs
-------------------------------------------------------------------------------}

-- | Whether a block is an Epoch Boundary Block (EBB)
--
-- See "Ouroboros.Storage.ImmutableDB.API" for a discussion of EBBs. Key
-- idiosyncracies:
--
-- * An EBB carries no unique information.
--
-- * An EBB has the same 'BlockNo' as its predecessor.
--
-- * EBBs are vestigial. As of Shelley, nodes no longer forge EBBs: they are
-- only a legacy/backwards-compatibility concern.
data IsEBB
= IsEBB
| IsNotEBB
deriving (Eq, Show)

instance Condense IsEBB where
condense = show

toIsEBB :: Bool -> IsEBB
toIsEBB b = if b then IsEBB else IsNotEBB
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,13 @@ newtype LeaderSchedule = LeaderSchedule {getLeaderSchedule :: Map SlotNo [CoreNo
deriving stock (Show, Eq, Ord, Generic)
deriving anyclass (NoUnexpectedThunks)

instance Semigroup LeaderSchedule where
LeaderSchedule l <> LeaderSchedule r =
LeaderSchedule $
Map.unionWith comb l r
where
comb ls rs = ls ++ filter (`notElem` ls) rs

instance Condense LeaderSchedule where
condense (LeaderSchedule m) = condense
$ map (\(s, ls) -> (s, map fromCoreNodeId ls))
Expand Down
2 changes: 2 additions & 0 deletions ouroboros-consensus/src/Ouroboros/Storage/ChainDB/Impl.hs
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ module Ouroboros.Storage.ChainDB.Impl (

import Control.Monad (when)
import qualified Data.Map.Strict as Map
import Data.Maybe (isJust)

import Control.Tracer

Expand Down Expand Up @@ -143,6 +144,7 @@ openDBInternal args launchBgTasks = do
, cdbGcDelay = Args.cdbGcDelay args
, cdbBgThreads = varBgThreads
, cdbEpochInfo = Args.cdbEpochInfo args
, cdbIsEBB = isJust . Args.cdbIsEBB args
}
h <- fmap CDBHandle $ newTVarM $ ChainDbOpen env
let chainDB = ChainDB
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,8 @@ import Ouroboros.Network.Block (BlockNo, HasHeader (..), HeaderHash,
Point, SlotNo, blockPoint, castPoint, pointHash)
import Ouroboros.Network.Point (WithOrigin)

import Ouroboros.Consensus.Block (BlockProtocol, GetHeader (..))
import Ouroboros.Consensus.Block (BlockProtocol, GetHeader (..),
toIsEBB)
import Ouroboros.Consensus.Ledger.Abstract
import Ouroboros.Consensus.Protocol.Abstract
import Ouroboros.Consensus.Util.IOLike
Expand Down Expand Up @@ -221,7 +222,7 @@ addBlock cdb@CDB{..} b = do

-- Write the block to the VolatileDB in all other cases
VolDB.putBlock cdbVolDB b
trace (AddedBlockToVolDB (blockPoint b))
trace $ AddedBlockToVolDB (blockPoint b) (blockNo b) (toIsEBB (cdbIsEBB b))

-- We need to get these after adding the block to the VolatileDB
(isMember', succsOf, predecessor) <- atomically $
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ import Ouroboros.Network.Block (BlockNo, HasHeader, HeaderHash, Point,
SlotNo, StandardHash)
import Ouroboros.Network.Point (WithOrigin)

import Ouroboros.Consensus.Block (BlockProtocol, Header)
import Ouroboros.Consensus.Block (BlockProtocol, Header, IsEBB (..))
import Ouroboros.Consensus.Ledger.Abstract (ProtocolLedgerView)
import Ouroboros.Consensus.Ledger.Extended (ExtValidationError)
import Ouroboros.Consensus.Protocol.Abstract (NodeConfig)
Expand Down Expand Up @@ -207,6 +207,7 @@ data ChainDbEnv m blk = CDB
, cdbBgThreads :: !(StrictTVar m [Thread m ()])
-- ^ The background threads.
, cdbEpochInfo :: !(EpochInfo m)
, cdbIsEBB :: !(blk -> Bool)
} deriving (Generic)

-- | We include @blk@ in 'showTypeOf' because it helps resolving type families
Expand Down Expand Up @@ -333,7 +334,7 @@ data TraceOpenEvent blk

-- | Trace type for the various events that occur when adding a block.
data TraceAddBlockEvent blk
= AddedBlockToVolDB (Point blk)
= AddedBlockToVolDB !(Point blk) !BlockNo !IsEBB
-- ^ A block was added to the Volatile DB

| TryAddToCurrentChain (Point blk)
Expand Down
2 changes: 1 addition & 1 deletion ouroboros-consensus/test-consensus/Test/Dynamic/BFT.hs
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ prop_simple_bft_convergence k
testConfig@TestConfig{numCoreNodes, numSlots} seed =
prop_general k
testConfig
(roundRobinLeaderSchedule numCoreNodes numSlots)
(Just $ roundRobinLeaderSchedule numCoreNodes numSlots)
testOutput
where
testOutput =
Expand Down
152 changes: 132 additions & 20 deletions ouroboros-consensus/test-consensus/Test/Dynamic/General.hs
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Test.Dynamic.General (
Expand All @@ -15,16 +16,17 @@ module Test.Dynamic.General (
) where

import Control.Monad (guard, join)
import Data.Coerce (coerce)
import qualified Data.Map as Map
import Data.Maybe (fromMaybe)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Word (Word64)
import GHC.Stack (HasCallStack)
import Test.QuickCheck

import Control.Monad.IOSim (runSimOrThrow)

import Ouroboros.Network.Block (BlockNo (..), HasHeader, blockPoint)
import Ouroboros.Network.Block (BlockNo (..), pattern BlockPoint,
pattern GenesisPoint, HasHeader, Point, blockPoint)

import Ouroboros.Consensus.BlockchainTime
import Ouroboros.Consensus.Node.ProtocolInfo
Expand Down Expand Up @@ -171,23 +173,24 @@ runTestNetwork pInfo
-- * The nodes do not leak file handles
--
prop_general ::
forall blk.
( Condense blk
, Eq blk
, HasHeader blk
, RunNode blk
)
=> SecurityParam
-> TestConfig
-> LeaderSchedule
-> Maybe LeaderSchedule
-> TestOutput blk
-> Property
prop_general k TestConfig{numSlots, nodeJoinPlan, nodeTopology} schedule
prop_general k TestConfig{numSlots, nodeJoinPlan, nodeTopology} mbSchedule
TestOutput{testOutputNodes, testOutputTipBlockNos} =
counterexample ("nodeChains: " <> unlines ("" : map (\x -> " " <> condense x) (Map.toList nodeChains))) $
counterexample ("nodeJoinPlan: " <> condense nodeJoinPlan) $
counterexample ("nodeTopology: " <> condense nodeTopology) $
counterexample ("slot-node-tipBlockNo: " <> condense tipBlockNos) $
counterexample ("schedule: " <> condense schedule) $
counterexample ("mbSchedule: " <> condense mbSchedule) $
counterexample ("growth schedule: " <> condense growthSchedule) $
counterexample ("consensus expected: " <> show isConsensusExpected) $
tabulate "consensus expected" [show isConsensusExpected] $
Expand All @@ -198,13 +201,18 @@ prop_general k TestConfig{numSlots, nodeJoinPlan, nodeTopology} schedule
maxForkLength
(Map.elems nodeChains) .&&.
prop_all_growth .&&.
prop_no_unexpected_message_delays .&&.
conjoin
[ fileHandleLeakCheck nid nodeDBs
| (nid, nodeDBs) <- Map.toList nodeOutputDBs ]
where
schedule = case mbSchedule of
Nothing -> growthSchedule
Just sched -> sched

NumBlocks maxForkLength = determineForkLength k nodeJoinPlan schedule

-- remove entries from @schedule@ if any of:
-- build a leader schedule which includes every node that forged unless:
--
-- * the node just joined in this slot (unless it's the earliest slot in
-- which any nodes joined)
Expand All @@ -215,23 +223,37 @@ prop_general k TestConfig{numSlots, nodeJoinPlan, nodeTopology} schedule
--
growthSchedule :: LeaderSchedule
growthSchedule =
Map.mapWithKey (filter . actuallyLead) `coerce` schedule
foldl (<>) (emptyLeaderSchedule numSlots) $
[ let NodeOutput
{ nodeOutputForges
, nodeOutputInvalids
} = no
in
LeaderSchedule $
Map.mapMaybeWithKey
(actuallyLead cid nodeOutputInvalids)
nodeOutputForges
| (cid, no) <- Map.toList testOutputNodes
]
where
actuallyLead s cid = fromMaybe False $ do
let nid = fromCoreNodeId cid
let j = nodeIdJoinSlot nodeJoinPlan nid

actuallyLead ::
NodeId
-> Set (Point blk)
-> SlotNo
-> blk
-> Maybe [CoreNodeId]
actuallyLead nid invalids s b = do
cid <- case nid of
CoreId i -> Just (CoreNodeId i)
RelayId _ -> Nothing

let j = nodeIdJoinSlot nodeJoinPlan nid
guard $ j < s || (j == s && isFirstJoinSlot s)

NodeOutput
{ nodeOutputForges
, nodeOutputInvalids
} <- Map.lookup nid testOutputNodes
b <- Map.lookup s nodeOutputForges
guard $ not $
nodeIsEBB b || Set.member (blockPoint b) invalids

pure $ not $
(||) (nodeIsEBB b) $
Set.member (blockPoint b) nodeOutputInvalids
pure [cid]

isFirstJoinSlot s =
Just s == (snd <$> Map.lookupMin m)
Expand Down Expand Up @@ -336,3 +358,93 @@ prop_general k TestConfig{numSlots, nodeJoinPlan, nodeTopology} schedule
Map.toAscList $
fmap Map.toAscList $
testOutputTipBlockNos

-- In the paper <https://eprint.iacr.org/2017/573/20171115:00183>, a
-- /message/ carries a chain from one party to another. When a party forges
-- a block, it \"diffuses\" the chain with that block as its head by
-- sending a message to each other party (actually, to itself too, but
-- that's ultimately redundant). The adversary is able to delay each
-- message differently, so some parties may receive it before others do.
-- Once a party receives a message, the party can consider that chain for
-- selection.
--
-- In the implementation, on the other hand, our messages are varied and
-- much more granular than a whole chain. We therefore observe a delay
-- analogous to the paper's /message/ /delay/ by comparing the slot in
-- which a block is added to each node's ChainDB against the slot in which
-- that block was forged.
--
-- Since our mock network currently introduces only negligible latency
-- compared to the slot duration, we generally expect all messages to have
-- no delay: they should arrive to all nodes during the same slot in which
-- they were forged. However, some delays are expected, due to nodes
-- joining late and also due to the practicality of the ChainSync and
-- BlockFetch policies, which try to avoid /unnecessary/ header/block
-- fetches. See the relevant comments below.
--
-- NOTE: This current property does not check for interminable message
-- delay: i.e. for blocks that were never added to some ChainDBs. It only
-- checks the slot difference once a message does arrive. This seems
-- acceptable: if there are no Common Prefix or Chain Growth violations,
-- then each message must have either arrived or ultimately been
-- irrelevant.
--
prop_no_unexpected_message_delays :: HasCallStack => Property
prop_no_unexpected_message_delays =
conjoin $
[ case p of
GenesisPoint -> error "impossible"
BlockPoint sendSlot hsh ->
prop1 nid recvSlot sendSlot hsh bno
| (nid, m) <- Map.toList adds
, (recvSlot, pbnos) <- Map.toList m
, (p, bno) <- Set.toList pbnos
]
where
-- INVARIANT: these AddBlock events are *not* for EBBs
adds = nodeOutputAdds <$> testOutputNodes

prop1 nid recvSlot sendSlot hsh bno =
counterexample msg $
delayOK || noDelay
where
msg =
"Unexpected message delay " <>
"(" <> "recipient: " <> condense nid <>
"," <> "expected receive slot: "
<> condense firstPossibleReception <>
"," <> "actual receive slot: " <> condense recvSlot <>
"," <> "blockHash: " <> show hsh <>
"," <> "blockNo: " <> condense (unBlockNo bno) <>
")"

-- a node cannot receive a block until both exist
firstPossibleReception =
nodeIdJoinSlot nodeJoinPlan nid `max` sendSlot

noDelay = recvSlot == firstPossibleReception

delayOK = delayOK1 || delayOK2

-- When a node leads in the same slot in which it joins the
-- network, it immediately forges a single block on top of Genesis;
-- this block then prevents it from fetching the network's current
-- chain if that also consists of just one block.
--
-- NOTE This predicate is more general than that specific scenario,
-- but we don't anticipate it wholly masking any interesting cases.
delayOK1 = 1 == bno

-- When a slot has multiple leaders, each node chooses one of the
-- mutually-exclusive forged blocks and won't fetch any of the
-- others until it's later compelled to switch to a chain
-- containing one of them
--
-- TODO This predicate is more general than that specific scenario,
-- and should be tightened accordingly. We currently anticipate
-- that Issues #229 and #230 will handle that.
delayOK2 = case Map.lookup sendSlot sched of
Just (_:_:_) -> True
_ -> False
where
LeaderSchedule sched = growthSchedule
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@ prop_simple_leader_schedule_convergence
params@PraosParams{praosSecurityParam = k}
testConfig@TestConfig{numCoreNodes} schedule seed =
counterexample (tracesToDot testOutputNodes) $
prop_general k testConfig schedule testOutput
prop_general k testConfig (Just schedule) testOutput
where
testOutput@TestOutput{testOutputNodes} =
runTestNetwork
Expand Down
Loading

0 comments on commit 6016f49

Please sign in to comment.