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

[Matej Kosik]

Hi all,

Mark S. Miller wrote:
> Jed at Webstart wrote:
>> I had imagined that the concern about wall listening was mainly
>> for cases where the program was a black box (e.g. proprietary code).
>> Once you get to the point of auditing source code it seems to me that
>> the costs are so high and the means of control so good that worrying
>> about non deterministic inputs is likely a small part of the problem.
> 
> In E, no auditing of source code is necessary to enforce determinism, and so 
> it can be enforced on black boxes. The safe scope, containing the caps 
> universally provided by convention, contain no caps that would enable a 
> program to escape determinism. Unless a program is provided a cap that enables 
> non-determinism, it cannot be non-deterministic.
> 

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."

If it were true, that would be great, however if I understand the
semantics of E correctly, it is not. Here is a trivial counter example:

Let there be four objects: objectA, objectB, objectC and objectD each of
them placed in a distinct vat with the following behavior:

  # objectA is in vatA
  def objectA() {
    objectB <- ()
    objectC <- ()
  }
-------------------------
  # objectB is in vatB
  def objectB() {
    objectD <- add("B")
  }
-------------------------
  # objectC is in vatC
  def objectC() {
    objectD <- add("C")
  }
-------------------------
  # objectD is in vatD
  def fifo := makeFifo()
  def objectD() {
    to add(s) {
      # add a given string `s' at the end of the FIFO queue
      fifo.add(s)
    }
    to first() {
      # return the first element of the queue
      fifo.first()
    }
    to second() {
      # return the second element of the queue
      fifo.second()
    }
  }

Interconnected as shown in the attached figure `abcd.png'
-------------------------
The system of vats above might end up in two distinct states:
  S' and S''.

In one, when we request objectD the first element of the FIFO queue, it
will say "A". In the other, it will say "B".
-------------------------
In other words:

- vatA' is weakly deterministic
- vatB is weakly deterministic
- vatC is weakly deterministic
- vatD is weakly deterministic
(none of the vats is provided capabilities to non-deterministic
vats/processes)
- unfortunatelly, their composition
    S = vatA | vatB | vatC | vatD
  is not weakly deterministic because
  - S has two descendands S' and S'' such that
    S => S'
    S => S''
    and they are not weakly bisimilar

With
- weak determinism
- descendant
I mean those terms as defined in
http://www.amazon.co.uk/Communication-Concurrency-Prentice-International-Computer/dp/0131150073/sr=8-1/qid=1164882342/ref=sr_1_1/203-4943963-2819122?ie=UTF8&s=books
the particular system vatA | vatB | vatC | vatD could be modelled in CCS
calculus (even though not all things which can be expressed in E (namely
mobility) can be captured by CCS).

If I am wrong, I would be glad to be corrected.

Regards
-- 
Matej Kosik
-------------- next part --------------
A non-text attachment was scrubbed...
Name: abcd.png
Type: image/png
Size: 6843 bytes
Desc: not available
Url : http://www.eros-os.org/pipermail/cap-talk/attachments/20061130/661841c8/attachment-0001.png 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
Url : http://www.eros-os.org/pipermail/cap-talk/attachments/20061130/661841c8/attachment-0001.bin