Termination detection using causality and vector time

A problem unique to distributed systems is the need to determine that a computation is terminated. We use vector clocks as a basis for a termination detection protocol in which each process is only contacted once following termination. In addition we also present a definition of termination that does not depend on global state. This definition is based on the causal relationships between events and is stated in terms of Lamport´s “happens before” relation. Because the protocol is also specified in causal terms, this definition can be easily used to formally argue the correctness of the algorithm