Vector Clocks

[Andy Hutchinson]

Raghav and I have a working vector clock spec, an implementation, and some test cases that are up for review (really for other Quroum people to look at).  The file are attached, I think?  Email me if they aren't.  I suggest reading the original paper at http://sky.scitech.qut.edu.au/~fidgec/Publications/fidge88ahttp://en.wikipedia.org/wiki/Vector_clock.pdf and the wiki article for background information, http://en.wikipedia.org/wiki/Vector_clock.  Here's the protocol-only stuff:

# ===============
# =Vector Clocks=
# ===============
# This module implements the logic for updating a vector clock given
# local signals and remote signals for a particular group of
# processes.  A group is signified by a group identifier, :g_ident. A
# process is signified by an agent identifier, :a_ident.
#
# Note about ordering:
# --------------------
# This implementation does not decide event arrival order (i.e. two
# events modifying the same group in the same timestep).  Therefore, it
# is incapable of receiving more than one update in any particular
# timestep.  External users decide what message they consider to have
# arrived first.
#
# **Perhaps a future module could receive a buffered but ordered,
# uniquely identified set of updates which it then batch computes the
# resulting update all in one timestep.  Seemed like too much work
# without a solid use case.
#
# Note about Interface Usage Rules:
# ---------------------------------
# 0) One must use set_local_agent before receiving any signals, remote
#    or local.
#
# 1) One signal per group allowed per timestep!
#
# 2) A remote signal must be completely specified in the input. Do not
#    spread any particular remote signal across multiple timesteps.
#
# 3) The remote sender of the remote signal MUST be specified in
#    the same timestep as the remote signal.
#
# Usage violating these rules will result in non-deterministic
# behavior (either key-violation crash or inconsistent update)
#
# Output Behavior:
# ----------------
# This module will render an event clock every timestep. If no input
# is specified in a timestep, the clock will be THE SAME as it was the
# last timestep.  If an input is specified, the clock will immediately
# reflect the the new clock in the same timestep.
#
# Note about storage:
# -------------------
# This module does not store old versions of the clock which
# correspond to a previous event.  It is up to external users to read
# the resulting vector clock associated with the event and place it in
# storage if needed.
#
# Note about Dynamic Processes and Groups:
# -----------------------------
# This module supports dynamic addition (not subtraction!) of new
# processes in the system and groups as well.  If a (group,agent) pair
# is not present in a vector clock, it is assumed to be 0.
module VectorClockProtocol
  state do
    interface input, :set_local_agent, [:g_ident] => [:a_ident]
    interface input, :local_signal, [:g_ident] => []
    interface input, :remote_signal, [:g_ident, :a_ident] => [:stamp]
    interface input, :remote_sender, [:g_ident] => [:a_ident]
    interface output, :event_clock, [:g_ident, :a_ident] => [:stamp]
  end
end

# =======================
# =Vector Clock Ordering=
# =======================
#
# Computes a same timestep result of the comparison between
# events x and y:
#
# if VC(x)  --> VC(y) => result = -1   => x occured before y
# if VC(x) <--> VC(y) => result =  0   => x occured concurrently with y
# if VC(x) <--  VC(y) => result =  1   => x occured after y
module VectorClockOrderingProtocol
  state do
    interface input, :vc_x, [:g_ident, :a_ident] => [:stamp]
    interface input, :vc_y, [:g_ident, :a_ident] => [:stamp]
    interface output, :order, [:g_ident] => [:result]
  end
end