15 Vector Time

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

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,O2be 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 v1is 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 ≠ 1(s) } ∪ { (s,0) | s ∈ sites(1) \ 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.

References

[1] Time, clocks, and the ordering of events in a distributed system
Communications of the ACM 21 (7): 558-565.
Leslie Lamport (1978).

TVectorTime.h in cxOT

Source: Ceda/cxOT/TVectorTime.h