[cap-talk] Another "core" principle - Brinkmann

[Jonathan S. Shapiro]

On Fri, 2006-12-29 at 01:25 +0100, Valerio Bellizzomi wrote:
> >Precisely. If the model ignores this, it's both non-believable and fails
> >to model observability correctly.
> 
> 
> Can you expand on Observability ?
> I will read your reply tomorrow, heading to bed now :-)

Suppose that I (a keeper of the space) can write a mapping slot. You (a
client of the space) cannot read the capability in that slot, but you
can traverse it. By reading the thing that it points to, you can
determine that the capability in that slot has been altered.

So it is clear that

   Keeper ---G---> MappingTable,  Client ---I---> MappingTable
   ___________________________________________________________
   Client ---(R)---> Keeper, Keeper ---(W)---> Client

where parenthesis indicate "de facto" access rights. This is actually
not a big deal, because the keeper could map a capability page at a leaf
position and then hand the client any capability that it wants in any
case.

The tricky bit to understand is whether the fact the the client can
indirectly observe that the slot has been changed may imply


  Client ---(R)--->MappingTable


shap