28 Operation factorisation

Let L be a contextually serialised list of operations, associated with operations in 𝜒(v2)\𝜒(v1) where v1 and v2 are causally valid vector times satisfying v1 ≤ v2 and v1 represents the execution context of L. Let ∑L denote the merge of all operations in L into a single composite operation.

Let v be a causally valid vector time satisfying v1 ≤ v ≤ v2. It should therefore be possible to transpose operations in L as required so that L is L2 appended to L1 - i.e. L = L1 L2 where L1 corresponds to operations in 𝜒(v)\𝜒(v1), and L2 are the operations in 𝜒(v2)\𝜒(v). Note that L1 >> L2, vin(L1) = v1, vin(L2) = v.

The factorization of operation ∑L for given v returns ∑L1 and ∑L2. Factorisation can be regarded as the opposite of merging because ∑L = ∑L1 ⊕>> ∑L2.

We therefore define the following functions that return the left and right factors of a given composite operation ∑L for a given vector time v.

Definition: Lf(∑L,v) = ∑L1 denotes the Lfactor with respect to v, and Rf(∑L,v) = ∑L2 denotes the Rfactor with respect to v.

Note that transpose and pop on a transient HB-suffix is analogous to replacing it by its Rfactor.

More formal definition

Definition: Let O be a composite operation and v be a causally valid vector time satisfying

vin(O) ≤ v ≤ vout(O).

Then Lf(O,v) = ∑[vin(O) , v) and

Rf(O,v) = ∑[v , vout(O))

Rf2 function

It is convenient to define the following function: 


Operation Rf2(Operation o, VectorTime v)
{
    assert(vin(o) ≤ v);
    return Rf(o,vout(o) ↓ v);
}

This relates to the following picture where from composite operation o associated with vout(o)\vin(o) we want to exclude that part that overlaps with some vector time v that is known to contain vin(o):