Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,14 @@ data PerasCertDB m blk = PerasCertDB
-- The 'Fingerprint' is updated every time a new certificate is added, but it
-- stays the same when certificates are garbage-collected.
, getCertSnapshot :: STM m (PerasCertSnapshot blk)
, getLatestCertSeen :: STM m (Maybe (WithArrivalTime (ValidatedPerasCert blk)))
-- ^ Get the certificate with the highest round number that has been added to
-- the db since it has been opened. This certificate is not affected by garbage
-- collection, but it's forgotten when the db is closed.
--
-- NOTE: having seen a certificate is a precondition to start voting in every
-- round except for the first one (at origin). As a consequence, only caught-up
-- nodes can actively participate in the Peras protocol for now.
, garbageCollect :: SlotNo -> m ()
-- ^ Garbage-collect state older than the given slot number.
, closeDB :: m ()
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -79,6 +79,7 @@ openDB args = do
{ addCert = getEnv1 h implAddCert
, getWeightSnapshot = getEnvSTM h implGetWeightSnapshot
, getCertSnapshot = getEnvSTM h implGetCertSnapshot
, getLatestCertSeen = getEnvSTM h implGetLatestCertSeen
, garbageCollect = getEnv1 h implGarbageCollect
, closeDB = implCloseDB h
}
Expand Down Expand Up @@ -170,18 +171,22 @@ implAddCert env cert = do
if Map.member roundNo pvcsCerts
then pure PerasCertAlreadyInDB
else do
let pvcsCerts' = Map.insert roundNo cert pvcsCerts
let pvcsLastTicketNo' = succ pvcsLastTicketNo
writeTVar pcdbVolatileState $
WithFingerprint
PerasVolatileCertState
{ pvcsCerts =
Map.insert roundNo cert pvcsCerts
pvcsCerts'
, -- Note that the same block might be boosted by multiple points.
pvcsWeightByPoint =
addToPerasWeightSnapshot boostedPt (getPerasCertBoost cert) pvcsWeightByPoint
, pvcsCertsByTicket =
Map.insert pvcsLastTicketNo' cert pvcsCertsByTicket
, pvcsLastTicketNo = pvcsLastTicketNo'
, pvcsLastTicketNo =
pvcsLastTicketNo'
, pvcsLatestCertSeen =
snd <$> Map.lookupMax pvcsCerts'
}
(succ fp)
pure AddedPerasCertToDB
Expand Down Expand Up @@ -220,6 +225,14 @@ implGetCertSnapshot PerasCertDbEnv{pcdbVolatileState} =
snd $ Map.split ticketNo pvcsCertsByTicket
}

implGetLatestCertSeen ::
IOLike m =>
PerasCertDbEnv m blk -> STM m (Maybe (WithArrivalTime (ValidatedPerasCert blk)))
implGetLatestCertSeen PerasCertDbEnv{pcdbVolatileState} =
readTVar pcdbVolatileState
<&> forgetFingerprint
<&> pvcsLatestCertSeen

implGarbageCollect ::
forall m blk.
IOLike m =>
Expand All @@ -236,12 +249,14 @@ implGarbageCollect PerasCertDbEnv{pcdbVolatileState} slot =
, pvcsWeightByPoint
, pvcsLastTicketNo
, pvcsCertsByTicket
, pvcsLatestCertSeen
} =
PerasVolatileCertState
{ pvcsCerts = Map.filter keepCert pvcsCerts
, pvcsWeightByPoint = prunePerasWeightSnapshot slot pvcsWeightByPoint
, pvcsCertsByTicket = Map.filter keepCert pvcsCertsByTicket
, pvcsLastTicketNo = pvcsLastTicketNo
, pvcsLatestCertSeen = pvcsLatestCertSeen
}
where
keepCert cert =
Expand Down Expand Up @@ -269,6 +284,9 @@ data PerasVolatileCertState blk = PerasVolatileCertState
, pvcsLastTicketNo :: !PerasCertTicketNo
-- ^ The most recent 'PerasCertTicketNo' (or 'zeroPerasCertTicketNo'
-- otherwise).
, pvcsLatestCertSeen :: !(Maybe (WithArrivalTime (ValidatedPerasCert blk)))
-- ^ The certificate with the highest round number that has been added to the
-- db since it has been opened.
}
deriving stock (Show, Generic)
deriving anyclass NoThunks
Expand All @@ -281,6 +299,7 @@ initialPerasVolatileCertState =
, pvcsWeightByPoint = emptyPerasWeightSnapshot
, pvcsCertsByTicket = Map.empty
, pvcsLastTicketNo = zeroPerasCertTicketNo
, pvcsLatestCertSeen = Nothing
}
(Fingerprint 0)

Expand All @@ -305,7 +324,6 @@ invariantForPerasVolatileCertState pvcs = do
<> " > "
<> show pvcsLastTicketNo
where
PerasVolatileCertState _ _ _ _keep = forgetFingerprint pvcs
PerasVolatileCertState
{ pvcsCerts
, pvcsWeightByPoint
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ module Test.Ouroboros.Storage.PerasCertDB.Model
, closeDB
, addCert
, getWeightSnapshot
, getLatestCertSeen
, garbageCollect
, hasRoundNo
) where
Expand All @@ -19,35 +20,40 @@ import Data.Set (Set)
import qualified Data.Set as Set
import GHC.Generics (Generic)
import Ouroboros.Consensus.Block
import Ouroboros.Consensus.BlockchainTime.WallClock.Types (WithArrivalTime)
import Ouroboros.Consensus.BlockchainTime.WallClock.Types (WithArrivalTime, forgetArrivalTime)
import Ouroboros.Consensus.Peras.Weight
( PerasWeightSnapshot
, mkPerasWeightSnapshot
)
import Ouroboros.Consensus.Util (safeMaximumOn)

data Model blk = Model
{ certs :: Set (WithArrivalTime (ValidatedPerasCert blk))
, latestCertSeen :: Maybe (WithArrivalTime (ValidatedPerasCert blk))
, open :: Bool
}
deriving Generic

deriving instance StandardHash blk => Show (Model blk)

initModel :: Model blk
initModel = Model{open = False, certs = Set.empty}
initModel = Model{open = False, certs = Set.empty, latestCertSeen = Nothing}

openDB :: Model blk -> Model blk
openDB model = model{open = True}

closeDB :: Model blk -> Model blk
closeDB _ = Model{open = False, certs = Set.empty}
closeDB _ = Model{open = False, certs = Set.empty, latestCertSeen = Nothing}

addCert ::
StandardHash blk =>
Model blk -> WithArrivalTime (ValidatedPerasCert blk) -> Model blk
addCert model@Model{certs} cert
| certs `hasRoundNo` cert = model
| otherwise = model{certs = Set.insert cert certs}
| otherwise = model{certs = certs', latestCertSeen = safeMaximumOn roundNo (Set.toList certs')}
where
certs' = Set.insert cert certs
roundNo = getPerasCertRound . forgetArrivalTime

hasRoundNo ::
Set (WithArrivalTime (ValidatedPerasCert blk)) ->
Expand All @@ -65,6 +71,11 @@ getWeightSnapshot Model{certs} =
| cert <- Set.toList certs
]

getLatestCertSeen ::
Model blk -> Maybe (WithArrivalTime (ValidatedPerasCert blk))
getLatestCertSeen Model{latestCertSeen} =
latestCertSeen

garbageCollect :: SlotNo -> Model blk -> Model blk
garbageCollect slot model@Model{certs} =
model{certs = Set.filter keepCert certs}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,7 @@ instance StateModel Model where
CloseDB :: Action Model ()
AddCert :: WithArrivalTime (ValidatedPerasCert TestBlock) -> Action Model AddPerasCertResult
GetWeightSnapshot :: Action Model (PerasWeightSnapshot TestBlock)
GetLatestCertSeen :: Action Model (Maybe (WithArrivalTime (ValidatedPerasCert TestBlock)))
GarbageCollect :: SlotNo -> Action Model ()

arbitraryAction _ (Model model)
Expand All @@ -80,6 +81,7 @@ instance StateModel Model where
[ (1, pure $ Some CloseDB)
, (20, Some <$> genAddCert)
, (20, pure $ Some GetWeightSnapshot)
, (10, pure $ Some GetLatestCertSeen)
, (5, Some . GarbageCollect . SlotNo <$> arbitrary)
]
| otherwise = pure $ Some OpenDB
Expand Down Expand Up @@ -128,6 +130,7 @@ instance StateModel Model where
CloseDB -> Model.closeDB model
AddCert cert -> Model.addCert model cert
GetWeightSnapshot -> model
GetLatestCertSeen -> model
GarbageCollect slot -> Model.garbageCollect slot model

precondition (Model model) = \case
Expand All @@ -140,6 +143,7 @@ instance StateModel Model where
where
p cert' = getPerasCertRound cert /= getPerasCertRound cert' || cert == cert'
GetWeightSnapshot -> True
GetLatestCertSeen -> True
GarbageCollect _slot -> True

deriving stock instance Show (Action Model a)
Expand All @@ -162,6 +166,9 @@ instance RunModel Model (StateT (PerasCertDB IO TestBlock) IO) where
GetWeightSnapshot -> do
perasCertDB <- get
lift $ atomically $ forgetFingerprint <$> PerasCertDB.getWeightSnapshot perasCertDB
GetLatestCertSeen -> do
perasCertDB <- get
lift $ atomically $ PerasCertDB.getLatestCertSeen perasCertDB
GarbageCollect slot -> do
perasCertDB <- get
lift $ PerasCertDB.garbageCollect perasCertDB slot
Expand All @@ -177,6 +184,11 @@ instance RunModel Model (StateT (PerasCertDB IO TestBlock) IO) where
counterexamplePost $ "Model: " <> show expected
counterexamplePost $ "SUT: " <> show actual
pure $ expected == actual
postcondition (Model model, _) GetLatestCertSeen _ actual = do
let expected = Model.getLatestCertSeen model
counterexamplePost $ "Model: " <> show expected
counterexamplePost $ "SUT: " <> show actual
pure $ expected == actual
postcondition _ _ _ _ = pure True

monitoring (Model model, _) (AddCert cert) _ _ prop =
Expand Down
Loading