[cap-talk] Wall banging (was: Bellizzomi, Capabilities, Shapiro's focus, Coyotos, etc.)

[Mark S. Miller]

Short answer for now. More later.


>> Do you say that the following statement is true?
>>
>>   "let vat1, vat2, vat3, ... , vatN be deterministic vats
>>    then system of these vats is also deterministc."

This statement is not true. Some other weaker statements (yet to be stated) 
are true.


Kevin Reid wrote:
> The safe scope does not include inter-vat references (which do enable  
> nondeterminism as you described). I expect MarkM was including such  
> references as 'caps that enable nondeterminism'.

Yes. In particular, the capability for spawning a vat is not available in the 
safe scope for this reason:

     ? def makeVat := <elib:vat.makeVat>
     # problem: <SecurityException: \
     #           org.erights.e.elib.vat.Vat not approved as safe>

     ? def makeVat := <unsafe:org.erights.e.elib.vat.makeVat>
     # value: <makeVat>

Similarly, the occurrence of GC is non-deterministic, so the caps that let you 
sense GC are not available in the safe scope:

     ? def makeVat := <elib:vat.makeWeakPtr>
     # problem: <SecurityException: \
     #           org.erights.e.elib.vat.WeakPtr not approved as safe>

     ? def makeVat := <unsafe:org.erights.e.elib.vat.makeWeakPtr>
     # value: <makeWeakPtr>

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

     Cheers,
     --MarkM