20 Control algorithm with transient HB-suffix

Transient per session state:

struct WorkingSet
{
    // Persistent state
    SiteId s;
    int t;
    Operation hb;

    // Transient state
    set<Session*> sessions; // The current set of active sessions
};

struct Session
{
    VectorTime vr;
    Operation suffix;
};

void DoOperation(WorkingSet* w, Session* y, Operation o)
{
    w->hb ⊕= o;
    o.Execute();
    for each x ∈ w->sessions such that x ≠ y
    {
        x->suffix ⊕= o;
    }
}

void DoLocalOperation(WorkingSet* w,Operation o)
{
    o.Init(w->s, w->t++);       // Set (s,t) in all intervals
    DoOperation(w,NULL,o);
}

void RunSession(WorkingSet* w,Session* y)
{
    os << vout(w->hb); // Send vector time describing content of local HB
    is >> y->vr;      // Receive vector time describing content of remote HB
    y->suffix = Rf2(w->hb,y->vr);
    async repeat      // Separate thread to send operations
    {
        os << Rf2(y->suffix, y->vr);
        y->vr ↑= vout(y->suffix);
    }
    async repeat      // Separate thread to receive operations
    {
        Operation o;
        is >> o;
        o = Rf2(o,vout(w->hb));
        y->suffix = Rf2(y->suffix, vin(o));
        DualIT(o,y->suffix);
        DoOperation(w,y,o);
    }
}

Notes:

• When the vector time describing the context of the remote HB is received, a session is able to calculate the inial value of its suffix which is a composite operation that is an RFactor of the site’s HB.
• For simplicity we have ignored showing where mutexes are required. Each session needs a mutex to protect access to its suffix by its sender and receiver threads. A working set needs a mutex to protect the database objects and its hb.
• A received operation o must be transformed against all the local atomic operations that are outside its execution context. This is basically the session's transient suffix. However it is first necessary to take the RFactor of the suffix to exclude any atomic operations that are already in v_in(o) which is the execution context of o. Note that the assertion in the call to Rf2 won’t fail – ie v_in (suffix) ≤ v_in(o). The proof follows.

Proof (by induction)

(initial case)

When two sites first connect they exchange values of v_out(hb) and compute initial suffixes as follows:

Initially v_in(suffix_local) = v_in(suffix_remote) = v_out(hb_local) ↓ v_out (hb_remote). When a remote site subsequently sends the first operation o, it is calculated as an RFactor from suffix_remote and therefore v_in(suffix_remote) ≤ v_in(o). It follows therefore that v_in(suffix_local) ≤ v_in(o).

(inductive step)

We have shown that the execution context of sent operations can only increase. ie if O₁ is sent before O₂ then v_in(O₁) ≤ v_in(O₂). Therefore if v_in(suffix_local) ≤ v_in(O₁) then for the same suffix it must follow that v_in(suffix_local) ≤ v_in(O₂).

The only way that v_in(suffix_local) may change is be assigning it to v_in(O) for some received operation O. Of course this also preserves v_in(suffix_local) ≤ v_in (O).