Skip to content

Commit ae48bb8

Browse files
geo2ageo2a
committed
Test Genesis State Machine with quickcheck-dynamic (QD)
- add QD-based tests - group definition used in both QSM and QD tests - in QD-based tests, use reflection to pass static model parameters
1 parent 2b11926 commit ae48bb8

File tree

7 files changed

+1161
-248
lines changed

7 files changed

+1161
-248
lines changed

‎cabal.project

+7
Original file line numberDiff line numberDiff line change
@@ -44,3 +44,10 @@ package ouroboros-network
4444
if(os(windows))
4545
constraints:
4646
bitvec -simd
47+
48+
49+
source-repository-package
50+
type: git
51+
location: https://github.com/input-output-hk/quickcheck-dynamic.git
52+
tag: 071092c90c3643c6594a2c321ba3501576af2ac8
53+
--sha256: QiPVxjcVlYsiSq0a7SmGoueViuyymkADNTGaGchLVt4=

‎ouroboros-consensus-diffusion/ouroboros-consensus-diffusion.cabal

+5
Original file line numberDiff line numberDiff line change
@@ -229,8 +229,10 @@ test-suite consensus-test
229229
main-is: Main.hs
230230
other-modules:
231231
Test.Consensus.BlockTree
232+
Test.Consensus.GSM.Common
232233
Test.Consensus.GSM.QSM
233234
Test.Consensus.GSM.QSM.Model
235+
Test.Consensus.GSM.QD
234236
Test.Consensus.Genesis.Setup
235237
Test.Consensus.Genesis.Setup.Classifiers
236238
Test.Consensus.Genesis.Setup.GenChains
@@ -301,10 +303,13 @@ test-suite consensus-test
301303
ouroboros-network-framework,
302304
ouroboros-network-mock,
303305
ouroboros-network-protocols,
306+
pretty,
304307
pretty-show,
308+
quickcheck-dynamic,
305309
quickcheck-state-machine:no-vendored-treediff,
306310
quiet,
307311
random,
312+
reflection,
308313
resource-registry,
309314
serialise,
310315
si-timers,

‎ouroboros-consensus-diffusion/test/consensus-test/Main.hs

+4-1
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ module Main (main) where
22

33
import qualified Test.Consensus.Genesis.Tests (tests)
44
import qualified Test.Consensus.GSM.QSM (tests)
5+
import qualified Test.Consensus.GSM.QD (tests)
56
import qualified Test.Consensus.HardFork.Combinator (tests)
67
import qualified Test.Consensus.Node (tests)
78
import qualified Test.Consensus.PeerSimulator.Tests (tests)
@@ -24,7 +25,9 @@ tests =
2425
]
2526
]
2627
, Test.Consensus.Genesis.Tests.tests
27-
, testGroup "GSM" Test.Consensus.GSM.QSM.tests
28+
, testGroup "GSM" [ testGroup "QSM" Test.Consensus.GSM.QSM.tests
29+
, testGroup "QD" Test.Consensus.GSM.QD.tests
30+
]
2831
, Test.Consensus.PeerSimulator.Tests.tests
2932
, Test.Consensus.PointSchedule.Shrinking.Tests.tests
3033
, Test.Consensus.PointSchedule.Tests.tests

‎ouroboros-consensus-diffusion/test/consensus-test/Test/Consensus/GSM/Common.hs

+268
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,268 @@
1+
{-# LANGUAGE LambdaCase #-}
2+
{-# LANGUAGE ScopedTypeVariables #-}
3+
{-# LANGUAGE MultiParamTypeClasses #-}
4+
{-# LANGUAGE GeneralisedNewtypeDeriving #-}
5+
{-# LANGUAGE DeriveAnyClass #-}
6+
{-# LANGUAGE DerivingStrategies #-}
7+
{-# LANGUAGE FlexibleInstances #-}
8+
{-# LANGUAGE StandaloneDeriving #-}
9+
{-# LANGUAGE GADTs #-}
10+
{-# LANGUAGE TypeFamilies #-}
11+
{-# LANGUAGE DeriveGeneric #-}
12+
{-# LANGUAGE Rank2Types #-}
13+
14+
{-# OPTIONS_GHC -Wno-orphans #-}
15+
16+
module Test.Consensus.GSM.Common (module Test.Consensus.GSM.Common) where
17+
18+
import qualified Control.Monad.IOSim as IOSim
19+
import Control.Monad.Class.MonadFork (MonadFork, yield)
20+
import Control.Monad (replicateM_)
21+
import qualified Control.Monad.Class.MonadTime.SI as SI
22+
import Data.Time (diffTimeToPicoseconds)
23+
import qualified Data.TreeDiff as TD
24+
import GHC.Generics (Generic)
25+
import qualified Ouroboros.Consensus.Node.GSM as GSM
26+
import Ouroboros.Network.PeerSelection.LedgerPeers.Type
27+
(LedgerStateJudgement (..))
28+
import qualified Test.QuickCheck as QC
29+
import Test.QuickCheck (elements, shrink)
30+
import Test.Util.Orphans.ToExpr ()
31+
32+
-- | A block count
33+
newtype B = B Int
34+
deriving stock (Eq, Ord, Generic, Read, Show)
35+
deriving newtype (Enum, Num)
36+
deriving anyclass (TD.ToExpr)
37+
38+
-- | A slot count
39+
newtype S = S Int
40+
deriving stock (Eq, Ord, Generic, Read, Show)
41+
deriving newtype (Enum, Num)
42+
deriving anyclass (TD.ToExpr)
43+
44+
data UpstreamPeer = Amara | Bao | Cait | Dhani | Eric
45+
deriving stock (Bounded, Enum, Eq, Ord, Generic, Read, Show)
46+
deriving anyclass (TD.ToExpr, QC.CoArbitrary, QC.Function)
47+
48+
-- | The cumulative growth relative to whatever length the initial selection
49+
-- was and the slot relative to the start of the test (which is assumed to be
50+
-- the exact onset of some slot)
51+
data Selection = Selection !B !S
52+
deriving stock (Eq, Ord, Generic, Show)
53+
deriving anyclass (TD.ToExpr)
54+
55+
-- | The age of the candidate is irrelevant, only its length matters
56+
newtype Candidate = Candidate B
57+
deriving stock (Eq, Ord, Generic, Show)
58+
deriving anyclass (TD.ToExpr)
59+
60+
data MarkerState = Present | Absent
61+
deriving stock (Eq, Ord, Generic, Read, Show)
62+
deriving anyclass (TD.ToExpr)
63+
64+
newtype WhetherPrevTimePasses = WhetherPrevTimePasses Bool
65+
deriving stock (Eq, Ord, Generic, Show)
66+
deriving anyclass (TD.ToExpr)
67+
68+
data ModelState =
69+
ModelPreSyncing
70+
|
71+
ModelSyncing
72+
|
73+
ModelCaughtUp !SI.Time
74+
-- ^ when the model most recently transitioned to 'GSM.CaughtUp'.
75+
deriving stock (Eq, Ord, Generic, Show)
76+
deriving anyclass (TD.ToExpr)
77+
78+
-- | Interesting events to record /within the model/
79+
--
80+
-- TODO some less superficial ones (eg even just combinations of these)
81+
data Notable =
82+
BigDurN
83+
-- ^ there was a "big" 'TimesPasses' command
84+
|
85+
CaughtUpN
86+
-- ^ the node transitioned from Syncing to CaughtUp
87+
|
88+
FellBehindN
89+
-- ^ the node transitioned from CaughtUp to PreSyncing
90+
|
91+
SyncingToPreSyncingN
92+
-- ^ the node transition from Syncing to PreSyncing
93+
|
94+
PreSyncingToSyncingN
95+
-- ^ the node transition from PreSyncing to Syncing
96+
|
97+
FlickerN
98+
-- ^ the node transitioned from CaughtUp to PreSyncing to Syncing and back
99+
-- to CaughtUp "instantly"
100+
|
101+
NotThrashingN
102+
-- ^ the anti-thrashing would have allowed 'FellBehindN', but the selection
103+
-- wasn't old enough
104+
|
105+
TooOldN
106+
-- ^ the selection was old enough for 'FellBehindN', but the anti-thrashing
107+
-- prevented it
108+
deriving (Eq, Ord, Show)
109+
110+
instance TD.ToExpr Notable where toExpr = TD.defaultExprViaShow
111+
112+
---
113+
114+
newtype Idling = Idling Bool
115+
deriving (Eq, Ord, Show)
116+
117+
data PeerState = PeerState { psCandidate :: !Candidate, psIdling :: !Idling }
118+
deriving (Eq, Ord, Show)
119+
120+
isIdling :: PeerState -> Bool
121+
isIdling (PeerState {psIdling = Idling i}) = i
122+
123+
-- | Ensure the GSM thread's transactions quiesce
124+
--
125+
-- I'm unsure how many 'yield's are actually necessary, but ten is both small
126+
-- and also seems likely to suffice.
127+
--
128+
-- Despite the crudeness, this seems much more compositional than invasive
129+
-- explicit synchronization.
130+
yieldSeveralTimes :: MonadFork m => m ()
131+
yieldSeveralTimes = replicateM_ 10 yield
132+
133+
{-
134+
135+
Note [Why yield after the command]
136+
137+
For this 'prop_sequential1' repro
138+
139+
@
140+
YoungEnough
141+
142+
Command (NewCandidate Amara (B 1)) Unit []
143+
Command (StartIdling Amara) Unit []
144+
Command (TimePasses 61) Unit []
145+
Command (ExtendSelection (S (-4))) Unit []
146+
Command ReadMarker (ReadThisMarker Absent) []
147+
148+
(Command ReadGsmState _ []) -- this last command is baked into the property
149+
@
150+
151+
If we yield after the command, then both GSM flicker writes happen during the
152+
'ExtendSelection'.
153+
154+
If we yield before the command, then both GSM flicker writes happen during the
155+
'ReadMarker'.
156+
157+
If we don't yield, one write happens during the ReadMarker and the other
158+
happens /between/ 'ReadMarker' and 'ReadGsmState'.
159+
160+
It seems most intuitive for the updates to happen "as part of" the
161+
'ExtendSelection', so I'm favoring yielding after.
162+
163+
And since we're yielding after the command, we should also yield before the
164+
first command, for consistency.
165+
166+
-}
167+
168+
----- orphans
169+
170+
deriving instance Read LedgerStateJudgement
171+
172+
deriving anyclass instance TD.ToExpr LedgerStateJudgement
173+
174+
instance QC.Arbitrary LedgerStateJudgement where
175+
arbitrary = elements [TooOld, YoungEnough]
176+
shrink = \case
177+
TooOld -> [YoungEnough]
178+
YoungEnough -> []
179+
180+
instance QC.Arbitrary MarkerState where
181+
arbitrary = elements [Absent, Present]
182+
shrink = \case
183+
Absent -> [Present]
184+
Present -> []
185+
186+
-----
187+
188+
toGsmState :: ModelState -> GSM.GsmState
189+
toGsmState = \case
190+
ModelPreSyncing -> GSM.PreSyncing
191+
ModelSyncing -> GSM.Syncing
192+
ModelCaughtUp{} -> GSM.CaughtUp
193+
194+
toMarker :: GSM.GsmState -> MarkerState
195+
toMarker = \case
196+
GSM.PreSyncing -> Absent
197+
GSM.Syncing -> Absent
198+
GSM.CaughtUp -> Present
199+
200+
-----
201+
202+
onset :: Selection -> SI.Time
203+
onset (Selection _b (S s)) = SI.Time $ fromIntegral s
204+
205+
ageLimit :: Num a => a
206+
ageLimit = 10 -- seconds
207+
208+
thrashLimit :: Num a => a
209+
thrashLimit = 8 -- seconds
210+
211+
durationUntilTooOld :: Selection -> IOSim.IOSim s GSM.DurationFromNow
212+
durationUntilTooOld sel = do
213+
let expiryAge = ageLimit `SI.addTime` onset sel
214+
now <- SI.getMonotonicTime
215+
pure $ case compare expiryAge now of
216+
LT -> GSM.Already
217+
GT -> GSM.After $ realToFrac $ expiryAge `SI.diffTime` now
218+
219+
-- 'boringDur' cannot prevent this case. In particular, this case
220+
-- necessarily arises in the GSM itself during a 'TimePasses' that
221+
-- incurs a so-called /flicker/ event, in which the anti-thrashing
222+
-- timer expires and yet the node state at that moment still
223+
-- _immediately_ indicates that it's CaughtUp. For the specific case of
224+
-- this test suite, the answer here must be 'GSM.Already'.
225+
EQ -> GSM.Already
226+
227+
candidateOverSelection ::
228+
Selection
229+
-> Candidate
230+
-> GSM.CandidateVersusSelection
231+
candidateOverSelection (Selection b _s) (Candidate b') =
232+
-- TODO this ignores CandidateDoesNotIntersect, which seems harmless, but
233+
-- I'm not quite sure
234+
GSM.WhetherCandidateIsBetter (b < b')
235+
236+
-- | Checks that a 'TimePasses' command does not end exactly when a timeout
237+
-- could fire and that a 'ExtendSelection' does not incur a timeout that would
238+
-- fire immediately
239+
--
240+
-- This insulates the test from race conditions that are innocuous in the real
241+
-- world.
242+
boringDurImpl :: SI.Time -> Selection -> ModelState -> Int -> Bool
243+
boringDurImpl clk sel st dur =
244+
boringSelection && boringState
245+
where
246+
-- the first time the node would transition to PreSyncing
247+
expiry timestamp = expiryAge `max` expiryThrashing timestamp
248+
expiryAge = SI.addTime ageLimit (onset sel)
249+
expiryThrashing timestamp = SI.addTime thrashLimit timestamp
250+
251+
clk' = SI.addTime (0.1 * fromIntegral dur) clk
252+
253+
boringSelection = clk' /= expiryAge
254+
255+
boringState = case st of
256+
ModelPreSyncing -> True
257+
ModelSyncing -> True
258+
ModelCaughtUp timestamp ->
259+
let gap = clk' `SI.diffTime` expiry timestamp
260+
n =
261+
mod
262+
(diffTimeToPicoseconds gap)
263+
(secondsToPicoseconds thrashLimit)
264+
in gap < 0 || 0 /= n
265+
266+
secondsToPicoseconds x = x * 10 ^ (12 :: Int)
267+
268+
-----

0 commit comments

Comments
 (0)