kernel.core.vector-clock

Vector Clock, VC for short. Vector clocks are used to track causality of operations in the system.

An operation causes another if it happened before. This is difficult to achieve with physical clocks because of clock skew. Also, physical time can not capture whether two operations are concurrent (i.e., generated without knowledge of the other).

In contrast, vector clocks can capture the causally-preceding relation precisely. The algorithms were introduced by Fidge and Mattern. Adapted from https://github.com/michaelklishin/vclock.

Here, a vector clock maps from sites to integers counting events. This is not the most efficient implementation (there are garbage collection techniques in the literature).

_<

(_< VC-a VC-b)

Compares two vector clocks in O(n) for n sites. Returns true if one vector clock causally precedes the other.

Because new sites may join at any time, some sites may be missing in one of the vector clocks, so they are explicitly collected first.

Derivation of the algorithm from the vector clock definition (z refers to sites, x and y are the compared vector clocks):

  (for all z: xz <= yz) and (exists z: xz < yz)
= not not ((for all z: xz <= yz) and (exists z: xz < yz))
= not (not (for all z: xz <= yz) or not (exists z: xz < yz))
= not ((exists z: not xz <= yz) or (for all z: not xz < yz))
= not ((exists z: xz > yz) or (for all z: xz >= yz))
i.e.: check if all z: xz >= yz, and if a z: xz > yz is found, return early
i.e.: cond > return early (true)
      else = continue with current value
      else < continue with false (but no early return, as exists may still be true)
   => then do final not

view source