37 Dom relation for assignment

This solution using the dom relation was developed in 2008.

According to Lossy assignment operations we can avoid the whole need for a HB suffix to transform remote operations by using a map from FieldId to the right most enabled assignment in the HB, and by using backward chaining of enabled assignment operations for a given FieldId.

In the following treatment we go even further because we don't even want to store a history buffer as a linear list of operations.

Consider that a composite assignment operation O stores the following state:

• v_in(O) and v_out(O), or what amounts to the same thing, for each siteid record a half open interval [t₁,t₂) for the operations that are present in the operation.
• A map<FieldId, list<AssignmentEntry> > that records entries for enabled assignments. Disabled assignments are not recorded.

where we have defined

struct AssignmentEntry
{
    SiteId s;
    int t;
    Value v;
};

Definition: Let L_i denote the i^th element of list L. We say that list L of assignment entries is causally ordered if

i < j ⇔ L_i → L_j

Note that if L is causally ordered then there can be no entries with L_i || L_j.

Definition: A subsequence of a list is any list formed from a subset of the elements as long as they appear in the same relative order.

Obviously any sub-sequence of a causally ordered list is also causally ordered.

Definition: Given causally valid vector time v, let Q(v) be characterised as follows:

1. v_in(Q(v)) = v_∅ and v_out(Q(v)) = v
2. Q(v) only contains a subset of the atomic assignments op(s,t) ∈ 𝜒(v) on the field.
3. Q(v) is causally ordered.
4. Q(v) is maximal, meaning no additional operations can be inserted into the sequence without breaking the causal ordering.

Claim: Q(v) is uniquely defined.

The list<AssignmentEntry> is interpreted as an ordered sequence of enabled assignments, where each assignment dominates all previous assignments in the sequence. The list is assumed to be causally ordered.

The justification for not storing disabled assignments (or indeed q positions) is that the proposed control algorithm never uses transpose (or ET).

In the following we focus attention on assignment operations on the same FieldId.

Dual IT between two lists

Let L₁, L₂ be concurrent, context equivalent, causally ordered lists of atomic assignment operations on the same field.

The dualIT transforms every operation in L₁ with every operation in L₂ according to the following figure.

Definition:

• Let s_∞ be a special siteid value which compares larger to all other siteids. A site cannot use s_∞ for its siteid.
• Let s_min(L) be the minimum siteid that appears in L, or else s_∞ if L = [].
• L₁ ⊕ L₂ = (s_min(L₁) < s_min(L₂)) ? L₁ : L₂

L₁,L₂ are causally ordered so therefore L₁ ⊕ L₂ must be causally ordered.

Claim: L₁ ⊕ L₂ = L₂ ⊕ L₁

Claim: (L₁ ⊕ L₂) ⊕ L₃ = L₁ ⊕ (L₂ ⊕ L₃)

Associativity and commutativity of ⊕ shows that at quiescence all sites will converge to the same representation of the operation which represents the merge over all assignments performed across all sites. ie we have a uniqueness of representation.

Claim: (L₁ ⊕ L₂) ~ (L₁ + IT(L₂,L₁)).

Claim: L₁ ⊕ L₂ is maximal in its use of atomic operations compatible with the constraint that it be causally ordered and all operations in the sequence are enabled.

We now extend the definition of ⊕ to deal with context equivalent operations O₁,O₂ (ie satisfying v_in(O₁) = v_in(O₂)). Let O₁ ⊕_C O₂ = Lf(O₁,v) + (Rf(O₁,v) ⊕_|| Rf(O₂,v)) where v = v_out(O₁) ↓ v_out(O₂).

Claim: O₁ ⊕_C O₂ = O₂ ⊕_C O₁

Proof: This is true if Lf(O₁,v) = Lf(O₂,v), and we could only assume that with some kind of inductive argument!

Factorising an assignment operation

Note that

Factorisation of a list of assignment entries doesn't require transposing of entries because there is no pair O₁,O₂ that are concurrent (O₁ || O₂).

Instead factorisation with respect to a causally valid vector time v simply involves splitting the list into prefix and suffix where assignment entries in the prefix satisfy t < v(s), and in the suffix satisfy t ≥ v(s).

That this is always possible without need for transpose follows directly from the definition of a causally valid vector time.

v is causally valid so O₁ → O₂ and O₂ ∈ 𝜒(v) ⇒ O₁ ∈ 𝜒(v)

so if O₁ appears before O₂ in the list, O₂ ∈ 𝜒(v) ⇒ O₁ ∈ 𝜒(v)

Note that since both an LFactor or RFactor of a list is a subsequence of the original, each preserves the causal ordering.

Merge of assignments

Let O₁,O₂ be two composite assignment operations on the same FieldId, and satisfying v_in(O₁) ≤ v and v_in(O₂) ≤ v where

v = v_out(O₁) ↓ v_out(O₂).

By definition O₁ ⊕_R O₂ = ∑[ v_in (O₁), v_out(O₁)↑v_out(O₂) )

Consider that we factorise O₁ with respect to v. From the above we have seen that this simply involves splitting its list of assignment entries into two parts without any need for transposition. Similarly we factorise O₂ with respect to v.

It was shown previously that Rf(O₁,v) || Rf(O₂,v). Therefore given an assignment entry in Rf(O₁,v) and an assignment entry in Rf(O2,v) we can assume they are concurrent. Therefore they were generated by different sites and the entry with smaller siteid is regarded as dominating the other.

We have previously treated the case of merging two concurrent lists.

Definition: O₁ ⊕_R O₂ = s_min (Rf(O₁,v)) < s_min(Rf(O₂,v)) ? O₁ : Lf(O₁,v) + Rf(O₂,v) where + denotes list concatenation.

Bogus

Further compression of assignment operations

Consider that a site never takes an LFactor of an operation, and it always sends an entire RFactor of the existing HB.

It would appear possible to achieve further compression of an assignment operation by only recording the value for the last assignment in the list, and by ignoring the relative order of the enabled assignments in the list.

It turns out that this is enough information to apply operations, take RFactors and to merge two operations. However, it doesn't allow for an LFactor to be calculated.

Definition: Let N be the set of non-negative integers. ie N = { 0,1,2,3,... }

Definition: Let T⊆ N and n ∈ N. Then we define

Note that ∀n, T = T_left(T,n) ⋃ T_right(T,n).

Definition: for a given FieldId, O and s, let

t_set(O,s) = { t | op(s,t) ∈ Ψ(O) } ⊆ N.

Claim: t_set(Lf(O,v),s) = T_left( t_set(O,s), v(s) )

Definition: Let predicate P_s(O₁,O₂) = (s_min(Rf(O₁,v)) < s_min(Rf(O₂ ,v)))

Implementation notes

A set of t values can be stored in increasing order in a vector. Binary search can be used to efficiently find a given t value, or to find the position to split the list into prefix and suffix according to v(s).

Assignable variables are often edited by dragging with the mouse, and therefore there can be many assignments per second (eg 50 Hz) by a given site. This makes some kind of run length encoding highly appropriate for representation of a set of t values, because it is quite likely there will be long runs of sequential t values in a range [t₁,t₂).

We can store both individual t values as well as pairs [t₁,t₂) in a single vector<int32> if we use the MSB to distinguish between an individual t values and the t₁ of a pair [t₁,t₂).

With some effort, binary search is compatible with run length encoding!

Proposed test

It is proposed that a self contained unit test be written that simulates n sites that generate and exchange assignment operations on a single assignable field.

An operation records the assigned value, plus a tset indexed by siteid.

struct Op
{
    VectorTime m_v1,m_v2;
    int m_value;
    map<SiteId, set<int> > m_tsets;
};

void Merge(Op& O1, const Op& O2)
{
    VectorTime v = O1.v2   O2.v2;
    for each s
    {
        set<int>& ts = O1.m_tsets[s];
         ...
    }
}

The test uses a single thread and doesn't use any IPC. In fact we don't even model a connection or transient HB-suffixes. Instead we emulate a sending of an operation by picking a sender site s₁ and receiver site s₂ at random and merging hb₁ into hb₂. This involves calculating v = v_out(hb₁) ↓ v_out(hb₂).

Dom relation on vector times

Definition: Let s₀ denote a special site id value (used as a "marker" - and not the identifier for any real site) that compares less to all other site ids. For any given vector time v, we assume v(s_o) = 0.

Definition: Given vector times v₁,v₂ we define s_m(v₁,v₂) as follows:

s_m(v₁,v₂) = (v₁ = v₂) ? s₀ : min { s | v₁(s) ≠ v₂(s) }

Claim: s_m(v₁,v₂) = s_m(v₂,v₁)

Definition: We say v₁ dominates v₂, written as dom(v₁,v₂) if

v₁(s_m(v₁,v₂)) > v₂(s_m(v₁,v₂))

Obviously dom(v₁,v₂) ⇒ v₁ ≠ v₂. In other words dom is irreflexive. ie ∀v, ¬dom(v,v)

The converse of this claim is false.

struct
{
    T value;
    VectorTime vend;
};