[cap-talk] A Taxonomy of Current Object-Cap Systems [correction]

[David-Sarah Hopwood]

David-Sarah Hopwood wrote:
>    Causal-order
>                If M1 is sent before M2, and both messages are
>                received, then M1 is received before M2.
> 
>    E-order     References are "forked" when sent between processes/vats.
>                If M1 is sent before M2 on the same reference, or if
>                M1 is sent to a reference R and then M2 is sent to a
>                reference forked (maybe indirectly) from R, and both
>                messages are received, then M1 is received before M2.
>                [E, A4]
> 
>    (Point-to-point) FIFO-order
>                If M1 and M2 are sent by process A to process B, and
>                M1 is sent before M2, and both messages are received,
>                then M1 is received before M2. [Erlang, Waterken]

These definitions are slightly weaker than I intended, because it
should not be possible for only M2 to be received without M1 having
been received.

(In systems that support selective or closed-set receives, or that
support both open and closed receives, a process can be modelled as
having a "mailbox" from which messages are selectively extracted.
"Received" means delivered to the target process mailbox, not
necessarily extracted from the mailbox.)

The corrected definitions are:

     Causal-order
                 If M1 is sent before M2, and M2 is received, then
                 M1 is received before M2.

     E-order     References are "forked" when sent between processes/vats.
                 If M1 is sent before M2 on the same reference, or if
                 M1 is sent to a reference R and then M2 is sent to a
                 reference forked (maybe indirectly) from R, and M2 is
                 received, then M1 is received before M2.
                 [E, A4]

     (Point-to-point) FIFO-order
                 If M1 and M2 are sent by process A to process B, and
                 M1 is sent before M2, and M2 is received, then M1 is
                 received before M2. [Waterken]

Erlang/OTP apparently does not satisfy this stronger definition of
FIFO-order; only the weaker one in my previous message. See
<http://www.cs.chalmers.se/~hanssv/doc/ew07-dist.pdf>.
Note that the PID reuse bug described in section 4.1 of that paper would
need to be fixed in order for Erlang to be considered a capability system
at all. It's the bug described in section 4.2 that weakens the
implemented message ordering.

-- 
David-Sarah Hopwood ⚥