27 Notation

  • For vector times v1,v2, v1 ↑ v2 is a vector time that denotes the union of vector times v1,v2.
  • For vector times v1,v2, v1 ↓ v2 is a vector time that denotes the intersection of vector times v1,v2.
  • The empty vector time is denoted by v∅.
  • op(s,t) denotes the tth atomic operation performed on site s, starting at t = 0.
  • 𝜒(v) = { op(s,t) | t < v(s) } denotes the extent of vector time v
  • 𝜒[v1,v2) = 𝜒(v2)\𝜒(v1)
  • vin(O) denotes the vector time associated with the execution context (or input context) on which O is defined.
  • vout(O) denotes the vector time associated with the output state produced by execution of O.
  • Given composite operation O, the extent of O is the set of atomic operations represented by O and is denoted by Ψ(O) = 𝜒(vout (O)) \ 𝜒(vin(O)).
  • Composite operation O is empty if vin(O) = vout(O).
  • O1,O2 are context equivalent if vin(O1) = vin(O2).
  • O1,O2 are contextually serialised if vout(O1) = vin(O2).
  • The composite operation O1 ⊕ O2 denotes the (non lossy) merge of O1 and O2 where O1,O2 are contextually serialised operations.
  • ∑L denotes the merge of all operations in L into a single composite operation, where L is a list of contextually serialized operations.
  • ∑[v1,v2) denotes the composite operation obtained by merging a list of contextually serialised operations corresponding to 𝜒(v2)\𝜒(v1) and having execution context v1.
  • Lf(O,v) is shorthand for ∑[vin(O) , v), called the Lfactor of O with respect to v.
  • Rf(O,v) is shorthand for ∑[v , vout(O)) , called the Rfactor of O with respect to v.

Definition: Let the conditional (b ? x : y) evaluate to x if b is true, or otherwise it evaluates to y.

Note that

  • vin (∑[v1,v2)) = v1
  • vout(∑[v1,v2)) = v2
  • vin(O) ≤ vout(O)
  • Let O = op(s,t). Then vin(O)(s) = t and vout (O)(s) = t+1.
  • op(s,t) ∈ Ψ(O) ⇔ vin(O)(s) ≤ t < vout(O)(s)

Context equivalent and context serialized

Definition: We write O1 >> O2 if O1 ,O2 are contextually serialised. ie vout(O1) = vin(O2).

Definition: We write O1 <> O2 if O1 ,O2 are context equivalent. ie vin(O1) = vin(O2).

Definition: We write O1 >< O2 if O1 ,O2 are context convergent. ie vout(O1) = vout(O2).