I tried to create an async stateful protocol for streams, and got a very strange IPDL error message. Parsing specification ../../../src/dom/plugins/PBrowserStream.ipdl /builds/mozilla-central/src/dom/plugins/PBrowserStream.ipdl:78: error: in protocol `PBrowserStream', the sequence of events parent: +--`send Write'-->( state `ALIVE' ) / ( state `ALIVE' ) \ child: +--`send NPN_RequestRead'-->( state `ALIVE' ) lead to parent/child states in which parent/child state can become more than one step out of sync (though this divergence might not lead to error conditions) Specification is not well typed. I don't see how this is out of sync at all?

As we briefly discussed today, this error message is just the IPDL type checker saying "I refuse to check transitions for more than one 'step' (pair of potentially racy messages)". To get an alpha out the door, I think we should implement this protocol in C++ but comment it out in the IPDL. There's a bigger question of whether the one-'step' rule needs to be tweaked, but we can deal with that later.

Oops, there *is* an IPDL type checker bug here: if two "racing" messages are both self-loops (from state S to state S), then by definition they can't race. Turns out that with this type checker bug fixed, the protocol is indeed non-racy by current standards. Apologies for overlooking this earlier. The rule I thought this protocol violated was two messages that both transition (S --M1--> T), (S --M2--> T), where T has racy messages, are "unchecked" by IPDL; it would need to look more than one "step" ahead to check. In that case it errors out with a message similar to the above.

The above protocol passes the type checker with this patch applied.

Comment on attachment 428380 [details] [diff] [review] Self-loop messages don't race Struck me just before bed that this isn't quite right. Will fix tomorrow.

With a fixed-up patch, there's still a race reported: /home/cjones/mozilla/electrolysis/dom/plugins/PBrowserStream.ipdl:78: error: in protocol `PBrowserStream', the sequence of events parent: +--`send Write'-->( state `ALIVE' )--`recv NPN_DestroyStream'-->( state [error] ) / ( state `ALIVE' ) \ child: +--`send NPN_DestroyStream'-->( state `DYING' )--`recv Write'-->( state [error] ) results in error(s) or leaves parent/child state out of sync for more than one step and is thus a race hazard; i.e., triggers `Write' and `NPN_DestroyStream' fail to commute in state `ALIVE' Specification is not well typed. |discard| is probably the easiest way to resolve this, and we can fake it in the mean time.

I didn't find a way to write a test for this fix that didn't hit bug 548069. That said, I still think the implemented-in-C++-but-commented-out-in-IPDL protocol should go into the alpha.

Here's another protocol that I think should work but doesn't with this patch applied.

I turned this into an IPDL test. It's actually not a protocol error per se, in the sense of violating a safety property. Rather, the type checker refuses to explore more than one transition step to see if there is a safety error. The real fix for this is bug 548705.