/ elib / equality

4-Party Partial Orders

This page should be read after Partially Ordered Message Delivery.

So far we only have forks in the order specification. This creates only a tree order, not a general partial order. For pure capabilities without equality (as in Actors or Joule), this would be fine. However, E also has a distributed equality construct able to do distributed grant matching. To satisfy the constraints implied by the Grant Matcher Puzzle, this distributed equality construct must also introduce a join in the specification topology. Fortunately, this is easily implemented in E, in which the only special primitive is "==" (local immediate sameness):

def join(a, b) :any {
    def [result, resolver] := Ref.promise()
    var hasLeft := false
    var left := null
    var hasRight := false
    var right := null

    var reduce := null
    reduce := def realReduce() :void {
        def done(answer) :void {
            resolver.resolve(answer)
            reduce := def noop() :void {}
        }
        if (Ref.isBroken(left)) {
            done(left)
        } else if (Ref.isBroken(right)) {
            done(right)
        } else if (hasLeft && hasRight) {
            # Eventual equality bottoms out in immediate equality
            if (left == right) {
                done(left)
            } else {
                done(Ref.broken("No join found"))
            }
        }
    }

    Ref.whenResolved(a, def reduceA(aa) :void {
        hasLeft := true
        left := aa
        reduce()
    })
    Ref.whenResolved(b, def reduceB(bb) :void {
        hasRight := true
        right := bb
        reduce()
    })
    result
}

The above function is actually predefined as the join method of the object named "E".

Given a and b, "def c := E.join(a, b)" immediately defines c as a promise for a reference that will be acceptable as a valid interpretation what a meant, and a valid interpretation of what b meant. (Valid in the sense that the introducer that sent us each of these references would have no cause for complaint if we use the promised reference instead.) We may immediately start sending messages on this new reference, confident that these messages will only get delivered if the promise indeed gets fulfilled, and therefore a mutually acceptable reference could be obtained. If a mutually acceptable reference cannot be obtained, then the promise will become broken, and all messages sent to it will be discarded, using the usual broken promise contagion rules.

Joining The Orders

In fact, c, if it resolves, is a fork of a and a fork of b. This is where the join in the ordering comes from. Given the following sequence of actions

a <- u()
b <- v()
c := E.join(a, b)
a <- w()
c <- x()
b <- y()

if a and b are independent references to the same object, and assuming no partition occurs, then

• u() and v() may be delivered in any order.
• w() may only be delivered after u() is delivered.
• x() may only be delivered after u() is delivered, as implied by "c is a fork of a".
• x() may only be delivered after v() are delivered, as implied by "c is a fork of b".
• y() may only be delivered after v() is delivered.
• w(), x(), and y() may be delivered in any order.
• All these messages are delivered at most once.

If a and b do not designate the same object, then all the above statements hold except that x() must not be delivered. In addition, c must eventually resolve to BROKEN.

Should a partition occur, all the above statements continue to hold anyway, but not in the obvious way. For example, should v() be lost in a partition, never to be delivered, then x() and y() must never be delivered, and both b and c must eventually become BROKEN, as implied by "c is a fork of b".