Re: avoiding races in IPDL protocols

To provide a bit more context, the goal of IPDL is to allow "actors"
(threads) to communicate safely.  The actors' communication is described
by a finite-state machine.  *Both* actors have the *same* state in this
state machine --- put another way, the actors' states stay "entangled."
 This is to simplify reasoning about their interaction --- they act in
lockstep, in a sense.  Or rather they are supposed to, see below.

Jason Duell wrote:

Please allow me simplify this example slightly.

>     https://wiki.mozilla.org/IPDL/Getting_started
> 

Using the syntax of the guide above, the problem reduces to this example

protocol Test {
parent:
  async FooMsg();
child:
  async BarMsg();
//...

> state START:
>     recv FooMsg goto FOO;
>     send BarMsg goto BAR;
> 
> state FOO:
>     recv Foo2Msg goto MORE_FOO;
> 
> state BAR:
>     recv Bar2Msg goto MORE_BAR;
> 
};

The execution under which the issue arises is as follows.  Call the
thread in the parent process "P," and the thread in the child process
"C."  Each row of the table below contains execution steps that happen
"simultaneously."

P                    C
-----                -----
send BarMsg          send FooMsg    // both sends are legal
transition to BAR
recv FooMsg                         // ILLEGAL!?!?

The fact that IPDL allows this system to blow up when both actors have
behaved "correctly" according to their specifications is the problem to
be solved.

> 1) Make the programmer anticipate race conditions, and allow (and
> handle) BarMsg when in state FOO.  This might, alas, requires a lot of
> subtle thinking to get right (when we were hoping IPDL would make
> safely writing protocols fairly trivial).
> 

The original plan was to allow these protocols, but use static analysis
of the C++ implementation code to construct actor models, and check
those models against the IPDL specification to ensure these kinds of
errors didn't happen.  But I agree --- that fact that this isn't
prevented at the language level is a very serious bug.

> 3) Possibly loosen #2 to allow states with bidirectional traffic, but
> only if states that follow them can handle all possible race condition
> messages that might occur (the IPDL compiler should be able to figure
> these out).

This is pretty much what I want.  (For concurrency buffs, the difference
between (3) and (2) is that (3) tries to allow the IPDL programmer to
define commutative transitions.)

This can be implemented with extra checks of the protocol state machine;
it's already (er, will be soon) checked to ensure that all states are
reachable.  Here are the checks.

  *Rule 1*: from a state S, all sync triggers must be of the same
"direction," i.e. only |send| or only |recv|

(Otherwise deadlock can occur from simultaneously in-flight synchronous
requests.)

  *Rule 2*: the "Diamond Rule".
  from a state S,
    for any pair of triggers t1 and t2,
        where t1 and t2 have opposite direction,
        and t1 transitions to state T1 and t2 to T2,
      then the following must be true:
        T2 allows the trigger t1, transitioning to state U
        T1 allows the trigger t2, transitioning to state U

This is a more formal way of expressing "it doesn't matter in which
order the events t1 and t2 occur."  This sounds fairly complicated, but
in the common case, the states S, T1, T2, and U will probably all be the
same, in something like the following:

  state START:
    send Init goto CONFIGURE;
  state CONFIGURE:
    recv Configuration goto MAIN;
  state MAIN:
    send Foo goto MAIN;
    recv Bar goto MAIN;
    // ...

In this state machine, the MAIN transitions follow the Diamond Rule
because the actual state never changes.

Another case I envision is complicated state machines, with many states,
that allow "status"-type messages to be sent from or received in most
protocol states.  For example:

  state S1:
    send Status goto S1;
    recv Status goto S1;
    send NextState goto S2;
  state S2:
    send Status goto S2;
    recv Status goto S2;
    recv NextState2 goto S3;
  state S3:
    ...

From state S1, we have to check the pairs (send Status, recv Status),
and (send NextState, recv Status).  For the first pair, it's obvious
that they follow the Diamond Rule, because both transitions are
self-loops.  The second pair also follow the Diamond Rule.  The diagram
below, which means the same as the one above, shows why

P                    C
-----                -----
                                      // P, C @ state S1
send NextState       send Status
goto state S2        goto state S1
                                      // P@S2, C@S1
recv Status
goto state S2
                     recv NextState
                     goto state S2
                                      // P, C @ S2

Another way of implementing this example is to use a "Status"
sub-protocol, which would probably be superior.  (In general, if the
IPDL semantics seem too limiting within a single protocol, it's probably
indicative of an overly-complicated protocol that should instead be
represented as an hierarchy of sub-protocols.)

> I don't have enough of an idea of the communication patterns needed by
> electrolysis to know where in these options we'd fit.
> 

Yep, we'll have to figure this out as we go along.

> The classic way of doing things, of course, is to have each end of the
> protocol be its own state machine, and have sends and recvs of
> messages be separate events happening to different state machines.   I
> don't know the guts or theory behind IPDL to know if autogenerating
> that sort of setup is feasible.  On the plus side, our "network" is
> reliable, in-order, and low latency, so we avoid a *lot* of complexity
> there.
> 

IMHO, separate state machines would make things worse, not better.

Cheers,
Chris