[E-Lang] Reliance & Static Security Checking

[Mark S. Miller]

At 09:10 AM Friday 1/5/01, Karp, Alan wrote:
>We have a policy of allowing each person 3 really stupid remarks per meeting
>(at the level of 2+2=3), [...]

I like this policy, but how should we generalize "per meeting" to an ongoing 
email discussion list?  In any case, in order to avoid disqualifying 
myself, I'd request a larger budget. ;)


>I do have one question about your example.  What does it mean to declare
>rely(Foo) in one place and suspect(Foo) in another?  Either Foo obeys the
>contract, or it does not.

In "rely(Foo)" or "suspect(Foo)", "Foo" is supposed to be a type name, not a 
name for an individual object or a concrete implementation.  If two such 
declarations appear, they are making statements about different variables or 
return values.

Let's take Bill's hashtable example again, but turn it into ordered 
collections such as are provided by Tyler's Hydro library.  Ordered 
collections are a good example, because unlike hashing, I don't encapsulate 
order into the E language definition.  Rather, an ordered collection relies 
on its keys to correctly implement the Order contract.

Tyler's expression of the Order contract as 
http://www.waterken.com/Hydro/2.0/doc/com/waterken/canal/Order.html is a 
perfect example of where the important terms of the contract are expressed 
only in the comments, and only as a means for humans to speak to other 
humans.  Here's Bill's transformed hashtable:

    def orderedTable {
        to put (key :rely(Order), value :suspect) :void { ... }
        to get(key :rely(Order)) :suspect { ... }
        to delete(key :rely(Order)) :suspect { ... }
    }

This means that the correctness of orderedTable depends on the correctness 
of the provided keys are being correct Orders, ie, at correctly implementing 
the order contract.  If a key is provided that isn't a correct Order, for 
example, its compare() isn't transitive, then orderedTable may deviate from 
its contract without being considered incorrect.  This is like a 
precondition, except we are not presuming to be able to formalize the Order 
contract.

Since orderedTable relies on at least one of its arguments, it therefore 
relies on its clients, ie, it's vulnerable to its client's misbehavior.  
Earlier, we defined such objects as "delicate", as opposed to being a 
"server".  E's Maps are servers, as will be Hydro's hashtables as presented 
to the E programmer, once Hydro is properly integrated into E.  E's 
ordered tables (which will also appear with the Hydro integration) are 
delicate because we know of no affordable way to make ordered tables be 
servers.

          --------------------------------------------------------------------------------

An example of a possible static reliance check failure:

    define foo : rely(Foo) := ... # where Foo is a delicate type
    define bar : suspect(Bar) := ...

    bar snorgle(foo)    # static reliance check failure

If the containing object relies on foo and foo is delicate, then it would 
seem to be a mistake to give bar access to foo, since bar is suspect.  bar 
might damage foo in a way that damages the containing object's correctness 
as well.

>I had thought that "suspect" propagated the way
>taint does in Perl, but I don't see that in your example.  Is that your
>intent?

I don't know "taint".  Could you explain?  (Please don't assume much 
knowledge of Perl.  I have learned it on occasion, but it doesn't stick to 
my brain.)


        Cheers,
        --MarkM