Changes
/* Definitions */ define an explicit-ack
Once ''m'' is fully-acked, ''u'' knows that everyone else has seen ''m'' and all messages before it. We'll call the process of gaining that knowledge, "reaching consistency for ''m''" (given context, ''m'' might be implicit). We don't have another mechanism for it, so henceforth we'll use "reach consistency" interchangeably with "reach full-ack", though strictly the former is a security property and the latter is a mechanism for achieving it.
An '''explicit-ack''' is a message with no other content, that is sent solely for the purpose of declaring (via recv-parent) what the sender has seen. We'll make use of these to ensure consistency is reached in a timely manner, even if no-one wants to send a normal message (that contains user-level contents, and which is an '''implicit-ack''').
== Consistency ==
