pub type ProtoTraceEvent<P> = TraceEvent<<P as Protocol>::Msg, <P as Protocol>::Ind, <P as Protocol>::Note, <P as Protocol>::Cmd>;Expand description
One event of a given protocol’s trace.
Aliased Type§
pub enum ProtoTraceEvent<P> {
Show 21 variants
Sent {
at: Time,
from: NodeId,
to: NodeId,
msg: <P as Protocol>::Msg,
},
Delivered {
at: Time,
from: NodeId,
to: NodeId,
msg: <P as Protocol>::Msg,
},
HandedToSelf {
at: Time,
node: NodeId,
msg: <P as Protocol>::Msg,
},
Dropped {
at: Time,
from: NodeId,
to: NodeId,
msg: <P as Protocol>::Msg,
reason: DropReason,
},
Duplicated {
at: Time,
from: NodeId,
to: NodeId,
msg: <P as Protocol>::Msg,
},
Reordered {
at: Time,
from: NodeId,
to: NodeId,
msg: <P as Protocol>::Msg,
},
TimerFired {
at: Time,
node: NodeId,
id: TimerId,
},
Indicated {
at: Time,
node: NodeId,
ind: <P as Protocol>::Ind,
},
SessionOpened {
at: Time,
a: NodeId,
b: NodeId,
epoch: u64,
},
SessionEnded {
at: Time,
a: NodeId,
b: NodeId,
epoch: u64,
reason: DropReason,
},
SuffixLost {
at: Time,
from: NodeId,
to: NodeId,
msg: <P as Protocol>::Msg,
},
Crashed {
at: Time,
node: NodeId,
},
Suspended {
at: Time,
node: NodeId,
},
Resumed {
at: Time,
node: NodeId,
},
Restarted {
at: Time,
node: NodeId,
},
Wrote {
at: Time,
node: NodeId,
kind: WriteKind,
},
DiedWriting {
at: Time,
node: NodeId,
},
Invoked {
at: Time,
node: NodeId,
op: OpId,
cmd: <P as Protocol>::Cmd,
},
NotInvoked {
at: Time,
node: NodeId,
op: OpId,
cmd: <P as Protocol>::Cmd,
why: NotBegun,
},
Said {
at: Time,
node: NodeId,
note: <P as Protocol>::Note,
},
Recovered {
at: Time,
node: NodeId,
had_state: bool,
},
}Variants§
Sent
A protocol asked for a message to be transmitted.
Delivered
A message was handed to the recipient protocol.
HandedToSelf
A message a process addressed to itself, handed over without the network.
Not a TraceEvent::Sent, because it crosses no wire: a driver is what turns a request to
send into a packet, and a packet addressed to the process it came from is a hand-off between
two roles in one state machine. Counting it among what a run put on the network overstates
what a deployment costs, and giving it a delivery bound makes every phase of a co-located
protocol slower than it is.
Recorded, and not merely elided, because ceasing to be a network message must not mean ceasing to be observable. A leader learning of a higher ballot from its own acceptor is a refusal like any other, and a suite that could not see it lost a non-vacuity floor two registered safety tests depend on — which is what an earlier draft, eliding it inside the protocol, actually did.
Dropped
A message was not delivered.
Duplicated
The network scheduled a second copy of a message.
Reordered
A message was selected for extreme delay.
TimerFired
A timer previously set by a protocol fired.
Indicated
A protocol delivered on its guarantee to the layer above.
SessionOpened
A session was established between two processes.
SessionEnded
A session ended. Anything still in flight may have been discarded.
SuffixLost
A message discarded because the session carrying it ended.
Crashed
A process crashed, losing its volatile state.
Suspended
A process was suspended, keeping its state.
Resumed
A suspended process resumed, and everything held for it was dispatched.
Restarted
A crashed process restarted, and took its startup branch.
Wrote
A durable write. kind distinguishes rewriting metadata from appending, so a claim about
a protocol’s write cost can be checked rather than asserted.
DiedWriting
A process died inside a write. Whether that write landed is decided by the seed and is deliberately not recorded: the point of the fault is that nobody knows until the recovered process reads its storage back.
Invoked
A process was given an operation, and handled it.
Recorded when the handler ran, not when the command was scheduled. A handler’s effects cannot precede the handler, so this is a valid left-hand end of the interval containing the operation’s effect, and a tighter one than the moment the caller asked — which matters, because a suite that schedules several commands at one instant would otherwise show them all overlapping each other.
NotInvoked
A process was given an operation and never handled it.
Recorded rather than discarded silently: an operation asked for and never begun is not the same as one never asked for, and a record that cannot tell them apart is one a checker would reason from falsely.
Said
A process narrated a decision it took.
The one event here that is not something that happened to a process. It is in the same account, on the same clock, precisely so that a claim can be read against the run — a process saying it refused an announcement is a process from which no acceptance followed, and a test can require that rather than trust it.
Recorded before the writes and effects of the handler that narrated it: a note marks the decision, and the write and the sends are what the decision led to.
Recovered
A restarted process was given back what it had written. had_state is false when it had
written nothing and started as if for the first time.