[E-Lang] Reliance & Static Security Checking

Mark S. Miller markm@caplet.com
Sun, 07 Jan 2001 09:49:11 -0800

At 11:49 AM Saturday 1/6/01, Tyler Close wrote:
>Markm wrote:
>> This means that the correctness of orderedTable depends on the
>> of the provided keys are being correct Orders, [...].
>com.waterken.canal.Order is actually the interface to the comparison
>predicate that the ordered table (or sorted map) is born with. The
>sorted map "relies" on its creator providing it with a valid Order

It looks like I'm already starting to use up my "per meeting" quota. ;)  I 
had intended to point at your PartiallyComparable 
type, rather than your Order type.

Although, as you point out, Order is also a valid illustration of the 
principle I have in mind, it isn't the illustration I'd intended.  Instead, 
your PartiallyComparable corresponds to what I meant, but, as you point out 
below, only when the ordering predicate used is LesserObject
(or possibly Reverse) as opposed to the other implementors of Order.

>Whether or not a sorted map is "delicate", or a "server", depends on
>the ability of the contained Order predicate to validate the input
>arguments. If the Order implementation can verify that the arguments
>are members of the expected irreflexive partial order, then the sorted
>map is a "server". If the Order implementation cannot provide this
>verification, then the sorted map is "delicate".
>The only case that I can think of where the Order predicate would not
>provide the needed verification is when the Order implementation
>delegates the comparison to one of the argument objects via the
>object's "compareTo" method, without knowing the concrete type of the
>object. I suspect that most Order implementations need to know the
>concrete type of the argument objects in order to calculate the
>comparison, thus implicitly providing the needed verification of the
>"suspect" arguments.

This is a really interesting point.  From a conventional object design perspective, it isn't clear why you need, for example, the ordering predicate LesserString if you could just make Strings implement PartiallyComparable and respond to compareTo correctly.  Your answer as I understand it, is that a sorted map using LesserString as its order predicate is a server, rather than delicate, because, although it relies on its order predicate, it does not rely on its keys, and therefore does not rely on its clients.

>So, how do we propagate this information into the sorted map's method

Notice that LesserString does more than enforce that its comparands are 
correctly comparable by the rules of an irreflexive partial order, it 
further enforces that these arguments are actually instances of 
java.lang.String, a UTCB provided concrete implementation.  Therefore, a 
sorted map using such an order predicate will enforce that its only keys are 

The conventional way type systems deal with this is with parameterized 
types.  However, there are enough different kinds of parameterized type 
systems that I'd wanted to postpone getting into these.  But since this is 
all a hypothetical exercise anyway, we can probably just use the macro 
expansion notion of parameterized types, which, IMHO, is the simplest 
semantics, since it is just the semantics of macro expansion combined with 
the semantics of a non-parameterized type system.

So, returning to our ordered table, where we would have declared, let's say, 
a non-parameterized type

     typedef OrderedTableType {
         to put (key :rely(Order), value :suspect) :void
         to get(key :rely(Order)) :suspect
         to delete(key :rely(Order)) :suspect

we might instead define

    define OrderedTableTypeMaker(K,V) :any {
        typedef OrderedTableType {
            to put (key :K, value :V) :void
            to get(key :K) :V
            to delete(key :K) :V

then, the value of OrderedTableTypeMaker(String, suspect) would be

     typedef _ {
         to put (key :String, value :suspect) :void
         to get(key :String) :suspect
         to delete(key :String) :suspect

Since "String" names a concrete implementation known to be part of the UTCB 
and therefore assumed to be correct, this type is statically known to be a 
server type, rather than delicate.