[cap-talk] Why is EQ so dang fascinating?

Mark Miller erights at gmail.com
Sat Oct 27 08:00:07 EDT 2007


On 10/27/07, Toby Murray <toby.murray at comlab.ox.ac.uk> wrote:
> The version of the object-cap model as described in Robust Composition
> (Mark Miller's  PhD thesis) specifically avoids dealing with EQ. In
> trying to come up with a more formal definition of the object-cap model,
> one needs to address the issue of EQ -- should it exist? If so, in what
> form?

Actually, there was one place in Robust Composition where I used EQ in
order to explain something else, but without explaining or dealing
with any of the interesting EQ issues. In section 19.5 ("Joins in
E-Order") and figures 19.2 and 19.3, I use EQ to define join:

    def join(left, right) {
        return when (left, right) -> {
            if (left == right) { left } else { throw("unequal") }
        }
    }

The concurrency control issues involved here are not germane to the
present discussion. What is germane is that join's actual contract
(not explained in the text) is only that it returns a reference
adequate for grant-matching equality
<http://erights.org/elib/equality/grant-matcher/>. In other words, if
the Grant Matcher receives x from Alice and y from Dana, does

    def z := join(x, y)

then observes that z resolves successfully, the Grant Matcher can then
safely send $20 to z. The join must ensure only that z designates the
same object that x did as far as Alice is concerned, and that z
designates the same object as y as far as Bob is concerned. More
specifically, Alice has no grounds for complaint if the Grant Matcher
sends $20 to z instead of x, and Bob has no grounds for complaint if
the Grant Matcher sends $20 to z instead of y.

The interesting thing about join is that it is only what Dean calls a
"coercing equality" operation, whereas EQ is a "authenticating
equality" operation. EQ doesn't return a reference. Instead it returns
a boolean. When it returns true, then either of the original arguments
themselves is already a valid interpretation of the other argument,
and the Grant Matcher can use either without providing either of its
customers any ground for complaint.

Although above we show a trivial implementation of join in terms of
EQ, Dean has previously posted techniques which can successfully
implement join in a system without EQ. However, in a system without
EQ, it seems it is impossible to build EQ. However, I have no idea how
one would attempt to prove this impossibility. Since join is adequate
for Grant Matching, Dean has indeed successfully answered this
longest-standing challenge to his position on the EQ debate.


> The best way to decide these questions, I believe, is to know what
> cannot be expressed without EQ. If useful patterns cannot be expressed
> without EQ, then this gives strong evidence that EQ should be included
> in a formal object-cap model. Otherwise, we may choose to leave   it
> out.

Funny how the timing on these things works out sometimes. I believe
the retroactive corroboration property of Horton cannot be implemented
without EQ.

Alice tells Carol to provide a separate identity tunnel for Bob's use
of Carol's C. Carol does so. Bob's B makes use of C. Carol logs these
uses, attributing them to Bob. However, so far, Carol has only heard
of Bob from Alice, so Carol hold Alice responsible for Bob's
misbehavior. Later, Carol also hears about Bob from Dave. Based on
Carol's prior relationship with Dave and what Dave says about Bob,
Carol now believes that Bob is independent of Alice. With join, Carol
can only absolve Alice of Bob's misbehavior after the corroborating
introduction. With EQ, Carol can also retroactively absolve Alice of
Bob's past misbehavior.

I pose this as a new challenge to EQ-less ocaps. Can we generate
either a counter-example or a proof that no counter-example is
possible?

-- 
Text by me above is hereby placed in the public domain

    Cheers,
    --MarkM


More information about the cap-talk mailing list