pub trait NotificationChannelIsLossy { }Expand description
Definition (The notification channel is lossy). The channel carrying Notifications from
a validator to a client may drop any message, without notice to either side. Delivery is never
retried, never acknowledged, and never durable.
Where this sits in the fault model. Network loss needs no separate treatment — a notification
is a message between participants, so EventualSynchrony already permits it to be dropped
before GST and forbids that after. What this definition adds are three local ways to lose one,
which the network model does not describe: Notifier::notify_chain returns immediately when the
chain has no entry in its sender map; a failed sender.send is ignored and the dead sender
reaped; and NotificationImpliesPersistedChange orders the save before the dispatch, leaving a
window in which a change is persisted and the process dies before anything is sent.
The third behaves like a crash and is modelled as one: CorrectValidator permits a crash at
any time, freely before GST and with bounded recovery after. So no result may assume a
particular notification arrives, and a result may assume that a client which stays connected
to a reachable correct validator eventually learns.
The model has no notion of a partial crash, and this is where one would be needed. A
validator whose notification dispatch stops while its consensus path keeps running is not
described by anything here: it is not faulty, since it signs nothing wrong; it is not crashed,
since the process is alive and answering; and it is not merely “slow or unreachable”, the escape
CorrectValidator does allow, because it responds normally to everything except this. The
crash model is whole-process — a validator stops and restarts, losing unpersisted state — with
nothing between up and down. Component-level failure inside a live validator is outside the
model, and LostNotificationsAreRepaired shows it is not a harmless omission: it defeats two
of the three mechanisms that would otherwise repair a loss.
This is why the alternative statement — “no result depends on notification delivery” — is not worth making. In a model where the channel is lossy it cannot fail to hold; it is a property of the specification rather than of the system.
What repairs an individual loss is LostNotificationsAreRepaired.