548705 - IPDL: Relax restriction of state only diverging for one "message step" into one "transition step" divergence

Status: RESOLVED WONTFIX

(Core :: IPC, defect)

Description

[Chris Jones [:cjones] inactive; ni?/f?/r? if you need me]

A simple example of where one message-step divergence doesn't quite do what one would expect is the protocol

 S:  send d --> S
     send q --> Q
     recv c --> C
 C:
     send q --> X
 Q:
     discard d
     recv c --> X
 X:
     __delete__

Even with the |discard| statement, the IPDL compiler will complain about state possibly diverging for more than one message-step because of

    +---d---> S ---d---> S ...
  (S)
    +---c---> C

IOW, the parent and child state don't sync back up after one pair of messages (one "message step").

This pattern has arisen in PNeckoChannel and PBrowserStream.  To support it, we can extend the notion of "message step" into "transition step".  The observation is that in the example above, the parent and child never actually get more than one *state transition* out of sync, even though they're out of sync for an unbounded number of messages.  Roughly, the parent just spins at state "S" sending "d"; nothing "interesting" happens until it either receives "c" from the child, or sends some other message.  So, the rules for one-"transition-step" commutativity are, given the racy messages

 S:  send s --> S;
     recv m2 --> T2;

 (1) At state T2, "s" is discarded or a self-loop to T2
 (2) \forall m1 \in { m | S : send m --> T1 } .
     (a) T1 is a "wait" state (defined below)
     (b) T2 is an "'s'-wait" state (defined below)
     (c) state T1 has the transition m2 --> U
     (d) state T2 has the transition m1 --> U

A "wait state" is one at which all messages have the same direction; after sending/receiving a message and transitioning to such a state, the actor can only recv/send.  An "'m'-wait state" is a wait state that additionally allows the opposite-directioned self-loop or discard of message 'm'.

If this relaxation proves insufficient, it is possible to extend this definition to k-transition-step divergence.  But TBH, I'd rather just drop the restrictions and go to full state machine validation.  (I worked out the rules for full validation before working out this relaxation, to hedge my bets.)

Comment 1

[Chris Jones [:cjones] inactive; ni?/f?/r? if you need me]

The updated plan is to change things to permit arbitrary transitions (except for restrictions like no racing destructors).