pub fn check_forwarded_count(tid: i32, produced: u64)Expand description
The COMPLETENESS RULE. A counted request from guest thread tid says it
produced produced records for forwarding since its previous counted request
(take_forwarded_since_request); it sent them before this request, and a
send on a message socket queues a record on the receiver before it returns,
so all of them have been received by now, as indexes 1 to produced in
order. Anything else means the records the coordinator holds for that
thread are not the ones it produced: fewer, or a skipped index, were lost on
the way (the guest disturbed the socket, the Tool could not adopt it, or a
stale descriptor was refused); more, or a repeated or earlier index, came
from something other than the Tool. Either way the coordinator writes a loss
notice and records the determinism loss, so verification refuses to compare
the run. UNCOUNTED (a thread could not be counted) is refused the same
way.
Without a registered source it does nothing.