21.12 Bogus solution for assignment

Rfactor of vector times

Definition:
For vector times v1,v2, let v2\v1 be the vector time satisfying, for each s:

(v2\v1)(s) = (v2(s) > v1(s)) ? v2(s) : 0

Claim:
v1↑(v2\v1) = v1↑v2
Proof:

Let s be given.

if v2(s) > v1(s)
(v1↑(v2\v1))(s)
=max(v1(s), (v2\v1)(s))
=max(v1(s), (v2(s) > v1(s)) ? v2(s) : 0)
=max(v1(s), v2(s))
=(v1↑v2)(s)
else
(v1↑(v2\v1))(s)
=max(v1(s), (v2\v1)(s))
=max(v1(s), 0)
=max(v1(s), v2(s))(because v1(s) ≥ v2(s))
=(v1↑v2)(s)
Claim:
v1 ≤ v2 ⇒ v1↑(v2\v1) = v2
Proof:
Suppose v1 ≤ v2.
v1↑(v2\v1)
=v1↑v2(previous claim)
=v2(because v1 ≤ v2)
Claim:
v ≤ v1 ⇒ v1↑v2 = v1↑(v2\v)
Proof:

Suppose v ≤ v1. Let s be given. Then v(s) ≤ v1(s).

if v1(s) < v2(s)
v(s) ≤ v1(s) < v2(s)
(v2\v)(s) = v2(s)
(v1↑v2)(s)
=max(v1(s), v2(s))
=max(v1(s), (v2\v)(s))(because v2(s) = (v2\v)(s))
=(v1↑(v2\v))(s)
else
v1(s) ≥ v2(s)
(v1↑v2)(s)
=max(v1(s), v2(s))
=v1(s)
=max(v1(s), (v2\v)(s))
=(v1↑(v2\v))(s)
Definition:
domf(v1,v2,v) = dom(v1, v2↑v)
Claim:
domf(v1, v2\v, v) ⇒ dom(v1,v2)
Proof:
domf(v1, v2\v, v)
=dom(v1, (v2\v)↑v)
=dom(v1, v2↑v)
⇒dom(v1,v2)
Claim:
v ≤ v1 and dom(v1,v2) ⇒ domf(v1, v2\v, v)
Proof:

This was recorded as a conjecture; the proof is incomplete.

We need a specialised version of the merge operator! Actually a different definition of dom(), that accounts for RFactors. We don't want v3 to appear to dominate (v2\v1), just because (v2\v1) has recorded some zeros. We only consider v3(s) > (v2\v1)(s) to be significant if v3(s) > v1(s) - which means that v3 has actually performed an assignment outside of 𝜒(v1) that beats v2. Note that (v2\v1)(s) > v3(s) is always significant.

That is:

if (v2\v1)(s) > v3(s) then v2 dominates v3 for that s;

if v3(s) > (v2\v1)(s) and v3 (s) > v1(s) then v3 dominates v2 for that s

otherwise neither dominates the other for that s.

We choose which operation dominates the other by finding the smallest s for which one dominates the other.

Note: we can use v1 ↑ (v2\v1) instead of (v2\v1), and go back to the conventional definition of dom!

Definition of merge

Definition:
Given operations O1,O2, define the merge O1 ⊕ O2 by:

(O1 ⊕ O2).vend = O1.vend ↑ O2.vend

(O1 ⊕ O2).value = dom(O1,O2) ? O1.value : O2.value

Claim:
O1 = O2 ⇒ O1 ⊕ O2 = O1 = O2
Claim:
¬dom(O1, O1 ⊕ O2)
Proof:

Follows from:

O1.vend ≤ (O1.vend ↑ O2.vend) = (O1 ⊕ O2).vend

Claim:
If X satisfies convergence then ∀O1,O2 ∈ X, O1 ⊕ O2 = O2 ⊕ O1
Proof:
(O1 ⊕ O2).vend
=O1.vend ↑ O2.vend
=O2.vend ↑ O1.vend(↑ commutes)
=(O2 ⊕ O1).vend
if O1 = O2
¬dom(O1,O2) ∧ ¬dom(O2,O1)(X satisfies convergence)
(O1 ⊕ O2).value = O2.value = O1.value = (O2 ⊕ O1).value
else
O1.vend ≠ O2.vend(X satisfies convergence)
dom(O1,O2) ⇔ ¬dom(O2,O1)
(O1 ⊕ O2).value
=dom(O1,O2) ? O1.value : O2.value
=dom(O2,O1) ? O2.value : O1.value
=(O2 ⊕ O1).value
Claim:
O1 ⊕ (O1 ⊕ O2) = O1 ⊕ O2 (absorption property)
Proof:
(O1 ⊕ (O1 ⊕ O2)).vend
=O1.vend ↑ (O1 ⊕ O2).vend
=O1.vend ↑ (O1.vend ↑ O2.vend)
=O1.vend ↑ O2.vend(absorption of ↑)
=(O1 ⊕ O2).vend
(O1 ⊕ (O1 ⊕ O2)).value
=dom(O1, O1 ⊕ O2) ? O1.value : (O1 ⊕ O2).value
=(O1 ⊕ O2).value(¬dom(O1, O1 ⊕ O2))
Claim:
If X satisfies convergence then ∀O1,O2,O3 ∈ X, (O1 ⊕ O2) ⊕ O3 = O1 ⊕ (O2 ⊕ O3)
Proof:
((O1 ⊕ O2) ⊕ O3).vend
=(O1 ⊕ O2).vend ↑ O3.vend
=(O1.vend ↑ O2.vend) ↑ O3.vend
=O1.vend ↑ (O2.vend ↑ O3.vend)(↑ is associative)
=O1.vend ↑ (O2 ⊕ O3).vend
=(O1 ⊕ (O2 ⊕ O3)).vend
if O1 = O2
O1 ⊕ O2 = O2(O1 = O2)
if O2 = O3
O1 = O2 ⊕ O3(O1 = O2 = O3)
O2 ⊕ O3 = O1 ⊕ (O2 ⊕ O3)(O1 = O2 ⊕ O3)
((O1 ⊕ O2) ⊕ O3).value
=(O2 ⊕ O3).value(O1 ⊕ O2 = O2)
=(O1 ⊕ (O2 ⊕ O3)).value(O1 = O2 ⊕ O3)
else
((O1 ⊕ O2) ⊕ O3).value
=(O2 ⊕ O3).value(O1 ⊕ O2 = O2)
=(O1 ⊕ (O2 ⊕ O3)).value(absorption)
else
if O2 = O3
Incomplete in the original: todo.
else
((O1 ⊕ O2) ⊕ O3).value
=dom(O1 ⊕ O2,O3) ? (O1 ⊕ O2).value : O3.value
=dom(O1 ⊕ O2,O3) ? (dom(O1,O2) ? O1.value : O2.value) : O3.value
=...
=(O1 ⊕ (O2 ⊕ O3)).value

Incomplete in the original: todo.

There is a concept of an overall winner that assigns its value in the merge. The merge is associative because the one and only winner always wins in the end, no matter what order we take, because the dom relation is asymmetric and transitive.

Definition:
Let X be a set of assignment operations on a given field. The merge closure of X is denoted by cl(X) and is the smallest set satisfying both:
  1. X ⊆ cl(X); and
  2. O1,O2 ∈ cl(X) ⇒ O1 ⊕ O2 ∈ cl(X).
Claim:
X satisfies convergence ⇒ cl(X) satisfies convergence
Proof:

We need to show ∀O1,O2 ∈ cl(X), O1.vend = O2.vend ⇒ O1.value = O2.value.

Let O1,O2 ∈ cl(X) and O1.vend = O2.vend. We will show O1.value = O2.value.

Proof is by induction.

If O1,O2 ∈ X then result follows from assumption that X satisfies convergence.

Inductive step incomplete.

We are now set for a proof of convergence at quiescence using an inductive proof. We need to formalise the control algorithm which is based on the merge operator. todo

Definition:
O' = Rf(O,v) is the operation satisfying:
  1. O'.value = O.value; and
  2. for each s, O'.vend(s) = O.vend(s) > v(s) ? O.vend(s) : 0.

[Note: If v(s) = t+1, then op(s,t) is the last op in 𝜒(v). If op(s,t) is in O, then O.vend(s) = t+1 = v(s). So need O.vend(s) > v(s) in order for there to be an operation in O not in 𝜒(v)]

Definition:
Given operations O1,O2, define the merge O1 ⊕ O2 by:

(O1 ⊕ O2).vend = O1.vend ↑ O2.vend

(O1 ⊕ O2).value = dom(O1,O2) ? O1.value : O2.value

We need a specialised version of the merge operator! Actually a different definition of dom(), that accounts for RFactors. We don't want O1 to appear to dominate Rf(O2,v), just because Rf(O2,v) has recorded some zeros in its vend. We only consider O1.vend(s) > Rf(O2,v).vend(s) to be significant if O1.vend(s) > v(s) - which means that O1 has actually performed an assignment outside of 𝜒(v) that beats O2. Note that Rf(O2,v).vend(s) > O1.vend(s) is always significant.

That is:

if Rf(O2,v).vend(s) > O1.vend(s) then O2 dominates O1 for that s;

if O1.vend(s) > Rf(O2,v).vend(s) and O1.vend(s) > v(s) then O1 dominates O2 for that s

otherwise neither dominates the other for that s.

We choose which operation dominates the other by finding the smallest s for which one dominates the other.

Note: we can use v ↑ Rf(O2,v).vend instead of Rf(O2,v).vend, and go back to the conventional definition of dom!

Claim:
v ≤ O1.vend ⇒ O1 ⊕ O2 = O1 ⊕ Rf(O2,v)
Proof:
Suppose v ≤ O1.vend.
Let s be given.
v(s) ≤ O1.vend(s)(because v ≤ O1.vend)
if O1.vend(s) < O2.vend(s)
v(s) ≤ O1.vend(s) < O2.vend(s)
Rf(O2,v).vend(s) = O2.vend(s)
(O1.vend ↑ O2.vend)(s)
=max(O1.vend(s), O2.vend(s))
=max(O1.vend(s), Rf(O2,v).vend(s))
=(O1.vend ↑ Rf(O2,v).vend)(s)
=(O1 ⊕ Rf(O2,v)).vend(s)
else
O1.vend(s) ≥ O2.vend(s)
(O1.vend ↑ O2.vend)(s)
=max(O1.vend(s), O2.vend(s))
=O1.vend(s)
=max(O1.vend(s), Rf(O2,v).vend(s))
=(O1.vend ↑ Rf(O2,v).vend)(s)
=(O1 ⊕ Rf(O2,v)).vend(s)
if dom(O1,O2)
∃s' st O1.vend(s') > O2.vend(s') and ∀s < s', O1.vend(s) = O2.vend(s)
O1.vend(s') > O2.vend(s') ≥ Rf(O2,v).vend(s')
∀s < s', O1.vend(s) = O2.vend(s) ≥ Rf(O2,v).vend(s)
Hence dom(O1, Rf(O2,v))
(O1 ⊕ O2).value
=dom(O1,O2) ? O1.value : O2.value
=O1.value
=dom(O1, Rf(O2,v)) ? O1.value : Rf(O2,v).value
=(O1 ⊕ Rf(O2,v)).value
else if dom(O2,O1)
∃s' st O2.vend(s') > O1.vend(s') and ∀s < s', O2.vend(s) = O1.vend(s)
v(s') ≤ O1.vend(s') < O2.vend(s')
Rf(O2,v).vend(s') = O2.vend(s')
Let s < s'. Then v(s) ≤ O1.vend(s) = O2.vend(s).
Suppose v(s) = O1.vend(s) = O2.vend(s).
Rf(O2,v).vend(s) = 0

We want to show dom(Rf(O2,v),O1) and ¬dom(O1,Rf(O2,v)).

(O1 ⊕ O2).value
=dom(O1,O2) ? O1.value : O2.value
=O2.value
=?
=dom(O1, Rf(O2,v)) ? O1.value : O2.value
=dom(O1, Rf(O2,v)) ? O1.value : Rf(O2,v).value
=(O1 ⊕ Rf(O2,v)).value

The original notes that this may be unprovable, suggesting a new definition of merge that accounts for RFactors is required.

Problem with the approach

It turns out that the above approach is incorrect! i.e. basically we cannot use a dom relation on vector times and use this to pick which operation dominates the other. The problem is that it doesn't account for causal relationships between operations.

For example, consider 3 sites S0,S1,S2 with S0 < S1 < S2. Consider the following sequence

  1. S0 assigns value 0, S1 assigns value 1.
  2. S2 receives 'assign 0' from S0.
  3. S2 assigns value 2.
  4. S0 receives 'assign 1' from S1.
  5. S0 receives 'assign 2' from S2.

The problem occurs in step 5, where S0 has S0.vout = (1,1,0), and receives operation from S2 with S2.vout = (1,0,1). When we compare these vector times we find dom(S0.vout, S2.vout), yet the assignment by S2 should dominate all other assignments.

How to fix the problem: Our earlier approach had a concept of discarding either the Rfactor of O1 or of O2 under the merge. We need to do exactly this with vend when we merge operations. i.e. instead of (O1 ⊕ O2).vend = O1 .vend ↑ O2.vend, we instead have:

Definition:
Given operations O1,O2, define the merge O1 ⊕ O2 by:

(O1 ⊕ O2).vend = dom(O1,O2) ? O1.vend : O2.vend

(O1 ⊕ O2).value = dom(O1,O2) ? O1.value : O2.value

This allows vend to discard information (i.e. losers because of causality). The problem with losers is that they can have low siteids and appear to be winners.

Note that a given site doesn't store historical information about vend, and instead trusts the received vend in order to revert due to losers.

Note however that it is not clear whether we can follow the idea of zeroing each vend(s) that doesn't exceed v(s) when we send a Rfactor.

Implementation notes

A universal operation stores information about all the assignments in a map keyed by fieldId. For each field it records the value (using a VectorOfByte), and the vector time vend.

From section 8, the control algorithm is:

Generate and apply local operation:

generate O;

Ohb = O;

Send operation:

send Rf(Ohb, v) for a v satisfying v ≤ remote-Ohb.hv;

Receive operation, merge with local HB and apply required changes:

receive O;

Ohb = Ohb ⊕ O;

It is assumed that Ohb records the vector time hv - which describes the entire set of operations in the history buffer.

The control algorithm involves

  • Generation of an assignment operation by applying op(s,t) = (assign field f with value v).
    • workingset.fields[f].value = v
    • Ohb.fields[f].value = v
    • Ohb.fields[f].vend(s) = t+1
    • Ohb.hv(s) = t+1
  • Extracting Rfactor to send, w.r.t. some underestimate of what's already present on the remote machine. This involves:
    • For each field f, for each s, if Ohb.fields[f].vend(s) > v(s) then need to send this. Only need to send Ohb.fields[f].value if there exists such an s.
  • Merging Ohb = Ohb ⊕ O where O is an Rfactor.
    • For each field f, for each s, Ohb.fields[f].vend ↑= O.fields[f].vend. and assign Ohb.fields[f].value = O.fields[f].value if dom(O,Ohb) on this field. We assume dom(O,Ohb) on field f if :

More on merging

A site receives an operation O. It needs to calculate Ohb = Ohb ⊕ O. This requires update to Ohb.fields[f].vend and Ohb.fields[f].value. The update to vend is easy. The update to the value depends on whether O dominates Ohb.

O is RFactor w.r.t. some vector time v. It only sends O.vend(s) values when O.vend(s) > v(s).

[Note: If v(s) = t+1, then op(s,t) is the last op in 𝜒(v). If op(s,t) is in O, then O.vend(s) = t+1 = v(s). So need O.vend(s) > v(s) in order for there to be an operation in O not in 𝜒(v)]

Algorithm: Iterate in order of increasing s. If O.vend(s) != 0 then we potentially have a dominating operation from O. We can assert O.vend(s) > v(s). We simply compare to Ohb.vend(s). If O.vend(s) > Ohb.vend(s) then we know that O dominates Ohb. Otherwise if Ohb.vend(s) > O.vend(s) then we know that Ohb dominates O. Otherwise it would appear that we have already received this operation! In that case we need to continue scanning!

Alternatively consider that O.vend(s) = 0. That means that O has performed no more ops by site s inside 𝜒(v). Therefore we evaluate Ohb.vend(s) and compare to v(s). If Ohb.vend(s) > v(s) then Ohb necessarily dominates O. If Ohb.vend(s) ≤ v(s) then we assume that both sites have recorded the same assignments by site s, and so neither dominates the other.

Algo: 


loop s in increasing order
{
    if (O.vend(s))
    {
        assert(O.vend(s) > v(s));
        if (Ohb.vend(s) > O.vend(s)) return <Ohb dominates>
        if (Ohb.vend(s) < O.vend(s)) return <O dominates>
    }
    else
    {
    if (Ohb.vend(s) > v(s)) return <Ohb dominates>
    }
}
return <Ohb dominates>