14.5 Vector Time

(February 2008)

Site identifiers

It is assumed that each site is uniquely identified with a site identifier. Let S be the set of site identifiers.

Vector times

Definition:
Let ℕ be the set of natural numbers (i.e. non-negative integers). A vector time v is a map
v : S → ℕ
Definition:
The vector time v∅ satisfies ∀s ∈ S, v∅(s) = 0.

Subset, intersection and union on vector times

Definition:
For vector times v1,v2, v = v1 ↑ v2 denotes the vector time satisfying
∀s ∈ S, v(s) = max( v1(s), v2(s) )
Definition:
For vector times v1,v2, v = v1 ↓ v2 denotes the vector time satisfying
∀s ∈ S, v(s) = min( v1(s), v2(s) )
Definition:
For vector times v1,v2, we write v1 ≤ v2 if ∀ s ∈ S, v1(s) ≤ v2(s)

Note

  • ∀v, v ↓ v = v
  • ∀v, v ↑ v = v
  • ∀v1,v2, v1 ↓ v2 = v2 ↓ v1
  • ∀v1,v2, v1 ↑ v2 = v2 ↑ v1
  • ∀v1,v2,v3, (v1 ↓ v2) ↓ v3 = v1 ↓ (v2 ↓ v3)
  • ∀v1,v2,v3, (v1 ↑ v2) ↑ v3 = v1 ↑ (v2 ↑ v3)
  • ∀v1,v2,v3, (v1 ↓ v2) ↑ v3 = (v1 ↑ v3) ↓ (v2 ↑ v3)
  • ∀v1,v2,v3, (v1 ↑ v2) ↓ v3 = (v1 ↓ v3) ↑ (v2 ↓ v3)
  • ∀v, v∅ ≤ v
  • ∀v, (v∅ ↑ v) = v
  • ∀v, (v∅ ↓ v) = v∅
  • ∀v1,v2, (v1 ↓ v2) ≤ v1
  • ∀v1,v2, v1 ≤ (v1 ↑ v2)
  • ∀v, v ≤ v
  • v1 ≤ v2 & v2 ≤ v1 ⇒ v1 = v2
  • v1 ≤ v2 & v2 ≤ v3 ⇒ v1 ≤ v3
  • v1 ≤ v & v2 ≤ v ⇒ (v1 ↑ v2) ≤ v

Identification of atomic operations

Each atomic operation is assumed to be generated at exactly one site. Each site independently assigns a zero based sequence number t to each atomic operation generated at that site.

Definition:
Let op(s,t) denote the atomic operation generated at site s with sequence number t.

Extent of a vector time

Definition:
The extent of vector time v is the set of atomic operations denoted by χ(v) satisfying
χ(v) = { op(s,t) | t < v(s) }

This definition relates to the whole purpose for vector times - for a given atomic operation O, we describe its execution context using the vector time v satisfying ec(O) = χ(v). This is a summary of the complete set of atomic operations that have been executed prior to O.

Note the following

  • χ(v2) \ χ(v1) = { op(s,t) | v1(s) ≤ t < v2(s) }
  • χ(v∅) = {}
  • χ(v1 ↑ v2) = χ(v1) ∪ χ(v2)
  • χ(v1 ↓ v2) = χ(v1) ∩ χ(v2)
  • v1 ≤ v2 ⇔ χ(v1) ⊆ χ(v2)

Precedes relation on atomic operations

Definition:
Let Ob be an atomic operation originally generated on site B. We write Oa → Ob if Oa was executed on B before Ob was generated on B.
Definition:
Oa and Ob are concurrent (written Oa || Ob) if Oa ≠ Ob and neither Oa → Ob nor Ob → Oa.
Definition:
The system enforces Causality Preservation if
Oa → Ob ⇒ Oa is executed before Ob on all sites
Claim:
Causality preservation ⇒ → is a transitive relation
Proof:
Suppose Oa → Ob and Ob → Oc.
Let Oc be generated on site C.
Ob → Oc so Ob was executed on site C before Oc was generated.
By causality preservation and Oa → Ob, we know that Oa is executed before Ob at all sites, and in particular at site C.
Therefore Oa was executed at site C before Oc was generated at site C, so we deduce Oa → Oc.

Execution context of an atomic operation

Definition:
Vector time gc(O) denotes the generation context of atomic operation O such that χ(gc(O)) is the set of operations that had been executed prior to the original generation of O.

It follows from the definitions that

Oa → Ob ⇔ Oa ∈ χ(gc(Ob))

Definition:
Vector time ec(O) denotes the execution context of atomic operation O such that χ(ec(O)) is the set of operations that have been performed prior to execution of O.
Claim:
Causality preservation ⇒ gc(O) ≤ ec(O)
Claim:
Oa → Ob ⇒ Oa ∈ χ(ec(Ob))
Proof:
Oa → Ob
⇔Oa ∈ χ(gc(Ob))
⇒Oa ∈ χ(ec(Ob))

It is assumed that a site generates operations in the context of previously generated operations at that site. Formally this means

t1 < t2 ⇔ op(s,t1) → op(s,t2)

Claim:
Oa || Ob ⇒ Oa.s ≠ Ob.s
Proof:

Suppose Oa || Ob and Oa.s = Ob.s.

if Oa.t < Ob.t
Oa → Ob(because t1< t2 ⇔ op(s,t1) → op(s,t2))
⇒contradiction to Oa || Ob
else if Ob.t < Oa.t
Ob → Oa(because t1< t2 ⇔ op(s,t1) → op(s,t2))
⇒contradiction to Oa || Ob
else
Oa.t = Ob.t
Oa = Ob(because Oa.s = Ob.s and Oa.t = Ob.t)
⇒contradiction(because Oa || Ob ⇒ Oa ≠ Ob)

Aggregate intersection and union on sets of vector times

Definition:
For set of vector times V, v = ↓(V) denotes the vector time satisfying
∀s ∈ S, v(s) = min { v'(s) | v' ∈ V }
Definition:
For set of vector times V, v = ↑ (V) denotes the vector time satisfying
∀s ∈ S, v(s) = max { v'(s) | v' ∈ V }

Causally valid vector times

Definition:
Vector time v is causally valid if
O1 ∈ χ(v), O2 ∉ χ(v) ⇒ ¬ (O2 → O1)

or equivalently

O2 ∈ χ(v) and O1 → O2 ⇒ O1 ∈ χ(v)

Taking the negation, vector time v breaks causality if

∃operations O1,O2 st O1 ∉ χ(v) and O2 ∈ χ(v) and O1 → O2

Claim:
Causality preservation ⇒ for every atomic operation, ec(O) is causally valid

Each site is assumed to have a linear sequence of operations that have been executed at that site called a history buffer. For a given site, let vh denote the vector time whose extent describes the current contents of the history buffer.

Let v be a causally valid vector time satisfying v ≤ vh. It can be proven that it is possible to transpose adjacent, concurrent operations within the history buffer to separate it into a prefix and suffix such that the set of operations in the prefix equals χ(v) and the suffix corresponds to χ(vh) \ χ(v). Furthermore no atomic operation in the suffix causally precedes an atomic operation in the prefix.

More specifically it won't be necessary to ever transpose a pair of contextually serialised operations [O1, O2] where O1 → O2.

Claim:
v1,v2 are causally valid ⇒ v1 ↓ v2 is causally valid
Proof:

Let v = v1 ↓ v2. Let O1,O2 be operations with O2 ∈ χ(v) and O1 → O2. Need to show O1 ∈ χ(v).

χ(v) = χ(v1 ↓ v2) = χ(v1) ∩ χ(v2)
O2 ∈ χ(v1)(because O2 ∈ χ(v) = χ(v1) ∩ χ(v2))
O2 ∈ χ(v2)(because O2 ∈ χ(v) = χ(v1) ∩ χ(v2))
O1 ∈ χ(v1)(because O2 ∈ χ(v1) and v1 is causally valid)
O1 ∈ χ(v2)(because O2 ∈ χ(v2) and v2 is causally valid)
O1 ∈ χ(v1) ∩ χ(v2)(because O1 ∈ χ(v1) and O1 ∈ χ(v2))
O1 ∈ χ(v)(because χ(v) = χ(v1) ∩ χ(v2))
Claim:
v1,v2 are causally valid ⇒ v1 ↑ v2 is causally valid
Proof:

Let v = v1 ↑ v2. Let O1,O2 be operations with O2 ∈ χ(v) and O1 → O2. Need to show O1 ∈ χ(v).

χ(v) = χ(v1 ↑ v2) = χ(v1) ∪ χ(v2)
if O2 ∈ χ(v1)
O1 ∈ χ(v1)(because O2 ∈ χ(v1) and v1 is causally valid)
O1 ∈ χ(v)(because χ(v1) ⊆ χ(v1) ∪ χ(v2) = χ(v))
else
O2 ∈ χ(v2)(because O2 ∈ χ(v1) ∪ χ(v2) and O2 ∉ χ(v1))
O1 ∈ χ(v2)(because O2 ∈ χ(v2) and v2 is causally valid)
O1 ∈ χ(v)(because χ(v2) ⊆ χ(v1) ∪ χ(v2) = χ(v))

It follows therefore that

∀ v ∈ V, v is causally valid ⇒ ↓(V) and ↑(V) are causally valid

Formulation that allows more sites over time

Usually a vector time is defined with respect to a fixed number of sites in the system. In practice we need a definition that naturally allows for new sites to be added over time.

Definition:
A vector time v is a set of (s,t) values where s is a site identifier and t is a positive integer, and the s values are never repeated. We write sites(v) for the set of s values in v. We write v(s) to retrieve t for given s. v(s) is defined to be zero for s ∉ sites(v)

It is straightforward to adjust the previous definitions to avoid reference to some fixed set of states S.

v1 ≤ v2 ⇔ ∀ s ∈ sites(v1), v1(s) ≤ v2(s)

For vector times v1,v2, v = v1 ↑ v2 denotes the vector time satisfying

sites(v) = sites(v1) ∪ sites(v2)
∀s ∈ sites(v), v(s) = max( v1(s), v2(s) )

For vector times v1,v2, v = v1 ↓ v2 denotes the vector time satisfying

sites(v) = sites(v1) ∩ sites(v2)
∀s ∈ sites(v), v(s) = min( v1(s), v2(s) )

Delta vector times

A delta vector time represents a change to a vector time which can be useful to reduce network bandwidth.

Definition:
A delta vector time Δv = v2-v1 where v1 and v2 are vector times is defined as follows
Δv = { (s,t) ∈ v2 | t ≠ v1(s) } ∪ { (s,0) | s ∈ sites(v1) \ sites(v2) }
and sites(Δv) = { s | (s,t) ∈ Δv }

We define v1+Δv as follows.

v1+ Δv = { (s,t) ∈ v1| s ∉ sites(Δv) } ∪ { (s,t) ∈ Δv | t > 0 }
Claim:
v1 + (v2-v1) = v2
Proof:
sites(v2-v1) = { s | (s,t) ∈ v2 and t ≠ v1(s) } ∪ sites(v1) \ sites(v2)
(⊆)
Suppose (s,t) ∈ v1 + (v2-v1)
so (s,t) ∈ ( { (s,t) ∈ v1| s ∉ sites(v2-v1) } ∪ { (s,t) ∈ (v2-v1) | t > 0 } )
if (s,t) ∈ (v2-v1) and t > 0
(s,t) ∈ v2 and t ≠ v1(s)
else
(s,t) ∈ v1 and s ∉ sites(v2-v1)
s ∈ sites(v1) (because (s,t) ∈ v1)
t > 0 (because (s,t) ∈ v1)
(s,t) ∉ (v2-v1)
if s ∉ sites(v2)
s ∈ sites(v1) \ sites(v2)
s ∈ sites(v2-v1) ⇒ contradiction
so s ∈ sites(v2)
Suppose v1(s) = t ≠ v2(s)
(s, v2(s)) ∈ (v2-v1)
so s ∈ sites(v2-v1) ⇒ contradiction
so v2(s) = t
so (s,t) ∈ v2
(⊇)
Suppose (s,t) ∈ v2
if t ≠ v1(s)
(s,t) ∈ v2-v1
t > 0 (because (s,t) ∈ v2)
(s,t) ∈ v1 + (v2-v1)
else
t = v1(s)
so (s,t) ∈ v1
Suppose s ∈ sites(v2-v1)
((s,t) ∈ v2 and t ≠ v1(s)) or (s ∈ sites(v1) and s ∉ sites(v2))
⇒ contradiction
So s ∉ sites(v2-v1)
So (s,t) ∈ { (s,t) ∈ v1 | s ∉ sites(v2-v1) }
So (s,t) ∈ v1+( v2-v1)

We can define addition of delta vector times Δv = Δv1+ Δv2, satisfying (for any given vector time v)

(v + Δv1) + Δv2 = v + (Δv1+ Δv2)

Note that addition of delta vector times doesn’t commute.

It can be show that

Δv1+ Δv2 = Δv2∪ { (s,t) ∈ Δv1| s ∉ sites(Δv2) }

Vector time implementation

To facilitate fast look up of a vector time, a suitable implementation is a red-black tree. However a delta vector time has no need for fast look up, and therefore may be more efficiently stored using a variable size array of (s,t) pairs.

We can define an add method on a vector time in pseudo code as follows 

v.add(s,t)
{
    if (v.hasentry(s))
    {
        v.remove(s);
    }
    if (t > 0)
    {
        v.insert(s,t);
    }
}

Applying a delta to a vector time simply involves calling add(s,t) for each (s,t) in the delta.

We can define an add method on a delta vector time in pseudo code as follows 

Δv.add(s,t)
{
    if (Δv.hasentry(s))
    {
        Δv.remove(s);
    }
    Δv.insert(s,t);
}

This may lead to a delta that has more (s,t) entries that it needs - because it doesn’t check for redundancy w.r.t the original vector time to which the delta applies.

Related work

The causally valid vector times in this chapter correspond to what the distributed-systems literature commonly calls consistent cuts. Under this correspondence, the extent χ(v) is the set of events in the cut, and the componentwise ordering of vector times is the inclusion ordering of their extents.

Mattern shows that consistent cuts form a sublattice of the lattice of all cuts [2]. In particular, consistent cuts are closed under infimum and supremum. This gives the standard literature counterpart of the claims above that causally valid vector times are closed under ↓ and ↑. Garg and Mittal likewise formulate the consistent cuts of a distributed computation as a distributive lattice [3]. The terminology and χ(v) notation used in this chapter are specific to the present treatment, but the underlying closure result is standard.

References

  1. Leslie Lamport, Time, Clocks, and the Ordering of Events in a Distributed System, Communications of the ACM, 21(7), pages 558–565, 1978.
  2. Friedemann Mattern, Virtual Time and Global States of Distributed Systems, 1989.
  3. Vijay K. Garg and Neeraj Mittal, On Slicing a Distributed Computation, 2001.

Source code

The surviving 2008 C++ implementation is retained as a documentation resource. The source browser also includes TestVectorTime.cpp, a comprehensive unit test written for the refactored TVectorTime implementation in 2019; it is included as later supporting material and is not part of the original 2008 source. Browse the source files.