On Sat, Dec 11, 2010 at 7:47 AM, Sandro Magi <smagi <at> higherlogics.com> wrote:

The OS semantics are matched by languages with region typing. Each
reference is a (pointer, region where object lives) pair, and
functions are annotated with the effects applying them have on the set
of input regions.

For the kind of complex OS machinery Bill is talking about, this may well be an informative analogy. But for the question David asked, I think there's a much simpler answer. See below.

 

The input regions are the regions transitively accessible via the
parameters, plus a region for the return value. Often regions are
associated with memory areas, but need not be, ie. you could have a
console region for checking when print commands are issued.

See the DDT language for a good example of this in action.

Sandro

On 2010-12-10, at 8:44 PM, David Wagner <daw-Sd3DkRwxp1uueSrTVlFI5A@public.gmane.org> wrote:

> Bill Frantz  wrote:
>> I would like to see if these ideas [System Enforced Transitive
>> Read-Only Objects] will map to language enforced systems.
>
> Some languages enable programmers to claim that all objects of a
> particular type are transitively read-only, in a way that allows the
> system to verify that these claims are accurate.  For instance, Joe-E
> supports this kind of reasoning.
>
> It would probably be possible to extend language-enforced systems so
> that
> for every type T, there is another type 'readonly T' which has a
> subset
> of T's methods and a subset of T's fields chosen so that a reference
> to an object of type 'readonly T' does not grant any authority to
> cause
> side effects.  The most obvious way to implement this would be to have
> the programmer declare, through some kind of annotations, which
> methods
> and fields should be included in the type 'readonly T', and have the
> compiler verify that these annotations suffice to achieve the desired
> property.  There are some non-trivial details here.  Put another way,
> it would probably be possible to design an object capability language
> where every type T is implicitly polymorphic over the type qualifier
> 'readwrite' vs 'readonly'.  I'm not sure whether the security benefits
> would be worth the additional complexity in the language.
>
> There has been some work along roughly similar lines.  See, e.g.,
> Javari and related work.
>
> Is this the kind of thing you are talking about?
>
> I see one difference in philosophy between language-based object
> capability systems and OS-based capability systems.  In many object
> capability languages, a capability is just a reference to an object,
> nothing more.  In many OS-based capability systems, a capability is
> the pair of a reference to an object and a set of access rights (e.g.,
> read, write, read-write).  This seems like a significant difference,
> and one that may make it harder to take ideas from EROS and translate
> them directly to an object capability language.  It's not clear to me
> that the OS way is superior.

Hi David, I think this contrast is an illusion due to the different ways you use "object" above. In an object language, an object reference does simply point at an object, but an object is an indivisible pair of its per-instance storage (instance variables, captured lexical environment, ...) and its code (vtable, lambda expression, ...). In like manner, in EROS a capability both designates a resource full of locations (page, domain, ...) and enables a set of actions to be performed on that resource (read, write, call, ...). For call-right capabilities, i.e., start keys, the capability also contains the facet id (keybits) that enable the called domain to further distinguish what behavior it should associate with the capability. See the rosetta table 9.1 in my thesis.

My favorite example for illustrating this remains my figure 6.5:

  def makeCounterPair () { 
      var count := 0 
      def upCounter { 
          to incr() { return count += 1 } 
      } 
      def downCounter { 
          to decr() { return count -= 1 } 
      } 
      return [upCounter, downCounter] 

  } 

Here, each counter pair, like each EROS domain, is a bit of storage that can be manipulated by multiple capabilities, each of whom gives different rights for manipulating this common storage.

--
    Cheers,
    --MarkM