Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- newtype NumBlocks = NumBlocks Word64
- determineForkLength ∷ SecurityParam → NodeJoinPlan → LeaderSchedule → NumBlocks
Documentation
determineForkLength ∷ SecurityParam → NodeJoinPlan → LeaderSchedule → NumBlocks Source #
Compute a bound for the length of the final forks
At the end of the test, the nodes' final chains will share a common prefix ("intersection"), though it may be empty. Each node's current chain is a fork off that prefix. No such fork will be longer than the result of this function.
ASSUMPTION: The network connectivity is such that -- barring other non-network considerations -- any block forged at the start of a slot will be fetched and possibly selected by every other node before the end of the slot.
How LeaderSchedule
affects this function
A round-robin LeaderSchedule
will always reach consensus, so the fork
length will be 0
. For other LeaderSchedule
s -- whether known a priori
(see Test.ThreadNet.LeaderSchedule) or a posteriori (see
Test.ThreadNet.Praos) -- we often will not expect consensus. The key
difference is that a round-robin schedule always has exactly one leader per
slot. Arbitrary schedules instead may have 0 or multiple leaders.
A sequence of slots in which no slot has exactly one leader can drive a
network away from consensus. This function bounds how far from consensus the
network could be after the last simulated slot. It determines a conservative
upper bound on the length of the contended suffix of the nodes' final
chains. The bound may be less than, equal, or greater than k
; regardless
of which, it should be used to test the nodes' final chains.
If such a sequence is long enough, it might even prevent the network from
every reaching consensus again: the nodes at the end of the sequence may
have chains that disagree by more than k
blocks, thereby exceeding the
security parameter k
. In particular, if the bound determined by a
LeaderSchedule
is greater than k
, then no extension of that
LeaderSchedule
can determine a lesser bound.
Multiple leaders create divergent chains as follows. Assume that every
leader of s + 1
begins the slot with a chain of length n
, and that no
chain in the network has a greater length. Each leader forges a unique
block. A race condition between ChainSync/BlockFetch and forging makes it
possible, though relatively unlikely, that a leader would have received
another leader's new block before it forges its own. In that case, the new
leader will forged a block but then not select it, since it already selected
the other leader's new block. This function assumes the "worst-case" in
which both leaders make separate chains, thereby breaking consensus. Hence
it computes an upper bound. Each leader thus selects a new n+1
-length
chain, and each non-leader will adopt one of them because they previously
had a chain of length <= n
. Thus the network is likely not in consensus at
the end of a multi-leader slot.
The network will reestablish consensus at the end of a single-leader slot,
because the leader creates the only chain of length n+1
and all other
nodes thus select it.
In a slot with no leaders, all nodes will simply retain their current chains.
How NodeJoinPlan
affects this function
Because the race condition between forging and ChainSync/BlockFetch is consistently won by forging, a node that leads in the same slot it joins always attempts to make a chain of length 1 (ASSUMPTION: new nodes start with an empty chain). Except for the edge cases when the longest chains in the network are of length 0 or 1, this means that leaders who are joining can be disregarded.